diff options
Diffstat (limited to 'mathcomp/ssreflect')
| -rw-r--r-- | mathcomp/ssreflect/bigop.v | 17 | ||||
| -rw-r--r-- | mathcomp/ssreflect/binomial.v | 12 | ||||
| -rw-r--r-- | mathcomp/ssreflect/choice.v | 9 | ||||
| -rw-r--r-- | mathcomp/ssreflect/div.v | 124 | ||||
| -rw-r--r-- | mathcomp/ssreflect/path.v | 21 | ||||
| -rw-r--r-- | mathcomp/ssreflect/prime.v | 36 | ||||
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 64 |
8 files changed, 163 insertions, 122 deletions
diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index adb4094..f596c3f 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -1392,10 +1392,10 @@ Lemma partition_big (I J : finType) (P : pred I) p (Q : pred J) F : Proof. move=> Qp; transitivity (\big[*%M/1]_(i | P i && Q (p i)) F i). by apply: eq_bigl => i; case Pi: (P i); rewrite // Qp. -elim: {Q Qp}_.+1 {-2}Q (ltnSn #|Q|) => // n IHn Q. -case: (pickP Q) => [j Qj | Q0 _]; last first. +have [n leQn] := ubnP #|Q|; elim: n => // n IHn in Q {Qp} leQn *. +case: (pickP Q) => [j Qj | Q0]; last first. by rewrite !big_pred0 // => i; rewrite Q0 andbF. -rewrite ltnS (cardD1x j Qj) (bigD1 j) //; move/IHn=> {n IHn} <-. +rewrite (bigD1 j) // -IHn; last by rewrite ltnS (cardD1x j Qj) in leQn. rewrite (bigID (fun i => p i == j)); congr (_ * _); apply: eq_bigl => i. by case: eqP => [-> | _]; rewrite !(Qj, simpm). by rewrite andbA. @@ -1408,14 +1408,13 @@ Lemma reindex_onto (I J : finType) (h : J -> I) h' (P : pred I) F : \big[*%M/1]_(i | P i) F i = \big[*%M/1]_(j | P (h j) && (h' (h j) == j)) F (h j). Proof. -move=> h'K; elim: {P}_.+1 {-3}P h'K (ltnSn #|P|) => //= n IHn P h'K. -case: (pickP P) => [i Pi | P0 _]; last first. +move=> h'K; have [n lePn] := ubnP #|P|; elim: n => // n IHn in P h'K lePn *. +case: (pickP P) => [i Pi | P0]; last first. by rewrite !big_pred0 // => j; rewrite P0. -rewrite ltnS (cardD1x i Pi); move/IHn {n IHn} => IH. rewrite (bigD1 i Pi) (bigD1 (h' i)) h'K ?Pi ?eq_refl //=; congr (_ * _). -rewrite {}IH => [|j]; [apply: eq_bigl => j | by case/andP; auto]. -rewrite andbC -andbA (andbCA (P _)); case: eqP => //= hK; congr (_ && ~~ _). -by apply/eqP/eqP=> [<-|->] //; rewrite h'K. +rewrite {}IHn => [|j /andP[]|]; [|by auto | by rewrite (cardD1x i) in lePn]. +apply: eq_bigl => j; rewrite andbC -andbA (andbCA (P _)); case: eqP => //= hK. +by congr (_ && ~~ _); apply/eqP/eqP=> [<-|->] //; rewrite h'K. Qed. Arguments reindex_onto [I J] h h' [P F]. diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v index 0c5be52..8bdb426 100644 --- a/mathcomp/ssreflect/binomial.v +++ b/mathcomp/ssreflect/binomial.v @@ -508,13 +508,13 @@ suffices [le_i_ti le_ti_ni]: i <= tnth t i /\ tnth t i <= i + n. by rewrite /sub_mn inordK ?subnKC // ltnS leq_subLR. pose y0 := tnth t i; rewrite (tnth_nth y0) -(nth_map _ (val i)) ?size_tuple //. case def_e: (map _ _) => [|x e] /=; first by rewrite nth_nil ?leq_addr. -rewrite def_e in inc_t; split. - case: {-2}i; rewrite /= -{1}(size_tuple t) -(size_map val) def_e. - elim=> //= j IHj lt_j_t; apply: leq_trans (pathP (val i) inc_t _ lt_j_t). - by rewrite ltnS IHj 1?ltnW. +set nth_i := nth (i : nat); rewrite def_e in inc_t; split. + have: i < size (x :: e) by rewrite -def_e size_map size_tuple ltn_ord. + elim: (val i) => //= j IHj lt_j_e. + by apply: leq_trans (pathP (val i) inc_t _ lt_j_e); rewrite ltnS IHj 1?ltnW. move: (_ - _) (subnK (valP i)) => k /=. -elim: k {-2}(val i) => /= [|k IHk] j def_m; rewrite -ltnS -addSn. - by rewrite [j.+1]def_m -def_e (nth_map y0) ?ltn_ord // size_tuple -def_m. +elim: k (val i) => /= [|k IHk] j; rewrite -ltnS -addSn ?add0n => def_m. + by rewrite def_m -def_e /nth_i (nth_map y0) ?ltn_ord // size_tuple -def_m. rewrite (leq_trans _ (IHk _ _)) -1?addSnnS //; apply: (pathP _ inc_t). rewrite -ltnS (leq_trans (leq_addl k _)) // -addSnnS def_m. by rewrite -(size_tuple t) -(size_map val) def_e. diff --git a/mathcomp/ssreflect/choice.v b/mathcomp/ssreflect/choice.v index 49d50fe..4d7843c 100644 --- a/mathcomp/ssreflect/choice.v +++ b/mathcomp/ssreflect/choice.v @@ -90,11 +90,12 @@ Qed. Lemma codeK : cancel code decode. Proof. elim=> //= v s IHs; rewrite -[_ * _]prednK ?muln_gt0 ?expn_gt0 //=. -rewrite -{3}[v]addn0; elim: v {1 4}0 => [|v IHv {IHs}] q. - rewrite mul1n /= -{1}addnn -{4}IHs; move: (_ s) {IHs} => n. - by elim: {1 3}n => //=; case: n. +set two := 2; rewrite -[v in RHS]addn0; elim: v 0 => [|v IHv {IHs}] q. + rewrite mul1n add0n /= -{}[in RHS]IHs; case: (code s) => // u; pose n := u.+1. + by transitivity [rec q, n + u.+1, n.*2]; [rewrite addnn | elim: n => //=]. rewrite expnS -mulnA mul2n -{1}addnn -[_ * _]prednK ?muln_gt0 ?expn_gt0 //. -by rewrite doubleS addSn /= addSnnS; elim: {-2}_.-1 => //=. +set u := _.-1 in IHv *; set n := u; rewrite [in u1 in _ + u1]/n. +by rewrite [in RHS]addSnnS -{}IHv; elim: n. Qed. Lemma ltn_code s : all (fun j => j < code s) s. diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v index 48fb9fb..06a6ff1 100644 --- a/mathcomp/ssreflect/div.v +++ b/mathcomp/ssreflect/div.v @@ -40,11 +40,10 @@ Variant edivn_spec m d : nat * nat -> Type := Lemma edivnP m d : edivn_spec m d (edivn m d). Proof. -rewrite -{1}[m]/(0 * d + m) /edivn; case: d => //= d. -elim: m {-2}m 0 (leqnn m) => [|n IHn] [|m] q //= le_mn. -have le_m'n: m - d <= n by rewrite (leq_trans (leq_subr d m)). -rewrite subn_if_gt; case: ltnP => [// | le_dm]. -by rewrite -{1}(subnKC le_dm) -addSn addnA -mulSnr; apply: IHn. +rewrite -[m in edivn_spec m]/(0 * d + m) /edivn; case: d => //= d. +elim/ltn_ind: m 0 => -[|m] IHm q //=; rewrite subn_if_gt. +case: ltnP => // le_dm; rewrite -[in m.+1](subnKC le_dm) -addSn. +by rewrite addnA -mulSnr; apply/IHm/leq_subr. Qed. Lemma edivn_eq d q r : r < d -> edivn (q * d + r) d = (q, r). @@ -75,10 +74,8 @@ Notation "m != n %[mod d ]" := (m %% d != n %% d) : nat_scope. Lemma modn_def m d : m %% d = (edivn m d).2. Proof. -case: d => //= d; rewrite /modn /edivn /=. -elim: m {-2}m 0 (leqnn m) => [|n IHn] [|m] q //=. -rewrite ltnS !subn_if_gt; case: (d <= m) => // le_mn. -by apply: IHn; apply: leq_trans le_mn; apply: leq_subr. +case: d => //= d; rewrite /modn /edivn /=; elim/ltn_ind: m 0 => -[|m] IHm q //=. +by rewrite !subn_if_gt; case: (d <= m) => //; apply/IHm/leq_subr. Qed. Lemma edivn_def m d : edivn m d = (m %/ d, m %% d). @@ -97,7 +94,7 @@ Proof. by move=> lt_md; rewrite /divn (edivn_eq 0). Qed. Lemma divnMDl q m d : 0 < d -> (q * d + m) %/ d = q + m %/ d. Proof. -move=> d_gt0; rewrite {1}(divn_eq m d) addnA -mulnDl. +move=> d_gt0; rewrite [in LHS](divn_eq m d) addnA -mulnDl. by rewrite /divn edivn_eq // modn_def; case: edivnP; rewrite d_gt0. Qed. @@ -109,22 +106,22 @@ Proof. by move=> d_gt0; rewrite mulnC mulnK. Qed. Lemma expnB p m n : p > 0 -> m >= n -> p ^ (m - n) = p ^ m %/ p ^ n. Proof. -by move=> p_gt0 /subnK{2}<-; rewrite expnD mulnK // expn_gt0 p_gt0. +by move=> p_gt0 /subnK-Dm; rewrite -[in RHS]Dm expnD mulnK // expn_gt0 p_gt0. Qed. Lemma modn1 m : m %% 1 = 0. Proof. by rewrite modn_def; case: edivnP => ? []. Qed. Lemma divn1 m : m %/ 1 = m. -Proof. by rewrite {2}(@divn_eq m 1) // modn1 addn0 muln1. Qed. +Proof. by rewrite [RHS](@divn_eq m 1) // modn1 addn0 muln1. Qed. Lemma divnn d : d %/ d = (0 < d). -Proof. by case: d => // d; rewrite -{1}[d.+1]muln1 mulKn. Qed. +Proof. by case: d => // d; rewrite -[n in n %/ _]muln1 mulKn. Qed. Lemma divnMl p m d : p > 0 -> p * m %/ (p * d) = m %/ d. Proof. move=> p_gt0; case: (posnP d) => [-> | d_gt0]; first by rewrite muln0. -rewrite {2}/divn; case: edivnP; rewrite d_gt0 /= => q r ->{m} lt_rd. +rewrite [RHS]/divn; case: edivnP; rewrite d_gt0 /= => q r ->{m} lt_rd. rewrite mulnDr mulnCA divnMDl; last by rewrite muln_gt0 p_gt0. by rewrite addnC divn_small // ltn_pmul2l. Qed. @@ -141,10 +138,10 @@ Lemma ltn_pmod m d : 0 < d -> m %% d < d. Proof. by rewrite ltn_mod. Qed. Lemma leq_trunc_div m d : m %/ d * d <= m. -Proof. by rewrite {2}(divn_eq m d) leq_addr. Qed. +Proof. by rewrite [m in _ <= m](divn_eq m d) leq_addr. Qed. Lemma leq_mod m d : m %% d <= m. -Proof. by rewrite {2}(divn_eq m d) leq_addl. Qed. +Proof. by rewrite [m in _ <= m](divn_eq m d) leq_addl. Qed. Lemma leq_div m d : m %/ d <= m. Proof. @@ -153,7 +150,7 @@ Qed. Lemma ltn_ceil m d : 0 < d -> m < (m %/ d).+1 * d. Proof. -by move=> d_gt0; rewrite {1}(divn_eq m d) -addnS mulSnr leq_add2l ltn_mod. +by move=> d_gt0; rewrite [in m.+1](divn_eq m d) -addnS mulSnr leq_add2l ltn_mod. Qed. Lemma ltn_divLR m n d : d > 0 -> (m %/ d < n) = (m < n * d). @@ -244,7 +241,7 @@ Qed. Lemma divnMA m n p : m %/ (n * p) = m %/ n %/ p. Proof. case: n p => [|n] [|p]; rewrite ?muln0 ?div0n //. -rewrite {2}(divn_eq m (n.+1 * p.+1)) mulnA mulnAC !divnMDl //. +rewrite [in RHS](divn_eq m (n.+1 * p.+1)) mulnA mulnAC !divnMDl //. by rewrite [_ %/ p.+1]divn_small ?addn0 // ltn_divLR // mulnC ltn_mod. Qed. @@ -252,7 +249,7 @@ Lemma divnAC m n p : m %/ n %/ p = m %/ p %/ n. Proof. by rewrite -!divnMA mulnC. Qed. Lemma modn_small m d : m < d -> m %% d = m. -Proof. by move=> lt_md; rewrite {2}(divn_eq m d) divn_small. Qed. +Proof. by move=> lt_md; rewrite [RHS](divn_eq m d) divn_small. Qed. Lemma modn_mod m d : m %% d = m %[mod d]. Proof. by case: d => // d; apply: modn_small; rewrite ltn_mod. Qed. @@ -287,7 +284,7 @@ Lemma modnDr m d : m + d = m %[mod d]. Proof. by rewrite addnC modnDl. Qed. Lemma modnn d : d %% d = 0. -Proof. by rewrite -{1}[d]addn0 modnDl mod0n. Qed. +Proof. by rewrite -[d in d %% _]addn0 modnDl mod0n. Qed. Lemma modnMl p d : p * d %% d = 0. Proof. by rewrite -[p * d]addn0 modnMDl mod0n. Qed. @@ -296,7 +293,7 @@ Lemma modnMr p d : d * p %% d = 0. Proof. by rewrite mulnC modnMl. Qed. Lemma modnDml m n d : m %% d + n = m + n %[mod d]. -Proof. by rewrite {2}(divn_eq m d) -addnA modnMDl. Qed. +Proof. by rewrite [in RHS](divn_eq m d) -addnA modnMDl. Qed. Lemma modnDmr m n d : m + n %% d = m + n %[mod d]. Proof. by rewrite !(addnC m) modnDml. Qed. @@ -316,7 +313,7 @@ Lemma eqn_modDr p m n d : (m + p == n + p %[mod d]) = (m == n %[mod d]). Proof. by rewrite -!(addnC p) eqn_modDl. Qed. Lemma modnMml m n d : m %% d * n = m * n %[mod d]. -Proof. by rewrite {2}(divn_eq m d) mulnDl mulnAC modnMDl. Qed. +Proof. by rewrite [in RHS](divn_eq m d) mulnDl mulnAC modnMDl. Qed. Lemma modnMmr m n d : m * (n %% d) = m * n %[mod d]. Proof. by rewrite !(mulnC m) modnMml. Qed. @@ -328,11 +325,11 @@ Lemma modn2 m : m %% 2 = odd m. Proof. by elim: m => //= m IHm; rewrite -addn1 -modnDml IHm; case odd. Qed. Lemma divn2 m : m %/ 2 = m./2. -Proof. by rewrite {2}(divn_eq m 2) modn2 muln2 addnC half_bit_double. Qed. +Proof. by rewrite [in RHS](divn_eq m 2) modn2 muln2 addnC half_bit_double. Qed. Lemma odd_mod m d : odd d = false -> odd (m %% d) = odd m. Proof. -by move=> d_even; rewrite {2}(divn_eq m d) odd_add odd_mul d_even andbF. +by move=> d_even; rewrite [in RHS](divn_eq m d) odd_add odd_mul d_even andbF. Qed. Lemma modnXm m n a : (a %% n) ^ m = a ^ m %[mod n]. @@ -349,7 +346,7 @@ Notation "m %| d" := (dvdn m d) : nat_scope. Lemma dvdnP d m : reflect (exists k, m = k * d) (d %| m). Proof. apply: (iffP eqP) => [md0 | [k ->]]; last by rewrite modnMl. -by exists (m %/ d); rewrite {1}(divn_eq m d) md0 addn0. +by exists (m %/ d); rewrite [LHS](divn_eq m d) md0 addn0. Qed. Arguments dvdnP {d m}. @@ -389,7 +386,7 @@ Proof. by move=> d_dv_n /dvdnP[n1 ->]; apply: dvdn_mull. Qed. Lemma dvdn_eq d m : (d %| m) = (m %/ d * d == m). Proof. apply/eqP/eqP=> [modm0 | <-]; last exact: modnMl. -by rewrite {2}(divn_eq m d) modm0 addn0. +by rewrite [RHS](divn_eq m d) modm0 addn0. Qed. Lemma dvdn2 n : (2 %| n) = ~~ odd n. @@ -428,11 +425,11 @@ Lemma muln_divCA d m n : d %| m -> d %| n -> m * (n %/ d) = n * (m %/ d). Proof. by move=> dv_d_m dv_d_n; rewrite mulnC divn_mulAC ?muln_divA. Qed. Lemma divnA m n p : p %| n -> m %/ (n %/ p) = m * p %/ n. -Proof. by case: p => [|p] dv_n; rewrite -{2}(divnK dv_n) // divnMr. Qed. +Proof. by case: p => [|p] dv_n; rewrite -[in RHS](divnK dv_n) // divnMr. Qed. Lemma modn_dvdm m n d : d %| m -> n %% m = n %[mod d]. Proof. -by case/dvdnP=> q def_m; rewrite {2}(divn_eq n m) {3}def_m mulnA modnMDl. +by case/dvdnP=> q def_m; rewrite [in RHS](divn_eq n m) def_m mulnA modnMDl. Qed. Lemma dvdn_leq d m : 0 < m -> d %| m -> d <= m. @@ -518,7 +515,7 @@ Hint Resolve dvdn_add dvdn_sub dvdn_exp : core. Lemma eqn_mod_dvd d m n : n <= m -> (m == n %[mod d]) = (d %| m - n). Proof. -by move=> le_mn; rewrite -{1}[n]add0n -{1}(subnK le_mn) eqn_modDr mod0n. +by move/subnK=> Dm; rewrite -[n in LHS]add0n -[in LHS]Dm eqn_modDr mod0n. Qed. Lemma divnDMl q m d : 0 < d -> (m + q * d) %/ d = (m %/ d) + q. @@ -531,16 +528,16 @@ Lemma divnBMl q m d : (m - q * d) %/ d = (m %/ d) - q. Proof. by case: d => [|d]//=; rewrite divnB// mulnK// modnMl ltn0 subn0. Qed. Lemma divnDl m n d : d %| m -> (m + n) %/ d = m %/ d + n %/ d. -Proof. by case: d => // d /divnK{1}<-; rewrite divnMDl. Qed. +Proof. by case: d => // d /divnK-Dm; rewrite -[in LHS]Dm divnMDl. Qed. Lemma divnDr m n d : d %| n -> (m + n) %/ d = m %/ d + n %/ d. Proof. by move=> dv_n; rewrite addnC divnDl // addnC. Qed. Lemma divnBl m n d : d %| m -> (m - n) %/ d = m %/ d - (n %/ d) - (~~ (d %| n)). -Proof. by case: d => [|d] // /divnK {1}<-; rewrite divnMBl. Qed. +Proof. by case: d => [|d] // /divnK-Dm; rewrite -[in LHS]Dm divnMBl. Qed. Lemma divnBr m n d : d %| n -> (m - n) %/ d = m %/ d - n %/ d. -Proof. by case: d => [|d]// /divnK {1}<-; rewrite divnBMl. Qed. +Proof. by case: d => [|d]// /divnK-Dm; rewrite -[in LHS]Dm divnBMl. Qed. Lemma edivnS m d : 0 < d -> edivn m.+1 d = if d %| m.+1 then ((m %/ d).+1, 0) else (m %/ d, (m %% d).+1). @@ -592,11 +589,11 @@ Definition gcdn := nosimpl gcdn_rec. Lemma gcdnE m n : gcdn m n = if m == 0 then n else gcdn (n %% m) m. Proof. -rewrite /gcdn; elim: m {-2}m (leqnn m) n => [|s IHs] [|m] le_ms [|n] //=. -case def_n': (_ %% _) => // [n']. -have{def_n'} lt_n'm: n' < m by rewrite -def_n' -ltnS ltn_pmod. -rewrite {}IHs ?(leq_trans lt_n'm) // subn_if_gt ltnW //=; congr gcdn_rec. -by rewrite -{2}(subnK (ltnW lt_n'm)) -addnS modnDr. +rewrite /gcdn; elim/ltn_ind: m n => -[|m] IHm [|n] //=. +case def_p: (_ %% _) => // [p]. +have{def_p} lt_pm: p.+1 < m.+1 by rewrite -def_p ltn_pmod. +rewrite {}IHm // subn_if_gt ltnW //=; congr gcdn_rec. +by rewrite -(subnK (ltnW lt_pm)) modnDr. Qed. Lemma gcdnn : idempotent gcdn. @@ -606,7 +603,7 @@ Lemma gcdnC : commutative gcdn. Proof. move=> m n; wlog lt_nm: m n / n < m. by case: (ltngtP n m) => [||-> //]; last symmetry; auto. -by rewrite gcdnE -{1}(ltn_predK lt_nm) modn_small. +by rewrite gcdnE -[in m == 0](ltn_predK lt_nm) modn_small. Qed. Lemma gcd0n : left_id 0 gcdn. Proof. by case. Qed. @@ -620,11 +617,11 @@ Proof. by move=> n; rewrite gcdnC gcd1n. Qed. Lemma dvdn_gcdr m n : gcdn m n %| n. Proof. -elim: m {-2}m (leqnn m) n => [|s IHs] [|m] le_ms [|n] //. -rewrite gcdnE; case def_n': (_ %% _) => [|n']; first by rewrite /dvdn def_n'. -have lt_n's: n' < s by rewrite -ltnS (leq_trans _ le_ms) // -def_n' ltn_pmod. -rewrite /= (divn_eq n.+1 m.+1) def_n' dvdn_addr ?dvdn_mull //; last exact: IHs. -by rewrite gcdnE /= IHs // (leq_trans _ lt_n's) // ltnW // ltn_pmod. +elim/ltn_ind: m n => -[|m] IHm [|n] //=. +rewrite gcdnE; case def_p: (_ %% _) => [|p]; first by rewrite /dvdn def_p. +have lt_pm: p < m by rewrite -ltnS -def_p ltn_pmod. +rewrite /= (divn_eq n.+1 m.+1) def_p dvdn_addr ?dvdn_mull //; last exact: IHm. +by rewrite gcdnE /= IHm // (ltn_trans (ltn_pmod _ _)). Qed. Lemma dvdn_gcdl m n : gcdn m n %| m. @@ -639,7 +636,7 @@ Lemma gcdnMDl k m n : gcdn m (k * m + n) = gcdn m n. Proof. by rewrite !(gcdnE m) modnMDl mulnC; case: m. Qed. Lemma gcdnDl m n : gcdn m (m + n) = gcdn m n. -Proof. by rewrite -{2}(mul1n m) gcdnMDl. Qed. +Proof. by rewrite -[m in m + n]mul1n gcdnMDl. Qed. Lemma gcdnDr m n : gcdn m (n + m) = gcdn m n. Proof. by rewrite addnC gcdnDl. Qed. @@ -665,7 +662,7 @@ rewrite /minn; case: leqP; [rewrite gcdnC | move/ltnW]; Qed. Lemma gcdn_modr m n : gcdn m (n %% m) = gcdn m n. -Proof. by rewrite {2}(divn_eq n m) gcdnMDl. Qed. +Proof. by rewrite [in RHS](divn_eq n m) gcdnMDl. Qed. Lemma gcdn_modl m n : gcdn (m %% n) n = gcdn m n. Proof. by rewrite !(gcdnC _ n) gcdn_modr. Qed. @@ -694,16 +691,16 @@ Proof. by case: n. Qed. Lemma egcdnP m n : m > 0 -> egcdn_spec m n (egcdn m n). Proof. -rewrite /egcdn; have: (n, m) = Bezout_rec n m [::] by []. -case: (posnP n) => [-> /=|]; first by split; rewrite // mul1n gcdn0. -move: {2 6}n {4 6}n {1 4}m [::] (ltnSn n) => s n0 m0. -elim: s n m => [[]//|s IHs] n m qs /= le_ns n_gt0 def_mn0 m_gt0. -case: edivnP => q r def_m; rewrite n_gt0 /= => lt_rn. -case: posnP => [r0 {s le_ns IHs lt_rn}|r_gt0]; last first. - by apply: IHs => //=; [rewrite (leq_trans lt_rn) | rewrite natTrecE -def_m]. +have [-> /= | n_gt0 m_gt0] := posnP n; first by split; rewrite // mul1n gcdn0. +rewrite /egcdn; set s := (s in egcdn_rec _ _ s); pose bz := Bezout_rec n m [::]. +have: n < s.+1 by []; move defSpec: (egcdn_spec bz.2 bz.1) s => Spec s. +elim: s => [[]|s IHs] //= in n m (qs := [::]) bz defSpec n_gt0 m_gt0 *. +case: edivnP => q r def_m; rewrite n_gt0 ltnS /= => lt_rn le_ns1. +case: posnP => [r0 {s le_ns1 IHs lt_rn}|r_gt0]; last first. + by apply: IHs => //=; [rewrite natTrecE -def_m | rewrite (leq_trans lt_rn)]. rewrite {r}r0 addn0 in def_m; set b := odd _; pose d := gcdn m n. pose km := ~~ b : nat; pose kn := if b then 1 else q.-1. -rewrite (_ : Bezout_rec _ _ _ = Bezout_rec km kn qs); last first. +rewrite [bz in Spec bz](_ : _ = Bezout_rec km kn qs); last first. by rewrite /kn /km; case: (b) => //=; rewrite natTrecE addn0 muln1. have def_d: d = n by rewrite /d def_m gcdnC gcdnE modnMl gcd0n -[n]prednK. have: km * m + 2 * b * d = kn * n + d. @@ -713,14 +710,13 @@ have{def_m}: kn * d <= m. have q_gt0 : 0 < q by rewrite def_m muln_gt0 n_gt0 ?andbT in m_gt0. by rewrite /kn; case b; rewrite def_d def_m leq_pmul2r // leq_pred. have{def_d}: km * d <= n by rewrite -[n]mul1n def_d leq_pmul2r // leq_b1. -move: km {q}kn m_gt0 n_gt0 def_mn0; rewrite {}/d {}/b. +move: km {q}kn m_gt0 n_gt0 defSpec; rewrite {}/b {}/d {}/bz. elim: qs m n => [|q qs IHq] n r kn kr n_gt0 r_gt0 /=. - case=> -> -> {m0 n0}; rewrite !addn0 => le_kn_r _ def_d; split=> //. - have d_gt0: 0 < gcdn n r by rewrite gcdn_gt0 n_gt0. - have: 0 < kn * n by rewrite def_d addn_gt0 d_gt0 orbT. - rewrite muln_gt0 n_gt0 andbT; move/ltn_pmul2l <-. + set d := gcdn n r; rewrite mul0n addn0 => <- le_kn_r _ def_d; split=> //. + have d_gt0: 0 < d by rewrite gcdn_gt0 n_gt0. + have /ltn_pmul2l<-: 0 < kn by rewrite -(ltn_pmul2r n_gt0) def_d ltn_addl. by rewrite def_d -addn1 leq_add // mulnCA leq_mul2l le_kn_r orbT. -rewrite !natTrecE; set m:= _ + r; set km := _ * _ + kn; pose d := gcdn m n. +rewrite !natTrecE; set m := _ + r; set km := _ + kn; pose d := gcdn m n. have ->: gcdn n r = d by rewrite [d]gcdnC gcdnMDl. have m_gt0: 0 < m by rewrite addn_gt0 r_gt0 orbT. have d_gt0: 0 < d by rewrite gcdn_gt0 m_gt0. @@ -773,9 +769,8 @@ Proof. by move=> m n p q; rewrite -!gcdnA (gcdnCA n). Qed. Lemma muln_gcdr : right_distributive muln gcdn. Proof. move=> p m n; case: (posnP p) => [-> //| p_gt0]. -elim: {m}m.+1 {-2}m n (ltnSn m) => // s IHs m n; rewrite ltnS => le_ms. -rewrite gcdnE [rhs in _ = rhs]gcdnE muln_eq0 (gtn_eqF p_gt0) -muln_modr //=. -by case: posnP => // m_gt0; apply: IHs; apply: leq_trans le_ms; apply: ltn_pmod. +elim/ltn_ind: m n => m IHm n; rewrite gcdnE [RHS]gcdnE muln_eq0 (gtn_eqF p_gt0). +by case: posnP => // m_gt0; rewrite -muln_modr //=; apply/IHm/ltn_pmod. Qed. Lemma muln_gcdl : left_distributive muln gcdn. @@ -825,8 +820,9 @@ Proof. by move=> m n p; rewrite -!(mulnC p) muln_lcmr. Qed. Lemma lcmnA : associative lcmn. Proof. -move=> m n p; rewrite {1 3}/lcmn mulnC !divn_mulAC ?dvdn_mull ?dvdn_gcdr //. -rewrite -!divnMA ?dvdn_mulr ?dvdn_gcdl // mulnC mulnA !muln_gcdr. +move=> m n p; rewrite [LHS]/lcmn [RHS]/lcmn mulnC. +rewrite !divn_mulAC ?dvdn_mull ?dvdn_gcdr // -!divnMA ?dvdn_mulr ?dvdn_gcdl //. +rewrite mulnC mulnA !muln_gcdr; congr (_ %/ _). by rewrite ![_ * lcmn _ _]mulnC !muln_lcm_gcd !muln_gcdl -!(mulnC m) gcdnA. Qed. diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index 0da7a16..abdf23b 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -882,10 +882,11 @@ by rewrite ihss !size_cat size_merge size_cat -addnA addnCA -size_cat. Qed. Lemma sort_stable s : - sorted leT' s -> + sorted leT' s -> sorted [rel x y | leT x y && (leT y x ==> leT' x y)] (sort leT s). Proof. -case: {-2}s (erefl s) => // x _ -> sorted_s; rewrite -(mkseq_nth x s) sort_map. +move=> sorted_s; case Ds: s => // [x s1]; rewrite -{s1}Ds. +rewrite -(mkseq_nth x s) sort_map. apply/(homo_sorted_in (f := nth x s)): (sort_iota_stable x s (size s)). move=> /= y z; rewrite !mem_sort !mem_iota !leq0n add0n /= => y_le_s z_le_s. case/andP => -> /= /implyP yz; apply/implyP => /yz {yz} y_le_z. @@ -916,7 +917,7 @@ Qed. Lemma filter_sort p s : filter p (sort leT s) = sort leT (filter p s). Proof. -case: {-2}s (erefl s) => // x _ ->. +case Ds: s => // [x s1]; rewrite -{s1}Ds. rewrite -(mkseq_nth x s) !(filter_map, sort_map). congr map; apply/(@eq_sorted_irr _ (le_lex x s)) => //. - by move=> ?; rewrite /= ltnn implybF andbN. @@ -935,7 +936,7 @@ Variables (leT_total : total leT) (leT_tr : transitive leT). Lemma mask_sort s m : {m_s : bitseq | mask m_s (sort leT s) = sort leT (mask m s)}. Proof. -case: {-2}s (erefl s) => [|x _ ->]; first by case: m; exists [::]. +case Ds: {-}s => [|x s1]; [by rewrite Ds; case: m; exists [::] | clear s1 Ds]. rewrite -(mkseq_nth x s) -map_mask !sort_map. exists [seq i \in mask m (iota 0 (size s)) | i <- sort (xrelpre (nth x s) leT) (iota 0 (size s))]. @@ -1059,8 +1060,8 @@ Qed. Lemma looping_uniq x n : uniq (traject f x n.+1) = ~~ looping x n. Proof. rewrite /looping; elim: n x => [|n IHn] x //. -rewrite {-3}[n.+1]lock /= -lock {}IHn -iterSr -negb_or inE; congr (~~ _). -apply: orb_id2r => /trajectP no_loop. +rewrite [n.+1 in LHS]lock [iter]lock /= -!lock {}IHn -iterSr -negb_or inE. +congr (~~ _); apply: orb_id2r => /trajectP no_loop. apply/idP/eqP => [/trajectP[m le_m_n def_x] | {1}<-]; last first. by rewrite iterSr -last_traject mem_last. have loop_m: looping x m.+1 by rewrite /looping iterSr -def_x mem_head. @@ -1084,9 +1085,9 @@ Hypothesis Up : uniq p. Lemma prev_next : cancel (next p) (prev p). Proof. move=> x; rewrite prev_nth mem_next next_nth; case p_x: (x \in p) => //. -case def_p: p Up p_x => // [y q]; rewrite -{-1}def_p => /= /andP[not_qy Uq] p_x. -rewrite -{2}(nth_index y p_x); congr (nth y _ _); set i := index x p. -have: i <= size q by rewrite -index_mem -/i def_p in p_x. +case Dp: p Up p_x => // [y q]; rewrite [uniq _]/= -Dp => /andP[q'y Uq] p_x. +rewrite -[RHS](nth_index y p_x); congr (nth y _ _); set i := index x p. +have: i <= size q by rewrite -index_mem -/i Dp in p_x. case: ltngtP => // [lt_i_q|->] _; first by rewrite index_uniq. by apply/eqP; rewrite nth_default // eqn_leq index_size leqNgt index_mem. Qed. @@ -1103,7 +1104,7 @@ Qed. Lemma cycle_next : fcycle (next p) p. Proof. -case def_p: {-2}p Up => [|x q] Uq //. +case def_p: p Up => [|x q] Uq //; rewrite -[in next _]def_p. apply/(pathP x)=> i; rewrite size_rcons => le_i_q. rewrite -cats1 -cat_cons nth_cat le_i_q /= next_nth {}def_p mem_nth //. rewrite index_uniq // nth_cat /= ltn_neqAle andbC -ltnS le_i_q. diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v index 1185e67..4e55abe 100644 --- a/mathcomp/ssreflect/prime.v +++ b/mathcomp/ssreflect/prime.v @@ -202,12 +202,12 @@ have{def_m bc def_bc ltc2 ltbc3}: let kb := (ifnz e k 1).*2 in [&& k > 0, p < m, lb_dvd p m, c < kb & lb_dvd p p || (e == 0)] /\ m + (b * kb + c).*2 = p ^ 2 + (a * p).*2. -- rewrite -{-2}def_m; split=> //=; last first. +- rewrite -def_m [in lb_dvd _ _]def_m; split=> //=; last first. by rewrite -def_bc addSn -doubleD 2!addSn -addnA subnKC // addnC. rewrite ltc2 /lb_dvd /index_iota /= dvdn2 -def_m. by rewrite [_.+2]lock /= odd_double. -move: {2}a.+1 (ltnSn a) => n; clearbody k e. -elim: n => // n IHn in a k p m b c e *; rewrite ltnS => le_a_n []. +have [n] := ubnP a. +elim: n => // n IHn in a (k) p m b c (e) * => /ltnSE-le_a_n []. set kb := _.*2; set d := _ + c => /and5P[lt0k ltpm leppm ltc pr_p def_m]. have def_k1: k.-1.+1 = k := ltn_predK lt0k. have def_kb1: kb.-1.+1 = kb by rewrite /kb -def_k1; case e. @@ -618,17 +618,17 @@ Lemma lognE p m : logn p m = if [&& prime p, 0 < m & p %| m] then (logn p (m %/ p)).+1 else 0. Proof. rewrite /logn /dvdn; case p_pr: (prime p) => //. -rewrite /divn modn_def; case def_m: {2 3}m => [|m'] //=. +case def_m: m => // [m']; rewrite !andTb [LHS]/= -def_m /divn modn_def. case: edivnP def_m => [[|q] [|r] -> _] // def_m; congr _.+1; rewrite [_.1]/=. have{m def_m}: q < m'. by rewrite -ltnS -def_m addn0 mulnC -{1}[q.+1]mul1n ltn_pmul2r // prime_gt1. -elim: {m' q}_.+1 {-2}m' q.+1 (ltnSn m') (ltn0Sn q) => // s IHs. -case=> [[]|r] //= m; rewrite ltnS => lt_rs m_gt0 le_mr. -rewrite -{3}[m]prednK //=; case: edivnP => [[|q] [|_] def_q _] //. -have{def_q} lt_qm': q < m.-1. - by rewrite -[q.+1]muln1 -ltnS prednK // def_q addn0 ltn_pmul2l // prime_gt1. -have{le_mr} le_m'r: m.-1 <= r by rewrite -ltnS prednK. -by rewrite (IHs r) ?(IHs m.-1) // ?(leq_trans lt_qm', leq_trans _ lt_rs). +elim/ltn_ind: m' {q}q.+1 (ltn0Sn q) => -[_ []|r IHr m] //= m_gt0 le_mr. +rewrite -[m in logn_rec _ _ m]prednK //=. +case: edivnP => [[|q] [|_] def_q _] //; rewrite addn0 in def_q. +have{def_q} lt_qm1: q < m.-1. + by rewrite -[q.+1]muln1 -ltnS prednK // def_q ltn_pmul2l // prime_gt1. +have{le_mr} le_m1r: m.-1 <= r by rewrite -ltnS prednK. +by rewrite (IHr r) ?(IHr m.-1) // (leq_trans lt_qm1). Qed. Lemma logn_gt0 p n : (0 < logn p n) = (p \in primes n). @@ -803,9 +803,10 @@ Lemma trunc_log_bounds p n : 1 < p -> 0 < n -> let k := trunc_log p n in p ^ k <= n < p ^ k.+1. Proof. rewrite {+}/trunc_log => p_gt1; have p_gt0 := ltnW p_gt1. -elim: n {-2 5}n (leqnn n) => [|m IHm] [|n] //=; rewrite ltnS => le_n_m _. +set loop := (loop in loop n n); set m := n; rewrite [in n in loop m n]/m. +have: m <= n by []; elim: n m => [|n IHn] [|m] //= /ltnSE-le_m_n _. have [le_p_n | // ] := leqP p _; rewrite 2!expnSr -leq_divRL -?ltn_divLR //. -by apply: IHm; rewrite ?divn_gt0 // -ltnS (leq_trans (ltn_Pdiv _ _)). +by apply: IHn; rewrite ?divn_gt0 // -ltnS (leq_trans (ltn_Pdiv _ _)). Qed. Lemma trunc_log_ltn p n : 1 < p -> n < p ^ (trunc_log p n).+1. @@ -1368,7 +1369,7 @@ Qed. Lemma totient_count_coprime n : totient n = \sum_(0 <= d < n) coprime n d. Proof. -elim: {n}_.+1 {-2}n (ltnSn n) => // m IHm n; rewrite ltnS => le_n_m. +elim/ltn_ind: n => // n IHn. case: (leqP n 1) => [|lt1n]; first by rewrite unlock; case: (n) => [|[]]. pose p := pdiv n; have p_pr: prime p by apply: pdiv_prime. have p1 := prime_gt1 p_pr; have p0 := ltnW p1. @@ -1378,11 +1379,10 @@ have [n0 np0 np'0]: [/\ n > 0, np > 0 & np' > 0] by rewrite ltnW ?part_gt0. have def_n: n = np * np' by rewrite partnC. have lnp0: 0 < logn p n by rewrite lognE p_pr n0 pdiv_dvd. pose in_mod k (k0 : k > 0) d := Ordinal (ltn_pmod d k0). -rewrite {1}def_n totient_coprime // {IHm}(IHm np') ?big_mkord; last first. - apply: leq_trans le_n_m; rewrite def_n ltn_Pmull //. - by rewrite /np p_part -(expn0 p) ltn_exp2l. +rewrite {1}def_n totient_coprime // {IHn}(IHn np') ?big_mkord; last first. + by rewrite def_n ltn_Pmull // /np p_part -(expn0 p) ltn_exp2l. have ->: totient np = #|[pred d : 'I_np | coprime np d]|. - rewrite {1}[np]p_part totient_pfactor //=; set q := p ^ _. + rewrite [np in LHS]p_part totient_pfactor //=; set q := p ^ _. apply: (@addnI (1 * q)); rewrite -mulnDl [1 + _]prednK // mul1n. have def_np: np = p * q by rewrite -expnS prednK // -p_part. pose mulp := [fun d : 'I_q => in_mod _ np0 (p * d)]. diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 74b3f15..5566a44 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -1453,7 +1453,7 @@ Definition perm_eq s1 s2 := Lemma permP s1 s2 : reflect (count^~ s1 =1 count^~ s2) (perm_eq s1 s2). Proof. apply: (iffP allP) => /= [eq_cnt1 a | eq_cnt x _]; last exact/eqP. -elim: {a}_.+1 {-2}a (ltnSn (count a (s1 ++ s2))) => // n IHn a le_an. +have [n le_an] := ubnP (count a (s1 ++ s2)); elim: n => // n IHn in a le_an *. have [/eqP|] := posnP (count a (s1 ++ s2)). by rewrite count_cat addn_eq0; do 2!case: eqP => // ->. rewrite -has_count => /hasP[x s12x a_x]; pose a' := predD1 a x. diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index d47a3ba..9f826aa 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -400,6 +400,51 @@ Proof. by move=> lt_mn /ltnW; apply: leq_trans. Qed. Lemma leq_total m n : (m <= n) || (m >= n). Proof. by rewrite -implyNb -ltnNge; apply/implyP; apply: ltnW. Qed. +(* Helper lemmas to support generalized induction over a nat measure. *) +(* The idiom for a proof by induction over a measure Mxy : nat involving *) +(* variables x, y, ... (e.g., size x + size y) is *) +(* have [m leMn] := ubnP Mxy; elim: n => // n IHn in x y ... leMn ... *. *) +(* after which the current goal (possibly modified by generalizations in the *) +(* in ... part) can be proven with the extra context assumptions *) +(* n : nat *) +(* IHn : forall x y ..., Mxy < n -> ... -> the_initial_goal *) +(* leMn : Mxy < n.+1 *) +(* This is preferable to the legacy idiom relying on numerical occurrence *) +(* selection, which is fragile if there can be multiple occurrences of x, y, *) +(* ... in the measure expression Mxy (e.g., in #|y| with x : finType and *) +(* y : {set x}). *) +(* The leMn statement is convertible to Mxy <= n; if it is necessary to *) +(* have _exactly_ leMn : Mxy <= n, the ltnSE helper lemma may be used as *) +(* follows *) +(* have [m] := ubnP Mxy; elim: n => // n IHn in x y ... * => /ltnSE-leMn. *) +(* We also provide alternative helper lemmas for proofs where the upper *) +(* bound appears in the goal, and we assume nonstrict (in)equality. *) +(* In either case the proof will have to dispatch an Mxy = 0 case. *) +(* have [m defM] := ubnPleq Mxy; elim: n => [|n IHn] in x y ... defM ... *. *) +(* yields two subgoals, in which Mxy has been replaced by 0 and n.+1, *) +(* with the extra assumption defM : Mxy <= 0 / Mxy <= n.+1, respectively. *) +(* The second goal also has the inductive assumption *) +(* IHn : forall x y ..., Mxy <= n -> ... -> the_initial_goal[n / Mxy]. *) +(* Using ubnPgeq or ubnPeq instead of ubnPleq yields assumptions with *) +(* Mxy >= 0/n.+1 or Mxy == 0/n.+1 instead of Mxy <= 0/n.+1, respectively. *) +(* These introduce a different kind of induction; for example ubnPgeq M lets *) +(* us remember that n < M throughout the induction. *) +(* Finally, the ltn_ind lemma provides a generalized induction view for a *) +(* property of a single integer (i.e., the case Mxy := x). *) +Lemma ubnP m : {n | m < n}. Proof. by exists m.+1. Qed. +Lemma ltnSE m n : m < n.+1 -> m <= n. Proof. by []. Qed. +Variant ubn_leq_spec m : nat -> Type := UbnLeq n of m <= n : ubn_leq_spec m n. +Variant ubn_geq_spec m : nat -> Type := UbnGeq n of m >= n : ubn_geq_spec m n. +Variant ubn_eq_spec m : nat -> Type := UbnEq n of m == n : ubn_eq_spec m n. +Lemma ubnPleq m : ubn_leq_spec m m. Proof. by []. Qed. +Lemma ubnPgeq m : ubn_geq_spec m m. Proof. by []. Qed. +Lemma ubnPeq m : ubn_eq_spec m m. Proof. by []. Qed. +Lemma ltn_ind P : (forall n, (forall m, m < n -> P m) -> P n) -> forall n, P n. +Proof. +move=> accP M; have [n leMn] := ubnP M; elim: n => // n IHn in M leMn *. +by apply/accP=> p /leq_trans/(_ leMn)/IHn. +Qed. + (* Link to the legacy comparison predicates. *) Lemma leP m n : reflect (m <= n)%coq_nat (m <= n). @@ -412,15 +457,14 @@ Arguments leP {m n}. Lemma le_irrelevance m n le_mn1 le_mn2 : le_mn1 = le_mn2 :> (m <= n)%coq_nat. Proof. -elim: {n}n.+1 {-1}n (erefl n.+1) => // n IHn _ [<-] in le_mn1 le_mn2 *. -pose def_n2 := erefl n; transitivity (eq_ind _ _ le_mn2 _ def_n2) => //. -move def_n1: {1 4 5 7}n le_mn1 le_mn2 def_n2 => n1 le_mn1. -case: n1 / le_mn1 def_n1 => [|n1 le_mn1] def_n1 [|n2 le_mn2] def_n2. -- by rewrite [def_n2]eq_axiomK. -- by move/leP: (le_mn2); rewrite -{1}def_n2 ltnn. -- by move/leP: (le_mn1); rewrite {1}def_n2 ltnn. -case: def_n2 (def_n2) => ->{n2} def_n2 in le_mn2 *. -by rewrite [def_n2]eq_axiomK /=; congr le_S; apply: IHn. +elim/ltn_ind: n => n IHn in le_mn1 le_mn2 *; set n1 := n in le_mn1 *. +pose def_n : n = n1 := erefl n; transitivity (eq_ind _ _ le_mn2 _ def_n) => //. +case: n1 / le_mn1 le_mn2 => [|n1 le_mn1] {n}[|n le_mn2] in (def_n) IHn *. +- by rewrite [def_n]eq_axiomK. +- by case/leP/idPn: (le_mn2); rewrite -def_n ltnn. +- by case/leP/idPn: (le_mn1); rewrite def_n ltnn. +case: def_n (def_n) => <-{n1} def_n in le_mn1 *. +by rewrite [def_n]eq_axiomK /=; congr le_S; apply: IHn. Qed. Lemma ltP m n : reflect (m < n)%coq_nat (m < n). @@ -1681,7 +1725,7 @@ Definition bin_of_nat n0 := if n0 is n.+1 then Npos (pos_of_nat n n) else 0%num. Lemma bin_of_natK : cancel bin_of_nat nat_of_bin. Proof. have sub2nn n : n.*2 - n = n by rewrite -addnn addKn. -case=> //= n; rewrite -{3}[n]sub2nn. +case=> //= n; rewrite -[n in RHS]sub2nn. by elim: n {2 4}n => // m IHm [|[|n]] //=; rewrite IHm // natTrecE sub2nn. Qed. |