Skip to content

Adapt to gentype branch of vcfloat #8

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
andrew-appel wants to merge 3 commits into
base: main
Choose a base branch
from
Open

Adapt to gentype branch of vcfloat #8

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
16a1901
Adapt to gentype branch of vcfloat
andrew-appel Jun 2, 2023
f092f8e
Brought things up to date for vcfloat 2.1.1 and Coquelicot 3.4.0 (Coq…
andrew-appel Sep 1, 2023
dfc7316
Brought gentype branch of leapfrog up to date w.r.t. vcfloat gentype …
andrew-appel Nov 3, 2023
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
4 changes: 2 additions & 2 deletions leapfrog_project/global_roundoff_error.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,8 +25,8 @@ Proof.
intros.
rewrite <- sqrt_1.
replace (FT2R q_init) with 1.
simpl. unfold Rprod_norm, fst, snd.
f_equal; nra.
unfold Rprod_norm, fst, snd, FT2R.
f_equal. simpl. nra.
unfold FT2R, q_init.
cbv [B2R]. simpl. cbv [Defs.F2R IZR IPR]. simpl;
field_simplify; nra.
Expand Down
21 changes: 2 additions & 19 deletions leapfrog_project/local_roundoff_error.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -65,21 +65,6 @@ intros.
apply (prove_roundoff_bound_p pq H).
Qed.

Ltac unfold_all_fval := (* move this to vcfloat *)
repeat
match goal with
| |- context [fval (env_ ?e) ?x] =>
pattern (fval (env_ e) x);
let M := fresh in match goal with |- ?MM _ => set (M := MM) end;
unfold fval; try unfold x; unfold type_of_expr; unfold_fval;
repeat match goal with |- context [env_ ?a ?b ?c] =>
let u := constr:(env_ a b c) in
let u1 := eval hnf in u in
change u with u1
end;
subst M; cbv beta
end.

Lemma itern_implies_bmd_aux:
forall pq0 : state,
forall n : nat,
Expand All @@ -96,14 +81,12 @@ split.
destruct (prove_roundoff_bound_p _ H) as [? _]; clear H.
rewrite <- H0; clear H0.
simple apply f_equal.
unfold_all_fval.
reflexivity.
simpl. reflexivity.
-
destruct (prove_roundoff_bound_q _ H) as [? _]; clear H.
rewrite <- H0; clear H0.
simple apply f_equal.
unfold_all_fval.
reflexivity.
simpl. reflexivity.
Qed.

Definition local_round_off := ∥(1.235*(1/10^7) , 6.552*(1/10^8))∥.
Expand Down
16 changes: 8 additions & 8 deletions leapfrog_project/matrix_analysis.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -417,7 +417,7 @@ assert (i = 0)%nat by lia; subst i.
assert (j = 0)%nat by lia; subst j.
subst x.
red in H0.
change (@zero C_AbelianGroup) with (@zero C_Ring) in *.
change (@zero C_AbelianMonoid) with (@zero C_Ring) in *.
unfold Mmult at 1.
rewrite coeff_mat_bij by lia.
simpl.
Expand Down Expand Up @@ -479,7 +479,7 @@ assert (forall m1 m2 : @matrix C 2 2, m1=m2 ->
apply H3 in H1; destruct H1 as [H1a [H1b [H1c H1d]]].
apply H3 in H2; destruct H2 as [H2a [H2b [H2c H2d]]].
clear H3.
set (u := @coeff_mat C_AbelianGroup 2 2 (@zero C_AbelianGroup)
set (u := @coeff_mat C_AbelianMonoid 2 2 (@zero C_AbelianMonoid)
(@Mone C_Ring 2)) in *.
hnf in u. simpl in u. subst u.
simpl in *.
Expand Down Expand Up @@ -593,17 +593,17 @@ destruct i as [|[|]]; [ | | lia].
rewrite sum_Sn, sum_O.
specialize (H3 0%nat 1%nat ltac:(lia)).

change ((@coeff_mat (AbelianGroup.sort (Ring.AbelianGroup C_Ring)) 2 2
(@zero (Ring.AbelianGroup C_Ring)) Λ 0 1))
change ((@coeff_mat (AbelianMonoid.sort (Ring.AbelianMonoid C_Ring)) 2 2
(@zero (Ring.AbelianMonoid C_Ring)) Λ 0 1))
with
(@coeff_mat C 2 2 (@zero C_AbelianGroup) Λ 0 1).
(@coeff_mat C 2 2 (@zero C_AbelianMonoid) Λ 0 1).
rewrite H3.
rewrite ?@mult_zero_l, ?@mult_zero_r, ?@plus_zero_l, ?@plus_zero_r.
auto.
--
rewrite sum_Sn, sum_O.
specialize (H3 1%nat 0%nat ltac:(lia)).
change (@zero C_AbelianGroup) with (@zero C_Ring) in *.
change (@zero C_AbelianMonoid) with (@zero C_Ring) in *.
change (@coeff_mat _ 2 2 (@zero C_Ring) Λ 1 0)
with (@coeff_mat C 2 2 (@zero C_Ring) Λ 1 0).
simpl.
Expand Down Expand Up @@ -709,7 +709,7 @@ intros.
unfold MTM_eigenvector_matrix, matrix_conj_transpose.
repeat match goal with |- context [(@mk_matrix C 2 2 ?a)] =>
change (@mk_matrix C 2 2 a) with
(@mk_matrix (AbelianGroup.sort C_AbelianGroup) 2 2 a)
(@mk_matrix (AbelianMonoid.sort C_AbelianMonoid) 2 2 a)
end.
unfold Mmult, Mone.
apply mk_matrix_ext => i j Hi Hj.
Expand Down Expand Up @@ -885,7 +885,7 @@ intros.
unfold MTM_eigenvector_matrix, matrix_conj_transpose.
repeat match goal with |- context [(@mk_matrix C 2 2 ?a)] =>
change (@mk_matrix C 2 2 a) with
(@mk_matrix (AbelianGroup.sort C_AbelianGroup) 2 2 a)
(@mk_matrix (AbelianMonoid.sort C_AbelianMonoid) 2 2 a)
end.
unfold Mmult, Mone.
apply mk_matrix_ext => i j Hi Hj.
Expand Down
7 changes: 4 additions & 3 deletions leapfrog_project/matrix_lemmas.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -972,15 +972,16 @@ set ( D' :=
(@mk_matrix C m m
(fun i j : nat =>
if i =? j
then Cpow (@coeff_mat C m m (@zero C_AbelianGroup) D i j) n
then Cpow (@coeff_mat C m m (@zero C_AbelianMonoid) D i j) n
else C0))).
replace (@Mmult C_Ring m m m D' D) with
(@mk_matrix C m m
(fun i j : nat =>
if i =? j
then (Cmult (@coeff_mat C m m (@zero C_AbelianGroup) D' i j)
(@coeff_mat C m m (@zero C_AbelianGroup) D i j))
then (Cmult (@coeff_mat C m m (@zero C_AbelianMonoid) D' i j)
(@coeff_mat C m m (@zero C_AbelianMonoid) D i j))
else C0)).
simpl.
unfold D'.
apply mk_matrix_ext => i j Hi Hj.
rewrite coeff_mat_bij; try lia.
Expand Down
23 changes: 11 additions & 12 deletions leapfrog_project/vcfloat_lemmas.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,15 +48,13 @@ Definition q' := ltac:(let e' :=
make an association list mapping _q to q, and _p to p, each labeled
by its floating-point type. **)
Definition leapfrog_vmap_raw (pq: state) :=
valmap_of_list [(_p, existT ftype _ (fst pq));(_q, existT ftype _ (snd pq))].

[(_p, existT ftype _ (fst pq));(_q, existT ftype _ (snd pq))].

(** Step two, build that into "varmap" data structure, taking care to
compute it into a lookup-tree ___here___, not later in each place
where we look something up. *)
Definition leapfrog_vmap (pq : state) : valmap :=
ltac:(let z := compute_PTree (leapfrog_vmap_raw pq) in exact z).

ltac:(make_valmap_of_list (leapfrog_vmap_raw pq)).

(** Reification and reflection. When you have a
deep-embedded "expr"ession, you can get back the shallow embedding
Expand Down Expand Up @@ -103,9 +101,10 @@ forall pq,
let e := env_ (leapfrog_vmap pq)
in (rval e p', rval e q') = leapfrog_stepR h (FT2R_prod pq).
Proof.
intros. subst e. destruct pq as [p q]. unfold p', q'.
intros. subst e. destruct pq as [p q]. unfold p', q'.
unfold_rval.
unfold leapfrog_stepR,FT2R_prod, fst,snd, h,ω. f_equal; nra.
unfold leapfrog_stepR,FT2R_prod, fst,snd, h,ω; simpl; unfold Defs.F2R; simpl.
f_equal; nra.
Qed.

Definition sametype (v1 v2: sigT ftype) := projT1 v1 = projT1 v2.
Expand All @@ -116,34 +115,34 @@ split; intro; intros; hnf; auto.
red in H,H0. congruence.
Qed.

Lemma leapfrog_vmap_shape:
Remark leapfrog_vmap_shape:
forall pq1 pq0,
Maps.PTree_Properties.Equal Equivalence_sametype
(leapfrog_vmap pq0) (leapfrog_vmap pq1).
(proj1_sig (leapfrog_vmap pq0)) (proj1_sig (leapfrog_vmap pq1)).
Proof.
intros.
intro i.
destruct (Maps.PTree.get i (leapfrog_vmap pq0)) eqn:H.
destruct (Maps.PTree.get i _) eqn:H.
-
apply Maps.PTree.elements_correct in H.
repeat (destruct H; [inversion H; clear H; subst; simpl; reflexivity | ]).
destruct H.
-
rename H into H0.
destruct (Maps.PTree.get i (leapfrog_vmap pq1)) eqn:H.
destruct (Maps.PTree.get i (proj1_sig (leapfrog_vmap pq1))) eqn:H.
apply Maps.PTree.elements_correct in H.
repeat (destruct H; [inversion H; clear H; subst; inversion H0 | ]).
destruct H.
auto.
Qed.

Lemma bmd_init :
Remark bmd_init :
boundsmap_denote leapfrog_bmap (leapfrog_vmap pq_init) .
Proof.
intros.
apply boundsmap_denote_i.
repeat constructor;
(eexists; split; [reflexivity | split; [reflexivity | split; [reflexivity | simpl; interval]]]).
(eexists; split; [reflexivity | split; [reflexivity | split; [reflexivity | simpl; unfold FT2R; simpl; interval]]]).
repeat constructor.
Qed.

Expand Down