From 56178d1c8bc48c0ec816e474a6e8e8d2d2dc116c Mon Sep 17 00:00:00 2001
From: Arthur Correnson <arthur.correnson@gmail.com>
Date: Thu, 17 Jun 2021 17:21:28 +0200
Subject: [PATCH] [ieee/coq] clean sources
---
src_common/ieee/coq/finterval.v | 151 +++++++++-----------------------
1 file changed, 42 insertions(+), 109 deletions(-)
diff --git a/src_common/ieee/coq/finterval.v b/src_common/ieee/coq/finterval.v
index 023419a50..8d3e27755 100644
--- a/src_common/ieee/coq/finterval.v
+++ b/src_common/ieee/coq/finterval.v
@@ -306,36 +306,6 @@ Proof.
auto using le_is_infm.
Qed.
-Ltac idestruct x :=
- destruct x as [?a ?b ?n];
- destruct a as [ [ ] | [ ] | | ] eqn:?Ea;
- destruct b as [ [ ] | [ ] | | ] eqn:?Eb;
- destruct n as [ | ] eqn:?En;
- simpl;
- try easy.
-
-
-(* Definition Iadd2 (m : mode) (A B : Interval) : Interval :=
- let (a1, b1) := (lo A, hi A) in
- let (a2, b2) := (lo B, hi B) in
- let a := Fadd m a1 a2 in
- let b := Fadd m b1 b2 in
- let nan := (nan A || nan B) in
- match a1, b1, a2, b2 with
- | -oo, +oo, -oo, +oo => MK_INTERVAL (-oo) (+oo) true
-
- | -oo, +oo, -oo, -oo
- | -oo, -oo, -oo, +oo => MK_INTERVAL (-oo) (-oo) true
-
- | -oo, _, -oo, _ => MK_INTERVAL (-oo) b nan
-
- | +oo, +oo, +oo, +oo => MK_INTERVAL (+oo) (+oo) nan
-
- | +oo, +oo, -oo, -oo
- | -oo, -oo, +oo, +oo => MK_INTERVAL (+oo) (-oo) true
- | _, _, _, _ => A
- end. *)
-
Record Interval2 := MK_INTERVAL2 {
lo2 : B32;
hi2 : B32;
@@ -435,7 +405,6 @@ Proof.
now intros [ [ ] | [ ] | | ] H.
Qed.
-
Ltac classify_nan x :=
match goal with
| [ H : is_nan x = true |- _ ] =>
@@ -454,56 +423,28 @@ Ltac classify_inf x :=
rewrite (proj1 (is_infp_iff x) H) in * ||
assert (Hx_infp : x = +oo) by now rewrite <- is_infp_iff
| [ H : +oo <= x |- _ ] =>
- rewrite (infp_le_is_infp _ H) in * ||
- assert (Hx_infp : x = +oo) by apply (infp_le_is_infp _ H)
+ rewrite (infp_le_is_infp _ H) in *
| [ H : is_infm x = true |- _ ] =>
- rewrite (proj1 (is_infm_iff x) H) in * ||
- assert (Hx_infm : x = -oo) by now rewrite <- is_infm_iff
+ rewrite (proj1 (is_infm_iff x) H) in *
| [ H : x <= -oo |- _ ] =>
- rewrite (le_infm_is_infm x H) in * ||
- assert (Hx_infm : x = -oo) by apply (le_infm_is_infm _ H)
+ rewrite (le_infm_is_infm x H) in *
| _ => fail "can't determine if" x "is +oo or -oo"
end.
-Ltac classify x :=
- match goal with
- | [ H : _ <= x |- _ ] =>
- assert (is_nan x = false) by apply (not_nan_comp _ _ H)
- | [ H : x <= _ |- _ ] =>
- assert (is_nan x = false) by apply (not_nan_comp2 _ _ H)
- | [ H : is_nan x = true |- _ ] =>
- assert (x = B754_nan) by now rewrite <- (is_nan_iff x)
- | [ H : (is_nan x = true /\ _) |- _ ] =>
- assert (x = B754_nan) by now rewrite <- (is_nan_iff x)
- end.
-
-Ltac sanitize :=
- match goal with
- | [ H : andb _ _ = true |- _ ] =>
- rewrite Bool.andb_true_iff in H; destruct H;
- sanitize
- | [ H : _ /\ _ |- _ ] =>
- destruct H; sanitize
- | _ => idtac
- end.
-
Ltac feasy :=
try easy;
match goal with
- | |- is_nan ?x = false => classify x; (try easy; intuition)
- | |- is_finite ?x = true => classify x; (try easy; intuition)
+ | |- is_nan ?x = false => classify_nan x; (try easy; intuition)
end.
Ltac auto_contain :=
- try easy; intuition; (right; simpl; intuition); (left; simpl; intuition).
+ try easy; first [ progress (right; simpl; intuition) | progress (left; simpl; intuition) ].
Lemma contains_nan :
forall I, contains2 I B754_nan <-> nan2 I = true.
Proof.
- (* intros [ ? ? ? ? [ ] ]; simpl; split; intros. try auto_contain.
- inversion H; auto_contain. *)
- intros [ ? ? ? ? [ ] ]; simpl; split; intros; try auto_contain.
- inversion H; auto_contain.
+ intros [ ? ? ? ? [ ] ]; simpl; split; intros; try auto_contain.
+ inversion H; try easy; intuition.
Qed.
Ltac boolean :=
@@ -516,6 +457,21 @@ Ltac boolean :=
replace x with true by boolean; boolean
end.
+Ltac irewrite :=
+ match goal with
+ | [ H : infp2 _ = _ |- _ ] => rewrite H; irewrite
+ | [ H : infm2 _ = _ |- _ ] => rewrite H; irewrite
+ | [ H : nan2 _ = _ |- _ ] => rewrite H; irewrite
+ | _ => idtac
+ end.
+
+Ltac fdiscriminate x :=
+ (classify_inf x; discriminate) ||
+ (classify_nan x; discriminate).
+
+Ltac fdestruct x :=
+ destruct x as [ [ ] | [ ] | | ].
+
Lemma Iadd2_correct :
forall m ix iy x y,
check2 ix = true ->
@@ -526,48 +482,25 @@ Lemma Iadd2_correct :
Proof.
intros.
checked2.
- contained2; intuition.
- + unfold Iadd2; left; split; simpl.
- - apply Fadd_le_compat; feasy.
- - apply Fadd_le_compat; feasy.
- + classify_nan x; unfold Iadd2; rewrite H7; auto_contain.
- + unfold Iadd2; rewrite H7; simpl.
- classify_inf x.
- destruct y as [ [ ] | [ ] | | ]; auto_contain.
- classify_inf (lo2 iy); discriminate.
- + unfold Iadd2; rewrite H7; simpl.
- classify_inf x.
- destruct y as [ [ ] | [ ] | | ]; auto_contain.
- classify_inf (hi2 iy); discriminate.
- + unfold Iadd2; rewrite H7.
- classify_nan y.
- destruct x as [ [ ] | [ ] | | ]; auto_contain.
+ contained2; intuition; unfold Iadd2; irewrite.
+ + left; split; simpl; apply Fadd_le_compat; feasy.
+ + classify_nan x; auto_contain.
+ + classify_inf x. fdestruct y;
+ try fdiscriminate (lo2 iy); auto_contain.
+ + classify_inf x. fdestruct y;
+ try fdiscriminate (hi2 iy); auto_contain.
+ + classify_nan y; fdestruct x; auto_contain.
+ + classify_nan x; auto_contain.
+ + classify_nan y; fdestruct x; auto_contain.
+ + classify_nan y; fdestruct x; auto_contain.
+ + classify_inf y; fdestruct x;
+ try fdiscriminate (lo2 ix); auto_contain.
+ + classify_inf y; fdestruct x;
+ try fdiscriminate (hi2 ix); auto_contain.
+ + classify_nan x; auto_contain.
+ classify_nan x; auto_contain.
- boolean.
- + unfold Iadd2; rewrite H6; simpl.
- classify_nan y;
- destruct x as [ [ ] | [ ] | | ]; auto_contain.
- + unfold Iadd2; rewrite H6; simpl.
- classify_nan y;
- destruct x as [ [ ] | [ ] | | ]; auto_contain.
- + unfold Iadd2; rewrite H7; simpl.
- classify_inf y;
- destruct x as [ [ ] | [ ] | | ]; auto_contain.
- classify_inf (lo2 ix); discriminate.
- + unfold Iadd2; rewrite H7; simpl.
- classify_inf y;
- destruct x as [ [ ] | [ ] | | ]; auto_contain.
- classify_inf (hi2 ix); discriminate.
- + unfold Iadd2; rewrite H6; simpl.
- classify_nan x; auto_contain.
- + unfold Iadd2; rewrite H6; simpl.
- classify_nan x; auto_contain.
- + unfold Iadd2; rewrite H6, H7; simpl.
- classify_inf x; classify_inf y; auto_contain.
- + unfold Iadd2; rewrite H6, H7; simpl.
- classify_inf x; classify_inf y; auto_contain.
- + unfold Iadd2; rewrite H6, H7; simpl.
- classify_inf x; classify_inf y; auto_contain.
- + unfold Iadd2; rewrite H6, H7; simpl.
- classify_inf x; classify_inf y; auto_contain.
+ + classify_inf x; classify_inf y; auto_contain.
+ + classify_inf x; classify_inf y; auto_contain.
+ + classify_inf x; classify_inf y; auto_contain.
+ + classify_inf x; classify_inf y; auto_contain.
Qed.
\ No newline at end of file
--
GitLab