adapt to MC#1256

coq-community · Aug 21, 2024 · 0119875 · 0119875
1 parent 910f96b
commit 0119875
Show file tree

Hide file tree

Showing 4 changed files with 8 additions and 6 deletions.
diff --git a/theories/algo_closures.v b/theories/algo_closures.v
@@ -48,6 +48,7 @@ rewrite /annotated_recs_d.Sn /annotated_recs_d.precond.Sn /d => n k m ?.
 rewrite addrAC !binSz /annotated_recs_d.Sn_cf0_0_0; [ | lia ..].
 have b1_pos: 0 < binomialz n m by apply: bin_nonneg; lia.
 have b2_pos: 0 < binomialz (n + m) m by apply: bin_nonneg; lia.
+have ->: @GRing.add (int : nmodType) n m = n + m by [].
 by field; ring_lia.
 Qed.
 
@@ -65,6 +66,7 @@ rewrite int.zshiftP !alt_sign addrA !(binzS, binSz); [ | lia ..].
 rewrite /annotated_recs_d.Sm_cf0_0_0.
 have b1_pos: 0 < binomialz n m by apply: bin_nonneg; lia.
 have b2_pos: 0 < binomialz (n + m) m by apply: bin_nonneg; lia.
+have ->: @GRing.add (int : nmodType) n m = n + m by [].
 by field; ring_lia.
 Qed.
 

diff --git a/theories/bigopz.v b/theories/bigopz.v
@@ -240,7 +240,7 @@ Proof.
 suff -> : index_iotaz (m + a) n = map (fun i => i + a) (index_iotaz m (n - a)).
   by rewrite big_map.
 apply: (@eq_from_nth _ 0).
-  by rewrite size_map !size_index_iotaz lerBDl addrC -addrA opprD.
+  by rewrite size_map !size_index_iotaz lerBDl [m + a]addrC -addrA opprD.
 move=> i; rewrite size_index_iotaz; case: ifP => // hman hi.
 rewrite nth_index_iotaz // (nth_map 0); last first.
   rewrite size_index_iotaz lerBDr hman.
@@ -290,7 +290,7 @@ apply: (@eq_from_nth _ 0); rewrite size_cat !size_index_iotaz hmn hnp.
   have hmn' : `|n - m |  = n - m by apply: ger0_norm; rewrite subr_gte0.
   rewrite nth_index_iotaz //; last first.
     rewrite -subzn; last by  rewrite leqNgt hi2.
-    by rewrite lterBDr addrC h ltz_nat.
+    by rewrite lterBDr [ltRHS]addrC h ltz_nat.
   rewrite nth_index_iotaz //; last exact: le_trans hnp.
   rewrite -subzn; last by  rewrite leqNgt hi2.
   move: hmn'; rewrite abszE; move->. rewrite addrCA opprB.
@@ -311,7 +311,7 @@ Lemma big_int_recr m n F : m <= n ->
      op  (\big[op/idx]_(m <= i < n :> int) F (i)) (F n).
 Proof.
 move=> hmn; rewrite (@big_cat_int n) ?ler_wpDr //=.
-rewrite big_addz2l (@big_ltz 0 1) // add0r (@big_geqz 1 1) // add0r.
+rewrite big_addz2l (@big_ltz 0 1) //= [0 + n]add0r (@big_geqz 1 1) //.
 by rewrite Monoid.Theory.mulm1.
 Qed.
 

diff --git a/theories/multinomial.v b/theories/multinomial.v
@@ -155,7 +155,7 @@ rewrite {}/s; elim/last_ind: l n m => [|l a ihl] n m /=.
 - move=> leqnm; rewrite size_rcons big_rcons /= exprDn.
   set s := size l.
   pose tlast s (t : s.-tuple 'I_m.+1) := last ord0 t.
-  have -> P F :
+  have -> P (F : _ -> R) :
    \sum_(t : s.+1.-tuple 'I_m.+1 | P t) F t =
    \sum_(j < m.+1) \sum_(t | P t && (tlast _ t == j)) F t.
      exact: partition_big.
@@ -171,7 +171,7 @@ rewrite {}/s; elim/last_ind: l n m => [|l a ihl] n m /=.
     by apply: (leq_trans (leq_subr _ _)); apply: (leq_trans leqnm).
   rewrite mulr_suml -sumrMnl.
   pose tsum a (t : a.-tuple 'I_m.+1) b := ((\sum_(j <- t) j) == b)%N.
-  have -> F :
+  have -> (F : _ -> R) :
   \sum_(t : s.+1.-tuple 'I_m.+1 | tsum _ t n && (tlast _ t == i)) F t =
   \sum_(t : s.-tuple 'I_m.+1    | tsum _ t (n - i)%N) F [tuple of (rcons t i)].
     pose indx (t : s.-tuple 'I_m.+1) := [tuple of rcons t i].

diff --git a/theories/posnum.v b/theories/posnum.v
@@ -46,7 +46,7 @@ Class infer (P : Prop) := Infer : P.
 Lemma inferP (P : Prop) : P -> infer P. Proof. by []. Qed.
 
 Lemma splitr (R : numFieldType) (x : R) : x = x / 2%:R + x / 2%:R.
-Proof. by rewrite -mulr2n -mulr_natr mulfVK //= pnatr_eq0. Qed.
+Proof. by rewrite -mulr2n -[RHS]mulr_natr mulfVK //= pnatr_eq0. Qed.
 
 Record posnum_def (R : numDomainType) := PosNumDef {
   num_of_pos :> R;