From 2f9037bbced8bd1cfd15c215154a14fd0758b10d Mon Sep 17 00:00:00 2001
From: Arthur Correnson <arthur.correnson@gmail.com>
Date: Tue, 20 Jul 2021 18:00:51 +0200
Subject: [PATCH] add a module for extraction
---
src_common/ieee/coq/Colibri2_interval.v | 176 ++++++++---------------
src_common/ieee/coq/Interval.v | 180 +++++++++++++++++++++++-
2 files changed, 234 insertions(+), 122 deletions(-)
diff --git a/src_common/ieee/coq/Colibri2_interval.v b/src_common/ieee/coq/Colibri2_interval.v
index 8724b1f28..29573a66e 100644
--- a/src_common/ieee/coq/Colibri2_interval.v
+++ b/src_common/ieee/coq/Colibri2_interval.v
@@ -1,127 +1,61 @@
-From Coq Require Import ZArith Extraction Bool.
-From F Require Import Utils Interval.
+From Coq Require Import ZArith Extraction Bool Psatz.
From Flocq Require Import IEEE754.BinarySingleNaN FLX.
+From F Require Import Utils Interval.
+
+Module Intv32.
+ Definition prec := 24%Z.
+ Definition emax := 128%Z.
+ Definition float32 := float prec emax.
+
+ Lemma Hprec : Prec_gt_0 prec.
+ Proof. unfold Prec_gt_0, prec; lia. Qed.
+
+ Lemma Hemax : Prec_lt_emax prec emax.
+ Proof. unfold Prec_lt_emax, prec, emax; lia. Qed.
+
+ Definition t := Interval prec emax.
+
+ Program Definition contains : t -> float32 -> Prop := contains prec emax.
+
+ Definition inter : t -> t -> t := @inter prec emax.
+
+ Definition add : mode -> t -> t -> t := @Iadd prec emax Hprec Hemax.
+
+ Lemma inter_correct :
+ forall (i1 i2 : t) (x : float32),
+ contains i1 x -> contains i2 x -> contains (inter i1 i2) x.
+ Proof. apply (inter_correct prec emax). Qed.
+
+ Lemma inter_precise :
+ forall (i1 i2 : t) (x : float32),
+ contains (inter i1 i2) x -> contains i1 x /\ contains i2 x.
+ Proof.
+ intros; split.
+ - apply (inter_precise_l prec emax _ _ _ H).
+ - apply (inter_precise_r prec emax _ _ _ H).
+ Qed.
+
+ Lemma add_correct :
+ forall (m : mode) (i1 i2 : t) (x y : float32),
+ contains i1 x -> contains i2 y -> contains (add m i1 i2) (@Bplus prec emax Hprec Hemax m x y).
+ Proof. apply Iadd_correct. Qed.
+
+ Program Definition top : t := Some (Intv prec emax -oo +oo true).
-Section Colibri2_interval.
-
-Variable prec : Z.
-Variable emax : Z.
-Context (Hprec : Prec_gt_0 prec).
-Context (Hemax : Prec_lt_emax prec emax).
-
-Definition float := binary_float prec emax.
-
-Inductive Interval' :=
- | Inan : Interval'
- | Intv : forall (lo hi : float) (nan : bool), Interval'.
-
-Definition valid (I : option Interval') :=
- match I with
- | Some (Intv lo hi _) => lo <= hi
- | _ => True
- end.
-
-Definition Interval := { I : option Interval' | valid I }.
-
-Program Definition contains (I : option Interval') (x : float) : Prop :=
- match I with
- | None => False
- | Some Inan => is_nan x = true
- | Some (Intv lo hi nan) =>
- lo <= x <= hi \/ (is_nan x && nan = true)
- end.
-
-Program Definition inter' (I1 I2 : option Interval') : option Interval' :=
- match I1, I2 with
- | None, _ => None
- | _, None => None
- | Some Inan, Some Inan => Some Inan
- | Some Inan, Some (Intv _ _ nan) =>
- if nan then Some Inan else None
- | Some (Intv _ _ nan), Some (Inan) =>
- if nan then Some (Inan) else None
- | Some (Intv lo1 hi1 nan1), Some (Intv lo2 hi2 nan2) =>
- if Bltb hi1 lo2 || Bltb hi2 lo1 then
- if nan1 && nan2 then Some Inan else None
- else
- Some (Intv (Bmax lo1 lo2) (Bmin hi1 hi2) (nan1 && nan2))
- end.
-
-Ltac ieasy :=
- simpl in *; try easy; try (intuition; fail).
-
-Ltac sdestruct x :=
- try destruct x; simpl; easy.
-
-
-Program Definition inter (I1 I2 : Interval) : Interval :=
- inter' I1 I2.
-Next Obligation with auto.
- destruct I1 as [[[ | lo1 hi1 nan1]|] H1], I2 as [[[ | lo2 hi2 nan2]|] H2]; ieasy; try (now destruct nan1 || now destruct nan2).
- case (Bltb (hi1) (lo2)) eqn:?, (Bltb (hi2) (lo1)) eqn:?; simpl; try (destruct nan1, nan2; simpl; easy).
- pose proof (le_not_nan_l _ _ H1).
- pose proof (le_not_nan_r _ _ H2).
- pose proof (le_not_nan_r _ _ H1).
- pose proof (le_not_nan_l _ _ H2).
- auto using Bmax_le, Bmin_le, Bltb_false_Bleb.
-Defined.
-
-Program Lemma inter_precise_l :
- forall I1 I2, forall x, contains (inter I1 I2) x -> contains I1 x.
-Proof with auto.
- intros [[[|lo1 hi1 [ ]]|] H1] [[[|lo2 hi2 [ ]]|] H2] x Hx; simpl in *...
- + intuition.
- + case (Bltb hi1 lo2) eqn:?, (Bltb hi2 lo1) eqn:?; simpl in *; intuition.
- left; split; [ apply (Bmax_le_inv _ _ _ _ _ H0) | apply (Bmin_le_inv _ _ _ _ _ H3) ].
- + case (Bltb hi1 lo2) eqn:?, (Bltb hi2 lo1) eqn:?; simpl in *; intuition.
- - left; split; [apply (Bmax_le_inv _ _ _ _ _ H0) | apply (Bmin_le_inv _ _ _ _ _ H3) ].
- - destruct x...
- + case (Bltb hi1 lo2) eqn:?, (Bltb hi2 lo1) eqn:?; simpl in *; intuition.
- left; split; [ apply (Bmax_le_inv _ _ _ _ _ H0) | apply (Bmin_le_inv _ _ _ _ _ H3) ].
- + case (Bltb hi1 lo2) eqn:?, (Bltb hi2 lo1) eqn:?; simpl in *; intuition.
- left; split; [ apply (Bmax_le_inv _ _ _ _ _ H0) | apply (Bmin_le_inv _ _ _ _ _ H3) ].
-Qed.
-
-Program Lemma inter_precise_r :
- forall I1 I2, forall x, contains (inter I1 I2) x -> contains I2 x.
-Proof with auto.
- intros [[[|lo1 hi1 [ ]]|] H1] [[[|lo2 hi2 [ ]]|] H2] x Hx; simpl in *...
- + intuition.
- + case (Bltb hi1 lo2) eqn:?, (Bltb hi2 lo1) eqn:?; simpl in *; intuition.
- left; split; [ apply (Bmax_le_inv _ _ _ _ _ H0) | apply (Bmin_le_inv _ _ _ _ _ H3) ].
- + case (Bltb hi1 lo2) eqn:?, (Bltb hi2 lo1) eqn:?; simpl in *; intuition.
- left; split; [apply (Bmax_le_inv _ _ _ _ _ H0) | apply (Bmin_le_inv _ _ _ _ _ H3) ].
- + case (Bltb hi1 lo2) eqn:?, (Bltb hi2 lo1) eqn:?; simpl in *; intuition.
- - left; split; [ apply (Bmax_le_inv _ _ _ _ _ H0) | apply (Bmin_le_inv _ _ _ _ _ H3) ].
- - destruct x...
- + case (Bltb hi1 lo2) eqn:?, (Bltb hi2 lo1) eqn:?; simpl in *; intuition.
- left; split; [ apply (Bmax_le_inv _ _ _ _ _ H0) | apply (Bmin_le_inv _ _ _ _ _ H3) ].
-Qed.
-
-Program Lemma inter_correct :
- forall (I1 I2 : Interval), forall x, contains I1 x -> contains I2 x -> contains (inter I1 I2) x.
-Proof with auto.
- intros [[[|lo1 hi1 nan1]|] H1] [[[|lo2 hi2 nan2]|] H2] x Hx1 Hx2; simpl in *...
- - fdestruct x; destruct nan2, Hx2; try easy.
- - fdestruct x; destruct nan1, Hx1; try easy.
- - pose proof (le_not_nan_l _ _ H1).
- pose proof (le_not_nan_r _ _ H1).
- pose proof (le_not_nan_l _ _ H2).
- pose proof (le_not_nan_r _ _ H2).
- destruct Hx1 as [[Hc1 Hc1'] |], Hx2 as [[Hc2 Hc2'] |]; try (fdestruct x ; fail).
- + pose proof (Hlt1 := Bleb_trans _ _ _ _ _ Hc2 Hc1').
- apply Bleb_true_Bltb in Hlt1...
- pose proof (Hlt2 := Bleb_trans _ _ _ _ _ Hc1 Hc2').
- apply Bleb_true_Bltb in Hlt2...
- rewrite Hlt1, Hlt2; simpl; left; split; auto using Bmax_le, Bmin_le.
- + fdestruct x; destruct nan2, nan1, (Bltb hi1 _), (Bltb hi2); simpl; try easy.
- now right.
-Qed.
-
-End Colibri2_interval.
-
-Recursive Extraction Interval.
+ Program Definition bot : t := None.
+ Lemma top_correct :
+ forall (x : float32), contains top x.
+ Proof with auto.
+ unfold top, contains; fdestruct x; simpl...
+ Qed.
+ Lemma bot_correct :
+ forall (x : float32), contains bot x -> False.
+ Proof with auto.
+ unfold bot, contains; fdestruct x.
+ Qed.
+End Intv32.
+Recursive Extraction Intv32.
diff --git a/src_common/ieee/coq/Interval.v b/src_common/ieee/coq/Interval.v
index 7ea3fdf19..a60513f92 100644
--- a/src_common/ieee/coq/Interval.v
+++ b/src_common/ieee/coq/Interval.v
@@ -15,6 +15,184 @@ Context (Hemax : Prec_lt_emax prec emax).
Definition float := binary_float prec emax.
+Inductive Interval' :=
+ | Inan : Interval'
+ | Intv : forall (lo hi : float) (nan : bool), Interval'.
+
+Definition valid (I : option Interval') :=
+ match I with
+ | Some (Intv lo hi _) => lo <= hi
+ | _ => True
+ end.
+
+Definition Interval := { I : option Interval' | valid I }.
+
+Program Definition contains (I : option Interval') (x : float) : Prop :=
+ match I with
+ | None => False
+ | Some Inan => is_nan x = true
+ | Some (Intv lo hi nan) =>
+ lo <= x <= hi \/ (is_nan x && nan = true)
+ end.
+
+Program Definition inter' (I1 I2 : option Interval') : option Interval' :=
+ match I1, I2 with
+ | None, _ => None
+ | _, None => None
+ | Some Inan, Some Inan => Some Inan
+ | Some Inan, Some (Intv _ _ nan) =>
+ if nan then Some Inan else None
+ | Some (Intv _ _ nan), Some (Inan) =>
+ if nan then Some (Inan) else None
+ | Some (Intv lo1 hi1 nan1), Some (Intv lo2 hi2 nan2) =>
+ if Bltb hi1 lo2 || Bltb hi2 lo1 then
+ if nan1 && nan2 then Some Inan else None
+ else
+ Some (Intv (Bmax lo1 lo2) (Bmin hi1 hi2) (nan1 && nan2))
+ end.
+
+Ltac ieasy :=
+ simpl in *; try easy; try (intuition; fail).
+
+Ltac sdestruct x :=
+ try destruct x; simpl; easy.
+
+
+Program Definition inter (I1 I2 : Interval) : Interval :=
+ inter' I1 I2.
+Next Obligation with auto.
+ destruct I1 as [[[ | lo1 hi1 nan1]|] H1], I2 as [[[ | lo2 hi2 nan2]|] H2]; ieasy; try (now destruct nan1 || now destruct nan2).
+ case (Bltb (hi1) (lo2)) eqn:?, (Bltb (hi2) (lo1)) eqn:?; simpl; try (destruct nan1, nan2; simpl; easy).
+ pose proof (le_not_nan_l _ _ H1).
+ pose proof (le_not_nan_r _ _ H2).
+ pose proof (le_not_nan_r _ _ H1).
+ pose proof (le_not_nan_l _ _ H2).
+ auto using Bmax_le, Bmin_le, Bltb_false_Bleb.
+Defined.
+
+Program Lemma inter_precise_l :
+ forall I1 I2, forall x, contains (inter I1 I2) x -> contains I1 x.
+Proof with auto.
+ intros [[[|lo1 hi1 nan1]|] H1] [[[|lo2 hi2 nan2]|] H2] x Hx; simpl in *...
+ + destruct nan2; fdestruct x.
+ + right; destruct nan1; fdestruct x.
+ + case (Bltb hi1 lo2) eqn:?, (Bltb hi2 lo1) eqn:?; simpl in *;
+ try (right; destruct nan1, nan2; simpl in *; fdestruct x; fail).
+ destruct Hx as [[Hc1 Hc2] | H ].
+ - left; split; [ apply (Bmax_le_inv _ _ _ _ _ Hc1) | apply (Bmin_le_inv _ _ _ _ _ Hc2) ].
+ - repeat rewrite andb_true_iff in H; intuition.
+Qed.
+
+Program Lemma inter_precise_r :
+ forall I1 I2, forall x, contains (inter I1 I2) x -> contains I2 x.
+Proof with auto.
+ intros [[[|lo1 hi1 nan1]|] H1] [[[|lo2 hi2 nan2]|] H2] x Hx; simpl in *...
+ + right; destruct nan2; fdestruct x.
+ + destruct nan1; fdestruct x.
+ + case (Bltb hi1 lo2) eqn:?, (Bltb hi2 lo1) eqn:?; simpl in *;
+ try (right; destruct nan1, nan2; simpl in *; fdestruct x; fail).
+ destruct Hx as [[Hc1 Hc2] | H ].
+ - left; split; [ apply (Bmax_le_inv _ _ _ _ _ Hc1) | apply (Bmin_le_inv _ _ _ _ _ Hc2) ].
+ - repeat rewrite andb_true_iff in H; intuition.
+Qed.
+
+Program Lemma inter_correct :
+ forall (I1 I2 : Interval), forall x, contains I1 x -> contains I2 x -> contains (inter I1 I2) x.
+Proof with auto.
+ intros [[[|lo1 hi1 nan1]|] H1] [[[|lo2 hi2 nan2]|] H2] x Hx1 Hx2; simpl in *...
+ - fdestruct x; destruct nan2, Hx2; try easy.
+ - fdestruct x; destruct nan1, Hx1; try easy.
+ - pose proof (le_not_nan_l _ _ H1).
+ pose proof (le_not_nan_r _ _ H1).
+ pose proof (le_not_nan_l _ _ H2).
+ pose proof (le_not_nan_r _ _ H2).
+ destruct Hx1 as [[Hc1 Hc1'] |], Hx2 as [[Hc2 Hc2'] |]; try (fdestruct x ; fail).
+ + pose proof (Hlt1 := Bleb_trans _ _ _ _ _ Hc2 Hc1').
+ apply Bleb_true_Bltb in Hlt1...
+ pose proof (Hlt2 := Bleb_trans _ _ _ _ _ Hc1 Hc2').
+ apply Bleb_true_Bltb in Hlt2...
+ rewrite Hlt1, Hlt2; simpl; left; split; auto using Bmax_le, Bmin_le.
+ + fdestruct x; destruct nan2, nan1, (Bltb hi1 _), (Bltb hi2); simpl; try easy.
+ now right.
+Qed.
+
+Definition Iadd' (m : mode) (I1 I2 : option Interval') : option Interval' :=
+ match I1, I2 with
+ | None, _ => None
+ | _, None => None
+ | Some Inan, _ => Some Inan
+ | _, Some Inan => Some Inan
+ | Some (Intv l h n) as i1, Some (Intv l' h' n') as i2 =>
+ let sum1 := Bplus m l l' in
+ let sum2 := Bplus m h h' in
+ match is_nan sum1 with
+ | true =>
+ match is_nan sum2 with
+ | true => Some Inan
+ | false => Some (Intv +oo +oo true)
+ end
+ | false =>
+ match is_nan sum2 with
+ | true => Some (Intv -oo -oo true)
+ | false => Some (Intv sum1 sum2 (n || n' || (Beqb h +oo && Beqb l' -oo) || (Beqb h' +oo && Beqb l -oo)))
+ end
+ end
+ end.
+
+Program Definition Iadd (m : mode) (I1 I2 : Interval) : Interval :=
+ Iadd' m I1 I2.
+Next Obligation with auto.
+ destruct I1 as [[[ | l1 h1 ]|] H1], I2 as [[[ | l2 h2 ]|] H2]; simpl in *...
+ destruct (is_nan (Bplus m l1 l2)) eqn:E1, (is_nan (Bplus m h1 h2)) eqn:E2; try easy; simpl.
+ apply B2Rx_le; auto.
+ repeat (rewrite Bplus_correct; auto).
+ apply round_le.
+ eapply leb_trans.
+ - apply (add_leb_mono_l _ _ _ (le_B2Rx _ _ H1)).
+ - apply (add_leb_mono_r _ _ _ (le_B2Rx _ _ H2)).
+Qed.
+
+Ltac tryit t a :=
+ try (t a; fail).
+
+
+Program Lemma Iadd_correct :
+ forall m (I1 I2 : Interval) (x y : float), contains I1 x -> contains I2 y -> contains (Iadd m I1 I2) (Bplus m x y).
+Proof with auto.
+ intros m [[[ | l1 h1 ]|] H1] [[[ | l2 h2 ]|] H2] x y Hx Hy; simpl in *; try (fdestruct x; fdestruct y; fail).
+ case (is_nan (Bplus m l1 l2)) eqn:E1, (is_nan (Bplus m h1 h2)) eqn:E2; intuition; simpl.
+ all: try (fdestruct x; fdestruct y; simpl; auto; fail).
+ - destruct (Bplus_nan_inv _ _ _ E1); intuition; subst; try easy.
+ * rewrite (infp_le_is_infp _ _ _ H0) in *.
+ rewrite (infp_le_is_infp _ _ _ H1) in *.
+ fdestruct h2.
+ rewrite (le_infm_is_infm _ _ _ H5) in *...
+ * rewrite (infp_le_is_infp _ _ _ H4) in *.
+ rewrite (infp_le_is_infp _ _ _ H2) in *.
+ fdestruct h1.
+ rewrite (le_infm_is_infm _ _ _ H3) in *...
+ - destruct (Bplus_nan_inv _ _ _ E1) as [[ -> -> ] | [ [ -> -> ] | [ -> | -> ]]]; try easy;
+ fdestruct x; fdestruct y; simpl...
+ - destruct (Bplus_nan_inv _ _ _ E2) as [[ -> -> ] | [ [ -> -> ] | [ -> | -> ]]]; try easy;
+ fdestruct x; fdestruct y; simpl...
+ - destruct (is_nan (Bplus m x y)) eqn:E.
+ + right. destruct (Bplus_nan_inv _ _ _ E) as [ [-> ->] | [ [ -> -> ] | ] ].
+ * rewrite (infp_le_is_infp _ _ _ H3) in *.
+ rewrite (le_infm_is_infm _ _ _ H4) in *.
+ fdestruct l2; simpl; fdestruct h1; simpl; intuition.
+ * rewrite (infp_le_is_infp _ _ _ H5) in *.
+ rewrite (le_infm_is_infm _ _ _ H0) in *.
+ fdestruct h1; simpl; fdestruct l2; simpl; intuition.
+ * destruct H as [ -> | -> ]; fdestruct h1.
+ + left. split; now apply Bplus_le_compat'.
+ - right; fdestruct y; fdestruct x; destruct nan0; simpl; intuition.
+ - right; fdestruct y; fdestruct x; destruct nan; simpl; intuition.
+ - right; fdestruct y; fdestruct x; destruct nan; simpl; intuition.
+Qed.
+
+
+(* Definition float := binary_float prec emax.
+
Inductive Interval_aux :=
| I_Bot : Interval_aux
| I_nan : Interval_aux
@@ -315,6 +493,6 @@ Proof.
* apply Bltb_true_Bleb in E2; auto.
now rewrite (Bleb_trans _ _ _ _ _ Hc1 Hc2') in E2.
* left; split; [ now apply Bmax_le | now apply Bmin_le ].
-Qed.
+Qed. *)
End Finterval.
\ No newline at end of file
--
GitLab