IBM · shinnar · Feb 29, 2024 · Feb 29, 2024
diff --git a/.github/workflows/build.yml b/.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

diff --git a/_CoqProject b/_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"
diff --git a/coq/CertRL/LM/lax_milgram.v b/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.

diff --git a/coq/CertRL/qvalues.v b/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.

diff --git a/coq/FHE/encode.v b/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.

diff --git a/coq/NeuralNetworks/DefinedFunctions.v b/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.
 
 

diff --git a/coq/ProbTheory/ConditionalExpectation.v b/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.
 

diff --git a/coq/ProbTheory/Expectation.v b/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).

diff --git a/coq/ProbTheory/Martingale.v b/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.

diff --git a/coq/ProbTheory/MartingaleConvergence.v b/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.

diff --git a/coq/ProbTheory/MartingaleStopped.v b/coq/ProbTheory/MartingaleStopped.v
@@ -166,7 +166,8 @@ Section stopped_process.
       forall n, RandomVariable dom borel_sa (process_stopped_at Y T n).
     Proof.
       intros.
-      eapply RandomVariable_proper; try apply process_stopped_at_as_alt; try reflexivity.
+      cut (RandomVariable dom borel_sa (process_stopped_at_alt Y T n))
+      ; [apply RandomVariable_proper; try reflexivity; apply process_stopped_at_as_alt; try reflexivity |].
       destruct n; simpl; trivial.
       apply rvplus_rv.
       - apply rvsum_rv; intros.
@@ -186,14 +187,17 @@ Section stopped_process.
       IsAdapted borel_sa (process_stopped_at Y T) F.
     Proof.
       intros n.
-      eapply (RandomVariable_proper _ (F n)); try apply process_stopped_at_as_alt; try reflexivity.
+      cut (RandomVariable (F n) borel_sa (process_stopped_at_alt Y T n))
+      ; [apply RandomVariable_proper; try reflexivity; apply process_stopped_at_as_alt; try reflexivity |].
       destruct n; simpl; trivial.
       apply rvplus_rv.
       - apply rvsum_rv_loc; intros.
         apply rvmult_rv; trivial.
-        + eapply (RandomVariable_proper_le (F m) _); try reflexivity.
-          * apply is_filtration_le; trivial; lia.
-          * apply adapt.
+        + cut (RandomVariable (F m) borel_sa (Y m)).
+          { eapply (RandomVariable_proper_le (F m) _); try reflexivity.
+            apply is_filtration_le; trivial; lia.
+          } 
+          apply adapt.
         + apply EventIndicator_pre_rv.
           generalize (is_stop m).
           apply is_filtration_le; trivial; lia.

diff --git a/coq/ProbTheory/RandomVariableFinite.v b/coq/ProbTheory/RandomVariableFinite.v
@@ -1310,7 +1310,7 @@ Lemma Fatou_FiniteExpectation
 
 End fe.
 
-Hint Rewrite FiniteExpectation_const FiniteExpectation_plus FiniteExpectation_scale FiniteExpectation_opp FiniteExpectation_minus: prob.
+Hint Rewrite @FiniteExpectation_const @FiniteExpectation_plus @FiniteExpectation_scale @FiniteExpectation_opp @FiniteExpectation_minus: prob.
 
 Section ExpNonNeg.
   Context {Ts:Type} 

diff --git a/coq/ProbTheory/RandomVariableL2.v b/coq/ProbTheory/RandomVariableL2.v
@@ -768,7 +768,7 @@ Section L2.
   Proof.
     unfold Hnorm; simpl.
     LpRRVq_simpl.
-    rewrite LpRRVq_normE.
+    try rewrite LpRRVq_normE.
     unfold LpRRVnorm.
     unfold L2RRVinner.
     rewrite power_sqrt.
@@ -789,7 +789,7 @@ Section L2.
     rewrite LpRRVq_ballE.
     unfold minus, plus, opp; simpl.
     autorewrite with quot.
-    rewrite LpRRVq_normE.
+    try rewrite LpRRVq_normE.
     unfold LpRRVball.
     now rewrite LpRRVminus_plus.
   Qed.
@@ -815,7 +815,7 @@ Section L2.
     rewrite LpRRVq_ballE.
     unfold minus, plus, opp; simpl.
     autorewrite with quot.
-    rewrite LpRRVq_normE.
+    try rewrite LpRRVq_normE.
     unfold LpRRVball.
     erewrite LpRRV_norm_proper; [reflexivity |].
     rewrite LpRRVminus_plus.
@@ -859,7 +859,8 @@ Section L2.
       destruct (Quot_inv x); subst; simpl in *.
       unfold minus, plus, opp; simpl.
       autorewrite with quot.
-      rewrite LpRRVq_ballE, LpRRVq_normE.
+      rewrite LpRRVq_ballE.
+      try rewrite LpRRVq_normE.
       unfold LpRRVball.
       erewrite LpRRV_norm_proper; [reflexivity |].
       rewrite LpRRVminus_plus.

diff --git a/coq/ProbTheory/RandomVariableLinf.v b/coq/ProbTheory/RandomVariableLinf.v
@@ -2348,7 +2348,7 @@ End Linf.
       apply LiRRV_norm_sproper.
       intros ?; simpl.
       rv_unfold; lra.
-    - revert HH.
+    - try revert HH.
       apply pow_nzero.
       lra.
   Qed.

diff --git a/coq/ProbTheory/RandomVariableLpNat.v b/coq/ProbTheory/RandomVariableLpNat.v
@@ -1630,20 +1630,20 @@ Section Lp.
 
 End Lp.
 
-Hint Rewrite LpRRVq_constE : quot.
-Hint Rewrite LpRRVq_zeroE : quot.
-Hint Rewrite LpRRVq_scaleE : quot.
-Hint Rewrite LpRRVq_oppE : quot.
-Hint Rewrite LpRRVq_plusE : quot.
-Hint Rewrite LpRRVq_minusE : quot.
 Hint Rewrite @LpRRVq_constE : quot.
 Hint Rewrite @LpRRVq_zeroE : quot.
 Hint Rewrite @LpRRVq_scaleE : quot.
 Hint Rewrite @LpRRVq_oppE : quot.
 Hint Rewrite @LpRRVq_plusE : quot.
 Hint Rewrite @LpRRVq_minusE : quot.
 Hint Rewrite @LpRRVq_constE : quot.
-Hint Rewrite LpRRVq_normE : quot.
+Hint Rewrite @LpRRVq_zeroE : quot.
+Hint Rewrite @LpRRVq_scaleE : quot.
+Hint Rewrite @LpRRVq_oppE : quot.
+Hint Rewrite @LpRRVq_plusE : quot.
+Hint Rewrite @LpRRVq_minusE : quot.
+Hint Rewrite @LpRRVq_constE : quot.
+Hint Rewrite @LpRRVq_normE : quot.
 
 Global Arguments LpRRVq_AbelianGroup {Ts} {dom} prts p.
 Global Arguments LpRRVq_ModuleSpace {Ts} {dom} prts p.

diff --git a/coq/ProbTheory/RandomVariableLpR.v b/coq/ProbTheory/RandomVariableLpR.v
@@ -2143,20 +2143,20 @@ Qed.
 
 End Lp.
 
-Hint Rewrite LpRRVq_constE : quot.
-Hint Rewrite LpRRVq_zeroE : quot.
-Hint Rewrite LpRRVq_scaleE : quot.
-Hint Rewrite LpRRVq_oppE : quot.
-Hint Rewrite LpRRVq_plusE : quot.
-Hint Rewrite LpRRVq_minusE : quot.
 Hint Rewrite @LpRRVq_constE : quot.
 Hint Rewrite @LpRRVq_zeroE : quot.
 Hint Rewrite @LpRRVq_scaleE : quot.
 Hint Rewrite @LpRRVq_oppE : quot.
 Hint Rewrite @LpRRVq_plusE : quot.
 Hint Rewrite @LpRRVq_minusE : quot.
 Hint Rewrite @LpRRVq_constE : quot.
-Hint Rewrite LpRRVq_normE : quot.
+Hint Rewrite @LpRRVq_zeroE : quot.
+Hint Rewrite @LpRRVq_scaleE : quot.
+Hint Rewrite @LpRRVq_oppE : quot.
+Hint Rewrite @LpRRVq_plusE : quot.
+Hint Rewrite @LpRRVq_minusE : quot.
+Hint Rewrite @LpRRVq_constE : quot.
+Hint Rewrite @LpRRVq_normE : quot.
 
 Global Arguments LpRRVq_AbelianGroup {Ts} {dom} prts p.
 Global Arguments LpRRVq_ModuleSpace {Ts} {dom} prts p.
@@ -2441,7 +2441,7 @@ Section complete.
       apply LpRRV_norm_sproper.
       intros ?; simpl.
       rv_unfold; lra.
-    - revert HH.
+    - try revert HH.
       apply pow_nzero.
       lra.
   Qed.

diff --git a/coq/ProbTheory/RbarExpectation.v b/coq/ProbTheory/RbarExpectation.v
@@ -1845,8 +1845,8 @@ 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.
@@ -4709,7 +4709,7 @@ Section rv_expressible.
           (X : nat -> Ts -> R) (n : nat) 
           (Y : Ts -> R)
           {rv_X : forall n, RandomVariable dom borel_sa (X n)}
-          {rv_y : RandomVariable (filtration_history_sa X n) borel_sa Y} :
+          {rv_y : RandomVariable (filtration_history_sa (cod:=borel_sa) X n) borel_sa Y} :
       exists g : vector R (S n) -> R,
          RandomVariable (Rvector_borel_sa (S n)) borel_sa g /\
          rv_eq Y (g ∘ (make_vector_from_seq X (S n))).
@@ -4736,7 +4736,7 @@ Section rv_expressible.
           (X : nat -> Ts -> R) (n : nat) 
           (g : vector R (S n) -> R)
           {rv_g : RandomVariable (Rvector_borel_sa (S n)) borel_sa g} :
-      RandomVariable (filtration_history_sa X n) borel_sa (g ∘ (make_vector_from_seq X (S n) )).
+      RandomVariable (filtration_history_sa (cod:=borel_sa) X n) borel_sa (g ∘ (make_vector_from_seq X (S n) )).
     Proof.
       rewrite filtrate_history_vector_equiv.
       now apply pullback_compose_rv.

diff --git a/coq/QLearn/Tsitsiklis.v b/coq/QLearn/Tsitsiklis.v
@@ -7436,7 +7436,7 @@ End FixedPoint_contract.
     }
     apply rv_vecrvnth; intros.
     unfold vecrvnth.
-    eapply RandomVariable_proper; [reflexivity | reflexivity | ..].
+    eapply (RandomVariable_proper _ _ (reflexivity _) _ _ (reflexivity _)).
     - intros ?.
       unfold our_iso_f; simpl.
       unfold finite_fun_to_vector.
@@ -7717,7 +7717,7 @@ End FixedPoint_contract.
          intros.
          typeclasses eauto.
        } 
-       eapply RandomVariable_proper; [reflexivity | reflexivity | ..].
+       eapply (RandomVariable_proper _ _ (reflexivity _) _ _ (reflexivity _)).
        {
          intros ?.
          rewrite (FiniteExpectation_simple _ _).
Original file line number	Diff line number	Diff line change
		@@ -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"