Add support for coq 8.18

Signed-off-by: Avi Shinnar <[email protected]>

Author: shinnar

.github/workflows/build.yml

@@ -13,6 +13,7 @@ jobs:
         coq_container:
 #        - coqorg/coq:8.12.2
         - coqorg/coq:8.16.1-ocaml-4.13.1-flambda
+        - coqorg/coq:8.18.0-ocaml-4.13.1-flambda
     container:
       image: ${{ matrix.coq_container }}
       options: --user root

_CoqProject

@@ -1 +1 @@
--R coq FormalML -arg -set -arg "Warnings=+default,-ambiguous-path,-typechecker,-ssr-search-moved,-deprecated,-notation-overridden"
+-R coq FormalML -arg -set -arg "Warnings=+default,-ambiguous-path,-coercions,-hiding-delimiting-key,-overwriting-delimiting-key,-redundant-canonical-projection,-typechecker,-ssr-search-moved,-deprecated,-notation-overridden"

coq/CertRL/LM/lax_milgram.v

@@ -1005,12 +1005,11 @@ intro x; field.
 repeat (rewrite Hx1 in HU0).
 rewrite Rmult_comm.
 trivial.
-absurd (norm u0 = 0).
+try revert HU0.
 apply Rgt_not_eq.
 apply Rlt_gt.
 apply norm_gt_0.
 trivial.
-trivial.
 apply norm_ge_0.
 simpl.
 apply is_finite_correct in Hfin.

coq/CertRL/qvalues.v

@@ -444,10 +444,11 @@ Qed.
   Proof.
     destruct (is_nil_dec l); try now subst.
     apply Rle_antisym.
-    + rewrite Rmax_list_le_iff; try rewrite map_not_nil; try easy.
-      intros x Hx. rewrite in_map_iff in Hx.
-      destruct Hx as [x0 [Hx0 Hx0']].
-      now subst. congruence.
+    + rewrite Rmax_list_le_iff; try rewrite map_not_nil.
+      * intros x Hx. rewrite in_map_iff in Hx.
+        destruct Hx as [x0 [Hx0 Hx0']].
+        now subst.
+      * congruence.
     + apply Rmax_spec.
       rewrite in_map_iff.
       rewrite BasicUtils.ne_symm in n.

coq/FHE/encode.v

@@ -1283,7 +1283,7 @@ Canonical ev_C_rmorphism (x:R[i]) := RMorphism (ev_C_is_rmorphism x).
   Proof.
     move=> p.
     rewrite /peval_C_quot -eq_lock.
-    case piP => a /EquivQuot.eqmodP.
+    case: piP => a /EquivQuot.eqmodP.
     rewrite /Quotient.equiv_equiv /Quotient.equiv /in_mem /mem /= /peval_C_ker_pred.
     destruct (ev_C_is_rmorphism x).
     rewrite base => eqq.
@@ -1713,7 +1713,7 @@ Section eval_vectors.
   Proof.
     move=> x.
     rewrite /mx_eval_quot -eq_lock.
-    case piP => a /EquivQuot.eqmodP.
+    case: piP => a /EquivQuot.eqmodP.
     rewrite /Quotient.equiv_equiv /Quotient.equiv /in_mem /mem /= /mx_eval_ker_pred.
     destruct mx_eval_is_rmorphism.
     rewrite base => eqq.

coq/NeuralNetworks/DefinedFunctions.v

@@ -11783,8 +11783,8 @@ Tactic Notation "DefinedFunction_scalar_cases" tactic(first) ident(c) :=
       intros fa.
       do 2 (apply functional_extensionality; intro).
       unfold scaleUnitVector; simpl.
-      match_destr.
-      now specialize (fa x1); simpl in fa.
+      match_destr
+      ; try now specialize (fa x1); simpl in fa.
     Qed.
 
 

coq/ProbTheory/ConditionalExpectation.v

@@ -4293,7 +4293,7 @@ Section cond_exp_l2.
     unfold norm, minus, plus, opp in *; simpl in *.
     rewrite L2RRVq_norm_norm in HH2.
     autorewrite with quot in HH2.
-    rewrite LpRRVq_normE in HH2.
+    try rewrite LpRRVq_normE in HH2.
     rewrite LpRRVminus_plus.
     unfold nonneg in HH2 |- *; simpl in *.
     rewrite HH2.
@@ -4315,7 +4315,7 @@ Section cond_exp_l2.
         exists w'.
         split; trivial.
         autorewrite with quot.
-        rewrite LpRRVq_normE.
+        try rewrite LpRRVq_normE.
         now rewrite LpRRVminus_plus.
       + subst.
         exists (Quot _ w).
@@ -4324,7 +4324,7 @@ Section cond_exp_l2.
           split; trivial.
         * rewrite L2RRVq_norm_norm.
           autorewrite with quot.
-          rewrite LpRRVq_normE.
+          try rewrite LpRRVq_normE.
           now rewrite LpRRVminus_plus.
     } 
     repeat split.
@@ -4360,7 +4360,7 @@ Section cond_exp_l2.
           eauto.
         * rewrite L2RRVq_norm_norm.
           autorewrite with quot.
-          rewrite LpRRVq_normE.
+          try rewrite LpRRVq_normE.
           rewrite <- LpRRVminus_plus.
           unfold nonneg in *; simpl in *.
           rewrite xeqq.
@@ -4490,7 +4490,7 @@ Section cond_exp_l2.
         rewrite L2RRVq_norm_norm.
         unfold minus, plus, opp; simpl.
         LpRRVq_simpl.
-        rewrite LpRRVq_normE.
+        try rewrite LpRRVq_normE.
         now rewrite LpRRVminus_plus.
     - intros [?[??]]; subst.
       destruct H0 as [?[??]]; subst.
@@ -4500,7 +4500,7 @@ Section cond_exp_l2.
       rewrite L2RRVq_norm_norm.
       unfold minus, plus, opp; simpl.
       LpRRVq_simpl.
-      rewrite LpRRVq_normE.
+      try rewrite LpRRVq_normE.
       now rewrite LpRRVminus_plus.
   Qed.
 

coq/ProbTheory/Expectation.v

@@ -1173,7 +1173,7 @@ Section Expectation_sec.
       + split; intros.
         * field_simplify in H.
           -- now apply INR_eq.
-          -- revert H.
+          -- try revert H.
              now apply pow_nzero.
         * subst.
           field_simplify; trivial.
@@ -4730,8 +4730,7 @@ Section EventRestricted.
       + typeclasses eauto.
       + intro z.
         unfold lift_event_restricted_domain_fun.
-        match_destr.
-        apply H5.
+        match_destr; try apply H5.
       + subst.
         erewrite event_restricted_SimpleExpectation; eauto.
         apply SimpleExpectation_ext.
@@ -4927,7 +4926,7 @@ Section indep.
         ; lra.
       } 
 
-      generalize (simple_approx_rv
+      generalize (simple_approx_rv (dom:= borel_sa)
                     (rvchoice (fun x => if Req_EM_T (c x) 0 then false else true)
                                        (fun x => x)
                                        (fun _ => 0)) n).

coq/ProbTheory/Martingale.v

@@ -1385,7 +1385,7 @@ Section martingale.
   Global Instance martingale_transform_adapted (H X : nat -> Ts -> R) sas
          {adapt:IsAdapted borel_sa X sas}
          {filt:IsFiltration sas} :
-    is_predictable H sas ->
+    is_predictable (saD:=borel_sa) H sas ->
     IsAdapted borel_sa (martingale_transform H X) sas.
   Proof.
     intros is_pre [|n]; simpl.
@@ -1419,7 +1419,7 @@ Section martingale.
         {isfeS:forall n, IsFiniteExpectation prts (rvmult (H (S n)) (rvminus (X (S n)) (X n)))}
         {isfe : forall n : nat, IsFiniteExpectation prts (martingale_transform H X n)}
         {adapt:IsAdapted borel_sa (martingale_transform H X) sas}
-        (predict: is_predictable H sas)
+        (predict: is_predictable (saD:=borel_sa) H sas)
         {mart:IsMartingale eq X sas} :
     IsMartingale eq (martingale_transform H X) sas.
   Proof.
@@ -1560,7 +1560,7 @@ Section martingale.
         {isfeS:forall n, IsFiniteExpectation prts (rvmult (H (S n)) (rvminus (X (S n)) (X n)))}
         {isfe : forall n : nat, IsFiniteExpectation prts (martingale_transform H X n)}
         {adapt:IsAdapted borel_sa (martingale_transform H X) sas}
-        (predict: is_predictable H sas)
+        (predict: is_predictable (saD:=borel_sa) H sas)
         (Hpos: forall n, almostR2 prts Rle (const 0) (H n))
         {mart:IsMartingale Rle X sas} :
     IsMartingale Rle (martingale_transform H X) sas.

coq/ProbTheory/MartingaleConvergence.v

@@ -167,7 +167,7 @@ Section mct.
                                    end)))).
 
     Lemma upcrossing_bound_is_predictable a b :
-      is_predictable (upcrossing_bound a b) sas.
+      is_predictable (saD:=borel_sa) (upcrossing_bound a b) sas.
     Proof.
       intros m.
       unfold upcrossing_bound.
@@ -2390,7 +2390,7 @@ Section mct.
       apply Rbar_plus_le_compat
       ; [| now rewrite IsFiniteNonnegExpectation; try reflexivity].
 
-      assert (ispredminus1:is_predictable (fun k : nat => rvminus (const 1) (upcrossing_bound Y a b k)) sas).
+      assert (ispredminus1:is_predictable (saD:=borel_sa) (fun k : nat => rvminus (const 1) (upcrossing_bound Y a b k)) sas).
       {
         red.
         apply is_adapted_minus.