From 0119875320367577da9eda433645ac14c5673d4c Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Wed, 21 Aug 2024 17:07:45 +0200 Subject: [PATCH] adapt to MC#1256 --- theories/algo_closures.v | 2 ++ theories/bigopz.v | 6 +++--- theories/multinomial.v | 4 ++-- theories/posnum.v | 2 +- 4 files changed, 8 insertions(+), 6 deletions(-) diff --git a/theories/algo_closures.v b/theories/algo_closures.v index 6db76a2..312c2f6 100644 --- 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 index 46388ac..9f2e3e0 100644 --- 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 index d8bab11..a5c17f8 100644 --- 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 index 2a2adc2..e2958d7 100644 --- 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;