From 16a19017695de498d585795681ee52e2fc5d779e Mon Sep 17 00:00:00 2001
From: Andrew Appel <appel@princeton.edu>
Date: Fri, 2 Jun 2023 09:03:33 -0400
Subject: [PATCH 1/3] Adapt to gentype branch of vcfloat

---
 leapfrog_project/global_roundoff_error.v |  4 ++--
 leapfrog_project/local_roundoff_error.v  | 21 ++-------------------
 leapfrog_project/vcfloat_lemmas.v        | 17 +++++++++--------
 3 files changed, 13 insertions(+), 29 deletions(-)

diff --git a/leapfrog_project/global_roundoff_error.v b/leapfrog_project/global_roundoff_error.v
index 7d64dee..ca1b963 100644
--- a/leapfrog_project/global_roundoff_error.v
+++ b/leapfrog_project/global_roundoff_error.v
@@ -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.
diff --git a/leapfrog_project/local_roundoff_error.v b/leapfrog_project/local_roundoff_error.v
index 2ea5b2a..15037a6 100644
--- a/leapfrog_project/local_roundoff_error.v
+++ b/leapfrog_project/local_roundoff_error.v
@@ -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,
@@ -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))∥.
diff --git a/leapfrog_project/vcfloat_lemmas.v b/leapfrog_project/vcfloat_lemmas.v
index 0062a37..9ca77cf 100644
--- a/leapfrog_project/vcfloat_lemmas.v
+++ b/leapfrog_project/vcfloat_lemmas.v
@@ -48,14 +48,14 @@ 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 
@@ -103,9 +103,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.
@@ -119,18 +120,18 @@ Qed.
 Lemma 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 (proj1_sig (leapfrog_vmap pq0))) 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.
@@ -143,7 +144,7 @@ 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.
 

From f092f8e504f495fe2cb11007f6c75beaaef36f28 Mon Sep 17 00:00:00 2001
From: Andrew Appel <appel@princeton.edu>
Date: Fri, 1 Sep 2023 12:56:56 -0400
Subject: [PATCH 2/3] Brought things up to date for vcfloat 2.1.1 and
 Coquelicot 3.4.0 (Coq Platform 2023.03)

---
 leapfrog_project/matrix_analysis.v | 16 ++++++++--------
 leapfrog_project/matrix_lemmas.v   |  7 ++++---
 leapfrog_project/vcfloat_lemmas.v  |  9 ++++-----
 3 files changed, 16 insertions(+), 16 deletions(-)

diff --git a/leapfrog_project/matrix_analysis.v b/leapfrog_project/matrix_analysis.v
index f6c8599..868ec5a 100644
--- a/leapfrog_project/matrix_analysis.v
+++ b/leapfrog_project/matrix_analysis.v
@@ -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.
@@ -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 *.
@@ -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.
@@ -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.
@@ -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.
diff --git a/leapfrog_project/matrix_lemmas.v b/leapfrog_project/matrix_lemmas.v
index 75ba68b..714a41f 100644
--- a/leapfrog_project/matrix_lemmas.v
+++ b/leapfrog_project/matrix_lemmas.v
@@ -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.
diff --git a/leapfrog_project/vcfloat_lemmas.v b/leapfrog_project/vcfloat_lemmas.v
index 9ca77cf..719f81b 100644
--- a/leapfrog_project/vcfloat_lemmas.v
+++ b/leapfrog_project/vcfloat_lemmas.v
@@ -55,8 +55,7 @@ Definition leapfrog_vmap_raw (pq: state) :=
   compute it into a lookup-tree ___here___, not later in each place
   where we look something up. *)
 Definition leapfrog_vmap (pq : state) : valmap :=
-  ltac:(make_valmap_of_list (leapfrog_vmap_raw pq)).
-
+ ltac:(let z := compute_PTree (valmap_of_list (leapfrog_vmap_raw pq)) in exact z).
 
 (**  Reification and reflection.   When you have a 
   deep-embedded "expr"ession, you can get back the shallow embedding
@@ -120,18 +119,18 @@ Qed.
 Lemma leapfrog_vmap_shape:
   forall  pq1 pq0,
   Maps.PTree_Properties.Equal Equivalence_sametype
-        (proj1_sig (leapfrog_vmap pq0)) (proj1_sig (leapfrog_vmap pq1)).
+        (leapfrog_vmap pq0) (leapfrog_vmap pq1).
 Proof.
 intros.
 intro i.
-destruct (Maps.PTree.get i (proj1_sig (leapfrog_vmap pq0))) eqn:H.
+destruct (Maps.PTree.get i (leapfrog_vmap pq0)) 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 (proj1_sig (leapfrog_vmap pq1))) eqn:H.
+destruct (Maps.PTree.get i (leapfrog_vmap pq1)) eqn:H.
 apply Maps.PTree.elements_correct in H.
 repeat (destruct H; [inversion H; clear H; subst; inversion H0 | ]).
 destruct H.

From dfc731637ad210928fc9b94d5be0dbb2362fb654 Mon Sep 17 00:00:00 2001
From: Andrew Appel <appel@princeton.edu>
Date: Fri, 3 Nov 2023 09:27:20 -0400
Subject: [PATCH 3/3] Brought gentype branch of leapfrog up to date w.r.t.
 vcfloat gentype branch

---
 leapfrog_project/vcfloat_lemmas.v | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

diff --git a/leapfrog_project/vcfloat_lemmas.v b/leapfrog_project/vcfloat_lemmas.v
index 719f81b..9d51ffb 100644
--- a/leapfrog_project/vcfloat_lemmas.v
+++ b/leapfrog_project/vcfloat_lemmas.v
@@ -50,12 +50,11 @@ Definition q' := ltac:(let e' :=
 Definition leapfrog_vmap_raw (pq: state) :=
   [(_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 (valmap_of_list (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
@@ -116,28 +115,28 @@ 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.