interval characterization proofs and worked examples

1 files changed, 80 insertions, 0 deletions

diff --git a/theories/Interval.v b/theories/Interval.v
new file mode 100644
index 0000000..7562170
--- /dev/null
+++ b/theories/Interval.v
@@ -0,0 +1,80 @@
+(* The integer-tightening facts behind the interval engine.
+
+   Propagate.lower_int and Propagate.upper_int in lib/vm.ml convert
+   rational bounds into integer endpoints: a non-strict lower bound
+   q becomes ceiling q, a strict one becomes floor q + 1, and dually
+   for upper bounds. These four characterizations say the
+   conversions are exactly right: an integer satisfies the rational
+   bound iff it satisfies the tightened integer bound. Both
+   propagation (enumeration endpoints, contradiction detection) and
+   symbolic discharge (entailment over integer kinds) lean on
+   them. *)
+
+From Stdlib Require Import QArith Qround ZArith Lia.
+
+Lemma inject_Z_le : forall a b : Z, (a <= b)%Z <-> (inject_Z a <= inject_Z b)%Q.
+Proof. intros a b; unfold Qle, inject_Z; simpl; lia. Qed.
+
+Lemma Qfloor_inject : forall z : Z, Qfloor (inject_Z z) = z.
+Proof. intro z; unfold Qfloor, inject_Z; simpl; apply Z.div_1_r. Qed.
+
+Lemma Qceiling_inject : forall z : Z, Qceiling (inject_Z z) = z.
+Proof.
+  intro z; unfold Qceiling, Qopp, Qfloor, inject_Z; simpl.
+  rewrite Z.div_1_r; lia.
+Qed.
+
+(* Non-strict lower bound: q <= z iff ceiling q <= z. *)
+Lemma lower_nonstrict : forall (q : Q) (z : Z),
+  (q <= inject_Z z)%Q <-> (Qceiling q <= z)%Z.
+Proof.
+  intros q z; split; intro H.
+  - rewrite <- (Qceiling_inject z). apply Qceiling_resp_le; exact H.
+  - apply Qle_trans with (inject_Z (Qceiling q)); [ apply Qle_ceiling | ].
+    exact (proj1 (inject_Z_le _ _) H).
+Qed.
+
+(* Strict lower bound: q < z iff floor q + 1 <= z. *)
+Lemma lower_strict : forall (q : Q) (z : Z),
+  (q < inject_Z z)%Q <-> (Qfloor q + 1 <= z)%Z.
+Proof.
+  intros q z; split; intro H.
+  - assert (Hle : (Qfloor q <= z)%Z).
+    { rewrite <- (Qfloor_inject z). apply Qfloor_resp_le.
+      apply Qlt_le_weak; exact H. }
+    destruct (Z.eq_dec (Qfloor q) z) as [ Heq | ]; [ | lia ].
+    exfalso.
+    apply (Qlt_irrefl (inject_Z z)).
+    eapply Qle_lt_trans; [ | exact H ].
+    rewrite <- Heq. apply Qfloor_le.
+  - apply Qlt_le_trans with (inject_Z (Qfloor q + 1)); [ apply Qlt_floor | ].
+    exact (proj1 (inject_Z_le _ _) H).
+Qed.
+
+(* Non-strict upper bound: z <= q iff z <= floor q. *)
+Lemma upper_nonstrict : forall (q : Q) (z : Z),
+  (inject_Z z <= q)%Q <-> (z <= Qfloor q)%Z.
+Proof.
+  intros q z; split; intro H.
+  - rewrite <- (Qfloor_inject z). apply Qfloor_resp_le; exact H.
+  - apply Qle_trans with (inject_Z (Qfloor q)); [ | apply Qfloor_le ].
+    exact (proj1 (inject_Z_le _ _) H).
+Qed.
+
+(* Strict upper bound: z < q iff z <= ceiling q - 1. *)
+Lemma upper_strict : forall (q : Q) (z : Z),
+  (inject_Z z < q)%Q <-> (z <= Qceiling q - 1)%Z.
+Proof.
+  intros q z; split; intro H.
+  - assert (Hle : (z <= Qceiling q)%Z).
+    { rewrite <- (Qceiling_inject z). apply Qceiling_resp_le.
+      apply Qlt_le_weak; exact H. }
+    destruct (Z.eq_dec z (Qceiling q)) as [ Heq | ]; [ | lia ].
+    exfalso.
+    apply (Qlt_irrefl (inject_Z z)).
+    eapply Qlt_le_trans; [ exact H | ].
+    rewrite Heq. apply Qle_ceiling.
+  - apply Qle_lt_trans with (inject_Z (Qceiling q - 1)).
+    + exact (proj1 (inject_Z_le _ _) H).
+    + apply Qceiling_lt.
+Qed.