adapt to MC#1256

theories/algo_closures.v

@@ -47,7 +47,9 @@ Proof.
 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.
+(* FIXME: get rid of this `set b` (lia should compare variables by (keyed) unification instead of term equality). *)
+set b := binomialz (n + m) _.
+have b2_pos: 0 < b by apply: bin_nonneg; lia.
 by field; ring_lia.
 Qed.
 
@@ -64,7 +66,9 @@ rewrite /annotated_recs_d.Sm /annotated_recs_d.precond.Sm /d => n k m ?.
 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.
+(* FIXME: get rid of this `set b` (lia should compare variables by (keyed) unification instead of term equality). *)
+set b := binomialz (n + m) _.
+have b2_pos: 0 < b by apply: bin_nonneg; lia.
 by field; ring_lia.
 Qed.
 

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) // add0r (@big_geqz 1 1) // ?add0r.
 by rewrite Monoid.Theory.mulm1.
 Qed.
 

theories/multinomial.v

@@ -35,7 +35,7 @@
 
 Lemma multi_singl n : 'C[[:: n]] = 1.
 Proof.
 by rewrite /multinomial; do 2! (rewrite !big_mkord /= zmodp.big_ord1 /=); rewrite binn.
 Qed.
 
 Lemma multi_gt0 l : 'C[l] > 0.
@@ -155,7 +155,7 @@
 - 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 @@
     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].

theories/posnum.v

@@ -46,7 +46,7 @@
 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;
@@ -100,7 +100,7 @@
 
 Lemma pos_Sn (n : nat) : 0 < n.+1%:R :> R.
 Proof. by []. Qed.
 Canonical Sn_posnum n := PosNum (pos_Sn n).
 
 Lemma posnumSz (n : nat) : 0 < n.+1%:~R :> R.
 Proof. by rewrite ltr0z. Qed.
@@ -112,13 +112,13 @@
 
 Lemma posnum_factn (n : nat) : 0 < n`!%:~R :> R.
 Proof. rewrite ltr0z; exact: fact_gt0. Qed.
 Canonical posum_factn n := PosNum (posnum_factn n).
 
 
 Lemma one_pos_gt0 : 0 < 1 :> R. Proof. by rewrite ltr01. Qed.
 Canonical oner_posnum := PosNum one_pos_gt0.
 
 End PosNum.
 #[export] Hint Extern 0 ((0 <= _)%R = true) => exact: posnum_ge0 : core.
 #[export] Hint Extern 0 ((_ != 0)%R = true) => exact: posnum_neq0 : core.