diff options
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 6 | ||||
| -rw-r--r-- | mathcomp/algebra/polydiv.v | 105 | ||||
| -rw-r--r-- | mathcomp/solvable/abelian.v | 4 | ||||
| -rw-r--r-- | mathcomp/solvable/extremal.v | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/div.v | 16 | ||||
| -rw-r--r-- | mathcomp/ssreflect/fintype.v | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/order.v | 4 | ||||
| -rw-r--r-- | mathcomp/ssreflect/prime.v | 10 | ||||
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 20 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 152 |
10 files changed, 164 insertions, 157 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 6c1cd5b..6d2d74f 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -93,6 +93,12 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). `Num` module. However, instances of the number structures may require changes. +- Extended comparison predicates `leqP`, `ltnP`, and `ltngtP` in ssrnat to + allow case analysis on `minn` and `maxn`. + + The compatibility layer for the version 1.10 is provided as the + `ssrnat.mc_1_10` module. One may compile proofs compatible with the version + 1.10 in newer versions by using this module. + ### Renamed - `real_lerP` -> `real_leP` diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v index afd0c6c..a7d3b1e 100644 --- a/mathcomp/algebra/polydiv.v +++ b/mathcomp/algebra/polydiv.v @@ -241,7 +241,7 @@ Qed. Lemma leq_rmodp m d : size (rmodp m d) <= size m. Proof. -case: (ltnP (size m) (size d)) => [|h]; first by move/rmodp_small->. +have [/rmodp_small -> //|h] := ltnP (size m) (size d). have [->|d0] := eqVneq d 0; first by rewrite rmodp0. by apply: leq_trans h; apply: ltnW; rewrite ltn_rmodp. Qed. @@ -1106,7 +1106,7 @@ Qed. Lemma dvdp_leq p q : q != 0 -> p %| q -> size p <= size q. Proof. move=> nq0 /modp_eq0P. -by case: ltngtP => // /modp_small -> /eqP; rewrite (negPf nq0). +by case: leqP => // /modp_small -> /eqP; rewrite (negPf nq0). Qed. Lemma eq_dvdp c quo q p : c != 0 -> c *: p = quo * q -> q %| p. @@ -1359,24 +1359,16 @@ by rewrite /eqp (dvdp_trans Dp) // (dvdp_trans qD). Qed. Lemma eqp_ltrans : left_transitive (@eqp R). -Proof. -by move=> p q r pq; apply/idP/idP; apply: eqp_trans; rewrite // eqp_sym. -Qed. +Proof. exact: sym_left_transitive eqp_sym eqp_trans. Qed. Lemma eqp_rtrans : right_transitive (@eqp R). -Proof. by move=> x y xy z; rewrite eqp_sym (eqp_ltrans xy) eqp_sym. Qed. +Proof. exact: sym_right_transitive eqp_sym eqp_trans. Qed. Lemma eqp0 p : (p %= 0) = (p == 0). -Proof. -have [->|Ep] := eqVneq; first by rewrite ?eqpxx. -by apply/negP => /andP [_]; rewrite /dvdp modp0 (negPf Ep). -Qed. +Proof. by apply/idP/eqP => [/andP [_ /dvd0pP] | -> //]. Qed. Lemma eqp01 : 0 %= (1 : {poly R}) = false. -Proof. -case: eqpP => // -[[c1 c2]] /andP [c1n0 c2n0] /= /esym /eqP. -by rewrite scaler0 alg_polyC polyC_eq0 (negPf c2n0). -Qed. +Proof. by rewrite eqp_sym eqp0 oner_eq0. Qed. Lemma eqp_scale p c : c != 0 -> c *: p %= p. Proof. @@ -1597,12 +1589,12 @@ Proof. have [r] := ubnP (minn (size q) (size p)); elim: r => // r IHr in p q *. have [-> | nz_p] := eqVneq p 0; first by rewrite gcd0p dvdpp andbT. have [-> | nz_q] := eqVneq q 0; first by rewrite gcdp0 dvdpp /=. -rewrite ltnS gcdpE minnC /minn; case: ltnP => [lt_pq | le_pq] le_qr. - suffices /IHr/andP[E1 E2]: minn (size p) (size (q %% p)) < r. - by rewrite E2 (dvdp_mod _ E2). +rewrite ltnS gcdpE; case: leqP => [le_pq | lt_pq] le_qr. + suffices /IHr/andP[E1 E2]: minn (size q) (size (p %% q)) < r. + by rewrite E2 andbT (dvdp_mod _ E2). by rewrite gtn_min orbC (leq_trans _ le_qr) ?ltn_modp. -suffices /IHr/andP[E1 E2]: minn (size q) (size (p %% q)) < r. - by rewrite E2 andbT (dvdp_mod _ E2). +suffices /IHr/andP[E1 E2]: minn (size p) (size (q %% p)) < r. + by rewrite E2 (dvdp_mod _ E2). by rewrite gtn_min orbC (leq_trans _ le_qr) ?ltn_modp. Qed. @@ -1623,10 +1615,10 @@ apply/idP/andP=> [dv_pmn | []]. have [r] := ubnP (minn (size n) (size m)); elim: r => // r IHr in m n *. have [-> | nz_m] := eqVneq m 0; first by rewrite gcd0p. have [-> | nz_n] := eqVneq n 0; first by rewrite gcdp0. -rewrite gcdpE minnC ltnS /minn; case: ltnP => [lt_mn | le_nm] le_r dv_m dv_n. - apply: IHr => //; last by rewrite -(dvdp_mod _ dv_m). +rewrite gcdpE ltnS; case: leqP => [le_nm | lt_mn] le_r dv_m dv_n. + apply: IHr => //; last by rewrite -(dvdp_mod _ dv_n). by rewrite gtn_min orbC (leq_trans _ le_r) ?ltn_modp. -apply: IHr => //; last by rewrite -(dvdp_mod _ dv_n). +apply: IHr => //; last by rewrite -(dvdp_mod _ dv_m). by rewrite gtn_min orbC (leq_trans _ le_r) ?ltn_modp. Qed. @@ -1702,11 +1694,8 @@ Proof. by move/dvdp_gcd_idl; exact/eqp_trans/gcdpC. Qed. Lemma gcdp_exp p k l : gcdp (p ^+ k) (p ^+ l) %= p ^+ minn k l. Proof. -wlog leqmn: k l / k <= l. - move=> hwlog; case: (leqP k l); first exact: hwlog. - by move/ltnW; rewrite minnC; move/hwlog; apply/eqp_trans/gcdpC. -rewrite (minn_idPl leqmn); move/subnK: leqmn<-; rewrite exprD. -by apply: eqp_trans (gcdp_mull _ _) _; apply: eqpxx. +case: leqP => [|/ltnW] /subnK <-; rewrite exprD; first exact: gcdp_mull. +exact/(eqp_trans (gcdpC _ _))/gcdp_mull. Qed. Lemma gcdp_eq0 p q : gcdp p q == 0 = (p == 0) && (q == 0). @@ -1730,40 +1719,33 @@ by rewrite -(eqp_dvdr _ eqr) dvdp_gcdl (eqp_dvdr _ eqr) dvdp_gcdl. Qed. Lemma eqp_gcd p1 p2 q1 q2 : p1 %= p2 -> q1 %= q2 -> gcdp p1 q1 %= gcdp p2 q2. -Proof. -move=> e1 e2. -by apply: eqp_trans (eqp_gcdr _ e2); apply: eqp_trans (eqp_gcdl _ e1). -Qed. +Proof. move=> e1 e2; exact: eqp_trans (eqp_gcdr _ e2) (eqp_gcdl _ e1). Qed. Lemma eqp_rgcd_gcd p q : rgcdp p q %= gcdp p q. Proof. move: {2}(minn (size p) (size q)) (leqnn (minn (size p) (size q))) => n. elim: n p q => [p q|n ihn p q hs]. - rewrite leqn0 /minn; case: ltnP => _; rewrite size_poly_eq0; move/eqP->. + rewrite leqn0; case: ltnP => _; rewrite size_poly_eq0; move/eqP->. by rewrite gcd0p rgcd0p eqpxx. by rewrite gcdp0 rgcdp0 eqpxx. have [-> | pn0] := eqVneq p 0; first by rewrite gcd0p rgcd0p eqpxx. have [-> | qn0] := eqVneq q 0; first by rewrite gcdp0 rgcdp0 eqpxx. -rewrite gcdpE rgcdpE; case: ltnP => sp. +rewrite gcdpE rgcdpE; case: ltnP hs => sp hs. have e := eqp_rmod_mod q p; apply/eqp_trans/ihn: (eqp_gcdl p e). - rewrite (eqp_size e) geq_min -ltnS (leq_trans _ hs) //. - by rewrite (minn_idPl (ltnW _)) ?ltn_modp. + by rewrite (eqp_size e) geq_min -ltnS (leq_trans _ hs) ?ltn_modp. have e := eqp_rmod_mod p q; apply/eqp_trans/ihn: (eqp_gcdl q e). -rewrite (eqp_size e) geq_min -ltnS (leq_trans _ hs) //. -by rewrite (minn_idPr _) ?ltn_modp. +by rewrite (eqp_size e) geq_min -ltnS (leq_trans _ hs) ?ltn_modp. Qed. -Lemma gcdp_modr m n : gcdp m (n %% m) %= gcdp m n. +Lemma gcdp_modl m n : gcdp (m %% n) n %= gcdp m n. Proof. -have [-> | mn0] := eqVneq m 0; first by rewrite modp0 eqpxx. -have : (lead_coef m) ^+ (scalp n m) != 0 by rewrite expf_neq0 // lead_coef_eq0. -move/(gcdp_scaler m n); apply/eqp_trans. -by rewrite divp_eq eqp_sym gcdp_addl_mul. +have [/modp_small -> // | lenm] := ltnP (size m) (size n). +by rewrite (gcdpE m n) ltnNge lenm. Qed. -Lemma gcdp_modl m n : gcdp (m %% n) n %= gcdp m n. +Lemma gcdp_modr m n : gcdp m (n %% m) %= gcdp m n. Proof. -apply: eqp_trans (gcdpC _ _); apply: eqp_trans (gcdp_modr _ _); exact: gcdpC. +apply: eqp_trans (gcdpC _ _); apply: eqp_trans (gcdp_modl _ _); exact: gcdpC. Qed. Lemma gcdp_def d m n : @@ -2798,10 +2780,7 @@ by rewrite modp_scaler ?eqpxx // mulf_eq0 negb_or invr_eq0 c1n0. Qed. Lemma eqp_mod p1 p2 q1 q2 : p1 %= p2 -> q1 %= q2 -> p1 %% q1 %= p2 %% q2. -Proof. -move=> e1 e2; apply: eqp_trans (eqp_modpr _ e2). -by apply: eqp_trans (eqp_modpl _ e1); apply: eqpxx. -Qed. +Proof. move=> e1 e2; exact: eqp_trans (eqp_modpl _ e1) (eqp_modpr _ e2). Qed. Lemma eqp_divr (d m n : {poly F}) : m %= n -> (d %/ m) %= (d %/ n). Proof. @@ -2811,10 +2790,7 @@ by rewrite divp_scaler ?eqp_scale // ?invr_eq0 mulf_eq0 negb_or invr_eq0 c1n0. Qed. Lemma eqp_div p1 p2 q1 q2 : p1 %= p2 -> q1 %= q2 -> p1 %/ q1 %= p2 %/ q2. -Proof. -move=> e1 e2; apply: eqp_trans (eqp_divr _ e2). -by apply: eqp_trans (eqp_divl _ e1); apply: eqpxx. -Qed. +Proof. move=> e1 e2; exact: eqp_trans (eqp_divl _ e1) (eqp_divr _ e2). Qed. Lemma eqp_gdcor p q r : q %= r -> gdcop p q %= gdcop p r. Proof. @@ -2847,42 +2823,33 @@ case: ifP=> // _; apply: ihn => //; apply: eqp_trans (eqp_rdiv_div _ _) _. by apply: eqp_div => //; apply: eqp_trans (eqp_rgcd_gcd _ _) _; apply: eqp_gcd. Qed. -Lemma modp_opp p q : (- p) %% q = - (p %% q). -Proof. -have [-> | qn0] := eqVneq q 0; first by rewrite !modp0. -by apply: IdomainUnit.modp_opp; rewrite unitfE lead_coef_eq0. -Qed. - -Lemma divp_opp p q : (- p) %/ q = - (p %/ q). -Proof. -have [-> | qn0] := eqVneq q 0; first by rewrite !divp0 oppr0. -by apply: IdomainUnit.divp_opp; rewrite unitfE lead_coef_eq0. -Qed. - Lemma modp_add d p q : (p + q) %% d = p %% d + q %% d. Proof. have [-> | dn0] := eqVneq d 0; first by rewrite !modp0. by apply: IdomainUnit.modp_add; rewrite unitfE lead_coef_eq0. Qed. -Lemma modNp p q : (- p) %% q = - (p %% q). +Lemma modp_opp p q : (- p) %% q = - (p %% q). Proof. by apply/eqP; rewrite -addr_eq0 -modp_add addNr mod0p. Qed. +Lemma modNp p q : (- p) %% q = - (p %% q). Proof. exact: modp_opp. Qed. + Lemma divp_add d p q : (p + q) %/ d = p %/ d + q %/ d. Proof. have [-> | dn0] := eqVneq d 0; first by rewrite !divp0 addr0. by apply: IdomainUnit.divp_add; rewrite unitfE lead_coef_eq0. Qed. -Lemma divp_addl_mul_small d q r : - size r < size d -> (q * d + r) %/ d = q. +Lemma divp_opp p q : (- p) %/ q = - (p %/ q). +Proof. by apply/eqP; rewrite -addr_eq0 -divp_add addNr div0p. Qed. + +Lemma divp_addl_mul_small d q r : size r < size d -> (q * d + r) %/ d = q. Proof. move=> srd; rewrite divp_add (divp_small srd) addr0 mulpK //. by rewrite -size_poly_gt0; apply: leq_trans srd. Qed. -Lemma modp_addl_mul_small d q r : - size r < size d -> (q * d + r) %% d = r. +Lemma modp_addl_mul_small d q r : size r < size d -> (q * d + r) %% d = r. Proof. by move=> srd; rewrite modp_add modp_mull add0r modp_small. Qed. Lemma divp_addl_mul d q r : d != 0 -> (q * d + r) %/ d = q + r %/ d. diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v index 5f93277..95bc562 100644 --- a/mathcomp/solvable/abelian.v +++ b/mathcomp/solvable/abelian.v @@ -2064,12 +2064,12 @@ apply: eq_bigr => p _; transitivity (p ^ logn p #[x])%N. suffices lti_lnO e: (i < lnO p e _ G) = (e < logn p #[x]). congr (p ^ _)%N; apply/eqP; rewrite eqn_leq andbC; apply/andP; split. by apply/bigmax_leqP=> e; rewrite lti_lnO. - case: (posnP (logn p #[x])) => [-> // | logx_gt0]. + have [-> //|logx_gt0] := posnP (logn p #[x]). have lexpG: (logn p #[x]).-1 < logn p #|G|. by rewrite prednK // dvdn_leq_log ?order_dvdG. by rewrite (@bigmax_sup _ (Ordinal lexpG)) ?(prednK, lti_lnO). rewrite /lnO -(count_logn_dprod_cycle _ _ defG). -case: (ltnP e _) (b_sorted p) => [lt_e_x | le_x_e]. +case: (ltnP e) (b_sorted p) => [lt_e_x | le_x_e]. rewrite -(cat_take_drop i.+1 b) -map_rev rev_cat !map_cat cat_path. case/andP=> _ ordb; rewrite count_cat ((count _ _ =P i.+1) _) ?leq_addr //. rewrite -{2}(size_takel ltib) -all_count. diff --git a/mathcomp/solvable/extremal.v b/mathcomp/solvable/extremal.v index 36c4d12..42882bc 100644 --- a/mathcomp/solvable/extremal.v +++ b/mathcomp/solvable/extremal.v @@ -2039,7 +2039,7 @@ have [n oG] := p_natP pG; right; rewrite p2 cG /= in oG *. rewrite oG (@leq_exp2l 2 4) //. rewrite /extremal2 /extremal_class oG pfactorKpdiv // in cG. case: andP cG => [[n_gt1 isoG] _ | _]; last first. - by rewrite leq_eqVlt; case: (3 < n); case: eqP => //= <-; do 2?case: ifP. + by case: (ltngtP 3 n) => //= <-; do 2?case: ifP. have [[x y] genG _] := generators_2dihedral n_gt1 isoG. have [_ _ _ [_ _ maxG]] := dihedral2_structure n_gt1 genG isoG. rewrite 2!ltn_neqAle n_gt1 !(eq_sym _ n). diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v index 06a6ff1..b366055 100644 --- a/mathcomp/ssreflect/div.v +++ b/mathcomp/ssreflect/div.v @@ -120,7 +120,7 @@ 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. +move=> p_gt0; have [->|d_gt0] := posnP d; first by rewrite muln0. 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. @@ -544,9 +544,9 @@ Lemma edivnS m d : 0 < d -> edivn m.+1 d = Proof. case: d => [|[|d]] //= _; first by rewrite edivn_def modn1 dvd1n !divn1. rewrite -addn1 /dvdn modn_def edivnD//= (@modn_small 1)// (@divn_small 1)//. -rewrite addn1 addn0 ltnS; case: (ltngtP _ d.+1) => [ | |->]. -- by rewrite addn0 mul0n subn0. +rewrite addn1 addn0 ltnS; have [||<-] := ltngtP d.+1. - by rewrite ltnNge -ltnS ltn_pmod. +- by rewrite addn0 mul0n subn0. - by rewrite addn1 mul1n subnn. Qed. @@ -656,10 +656,7 @@ Lemma gcdn_idPr {m n} : reflect (gcdn m n = n) (n %| m). Proof. by rewrite gcdnC; apply: gcdn_idPl. Qed. Lemma expn_min e m n : e ^ minn m n = gcdn (e ^ m) (e ^ n). -Proof. -rewrite /minn; case: leqP; [rewrite gcdnC | move/ltnW]; - by move/(dvdn_exp2l e)/gcdn_idPl. -Qed. +Proof. by case: leqP => [|/ltnW] /(dvdn_exp2l e) /gcdn_idPl; rewrite gcdnC. Qed. Lemma gcdn_modr m n : gcdn m (n %% m) = gcdn m n. Proof. by rewrite [in RHS](divn_eq n m) gcdnMDl. Qed. @@ -863,10 +860,7 @@ Lemma lcmn_idPl {m n} : reflect (lcmn m n = m) (n %| m). Proof. by rewrite lcmnC; apply: lcmn_idPr. Qed. Lemma expn_max e m n : e ^ maxn m n = lcmn (e ^ m) (e ^ n). -Proof. -rewrite /maxn; case: leqP; [rewrite lcmnC | move/ltnW]; - by move/(dvdn_exp2l e)/lcmn_idPr. -Qed. +Proof. by case: leqP => [|/ltnW] /(dvdn_exp2l e) /lcmn_idPl; rewrite lcmnC. Qed. (* Coprime factors *) diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index 14d623f..6c27b73 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -2037,7 +2037,7 @@ Proof. (* match representation is changed to omit these then this proof could reduce *) (* to by rewrite /split; case: ltnP; [left | right. rewrite subnKC]. *) set lt_i_m := i < m; rewrite /split. -by case: {-}_ lt_i_m / ltnP; [left | right; rewrite subnKC]. +by case: _ _ _ _ {-}_ lt_i_m / ltnP; [left | right; rewrite subnKC]. Qed. Definition unsplit {m n} (jk : 'I_m + 'I_n) := diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v index 5c8f251..b261072 100644 --- a/mathcomp/ssreflect/order.v +++ b/mathcomp/ssreflect/order.v @@ -4556,10 +4556,10 @@ Module NatOrder. Section NatOrder. Lemma minnE x y : minn x y = if (x <= y)%N then x else y. -Proof. by case: leqP => [/minn_idPl|/ltnW /minn_idPr]. Qed. +Proof. by case: leqP. Qed. Lemma maxnE x y : maxn x y = if (y <= x)%N then x else y. -Proof. by case: leqP => [/maxn_idPl|/ltnW/maxn_idPr]. Qed. +Proof. by case: leqP. Qed. Lemma ltn_def x y : (x < y)%N = (y != x) && (x <= y)%N. Proof. by rewrite ltn_neqAle eq_sym. Qed. diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v index d8f5939..b71f5e7 100644 --- a/mathcomp/ssreflect/prime.v +++ b/mathcomp/ssreflect/prime.v @@ -583,7 +583,7 @@ move=> m_gt0 n_gt0; apply/eqP/hasPn=> [mn1 p | no_p_mn]. rewrite /= !mem_primes m_gt0 n_gt0 /= => /andP[pr_p p_n]. have:= prime_gt1 pr_p; rewrite pr_p ltnNge -mn1 /=; apply: contra => p_m. by rewrite dvdn_leq ?gcdn_gt0 ?m_gt0 // dvdn_gcd ?p_m. -case: (ltngtP (gcdn m n) 1) => //; first by rewrite ltnNge gcdn_gt0 ?m_gt0. +apply/eqP; rewrite eqn_leq gcdn_gt0 m_gt0 andbT leqNgt; apply/negP. move/pdiv_prime; set p := pdiv _ => pr_p. move/implyP: (no_p_mn p); rewrite /= !mem_primes m_gt0 n_gt0 pr_p /=. by rewrite !(dvdn_trans (pdiv_dvd _)) // (dvdn_gcdl, dvdn_gcdr). @@ -956,8 +956,7 @@ Proof. by rewrite ltn_neqAle part_gt0 andbT eq_sym p_part_eq1 negbK. Qed. Lemma primes_part pi n : primes n`_pi = filter (mem pi) (primes n). Proof. -have ltnT := ltn_trans. -case: (posnP n) => [-> | n_gt0]; first by rewrite partn0. +have ltnT := ltn_trans; have [->|n_gt0] := posnP n; first by rewrite partn0. apply: (eq_sorted_irr ltnT ltnn); rewrite ?(sorted_primes, sorted_filter) //. move=> p; rewrite mem_filter /= !mem_primes n_gt0 part_gt0 /=. apply/andP/and3P=> [[p_pr] | [pi_p p_pr dv_p_n]]. @@ -1194,15 +1193,14 @@ Lemma part_pnat_id pi n : pi.-nat n -> n`_pi = n. Proof. case/andP=> n_gt0 pi_n. rewrite -{2}(partnT n_gt0) /partn big_mkcond; apply: eq_bigr=> p _. -case: (posnP (logn p n)) => [-> |]; first by rewrite if_same. +have [->|] := posnP (logn p n); first by rewrite if_same. by rewrite logn_gt0 => /(allP pi_n)/= ->. Qed. Lemma part_p'nat pi n : pi^'.-nat n -> n`_pi = 1. Proof. case/andP=> n_gt0 pi'_n; apply: big1_seq => p /andP[pi_p _]. -case: (posnP (logn p n)) => [-> //|]. -by rewrite logn_gt0; move/(allP pi'_n); case/negP. +by have [-> //|] := posnP (logn p n); rewrite logn_gt0; case/(allP pi'_n)/negP. Qed. Lemma partn_eq1 pi n : n > 0 -> (n`_pi == 1) = pi^'.-nat n. diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 5b9d047..65cc122 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -887,9 +887,7 @@ Lemma all_rev a s : all a (rev s) = all a s. Proof. by rewrite !all_count count_rev size_rev. Qed. Lemma rev_nseq n x : rev (nseq n x) = nseq n x. -Proof. -by elim: n => [// | n IHn]; rewrite -{1}(addn1 n) nseq_addn rev_cat IHn. -Qed. +Proof. by elim: n => // n IHn; rewrite -{1}(addn1 n) nseq_addn rev_cat IHn. Qed. End Sequences. @@ -1736,14 +1734,14 @@ Proof. exact (can_inj rotrK). Qed. Lemma take_rev s : take n0 (rev s) = rev (drop (size s - n0) s). Proof. set m := _ - n0; rewrite -[s in LHS](cat_take_drop m) rev_cat take_cat. -rewrite size_rev size_drop -minnE minnC ltnNge geq_minl [in take m s]/m /minn. +rewrite size_rev size_drop -minnE minnC leq_min ltnn /m. by have [_|/eqnP->] := ltnP; rewrite ?subnn take0 cats0. Qed. Lemma drop_rev s : drop n0 (rev s) = rev (take (size s - n0) s). Proof. set m := _ - n0; rewrite -[s in LHS](cat_take_drop m) rev_cat drop_cat. -rewrite size_rev size_drop -minnE minnC ltnNge geq_minl /= /m /minn. +rewrite size_rev size_drop -minnE minnC leq_min ltnn /m. by have [_|/eqnP->] := ltnP; rewrite ?take0 // subnn drop0. Qed. @@ -2411,11 +2409,10 @@ Proof. by move/subnKC <-; rewrite addSnnS iota_add nth_cat size_iota ltnn subnn. Qed. -Lemma mem_iota m n i : (i \in iota m n) = (m <= i) && (i < m + n). +Lemma mem_iota m n i : (i \in iota m n) = (m <= i < m + n). Proof. elim: n m => [|n IHn] /= m; first by rewrite addn0 ltnNge andbN. -rewrite -addSnnS leq_eqVlt in_cons eq_sym. -by case: eqP => [->|_]; [rewrite leq_addr | apply: IHn]. +by rewrite in_cons IHn addnS ltnS; case: ltngtP => // ->; rewrite leq_addr. Qed. Lemma iota_uniq m n : uniq (iota m n). @@ -2423,17 +2420,16 @@ Proof. by elim: n m => //= n IHn m; rewrite mem_iota ltnn /=. Qed. Lemma take_iota k m n : take k (iota m n) = iota m (minn k n). Proof. -rewrite /minn; case: ltnP => [lt_k_n|le_n_k]. - by elim: k n lt_k_n m => [|k IHk] [|n]//= H m; rewrite IHk. +have [lt_k_n|le_n_k] := ltnP. + by elim: k n lt_k_n m => [|k IHk] [|n] //= H m; rewrite IHk. by apply: take_oversize; rewrite size_iota. Qed. Lemma drop_iota k m n : drop k (iota m n) = iota (m + k) (n - k). Proof. -by elim: k m n => [|k IHk] m [|n]//=; rewrite ?addn0// IHk addSn addnS subSS. +by elim: k m n => [|k IHk] m [|n] //=; rewrite ?addn0 // IHk addnS subSS. Qed. - (* Making a sequence of a specific length, using indexes to compute items. *) Section MakeSeq. diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index bccb968..7de4ad4 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -474,47 +474,6 @@ Arguments ltP {m n}. Lemma lt_irrelevance m n lt_mn1 lt_mn2 : lt_mn1 = lt_mn2 :> (m < n)%coq_nat. Proof. exact: (@le_irrelevance m.+1). Qed. -(* Comparison predicates. *) - -Variant leq_xor_gtn m n : bool -> bool -> Set := - | LeqNotGtn of m <= n : leq_xor_gtn m n true false - | GtnNotLeq of n < m : leq_xor_gtn m n false true. - -Lemma leqP m n : leq_xor_gtn m n (m <= n) (n < m). -Proof. -by rewrite ltnNge; case le_mn: (m <= n); constructor; rewrite // ltnNge le_mn. -Qed. - -Variant ltn_xor_geq m n : bool -> bool -> Set := - | LtnNotGeq of m < n : ltn_xor_geq m n false true - | GeqNotLtn of n <= m : ltn_xor_geq m n true false. - -Lemma ltnP m n : ltn_xor_geq m n (n <= m) (m < n). -Proof. by case: leqP; constructor. Qed. - -Variant eqn0_xor_gt0 n : bool -> bool -> Set := - | Eq0NotPos of n = 0 : eqn0_xor_gt0 n true false - | PosNotEq0 of n > 0 : eqn0_xor_gt0 n false true. - -Lemma posnP n : eqn0_xor_gt0 n (n == 0) (0 < n). -Proof. by case: n; constructor. Qed. - -Variant compare_nat m n : - bool -> bool -> bool -> bool -> bool -> bool -> Set := - | CompareNatLt of m < n : compare_nat m n false false false true false true - | CompareNatGt of m > n : compare_nat m n false false true false true false - | CompareNatEq of m = n : compare_nat m n true true true true false false. - -Lemma ltngtP m n : compare_nat m n (n == m) (m == n) (n <= m) - (m <= n) (n < m) (m < n). -Proof. -rewrite !ltn_neqAle [_ == n]eq_sym; case: ltnP => [nm|]. - by rewrite ltnW // gtn_eqF //; constructor. -rewrite leq_eqVlt; case: ltnP; rewrite ?(orbT, orbF) => //= lt_mn eq_nm. - by rewrite ltn_eqF //; constructor. -by rewrite eq_nm; constructor; apply/esym/eqP. -Qed. - (* Monotonicity lemmas *) Lemma leq_add2l p m n : (p + m <= p + n) = (m <= n). @@ -656,13 +615,6 @@ Proof. by move=> np pm; rewrite !leq_subRL // addnC. Qed. Lemma ltn_subCl m n p : n <= m -> p <= m -> (m - n < p) = (m - p < n). Proof. by move=> nm pm; rewrite !ltn_subLR // addnC. Qed. -(* Eliminating the idiom for structurally decreasing compare and subtract. *) -Lemma subn_if_gt T m n F (E : T) : - (if m.+1 - n is m'.+1 then F m' else E) = (if n <= m then F (m - n) else E). -Proof. -by case: leqP => [le_nm | /eqnP-> //]; rewrite -{1}(subnK le_nm) -addSn addnK. -Qed. - (* Max and min. *) Definition maxn m n := if m < n then n else m. @@ -673,10 +625,13 @@ Lemma max0n : left_id 0 maxn. Proof. by case. Qed. Lemma maxn0 : right_id 0 maxn. Proof. by []. Qed. Lemma maxnC : commutative maxn. -Proof. by move=> m n; rewrite /maxn; case ltngtP. Qed. +Proof. by rewrite /maxn; elim=> [|m ih] [] // n; rewrite !ltnS -!fun_if ih. Qed. Lemma maxnE m n : maxn m n = m + (n - m). -Proof. by rewrite /maxn addnC; case: leqP => [/eqnP->|/ltnW/subnK]. Qed. +Proof. +rewrite /maxn; elim: m n => [|m ih] [|n]; rewrite ?addn0 //. +by rewrite ltnS subSS addSn -ih; case: leq. +Qed. Lemma maxnAC : right_commutative maxn. Proof. by move=> m n p; rewrite !maxnE -!addnA !subnDA -!maxnE maxnC. Qed. @@ -727,10 +682,10 @@ Lemma min0n : left_zero 0 minn. Proof. by case. Qed. Lemma minn0 : right_zero 0 minn. Proof. by []. Qed. Lemma minnC : commutative minn. -Proof. by move=> m n; rewrite /minn; case ltngtP. Qed. +Proof. by rewrite /minn; elim=> [|m ih] [] // n; rewrite !ltnS -!fun_if ih. Qed. Lemma addn_min_max m n : minn m n + maxn m n = m + n. -Proof. by rewrite /minn /maxn; case: ltngtP => // [_|->] //; apply: addnC. Qed. +Proof. by rewrite /minn /maxn; case: (m < n) => //; exact: addnC. Qed. Lemma minnE m n : minn m n = m - (m - n). Proof. by rewrite -(subnDl n) -maxnE -addn_min_max addnK minnC. Qed. @@ -765,7 +720,8 @@ Lemma leq_min m n1 n2 : (m <= minn n1 n2) = (m <= n1) && (m <= n2). Proof. wlog le_n21: n1 n2 / n2 <= n1. by case/orP: (leq_total n2 n1) => ?; last rewrite minnC andbC; auto. -by rewrite /minn ltnNge le_n21 /= andbC; case: leqP => // /leq_trans->. +rewrite /minn ltnNge le_n21 /=; case le_m_n1: (m <= n1) => //=. +apply/contraFF: le_m_n1 => /leq_trans; exact. Qed. Lemma gtn_min m n1 n2 : (m > minn n1 n2) = (m > n1) || (m > n2). @@ -820,6 +776,61 @@ Qed. Lemma minn_maxr : right_distributive minn maxn. Proof. by move=> m n1 n2; rewrite !(minnC m) minn_maxl. Qed. +(* Comparison predicates. *) + +Variant leq_xor_gtn m n : nat -> nat -> nat -> nat -> bool -> bool -> Set := + | LeqNotGtn of m <= n : leq_xor_gtn m n m m n n true false + | GtnNotLeq of n < m : leq_xor_gtn m n n n m m false true. + +Lemma leqP m n : leq_xor_gtn m n (minn n m) (minn m n) (maxn n m) (maxn m n) + (m <= n) (n < m). +Proof. +rewrite (minnC m) /minn (maxnC m) /maxn ltnNge. +by case le_mn: (m <= n); constructor; rewrite //= ltnNge le_mn. +Qed. + +Variant ltn_xor_geq m n : nat -> nat -> nat -> nat -> bool -> bool -> Set := + | LtnNotGeq of m < n : ltn_xor_geq m n m m n n false true + | GeqNotLtn of n <= m : ltn_xor_geq m n n n m m true false. + +Lemma ltnP m n : ltn_xor_geq m n (minn n m) (minn m n) (maxn n m) (maxn m n) + (n <= m) (m < n). +Proof. by case: leqP; constructor. Qed. + +Variant eqn0_xor_gt0 n : bool -> bool -> Set := + | Eq0NotPos of n = 0 : eqn0_xor_gt0 n true false + | PosNotEq0 of n > 0 : eqn0_xor_gt0 n false true. + +Lemma posnP n : eqn0_xor_gt0 n (n == 0) (0 < n). +Proof. by case: n; constructor. Qed. + +Variant compare_nat m n : nat -> nat -> nat -> nat -> + bool -> bool -> bool -> bool -> bool -> bool -> Set := + | CompareNatLt of m < n : + compare_nat m n m m n n false false false true false true + | CompareNatGt of m > n : + compare_nat m n n n m m false false true false true false + | CompareNatEq of m = n : + compare_nat m n m m m m true true true true false false. + +Lemma ltngtP m n : + compare_nat m n (minn n m) (minn m n) (maxn n m) (maxn m n) + (n == m) (m == n) (n <= m) (m <= n) (n < m) (m < n). +Proof. +rewrite !ltn_neqAle [_ == n]eq_sym; have [mn|] := ltnP m n. + by rewrite ltnW // gtn_eqF //; constructor. +rewrite leq_eqVlt; case: ltnP; rewrite ?(orbT, orbF) => //= lt_nm eq_nm. + by rewrite ltn_eqF //; constructor. +by rewrite eq_nm (eqP eq_nm); constructor. +Qed. + +(* Eliminating the idiom for structurally decreasing compare and subtract. *) +Lemma subn_if_gt T m n F (E : T) : + (if m.+1 - n is m'.+1 then F m' else E) = (if n <= m then F (m - n) else E). +Proof. +by have [le_nm|/eqnP-> //] := leqP; rewrite -{1}(subnK le_nm) -addSn addnK. +Qed. + (* Getting a concrete value from an abstract existence proof. *) Section ExMinn. @@ -1872,3 +1883,38 @@ Lemma ltngtP m n : compare_nat m n (m <= n) (n <= m) (m < n) Proof. by case: ltngtP; constructor. Qed. End mc_1_9. + +Module mc_1_10. + +Variant leq_xor_gtn m n : bool -> bool -> Set := + | LeqNotGtn of m <= n : leq_xor_gtn m n true false + | GtnNotLeq of n < m : leq_xor_gtn m n false true. + +Lemma leqP m n : leq_xor_gtn m n (m <= n) (n < m). +Proof. by case: leqP; constructor. Qed. + +Variant ltn_xor_geq m n : bool -> bool -> Set := + | LtnNotGeq of m < n : ltn_xor_geq m n false true + | GeqNotLtn of n <= m : ltn_xor_geq m n true false. + +Lemma ltnP m n : ltn_xor_geq m n (n <= m) (m < n). +Proof. by case: ltnP; constructor. Qed. + +Variant eqn0_xor_gt0 n : bool -> bool -> Set := + | Eq0NotPos of n = 0 : eqn0_xor_gt0 n true false + | PosNotEq0 of n > 0 : eqn0_xor_gt0 n false true. + +Lemma posnP n : eqn0_xor_gt0 n (n == 0) (0 < n). +Proof. by case: n; constructor. Qed. + +Variant compare_nat m n : + bool -> bool -> bool -> bool -> bool -> bool -> Set := + | CompareNatLt of m < n : compare_nat m n false false false true false true + | CompareNatGt of m > n : compare_nat m n false false true false true false + | CompareNatEq of m = n : compare_nat m n true true true true false false. + +Lemma ltngtP m n : compare_nat m n (n == m) (m == n) (n <= m) + (m <= n) (n < m) (m < n). +Proof. by case: ltngtP; constructor. Qed. + +End mc_1_10. |