Add knowledge about floor/ceil bounds

In the RIA prelude, we have axioms with semantic triggers to propagate
bounds on reals to bounds on integers using `real_of_int`
(`real_of_int_to_int_1` and `real_of_int_to_int_2`).

These state respectively that:

 - If `real_of_int(i) ≤ y` holds in the reals, then `i ≤ int_floor(y)`
   holds in the integers.

 - If `y ≤ real_of_int(i)` holds in the reals, then `int_ceil(y) ≤ i`
   holds in the integers.

This patch adds the corresponding propagations from bounds on integers
to bounds on reals. More precisely it adds the propagations:

 - If `int_floor(x) ≤ i` holds in the integers, `x < real_of_int(i + 1)`
   holds in the reals

 - If `i ≤ int_floor(x)` holds in the integers, `real_of_int(i) ≤ x`
   holds in the reals

 - If `int_ceil(x) ≤ i` holds in the integers, `x ≤ real_of_int(i)`
   holds in the reals

 - If `i ≤ int_ceil(x)` holds in the integers, `real_of_int(i - 1) < x`
   holds in the reals

(Note that the test has "unknown" expected but it should be SAT -- this
is because the ria prelude is disabled currently)

src/preludes/ria.ae

@@ -56,6 +56,34 @@ theory Real_of_Int extends RIA =
      {i <= real_of_int(x)}.
      k <= x
 
+  (* floor(x) ≤ i iff x < i + 1 *)
+  axiom int_floor_ub:
+    forall x, y : real, i : int
+    [ int_floor(x), not_theory_constant(x), int_floor(x) in ]?, i], y |-> real_of_int(i + 1) ]
+    { int_floor(x) <= i }.
+    x < y
+
+  (* i <= floor(x) iff i <= x *)
+  axiom int_floor_lb:
+    forall x, y : real, i : int
+    [ int_floor(x), not_theory_constant(x), int_floor(x) in [i, ?[, y |-> real_of_int(i) ]
+    { i <= int_floor(x) }.
+    y <= x
+
+  (* ceil(x) ≤ i iff x ≤ i *)
+  axiom int_ceil_ub:
+    forall x, y : real, i : int
+    [ int_ceil(x), not_theory_constant(x), int_ceil(x) in ]?, i], y |-> real_of_int(i) ]
+    { int_ceil(x) <= i }.
+    x <= y
+
+  (* i <= ceil(x) iff i - 1 < x *)
+  axiom int_ceil_lb:
+    forall x, y : real, i : int
+    [ int_ceil(x), not_theory_constant(x), int_ceil(x) in [i, ?[, y |-> real_of_int(i - 1) ]
+    { i <= int_ceil(x) }.
+    y < x
+
    (* can add other axioms on strict ineqs on rationals ? *)
 
 end

tests/arith/ceil_floor_propagate.ae

@@ -0,0 +1,2 @@
+logic x: real
+goal g: int_ceil(x) = 0 and int_floor(x) = 0 -> x = 0.

tests/arith/ceil_floor_propagate.expected

@@ -0,0 +1,2 @@
+
+unknown