From fbedd93cabac1fbd98a03851c5979dd36d362e7e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= <basile.clement@ocamlpro.com>
Date: Fri, 30 Jun 2023 12:06:08 +0200
Subject: [PATCH] Add knowledge about floor/ceil bounds
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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                       | 28 +++++++++++++++++++++++
 tests/arith/ceil_floor_propagate.ae       |  2 ++
 tests/arith/ceil_floor_propagate.expected |  2 ++
 3 files changed, 32 insertions(+)
 create mode 100644 tests/arith/ceil_floor_propagate.ae
 create mode 100644 tests/arith/ceil_floor_propagate.expected

diff --git a/src/preludes/ria.ae b/src/preludes/ria.ae
index 2378572ae..0dafe50e5 100644
--- a/src/preludes/ria.ae
+++ b/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
diff --git a/tests/arith/ceil_floor_propagate.ae b/tests/arith/ceil_floor_propagate.ae
new file mode 100644
index 000000000..ef5959bdf
--- /dev/null
+++ b/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.
diff --git a/tests/arith/ceil_floor_propagate.expected b/tests/arith/ceil_floor_propagate.expected
new file mode 100644
index 000000000..a6e005255
--- /dev/null
+++ b/tests/arith/ceil_floor_propagate.expected
@@ -0,0 +1,2 @@
+
+unknown