Skip to content

Improve commutativity lemma for Bplus #33

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
ak-2485 wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Improve commutativity lemma for Bplus #33

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
42 changes: 37 additions & 5 deletions vcfloat/FPCore.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -740,16 +740,48 @@ Definition Zconst (t: type) `{STD: is_standard t} (i: Z) : ftype t :=
ftype_of_float
(BofZ (fprec t) (femax t) (Pos2Z.is_pos (fprecp t)) (fprec_lt_femax t) i).

Lemma is_nan_false_bplus_if_finite {NANS: Nans}: forall (t: type) `{STD: is_standard t}
(a b: ftype t),
Binary.is_finite (fprec t) (femax t) (float_of_ftype a) = true ->
Binary.is_finite (fprec t) (femax t) (float_of_ftype b) = true ->
Binary.is_nan _ _ (float_of_ftype (BPLUS a b)) = false.
Proof.
intros.
unfold BPLUS, BINOP.
destruct (float_of_ftype a), (float_of_ftype b);
simpl in *; try discriminate; auto; rewrite float_of_ftype_of_float.
destruct s, s0; simpl; auto.
destruct s, s0; simpl; auto.
destruct s, s0; simpl; auto.
cbv [Bplus]; simpl.
rewrite is_nan_BSN2B.
apply BinarySingleNaN.is_nan_binary_normalize.
Qed.

Lemma BPLUS_commut {NANS: Nans}: forall (t: type) `{STD: is_standard t}
(a b: ftype t),
plus_nan (fprec t) (femax t) (fprec_gt_one t) (float_of_ftype a) (float_of_ftype b) =
plus_nan (fprec t) (femax t) (fprec_gt_one t) (float_of_ftype b) (float_of_ftype a) ->
BPLUS a b = BPLUS b a.
Binary.is_finite (fprec t) (femax t) (float_of_ftype a) = true ->
Binary.is_finite (fprec t) (femax t) (float_of_ftype b) = true ->
BPLUS a b = BPLUS b a.
Proof.
intros.
pose proof is_nan_false_bplus_if_finite t a b H H0 as H1.
revert H1.
unfold BPLUS, BINOP.
f_equal.
apply Bplus_commut; auto.
rewrite !float_of_ftype_of_float.
intros;
destruct (float_of_ftype a), (float_of_ftype b); simpl in *;
try discriminate; auto.
destruct s, s0 ; simpl in *; auto.
revert H1.
cbv [Bplus BSN2B]; simpl.
cbv [BinarySingleNaN.Fplus_naive].
replace (Z.min e e1) with (Z.min e1 e) by lia.
set (x1:= SpecFloat.cond_Zopp s _).
set (x2:= SpecFloat.cond_Zopp s0 _).
replace (x2 + x1) with (x1 + x2) by lia.
set (bnl := BinarySingleNaN.binary_normalize _ _ _ _ _ _ _ _).
destruct bnl; simpl; intros; try discriminate; auto.
Qed.

Lemma BMULT_commut {NANS: Nans}: forall t `{STD: is_standard t} a b,
Expand Down