add Intv32's constructor 'singleton'

farith2/Intv32.ml

@@ -49,6 +49,32 @@ module Intv32 =
   | Intv (a, b, n) ->
     if (&&) (coq_Beqb prec emax a b) (Pervasives.not n) then Some a else None
 
+  (** val singleton : float32 -> t **)
+
+  let singleton x = match x with
+  | B754_nan -> Inan
+  | _ -> Intv (x, x, false)
+
+  (** val ge : t -> t_opt **)
+
+  let ge =
+    coq_Ige prec emax
+
+  (** val le : t -> t_opt **)
+
+  let le =
+    coq_Ile prec emax
+
+  (** val lt : t -> t_opt **)
+
+  let lt =
+    coq_Ilt prec emax
+
+  (** val gt : t -> t_opt **)
+
+  let gt =
+    coq_Igt prec emax
+
   (** val le_inv : t -> t -> t_opt * t_opt **)
 
   let le_inv =

farith2/Intv32.mli

@@ -23,6 +23,16 @@ module Intv32 :
 
   val is_singleton : t -> float32 option
 
+  val singleton : float32 -> t
+
+  val ge : t -> t_opt
+
+  val le : t -> t_opt
+
+  val lt : t -> t_opt
+
+  val gt : t -> t_opt
+
   val le_inv : t -> t -> t_opt * t_opt
 
   val ge_inv : t -> t -> t_opt * t_opt

farith2/thry/Interval.v

@@ -21,7 +21,7 @@ Inductive Interval' :=
 
 Definition valid (I : Interval') :=
   match I with
-  |Intv lo hi _ => lo <= hi
+  | Intv lo hi _ => lo <= hi
   | _ => True
   end.
 
@@ -276,7 +276,7 @@ Next Obligation.
 Defined.
 
 Program Theorem Igt_correct :
-  forall (I : Interval) (x y : float), contains I y -> Bltb y x = true -> contains_opt (Ige I) x.
+  forall (I : Interval) (x y : float), contains I y -> Bltb y x = true -> contains_opt (Igt I) x.
 Proof.
   intros [[| l1 h1] H1] x y Hx Hxy; simpl in *.
   - fdestruct y; fdestruct x.

farith2/thry/Intv32.v

@@ -74,6 +74,50 @@ Module Intv32.
       else None
     end.
 
+  Program Lemma is_singleton_eq_aux :
+    forall (I : t) (x a b : float32) n H, is_singleton (exist (fun I : Interval' prec emax => valid prec emax I)
+    (Intv prec emax a b n) H) = Some x -> x = a.
+  Proof.
+    cbn; intros.
+    destruct Beqb, negb; simpl in *; congruence.
+  Qed.
+
+  Program Theorem is_singleton_correct :
+    forall (I : t) (x : float32), (is_singleton I = Some x) -> (forall y, contains I y -> Beqb x y = true \/ (is_nan x && is_nan y = true)).
+  Proof.
+    intros [[| a b n] H] x; cbn.
+    + intros. inversion H0; fdestruct y; now right.
+    + intros. destruct (Beqb a b) eqn:E1, (negb n) eqn:E; try easy; simpl in *.
+      inversion H0; subst. left.
+      destruct H1 as [ [H1 H2] | H1 ].
+      - assert (b <= y <= b) by eauto using E1, Beqb_symm, Beqb_Bleb, Bleb_trans.
+        apply Bleb_antisymm in H3.
+        eapply Beqb_trans; eauto using Beqb_symm.
+      - destruct n; fdestruct y.
+  Qed.
+
+  Program Definition singleton (x : float32) : t :=
+    match x with
+    | B754_nan => Inan prec emax
+    | _ => Intv _ _ x x false
+    end.
+  Next Obligation.
+    apply Bleb_refl.
+    fdestruct x.
+  Defined.
+
+  Program Theorem singleton_correct :
+    forall x, is_singleton (singleton x) = Some x.
+  Proof.
+    intros [ [ ] | [ ] |  | [ ] ]; try easy; cbn;
+    rewrite Z.compare_refl, Pcompare_refl; reflexivity.
+  Qed.
+
+  Program Definition ge : t -> t_opt := @Ige prec emax.
+  Program Definition le : t -> t_opt := @Ile prec emax.
+  Program Definition lt : t -> t_opt := @Ilt prec emax.
+  Program Definition gt : t -> t_opt := @Igt prec emax.
+
   Program Definition le_inv : t -> t -> (t_opt * t_opt) := @Ile_inv prec emax.
   Program Definition ge_inv : t -> t -> (t_opt * t_opt) := @Ige_inv prec emax.
   Program Definition lt_inv : t -> t -> (t_opt * t_opt) := @Ilt_inv prec emax.
@@ -110,4 +154,20 @@ Module Intv32.
       contains_opt (fst (eq_inv I1 I2)) x /\ contains_opt (snd (eq_inv I1 I2)) y.
   Proof. apply (@Ieq_inv_correct prec emax). Qed.
 
+  Theorem le_correct :
+    forall (I : t) (x y : float32), contains I y -> x <= y -> contains_opt (le I) x.
+  Proof. apply (@Ile_correct prec emax). Qed.
+
+  Theorem lt_correct :
+    forall (I : t) (x y : float32), contains I y -> Bltb x y = true -> contains_opt (lt I) x.
+  Proof. apply (@Ilt_correct prec emax). Qed.
+
+  Theorem ge_correct :
+    forall (I : t) (x y : float32), contains I y -> y <= x -> contains_opt (ge I) x.
+  Proof. apply (@Ige_correct prec emax). Qed.
+
+  Theorem gt_correct :
+  forall (I : t) (x y : float32), contains I y -> Bltb y x = true -> contains_opt (gt I) x.
+  Proof. apply (@Igt_correct prec emax). Qed.
+
 End Intv32.
\ No newline at end of file

farith2/thry/Utils.v

@@ -355,6 +355,24 @@ Proof.
   lra.
 Qed.
 
+Lemma Beqb_refl :
+  forall x : float, is_nan x = false -> Beqb x x = true.
+Proof.
+  intros; fdestruct x.
+  unfold Beqb; cbn.
+  destruct s;
+  rewrite (Zaux.Zcompare_Eq e e) by reflexivity;
+  now rewrite (Pcompare_refl m).
+Qed.
+
+Lemma Beqb_nan_l :
+  forall (x : float), Beqb NaN x = false.
+Proof. fdestruct x. Qed.
+
+Lemma Beqb_nan_r :
+  forall (x : float), Beqb x NaN = false.
+Proof. fdestruct x. Qed.
+
 Lemma Beqb_Bleb :
   forall x y : float, Beqb x y = true -> Bleb x y = true.
 Proof.
@@ -364,6 +382,7 @@ Proof.
   now apply Reqb_Req in Hxy.
 Qed.
 
+
 Lemma Bleb_refl :
   forall x:float, is_nan x = false -> Bleb x x = true.
 Proof.
@@ -381,6 +400,35 @@ Proof.
   lra.
 Qed.
 
+Lemma Bleb_antisymm :
+  forall x y : float, x <= y <= x -> Beqb x y = true.
+Proof.
+  intros x y [H1 H2].
+  fdestruct x; fdestruct y;
+  try (destruct s; try easy);
+  try (destruct s0; try easy).
+  - cbn in H1, H2.
+    destruct (e ?= e1)%Z eqn:E1; rewrite (Z.compare_antisym _ _), E1 in H2; simpl in H2; try discriminate.
+    rewrite <- ZC4 in H1.
+    destruct (Pos.compare_cont Eq m0 m) eqn:E2; try easy.
+    apply (Pcompare_Eq_eq _ _) in E2; subst.
+    apply (Z.compare_eq) in E1; subst; cbn.
+    now rewrite Z.compare_refl, Pcompare_refl.
+  - cbn in H1, H2.
+    destruct (e ?= e1)%Z eqn:E1; rewrite (Z.compare_antisym _ _), E1 in H2; simpl in H2; try discriminate.
+    destruct (Pos.compare_cont Eq m m0) eqn:E2; try easy.
+    + apply (Pcompare_Eq_eq) in E2; subst.
+      apply (Z.compare_eq) in E1; subst; cbn.
+      now rewrite Z.compare_refl, Pcompare_refl.
+    + destruct (Pos.compare_cont Eq m0 m) eqn:E3; try easy.
+      * apply Pos.compare_nge_iff in E2.
+        apply Pos.compare_eq_iff in E3.
+        intuition.
+      * apply Pos.compare_nge_iff in E2.
+        apply Pos.compare_nge_iff in E3.
+        intuition.
+Qed.
+
 Lemma Beqb_symm :
   forall x y : float, Beqb x y = true -> Beqb y x = true.
 Proof.
@@ -403,6 +451,15 @@ Proof.
     rewrite Raux.Rcompare_Eq; reflexivity.
 Qed.
 
+Lemma Beqb_trans :
+  forall x y z : float, Beqb x y = true -> Beqb y z = true -> Beqb x z = true.
+Proof.
+  intros x y z H1 H2.
+  apply Bleb_antisymm; split.
+  - apply (Bleb_trans _ _ _ (Beqb_Bleb _ _ H1) (Beqb_Bleb _ _ H2)).
+  - apply (Bleb_trans _ _ _ (Beqb_Bleb _ _ (Beqb_symm _ _ H2)) (Beqb_Bleb _ _ (Beqb_symm _ _ H1))).
+Qed.
+
 Lemma Bleb_false_Bltb :
   forall x y:float, is_nan x = false -> is_nan y = false -> Bleb x y = false -> Bltb y x = true.
 Proof.