From 837876a6da1d92ef4e9f329859f4feba72d74608 Mon Sep 17 00:00:00 2001
From: Arthur Correnson <arthur.correnson@gmail.com>
Date: Thu, 8 Jul 2021 17:22:55 +0200
Subject: [PATCH] [ieee/coq] cleaning proofs

---
 src_common/ieee/coq/.nra.cache        | Bin 1557 -> 1998 bytes
 src_common/ieee/coq/Correction_thms.v | 185 +++++---------------------
 src_common/ieee/coq/Rextended.v       |  16 +++
 3 files changed, 50 insertions(+), 151 deletions(-)

diff --git a/src_common/ieee/coq/.nra.cache b/src_common/ieee/coq/.nra.cache
index ddc240ee3583d254990ee9fa18e1ff3d2d5b7431..a3ffd9207cbe64a8ee0e7dcb6a377133632e88ac 100644
GIT binary patch
delta 122
zcmbQrbB=$5DBI*%R(9SB1_)ROq}ELqWR;nGj!}YT;lzm!lLMJWCeLD(oLt8&H1Ryg
z<PFRUlP54Kih$%cO;|9|!NFm|0tW}D1q&8Vn4G|D08%5soH$vHg>UjXCV|NTtXu*U
QCO9lvJOM}oF_3To0P24!RsaA1

delta 7
OcmX@dKb2>LC>sC^Tmnh}

diff --git a/src_common/ieee/coq/Correction_thms.v b/src_common/ieee/coq/Correction_thms.v
index 16ad45b4a..29969ef9a 100644
--- a/src_common/ieee/coq/Correction_thms.v
+++ b/src_common/ieee/coq/Correction_thms.v
@@ -55,52 +55,25 @@ Proof.
       destruct s1, s2; simpl in *; try easy.
       unfold Defs.F2R in Hs; simpl in Hs.
       apply sign_neg_inv in Hs.
-      assert (forall x, IZR (Z.pos x) > 0)%R.
-      { induction x; try lra.
-        + apply (Rgt_trans _ (IZR (Z.pos x))); auto.
-          apply IZR_lt; lia.
-        + apply (Rgt_trans _ (IZR (Z.pos x))); auto.
-          apply IZR_lt; lia.
-      }
-      pose proof (H m2).
-      pose proof (H m3).
-      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3).
-      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5).
-      nra.
+      pose proof (IZR_pos m2); pose proof (IZR_pos m3);
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3);
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5); nra.
     + simpl in *. rewrite H1; simpl.
       fdestruct x; fdestruct y.
       destruct s1, s2; simpl in *; try easy.
       unfold Defs.F2R in Hs; simpl in Hs.
       apply sign_pos_inv in Hs.
-      assert (forall x, IZR (Z.neg x) < 0)%R.
-      { induction x; try lra.
-        + apply (Rgt_trans _ (IZR (Z.neg x))); auto.
-          apply IZR_lt; lia.
-        + apply (Rgt_trans _ (IZR (Z.neg x))); auto.
-          apply IZR_lt; lia.
-      }
-      pose proof (H m2).
-      pose proof (H m3).
-      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3).
-      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5).
-      nra.
+      pose proof (IZR_neg m2); pose proof (IZR_neg m3);
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3);
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5); nra.
     + simpl in *. rewrite H1; simpl.
       fdestruct x; fdestruct y.
       destruct s1, s2; simpl in *; try easy.
       unfold Defs.F2R in Hs; simpl in Hs.
       apply sign_neg_inv in Hs.
-      assert (forall x, IZR (Z.pos x) > 0)%R.
-      { induction x; try lra.
-        + apply (Rgt_trans _ (IZR (Z.pos x))); auto.
-          apply IZR_lt; lia.
-        + apply (Rgt_trans _ (IZR (Z.pos x))); auto.
-          apply IZR_lt; lia.
-      }
-      pose proof (H m2).
-      pose proof (H m3).
-      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3).
-      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5).
-      nra.
+      pose proof (IZR_pos m2); pose proof (IZR_pos m3);
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3);
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5); nra.
     + simpl in *. rewrite H1; simpl.
       fdestruct x; fdestruct y.
       destruct s1, s2; simpl in *; try easy.
@@ -109,120 +82,58 @@ Proof.
       change (Z.neg m2) with (- Z.pos m2)%Z in Hs.
       change (Z.neg m3) with (- Z.pos m3)%Z in Hs.
       repeat rewrite opp_IZR in Hs.
-      assert (forall x, IZR (Z.pos x) > 0)%R.
-      { induction x; try lra.
-        + apply (Rgt_trans _ (IZR (Z.pos x))); auto.
-          apply IZR_lt; lia.
-        + apply (Rgt_trans _ (IZR (Z.pos x))); auto.
-          apply IZR_lt; lia.
-      }
-      pose proof (H m2).
-      pose proof (H m3).
-      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3).
-      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5).
-      nra.
+      pose proof (IZR_pos m2); pose proof (IZR_pos m3);
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3);
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5); nra.
     + simpl in *. rewrite H1; simpl.
       fdestruct x; fdestruct y.
       destruct s1, s2; simpl in *; try easy.
       unfold Defs.F2R in Hs; simpl in Hs.
       apply sign_neg_inv in Hs.
-      assert (forall x, IZR (Z.pos x) > 0)%R.
-      { induction x; try lra.
-        + apply (Rgt_trans _ (IZR (Z.pos x))); auto.
-          apply IZR_lt; lia.
-        + apply (Rgt_trans _ (IZR (Z.pos x))); auto.
-          apply IZR_lt; lia.
-      }
-      pose proof (H m2).
-      pose proof (H m3).
-      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3).
-      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5).
-      nra.
+      pose proof (IZR_pos m2); pose proof (IZR_pos m3);
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3);
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5); nra.
     + simpl in *. rewrite H1; simpl.
       fdestruct x; fdestruct y.
       destruct s1, s2; simpl in *; try easy.
       unfold Defs.F2R in Hs; simpl in Hs.
       apply sign_pos_inv in Hs.
-      assert (forall x, IZR (Z.neg x) < 0)%R.
-      { induction x; try lra.
-        + apply (Rgt_trans _ (IZR (Z.neg x))); auto.
-          apply IZR_lt; lia.
-        + apply (Rgt_trans _ (IZR (Z.neg x))); auto.
-          apply IZR_lt; lia.
-      }
-      pose proof (H m2).
-      pose proof (H m3).
-      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3).
-      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5).
+      pose proof (IZR_neg m2); pose proof (IZR_neg m3);
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5);
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3);
       nra.
     + simpl in *. rewrite H1; simpl.
       fdestruct x; fdestruct y.
       destruct s1, s2; simpl in *; try easy.
       unfold Defs.F2R in Hs; simpl in Hs.
       apply sign_neg_inv in Hs.
-      assert (forall x, IZR (Z.pos x) > 0)%R.
-      { induction x; try lra.
-        + apply (Rgt_trans _ (IZR (Z.pos x))); auto.
-          apply IZR_lt; lia.
-        + apply (Rgt_trans _ (IZR (Z.pos x))); auto.
-          apply IZR_lt; lia.
-      }
-      pose proof (H m2).
-      pose proof (H m3).
-      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3).
-      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5).
-      nra.
+      pose proof (IZR_pos m2); pose proof (IZR_pos m3);
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3);
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5); nra.
     + simpl in *. rewrite H1; simpl.
       fdestruct x; fdestruct y.
       destruct s1, s2; simpl in *; try easy.
       unfold Defs.F2R in Hs; simpl in Hs.
       apply sign_pos_inv in Hs.
-      assert (forall x, IZR (Z.neg x) < 0)%R.
-      { induction x; try lra.
-        + apply (Rgt_trans _ (IZR (Z.neg x))); auto.
-          apply IZR_lt; lia.
-        + apply (Rgt_trans _ (IZR (Z.neg x))); auto.
-          apply IZR_lt; lia.
-      }
-      pose proof (H m2).
-      pose proof (H m3).
-      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3).
-      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5).
-      nra.
+      pose proof (IZR_neg m2); pose proof (IZR_neg m3);
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3);
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5); nra.
     + simpl in *. rewrite H1; simpl.
       fdestruct x; fdestruct y.
       destruct s1, s2; simpl in *; try easy.
       unfold Defs.F2R in Hs; simpl in Hs.
       apply sign_neg_inv in Hs.
-      assert (forall x, IZR (Z.pos x) > 0)%R.
-      { induction x; try lra.
-        + apply (Rgt_trans _ (IZR (Z.pos x))); auto.
-          apply IZR_lt; lia.
-        + apply (Rgt_trans _ (IZR (Z.pos x))); auto.
-          apply IZR_lt; lia.
-      }
-      pose proof (H m2).
-      pose proof (H m3).
-      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3).
-      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5).
-      nra.
+      pose proof (IZR_pos m2); pose proof (IZR_pos m3);
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3);
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5); nra.
     + simpl in *. rewrite H1; simpl.
       fdestruct x; fdestruct y.
       destruct s1, s2; simpl in *; try easy.
       unfold Defs.F2R in Hs; simpl in Hs.
       apply sign_pos_inv in Hs.
-      assert (forall x, IZR (Z.neg x) < 0)%R.
-      { induction x; try lra.
-        + apply (Rgt_trans _ (IZR (Z.neg x))); auto.
-          apply IZR_lt; lia.
-        + apply (Rgt_trans _ (IZR (Z.neg x))); auto.
-          apply IZR_lt; lia.
-      }
-      pose proof (H m2).
-      pose proof (H m3).
-      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3).
-      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5).
-      nra.
+      pose proof (IZR_neg m2); pose proof (IZR_neg m3);
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3);
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5); nra.
   - apply do_overflow_false in Ho1.
     unfold dont_overflow in Ho1.
     rewrite <- Ex, <- Ey in *.
@@ -250,14 +161,7 @@ Proof.
   - destruct s; simpl; try easy.
     unfold Defs.F2R; simpl.
     apply Raux.Rle_bool_true.
-    assert (forall x, IZR (Z.pos x) > 0)%R.
-    { induction x; try lra.
-        + apply (Rgt_trans _ (IZR (Z.pos x))); auto.
-          apply IZR_lt; lia.
-        + apply (Rgt_trans _ (IZR (Z.pos x))); auto.
-          apply IZR_lt; lia.
-    }
-    pose proof (H m0).
+    pose proof (IZR_pos m0).
     pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
     nra.
   - apply Raux.Rle_bool_true; lra.
@@ -265,40 +169,19 @@ Proof.
   - destruct s; simpl; try easy.
     unfold Defs.F2R; simpl.
     apply Raux.Rle_bool_true.
-    assert (forall x, IZR (Z.pos x) > 0)%R.
-    { induction x; try lra.
-        + apply (Rgt_trans _ (IZR (Z.pos x))); auto.
-          apply IZR_lt; lia.
-        + apply (Rgt_trans _ (IZR (Z.pos x))); auto.
-          apply IZR_lt; lia.
-    }
-    pose proof (H m0).
+    pose proof (IZR_pos m0).
     pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
     nra.
   - destruct s; simpl; try easy.
     unfold Defs.F2R; simpl.
     apply Raux.Rle_bool_true.
-    assert (forall x, IZR (Z.neg x) < 0)%R.
-    { induction x; try lra.
-        + apply (Rgt_trans _ (IZR (Z.neg x))); auto.
-          apply IZR_lt; lia.
-        + apply (Rgt_trans _ (IZR (Z.neg x))); auto.
-          apply IZR_lt; lia.
-    }
-    pose proof (H m0).
+    pose proof (IZR_neg m0).
     pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
     nra.
   - destruct s; simpl; try easy.
     unfold Defs.F2R; simpl.
     apply Raux.Rle_bool_true.
-    assert (forall x, IZR (Z.neg x) < 0)%R.
-    { induction x; try lra.
-        + apply (Rgt_trans _ (IZR (Z.neg x))); auto.
-          apply IZR_lt; lia.
-        + apply (Rgt_trans _ (IZR (Z.neg x))); auto.
-          apply IZR_lt; lia.
-    }
-    pose proof (H m0).
+    pose proof (IZR_neg m0).
     pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
     nra.
   - destruct s, s0; simpl; try easy;
diff --git a/src_common/ieee/coq/Rextended.v b/src_common/ieee/coq/Rextended.v
index 3fda6b864..f15c5136b 100644
--- a/src_common/ieee/coq/Rextended.v
+++ b/src_common/ieee/coq/Rextended.v
@@ -42,6 +42,22 @@ Proof.
   intros; lra.
 Qed.
 
+Lemma IZR_neg :
+  (forall x, IZR (Z.neg x) < 0)%R.
+Proof.
+  induction x; try lra;
+  apply (Rgt_trans _ (IZR (Z.neg x))); auto;
+  apply IZR_lt; lia.
+Qed.
+
+Lemma IZR_pos :
+  (forall x, IZR (Z.pos x) > 0)%R.
+Proof.
+  induction x; try lra;
+  apply (Rgt_trans _ (IZR (Z.pos x))); auto;
+  apply IZR_lt; lia.
+Qed.
+
 End Rutils.
 
 
-- 
GitLab