Commit 197ee571 authored by Arthur Correnson's avatar Arthur Correnson Committed by François Bobot
Browse files

add Intv32's constructor 'singleton'

parent 25a70711
......@@ -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 =
......
......@@ -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
......
......@@ -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.
......
......@@ -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
......@@ -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.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment