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

[ieee/coq] Bplus_correct (Rx)

parent 97ba681c
No related branches found
No related tags found
1 merge request!16Fp/ieee
Pipeline #36408 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 @ e1badb4a
No preview for this file type
src_common/ieee/coq/Correction_thms.v
+ 206
− 1
View file @ e1badb4a
......@@ -11,6 +11,17 @@ Context (Hemax : Prec_lt_emax prec emax).
Definition float : Type := binary_float prec emax.
Lemma B2SF_eq :
forall (x : float) y H, B2SF x = y -> x = SF2B y H.
Proof.
intros.
apply B2SF_inj.
rewrite H0.
symmetry.
apply B2SF_SF2B.
Qed.
Lemma Bplus_correct :
forall (m : mode) (x y : float),
is_nan (Bplus m x y) = false ->
......@@ -24,6 +35,200 @@ Proof.
intros m x y HnanS.
destruct (Bplus_not_nan_inv _ _ _ HnanS) as [HnanX HnanY].
induction x as [ [ ] | [ ] | | ] eqn:Ex, y as [ [ ] | [ ] | | ] eqn:Ey; try easy; try compute0.
Admitted.
unfold add.
repeat rewrite (B2Rx_finite (B754_finite _ _ _ _)); auto.
unfold round.
assert (Fx : is_finite x = true) by (rewrite Ex; auto).
assert (Fy : is_finite y = true) by (rewrite Ey; auto).
pose proof (Bplus_correct _ _ _ _ m x y Fx Fy).
destruct (do_overflow _ _ _ _) eqn:Ho1.
- apply do_overflow_true in Ho1.
unfold dont_overflow in Ho1.
rewrite <- Ex, <- Ey in *.
unfold R_imax in Ho1.
rewrite Ho1 in H.
destruct H as [H1 H2].
apply (B2SF_eq _ _ (binary_overflow_correct _ _ _ _ _ _)) in H1.
destruct m eqn:Em, (sign (B2R x + B2R y)) eqn:Hs.
+ 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.
+ 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.
+ 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.
+ 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.
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.
+ 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.
+ 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.
+ 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.
+ 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.
+ 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.
+ 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.
- apply do_overflow_false in Ho1.
unfold dont_overflow in Ho1.
rewrite <- Ex, <- Ey in *.
unfold R_imax in Ho1.
rewrite Ho1 in H.
now destruct H as [<- [Hf _]], (Bplus _ _ _).
Qed.
End Correction.
\ No newline at end of file
src_common/ieee/coq/Rextended.v
+ 14
− 0
View file @ e1badb4a
......@@ -199,6 +199,13 @@ Proof.
now rewrite <- Raux.negb_Rlt_bool, H.
Qed.
Lemma do_overflow_true :
forall m r, do_overflow m r = true -> dont_overflow m r = false.
Proof.
intros. unfold do_overflow, dont_overflow in *.
now rewrite <- Raux.negb_Rlt_bool, H.
Qed.
Lemma dont_overflow_true :
forall m r, dont_overflow m r = true -> do_overflow m r = false.
Proof.
......@@ -206,6 +213,13 @@ Proof.
now rewrite <- Raux.negb_Rle_bool, Bool.negb_false_iff.
Qed.
Lemma dont_overflow_false :
forall m r, dont_overflow m r = false -> do_overflow m r = true.
Proof.
intros. unfold do_overflow, dont_overflow in *.
now rewrite <- Bool.negb_false_iff, Raux.negb_Rlt_bool.
Qed.
Lemma F2R_congr :
forall m1 e1 m2 e2, m1 = m2 -> e1 = e2 ->
@Defs.F2R Zaux.radix2 {| Defs.Fnum := m1; Defs.Fexp := e1 |} =
......
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