Compatibility with mathcomp.2.6

.github/workflows/coq.yml

@@ -13,7 +13,7 @@ jobs:
       fail-fast: false
       matrix:
         include:
-          - env: { COQ_VERSION: "9.0", DOCKER_MATHCOMP_VERSION: "2.4.0" }
+          - env: { COQ_VERSION: "9.1", DOCKER_MATHCOMP_VERSION: "2.6.0" }
 
     runs-on: ubuntu-latest
     env: ${{ matrix.env }}
@@ -30,6 +30,6 @@ jobs:
 
       - uses: coq-community/docker-coq-action@v1
         with:
-          opam_file: 'coq-laproof.opam'
+          opam_file: 'rocq-laproof.opam'
           custom_image: mathcomp/mathcomp:${{ matrix.env.DOCKER_MATHCOMP_VERSION }}-rocq-prover-${{ matrix.env.COQ_VERSION }}
           export: CI

C/densemat_lemmas.v

@@ -139,11 +139,10 @@ lia.
   rewrite ptrofs_add_repr.
   rewrite Ptrofs.unsigned_repr by rep_lia.
   unfold natural_alignment in H2.
-  repeat apply Z.divide_add_r.
-  destruct H2 as [x ?]. rewrite H2. 
-  exists (2*x)%Z. lia.
-  exists 2; lia.
-  apply Z.divide_mul_l. exists 2; lia.
+  unfold Archi.align_float64.
+  repeat apply Z.divide_add_r; auto.
+  apply Z.divide_refl.
+  apply Z.divide_factor_l.
 - split; simpl; auto. lia.
 Qed.
 

C/matrix_model.v

@@ -56,8 +56,8 @@ intros.
   set (H0 := ltnW _). clearbody H0.
   change (fun _ => _) with (@widen_ord k n H0).
   apply (@map_inj _ _ (@nat_of_ord n)). apply ord_inj.
-  rewrite map_take val_ord_enum take_iota /minn H /ord_enum -map_comp pmap_filter.
-  2: move => x; unfold insub; destruct idP; auto.
+  rewrite map_take val_ord_enum take_iota /minn H /ord_enum -map_comp pmap_filter;
+  try solve [move => x; unfold insub; destruct idP; auto].
   clear.
   destruct k; auto.
   set (n := S k) in *.
@@ -343,8 +343,7 @@ assert (Datatypes.is_true (leq (S (S (nat_of_ord k))) n)).
 assert (k1 = @Ordinal n (S k) H). apply ord_inj; auto.
 subst k1.
 unfold subtract_loop_jik at 1.
-rewrite (take_snoc i).
-  2: (rewrite  size_ord_enum; pose proof ltn_ord k;  lia).
+rewrite (take_snoc i); try solve [ rewrite  size_ord_enum; pose proof ltn_ord k;  lia].
 rewrite /subtract_loop !map_cat /= foldl_cat /= nth_ord_enum' //.
 Qed.
 
@@ -374,7 +373,7 @@ split; [ | split3]; intros; try split; hnf; intros; try lia.
    unfold update_mx at 1. rewrite mxE.
    destruct (Nat.eq_dec _ _); [lia  |]. simpl.
    destruct H2.
-   rewrite H1; [ |apply Hij]. f_equal.
+   rewrite H1; try solve [apply Hij]. f_equal.
    * unfold subtract_loop_jik. f_equal.
      apply eq_in_subrange.
      intros. unfold update_mx. rewrite !mxE.

C/verif_build_csr.v

@@ -61,6 +61,40 @@ replace (Zlength (coo_entries (add_to_coo coo i j x))) with (n+1)
 cancel.
 Qed.
 
+(* See:  https://github.com/PrincetonUniversity/VST/issues/869 *)
+
+Ltac freeze_tac_entail L name ::=
+  eapply (freeze_SEP''entail (map Z.to_nat L)); 
+   [solve_is_increasing
+   | match goal with |- _ = (my_freezelist_nth ?A _) => let j := eval compute in A in change A with j end;
+     cbv [my_freezelist_nth my_nth]; unfold map at 1;
+     match goal with |- _ = (_, my_delete_list ?A _) => let j := eval compute in A in change A with j end;
+     cbv [my_delete_list my_delete_nth];
+     reflexivity
+   | match goal with
+           | |- ENTAIL _, (PROPx _ (LOCALx _ (SEPx ((FRZL ?xs) :: my_delete_list ?A _)))) |-- _ =>
+           let D := fresh name in
+           set (D:=xs);
+           change xs with (@abbreviate (list mpred) xs) in D
+         end].
+
+
+Ltac freeze_tac L name ::=
+  eapply (freeze_SEP'' (map Z.to_nat L)); 
+   [solve_is_increasing
+   | match goal with |- _ = (my_freezelist_nth ?A _) => let j := eval compute in A in change A with j end;
+     cbv [my_freezelist_nth my_nth]; unfold map at 1;
+     match goal with |- _ = (_, my_delete_list ?A _) => let j := eval compute in A in change A with j end;
+     cbv [my_delete_list my_delete_nth];
+     reflexivity
+ | match goal with
+           | |- semax _ (PROPx _ (LOCALx _ (SEPx ((FRZL ?xs) ::  _)))) _ _ =>
+           let D := fresh name in
+           set (D:=xs);
+           change xs with (@abbreviate (list mpred) xs) in D
+    end
+].
+
 Lemma body_coo_count: semax_body Vprog Gprog f_coo_count coo_count_spec.
 Proof.
 start_function.

C/verif_densemat.v

@@ -118,10 +118,10 @@ destruct H4.
 rewrite H4.
 repeat apply Z.divide_add_r.
 apply Z.divide_mul_r.
-exists 2; auto.
-exists 2; auto.
+apply Z.divide_refl.
+apply Z.divide_refl.
 apply Z.divide_mul_l.
-exists 2; auto.
+apply Z.divide_refl.
 -
 sep_apply data_at__data_at.
 apply derives_refl'.

_CoqProject

@@ -19,7 +19,6 @@ accuracy_proofs/gemv_acc.v
 accuracy_proofs/vec_op_acc.v
 accuracy_proofs/gemm_acc.v
 accuracy_proofs/export.v
-accuracy_proofs/libvalidsdp.v
 accuracy_proofs/solve_model.v
 
 C/floatlib.v

accuracy_proofs/common.v

@@ -217,10 +217,10 @@ Definition default_abs : R :=
 
 Lemma default_rel_sep_0 : default_rel <> R0.
 Proof.
-  apply Rabs_lt_pos.
+  apply Rabs_lt_pos. unfold default_rel; simpl.
   rewrite Rabs_pos_eq;
-    [ apply Rmult_lt_0_compat; try Lra.nra
-    | apply Rmult_le_pos; try Lra.nra ];
+    first [apply Rmult_lt_0_compat | apply Rmult_le_pos]; (* Do it this way for backward compatibility *)
+    try Lra.nra;
     auto with commonDB.
 Qed.
 Hint Resolve default_rel_sep_0 : commonDB.
@@ -390,15 +390,17 @@ Proof.
   rewrite <- !Rmult_assoc.
   replace (bpow Zaux.radix2 1 * / 2) with 1 by (simpl; nra).
   rewrite !bpow_opp.
-  rewrite !Rcomplements.Rle_div_r.
-  - field_simplify; try nra.
-    replace 1 with (bpow Zaux.radix2 0) by (simpl; auto).
-    apply bpow_le.
-    pose proof fprec_gt_one t; lia.
-  - apply Rlt_gt.
+  rewrite !Rcomplements.Rle_div_r;
+  first [  (* do it this way for backward compatibility *)
+   apply Rlt_gt;
     replace (/ bpow Zaux.radix2 (fprec t))
-      with (1 / bpow Zaux.radix2 (fprec t)) by nra.
-    apply Rdiv_lt_0_compat; try nra.
+      with (1 / bpow Zaux.radix2 (fprec t)) by nra;
+    apply Rdiv_lt_0_compat; nra
+  | field_simplify; try nra;
+    replace 1 with (bpow Zaux.radix2 0) by (simpl; auto);
+    apply bpow_le;
+    pose proof fprec_gt_one t; lia
+ ].
 Qed.
 
 End WithType.

accuracy_proofs/dot_acc.v

@@ -119,16 +119,16 @@ Proof.
     assert (Heq : dotprodR (rev u) (map FT2R v2) = FT2R (dotprodF v1 v2) - eta).
     { eapply R_dot_prod_rel_eq; eauto.
       rewrite -dotprodR_rev;
-        [ | rewrite size_map; rewrite size_rev in Hsize_u; auto].
+      try solve [rewrite size_map; rewrite size_rev in Hsize_u; auto].
       rewrite -map_rev; auto. }
     nra.
   - (* per-element bound *)
     rewrite !size_rev in Helem_bound, Hsize_u, Heta_bound.
     intros n Hn.
     assert (Hlt : (size u - S n < size v2)%nat) by lia.
     specialize (Helem_bound (size u - S n)%nat Hlt).
-    rewrite nth_rev in Helem_bound; [ | rewrite Hlen' //].
-    rewrite nth_rev; [ | lia].
+    rewrite nth_rev in Helem_bound; try solve [rewrite Hlen' //].
+    rewrite nth_rev; try lia.
     destruct Helem_bound as (delta & Hval & Hdelta).
     exists delta; split.
     + rewrite Hval; repeat f_equal.

accuracy_proofs/dot_acc_lemmas.v

@@ -220,7 +220,7 @@ destruct Hl.
     rewrite <- !Rplus_assoc.
     replace (D * g1 n (n - 1) + g1 n (n - 1))
       with (g1 n (n - 1) * (1 + D)) by nra.
-    rewrite one_plus_d_mul_g1; [| lia].
+    rewrite one_plus_d_mul_g1; try lia.
     rewrite Rplus_assoc.
     replace (E + D * E) with ((1 + D) * E) by nra.
     eapply Rle_trans; [apply plus_d_e_g1_le; lia |].
@@ -288,7 +288,7 @@ assert (Hl : l = [] \/ l <> []).
 destruct Hl.
 - (* case: singleton list *)
   subst; simpl.
-  rewrite (R_dot_prod_rel_single rp (FR2 a)); [| auto].
+  rewrite (R_dot_prod_rel_single rp (FR2 a)); auto.
   inversion Hfp. inversion H2; subst.
   pose proof fma_accurate' (fst a) (snd a) (Zconst t 0) Hfin as Hacc.
   destruct Hacc as (e & d & Hz & He & Hd & A).
@@ -353,7 +353,8 @@ destruct Hl.
     with (D * F + ((1 + D) * g n * s1 + D * s1) +
           g1 n (n - 1) * (1 + D) + E)
     by nra.
-  rewrite one_plus_d_mul_g one_plus_d_mul_g1.
+  rewrite one_plus_d_mul_g one_plus_d_mul_g1;
+  try solve [unfold n; destruct l; try congruence; simpl; lia].
   rewrite Rplus_assoc.
   apply Rplus_le_compat; [apply Rplus_le_compat |].
   + rewrite <- Rabs_mult; fold F.
@@ -365,7 +366,6 @@ destruct Hl.
     apply Req_le; f_equal; auto; lia.
   + replace (n.+1 - 1)%nat with n by lia.
     apply plus_e_g1_le.
-  + unfold n; destruct l; try congruence; simpl; lia.
 Qed.
 
 End ForwardErrorRel2.
@@ -516,7 +516,7 @@ subst; clear Hlen1.
     destruct Hun as (delta & Hun & Hdelta).
     simpl.
     replace 0 with (Rmult (1 + d') 0) by nra.
-    rewrite (nth_map R0); [| lia].
+    rewrite (nth_map R0); try lia.
     rewrite Hun.
     exists ((1 + d') * (1 + delta) - 1).
     split; [nra |].
@@ -681,7 +681,7 @@ subst; clear Hlen1.
     specialize (B n H1).
     destruct B as (delta & B & HB); simpl.
     replace 0 with (Rmult (1 + d) 0) by nra.
-    rewrite (nth_map R0); [| lia].
+    rewrite (nth_map R0); try lia.
     rewrite B.
     exists ((1 + d) * (1 + delta) - 1).
     split; [nra |].
@@ -710,8 +710,8 @@ subst; clear Hlen1.
         rewrite Rabs_R1.
         eapply Rle_trans; [apply Rplus_le_compat_l; apply Hd |].
         apply Rle_refl. }
-    rewrite one_plus_d_mul_g1.
-    2: { destruct l; [contradiction | simpl; lia]. }
+    rewrite one_plus_d_mul_g1;
+      try solve [destruct l; [contradiction | simpl; lia]].
     unfold g1; field_simplify.
     rewrite Rplus_assoc.
     apply Rplus_le_compat.

accuracy_proofs/dotprod_model.v

@@ -357,11 +357,10 @@ Proof. reflexivity. Qed.
 
 Lemma sum_rev l : sum_fold l = sum_fold (rev l).
 Proof.
-  rewrite /sum_fold -foldl_rev foldl_foldr.
+  rewrite /sum_fold -foldl_rev foldl_foldr;
+  try solve [hnf; intros; lra].
   f_equal;
     do 2 (apply FunctionalExtensionality.functional_extensionality; intro); lra.
-  hnf; intros; lra.
-  hnf; intros; lra.
 Qed.
 
 (** [R_dot_prod_rel] characterizes [dotprodR]: for any v1 and v2,
@@ -379,9 +378,8 @@ Proof.
   apply R_dot_prod_rel_cons; apply IHl.
   subst z.
   clear.
-  rewrite !foldl_foldr; [ | compute; intros; lra..].
-  destruct a as [x y]; simpl.
-  rewrite Rplus_comm //.
+  rewrite !foldl_foldr;  try solve [compute; intros; lra].
+  destruct a;  rewrite Rplus_comm //.
 Qed.
 
 (** The value of the real dot product relation is injective in s. *)
@@ -448,8 +446,8 @@ Proof.
   move :(dotprodR_rel (rev (map FT2R v1)) (rev (map FT2R v2))).
   rewrite dotprodR_rev ?size_rev ?size_map // revK
           /sum_fold /dotprodR /dotprod
-          foldl_foldr //.
-  2,3: compute; intros; lra.
+          foldl_foldr //;
+  try solve [compute; intros; lra];
   rewrite -rev_zip ?size_map ?flip_Rplus //.
 Qed.
 
@@ -489,8 +487,8 @@ Proof.
                       (rev (map Rabs (map FT2R v2)))).
   rewrite dotprodR_rev ?size_rev ?size_map // revK
           /sum_fold /dotprodR /dotprod
-          foldl_foldr //.
-  2,3: compute; intros; lra.
+          foldl_foldr //;
+  try solve [compute; intros; lra].
   rewrite -rev_zip ?size_map ?flip_Rplus //.
 Qed.
 
@@ -603,8 +601,7 @@ Proof.
   replace (Rmult a (dotprodR u v)) with (dotprodR (map (Rmult a) u) v); auto.
   clear - H.
   unfold dotprodR, dotprod.
-  rewrite !foldl_foldr.
-  2,3,4,5: compute; intros; lra.
+  rewrite !foldl_foldr; try solve [compute; intros; lra].
   revert v H; induction u; destruct v; intros; inversion H; clear H; subst;
     simpl.
   compute; lra.
@@ -822,7 +819,7 @@ Proof.
     move :H => /eqP H.
     simpl in Hlen.
     rewrite -H Rmult_0_l.
-    rewrite (IHl _ _ H0 H3). lra. lia.
+    rewrite (IHl _ _ H0 H3); try lia; lra.
 Qed.
 
 (** Absolute-value dot product analogue of [R_dot_prod_rel_nnzR]:
@@ -845,8 +842,7 @@ Proof.
     move :H => /= /andP [H H0].
     move :H => /eqP H.
     simpl in Hlen.
-    rewrite -H Rabs_R0 Rmult_0_l (IHl _ _ H0 H3).
-    lra. lia.
+    rewrite -H Rabs_R0 Rmult_0_l (IHl _ _ H0 H3); try lia; lra.
 Qed.
 
 End NonZeroDP.

accuracy_proofs/float_acc_lems.v

@@ -308,9 +308,10 @@ Proof.
                 BinarySingleNaN.mode_NE
                 x y z Hfinx Hfiny Hfinz) as H.
   cbv zeta in H.
-  rewrite Rlt_bool_true in H.
-  - destruct H as [_ [HFIN _]]; exact HFIN.
-  - move: Hov; by rewrite /fma_no_overflow /rounded.
+  rewrite Rlt_bool_true in H;
+  first [ (* do it this way for backward compatibility *)
+    destruct H as [_ [HFIN _]]; exact HFIN
+  |  move: Hov; by rewrite /fma_no_overflow /rounded].
 Qed.
 
 

accuracy_proofs/fma_dot_acc.v

@@ -79,7 +79,7 @@ Proof.
   assert (Hlenr : size (rev v1) = size (rev v2)) by (rewrite !size_rev; auto).
   rewrite <- size_rev in Hlen.
   pose proof fma_dot_prod_rel_fold_right v1 v2 as Hrel.
-  rewrite rev_zip in Hrel. 2: revert Hlen; rewrite size_rev; auto.
+  rewrite rev_zip in Hrel; try solve [revert Hlen; rewrite size_rev; auto].
   revert Hlen; rewrite size_rev; intro Hlen.
   pose proof (fma_dotprod_mixed_error_rel
                 (rev v1) (rev v2) Hlenr
@@ -103,8 +103,8 @@ Proof.
     rewrite size_rev in Hsize.
     assert (Hlt : (size u - S n < size v2)%nat) by lia.
     specialize (Hbnd (size u - S n)%nat Hlt).
-    rewrite nth_rev in Hbnd. 2: rewrite Hlen //.
-    rewrite nth_rev.          2: rewrite Hsize Hlen //.
+    rewrite nth_rev in Hbnd; try solve [rewrite Hlen //].
+    rewrite nth_rev; try solve  [rewrite Hsize Hlen //].
     destruct Hbnd as (delta & Hnth & Hdelta).
     exists delta; split.
     + rewrite Hnth; repeat f_equal.

accuracy_proofs/fma_is_finite.v

@@ -309,8 +309,8 @@ Proof.
         } 
         apply He.
     (* Final algebraic inequality using fun_bnd structure *)
-    rewrite sqrt_def.
-    { unfold fun_bnd.
+    rewrite sqrt_def; try solve [apply fun_bound_pos; auto].
+      unfold fun_bnd.
       replace (length (a :: l)) with (S n) by (simpl; lia).
       set (x := (@g t (S n - 1) + 1)).
       set (y := (1 + INR (S n) * x)).
@@ -375,7 +375,6 @@ Proof.
               | apply le_INR; lia
               | replace (S n - 1)%nat with n%nat by lia; nra ].
           + unfold n; apply lt_INR; lia. } }
-    apply fun_bound_pos; auto. }
 Qed.
 
 End NAN.