Skip to content
Snippets Groups Projects
Commit 837876a6 authored by Arthur Correnson's avatar Arthur Correnson
Browse files

[ieee/coq] cleaning proofs

parent ef392fbc
No related branches found
No related tags found
1 merge request!16Fp/ieee
Pipeline #36412 waiting for manual action
Stage: test
Stage: deploy
Hide whitespace changes
Inline Side-by-side
src_common/ieee/coq/.nra.cache
+ 0
− 0
View file @ 837876a6
No preview for this file type
src_common/ieee/coq/Correction_thms.v
+ 34
− 151
View file @ 837876a6
......@@ -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;
......
src_common/ieee/coq/Rextended.v
+ 16
− 0
View file @ 837876a6
......@@ -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.
......
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