(* 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.