aboutsummaryrefslogtreecommitdiff
path: root/mathcomp
diff options
context:
space:
mode:
Diffstat (limited to 'mathcomp')
-rw-r--r--mathcomp/Make1
-rw-r--r--mathcomp/Make.test-suite1
-rw-r--r--mathcomp/algebra/fraction.v29
-rw-r--r--mathcomp/algebra/polydiv.v105
-rw-r--r--mathcomp/algebra/ssrnum.v25
-rw-r--r--mathcomp/fingroup/perm.v4
-rw-r--r--mathcomp/solvable/abelian.v4
-rw-r--r--mathcomp/solvable/extremal.v2
-rw-r--r--mathcomp/solvable/finmodule.v3
-rw-r--r--mathcomp/ssreflect/Make1
-rw-r--r--mathcomp/ssreflect/all_ssreflect.v1
-rw-r--r--mathcomp/ssreflect/bigop.v7
-rw-r--r--mathcomp/ssreflect/div.v16
-rw-r--r--mathcomp/ssreflect/fintype.v2
-rw-r--r--mathcomp/ssreflect/order.v48
-rw-r--r--mathcomp/ssreflect/prime.v10
-rw-r--r--mathcomp/ssreflect/seq.v74
-rw-r--r--mathcomp/ssreflect/ssrAC.v241
-rw-r--r--mathcomp/ssreflect/ssrnat.v152
-rw-r--r--mathcomp/test_suite/test_ssrAC.v100
20 files changed, 585 insertions, 241 deletions
diff --git a/mathcomp/Make b/mathcomp/Make
index 0a2c4a4..1d837c1 100644
--- a/mathcomp/Make
+++ b/mathcomp/Make
@@ -81,6 +81,7 @@ ssreflect/order.v
ssreflect/path.v
ssreflect/prime.v
ssreflect/seq.v
+ssreflect/ssrAC.v
ssreflect/ssrbool.v
ssreflect/ssreflect.v
ssreflect/ssrfun.v
diff --git a/mathcomp/Make.test-suite b/mathcomp/Make.test-suite
index bca6ed9..99d8289 100644
--- a/mathcomp/Make.test-suite
+++ b/mathcomp/Make.test-suite
@@ -1,4 +1,5 @@
test_suite/hierarchy_test.v
+test_suite/test_ssrAC.v
-I .
-R . mathcomp
diff --git a/mathcomp/algebra/fraction.v b/mathcomp/algebra/fraction.v
index b9aa3ca..41c6117 100644
--- a/mathcomp/algebra/fraction.v
+++ b/mathcomp/algebra/fraction.v
@@ -1,7 +1,7 @@
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq.
-From mathcomp Require Import choice tuple bigop ssralg poly polydiv.
+From mathcomp Require Import ssrAC choice tuple bigop ssralg poly polydiv.
From mathcomp Require Import generic_quotient.
(* This file builds the field of fraction of any integral domain. *)
@@ -157,13 +157,10 @@ Definition add := lift_op2 {fraction R} addf.
Lemma pi_add : {morph \pi : x y / addf x y >-> add x y}.
Proof.
-move=> x y; unlock add; apply/eqmodP; rewrite /= equivfE.
-rewrite /addf /= !numden_Ratio ?mulf_neq0 ?domP //.
-rewrite mulrDr mulrDl eq_sym; apply/eqP.
-rewrite !mulrA ![_ * \n__]mulrC !mulrA equivf_l.
-congr (_ + _); first by rewrite -mulrA mulrCA !mulrA.
-rewrite -!mulrA [X in _ * X]mulrCA !mulrA equivf_l.
-by rewrite mulrC !mulrA -mulrA mulrC mulrA.
+move=> x y; unlock add; apply/eqmodP; rewrite /= equivfE /addf /=.
+rewrite !numden_Ratio ?mulf_neq0 ?domP // mulrDr mulrDl; apply/eqP.
+symmetry; rewrite (AC (2*2)%AC (3*1*2*4)%AC) (AC (2*2)%AC (3*2*1*4)%AC)/=.
+by rewrite !equivf_l (ACl ((2*3)*(1*4))%AC) (ACl ((2*3)*(4*1))%AC)/=.
Qed.
Canonical pi_add_morph := PiMorph2 pi_add.
@@ -183,8 +180,7 @@ Lemma pi_mul : {morph \pi : x y / mulf x y >-> mul x y}.
Proof.
move=> x y; unlock mul; apply/eqmodP=> /=.
rewrite equivfE /= /addf /= !numden_Ratio ?mulf_neq0 ?domP //.
-rewrite mulrAC !mulrA -mulrA equivf_r -equivf_l.
-by rewrite mulrA ![_ * \d_y]mulrC !mulrA.
+by rewrite mulrACA !equivf_r mulrACA.
Qed.
Canonical pi_mul_morph := PiMorph2 pi_mul.
@@ -204,8 +200,8 @@ Canonical pi_inv_morph := PiMorph1 pi_inv.
Lemma addA : associative add.
Proof.
elim/quotW=> x; elim/quotW=> y; elim/quotW=> z; rewrite !piE.
-rewrite /addf /= !numden_Ratio ?mulf_neq0 ?domP // !mulrDl !mulrA !addrA.
-by congr (\pi (Ratio (_ + _ + _) _)); rewrite mulrAC.
+rewrite /addf /= !numden_Ratio ?mulf_neq0 ?domP // !mulrDl.
+by rewrite !mulrA !addrA ![_ * _ * \d_x]mulrAC.
Qed.
Lemma addC : commutative add.
@@ -252,13 +248,8 @@ Lemma mul_addl : left_distributive mul add.
Proof.
elim/quotW=> x; elim/quotW=> y; elim/quotW=> z; apply/eqP.
rewrite !piE /equivf /mulf /addf !numden_Ratio ?mulf_neq0 ?domP //; apply/eqP.
-rewrite !(mulrDr, mulrDl) !mulrA; congr (_ * _ + _ * _).
- rewrite ![_ * \n_z]mulrC -!mulrA; congr (_ * _).
- rewrite ![\d_y * _]mulrC !mulrA; congr (_ * _ * _).
- by rewrite [X in _ = X]mulrC mulrA.
-rewrite ![_ * \n_z]mulrC -!mulrA; congr (_ * _).
-rewrite ![\d_x * _]mulrC !mulrA; congr (_ * _ * _).
-by rewrite -mulrA mulrC [X in X * _] mulrC.
+rewrite !(mulrDr, mulrDl) (AC (3*(2*2))%AC (4*2*7*((1*3)*(6*5)))%AC)/=.
+by rewrite [X in _ + X](AC (3*(2*2))%AC (4*6*7*((1*3)*(2*5)))%AC)/=.
Qed.
Lemma nonzero1 : 1%:F != 0%:F :> type.
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/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index 78286cc..e1e5992 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -1,7 +1,7 @@
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
-From mathcomp Require Import div fintype path bigop order finset fingroup.
+From mathcomp Require Import ssrAC div fintype path bigop order finset fingroup.
From mathcomp Require Import ssralg poly.
(******************************************************************************)
@@ -3823,17 +3823,13 @@ Lemma oppr_min : {morph -%R : x y / min x y >-> max x y : R}.
Proof. by move=> x y; rewrite -[max _ _]opprK oppr_max !opprK. Qed.
Lemma addr_minl : @left_distributive R R +%R min.
-Proof.
-by move=> x y z; case: leP; case: leP => //; rewrite lter_add2; case: leP.
-Qed.
+Proof. by move=> x y z; case: (leP (_ + _)); rewrite lter_add2; case: leP. Qed.
Lemma addr_minr : @right_distributive R R +%R min.
Proof. by move=> x y z; rewrite !(addrC x) addr_minl. Qed.
Lemma addr_maxl : @left_distributive R R +%R max.
-Proof.
-by move=> x y z; case: leP; case: leP => //; rewrite lter_add2; case: leP.
-Qed.
+Proof. by move=> x y z; case: (leP (_ + _)); rewrite lter_add2; case: leP. Qed.
Lemma addr_maxr : @right_distributive R R +%R max.
Proof. by move=> x y z; rewrite !(addrC x) addr_maxl. Qed.
@@ -3841,7 +3837,7 @@ Proof. by move=> x y z; rewrite !(addrC x) addr_maxl. Qed.
Lemma minr_pmulr x y z : 0 <= x -> x * min y z = min (x * y) (x * z).
Proof.
case: sgrP=> // hx _; first by rewrite hx !mul0r meetxx.
-by case: leP; case: leP => //; rewrite lter_pmul2l //; case: leP.
+by case: (leP (_ * _)); rewrite lter_pmul2l //; case: leP.
Qed.
Lemma minr_nmulr x y z : x <= 0 -> x * min y z = max (x * y) (x * z).
@@ -4082,7 +4078,7 @@ have JE x : x^* = `|x|^+2 / x.
by apply: (canRL (mulfK _)) => //; rewrite mulrC -normCK.
move=> x; have [->|x_neq0] := eqVneq x 0; first by rewrite !rmorph0.
rewrite !JE normrM normfV exprMn normrX normr_id.
-rewrite invfM exprVn mulrA -[X in X * _]mulrA -invfM -exprMn.
+rewrite invfM exprVn (AC (2*2)%AC (1*(2*3)*4)%AC)/= -invfM -exprMn.
by rewrite divff ?mul1r ?invrK // !expf_eq0 normr_eq0 //.
Qed.
@@ -4331,12 +4327,11 @@ Lemma subC_rect x1 y1 x2 y2 :
(x1 + 'i * y1) - (x2 + 'i * y2) = x1 - x2 + 'i * (y1 - y2).
Proof. by rewrite oppC_rect addC_rect. Qed.
-Lemma mulC_rect x1 y1 x2 y2 :
- (x1 + 'i * y1) * (x2 + 'i * y2)
- = x1 * x2 - y1 * y2 + 'i * (x1 * y2 + x2 * y1).
+Lemma mulC_rect x1 y1 x2 y2 : (x1 + 'i * y1) * (x2 + 'i * y2) =
+ x1 * x2 - y1 * y2 + 'i * (x1 * y2 + x2 * y1).
Proof.
-rewrite mulrDl !mulrDr mulrCA -!addrA mulrAC -mulrA; congr (_ + _).
-by rewrite mulrACA -expr2 sqrCi mulN1r addrA addrC.
+rewrite mulrDl !mulrDr (AC (2*2)%AC (1*4*(2*3))%AC)/= mulrACA.
+by rewrite -expr2 sqrCi mulN1r -!mulrA [_ * ('i * _)]mulrCA [_ * y1]mulrC.
Qed.
Lemma normC2_rect :
@@ -4653,7 +4648,7 @@ have{lin_xy} def2xy: `|x| * `|y| *+ 2 = x * y ^* + y * x ^*.
have def_xy: x * y^* = y * x^*.
apply/eqP; rewrite -subr_eq0 -[_ == 0](@expf_eq0 _ _ 2).
rewrite (canRL (subrK _) (subr_sqrDB _ _)) opprK -def2xy exprMn_n exprMn.
- by rewrite mulrN mulrAC mulrA -mulrA mulrACA -!normCK mulNrn addNr.
+ by rewrite mulrN (@GRing.mul C).[AC (2*2)%AC (1*4*(3*2))%AC] -!normCK mulNrn addNr.
have{def_xy def2xy} def_yx: `|y * x| = y * x^*.
by apply: (mulIf nz2); rewrite !mulr_natr mulrC normrM def2xy def_xy.
rewrite -{1}(divfK nz_x y) invC_norm mulrCA -{}def_yx !normrM invfM.
diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v
index 34f230e..eb5e028 100644
--- a/mathcomp/fingroup/perm.v
+++ b/mathcomp/fingroup/perm.v
@@ -576,7 +576,3 @@ Qed.
End LiftPerm.
Prenex Implicits lift_perm lift_permK.
-
-Notation tuple_perm_eqP :=
- (deprecate tuple_perm_eqP tuple_permP) (only parsing).
-
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/solvable/finmodule.v b/mathcomp/solvable/finmodule.v
index 05c070e..7920a68 100644
--- a/mathcomp/solvable/finmodule.v
+++ b/mathcomp/solvable/finmodule.v
@@ -38,7 +38,8 @@ From mathcomp Require Import cyclic.
(* rcosets_cycle_partition), and for any transversal X of HG :* <[g]> the *)
(* function r mapping x : gT to rcosets (H :* x) <[g]> is (constructively) a *)
(* bijection from X to the <[g]>-orbit partition of HG, and Lemma *)
-(* transfer_pcycle_def gives a simplified expansion of the transfer morphism. *)
+(* transfer_cycle_expansion gives a simplified expansion of the transfer *)
+(* morphism. *)
(******************************************************************************)
Set Implicit Arguments.
diff --git a/mathcomp/ssreflect/Make b/mathcomp/ssreflect/Make
index 108f545..f8c640d 100644
--- a/mathcomp/ssreflect/Make
+++ b/mathcomp/ssreflect/Make
@@ -1,6 +1,7 @@
all_ssreflect.v
eqtype.v
seq.v
+ssrAC.v
ssrbool.v
ssreflect.v
ssrfun.v
diff --git a/mathcomp/ssreflect/all_ssreflect.v b/mathcomp/ssreflect/all_ssreflect.v
index 318d5ef..a73f073 100644
--- a/mathcomp/ssreflect/all_ssreflect.v
+++ b/mathcomp/ssreflect/all_ssreflect.v
@@ -17,3 +17,4 @@ Require Export finset.
Require Export order.
Require Export binomial.
Require Export generic_quotient.
+Require Export ssrAC.
diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v
index 698f2e7..601dfb3 100644
--- a/mathcomp/ssreflect/bigop.v
+++ b/mathcomp/ssreflect/bigop.v
@@ -1937,13 +1937,6 @@ Lemma biggcdn_inf (I : finType) i0 (P : pred I) F m :
Proof. by move=> Pi0; apply: dvdn_trans; rewrite (bigD1 i0) ?dvdn_gcdl. Qed.
Arguments biggcdn_inf [I] i0 [P F m].
-Notation "@ 'eq_big_perm'" :=
- (deprecate eq_big_perm perm_big) (at level 10, only parsing).
-
-Notation eq_big_perm :=
- ((fun R idx op I r1 P F r2 => @eq_big_perm R idx op I r1 r2 P F)
- _ _ _ _ _ _ _) (only parsing).
-
Notation filter_index_enum :=
((fun _ => @deprecated_filter_index_enum _)
(deprecate filter_index_enum big_enumP)) (only parsing).
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 14faf57..432c30f 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 259484a..38ee13d 100644
--- a/mathcomp/ssreflect/order.v
+++ b/mathcomp/ssreflect/order.v
@@ -1216,35 +1216,35 @@ Context {T : latticeType}.
Definition meet : T -> T -> T := Lattice.meet (Lattice.class T).
Definition join : T -> T -> T := Lattice.join (Lattice.class T).
-Variant lel_xor_gt (x y : T) : bool -> bool -> T -> T -> T -> T -> Set :=
- | LelNotGt of x <= y : lel_xor_gt x y true false x x y y
- | GtlNotLe of y < x : lel_xor_gt x y false true y y x x.
+Variant lel_xor_gt (x y : T) : T -> T -> T -> T -> bool -> bool -> Set :=
+ | LelNotGt of x <= y : lel_xor_gt x y x x y y true false
+ | GtlNotLe of y < x : lel_xor_gt x y y y x x false true.
-Variant ltl_xor_ge (x y : T) : bool -> bool -> T -> T -> T -> T -> Set :=
- | LtlNotGe of x < y : ltl_xor_ge x y false true x x y y
- | GelNotLt of y <= x : ltl_xor_ge x y true false y y x x.
+Variant ltl_xor_ge (x y : T) : T -> T -> T -> T -> bool -> bool -> Set :=
+ | LtlNotGe of x < y : ltl_xor_ge x y x x y y false true
+ | GelNotLt of y <= x : ltl_xor_ge x y y y x x true false.
Variant comparel (x y : T) :
- bool -> bool -> bool -> bool -> bool -> bool -> T -> T -> T -> T -> Set :=
+ T -> T -> T -> T -> bool -> bool -> bool -> bool -> bool -> bool -> Set :=
| ComparelLt of x < y : comparel x y
- false false false true false true x x y y
+ x x y y false false false true false true
| ComparelGt of y < x : comparel x y
- false false true false true false y y x x
+ y y x x false false true false true false
| ComparelEq of x = y : comparel x y
- true true true true false false x x x x.
+ x x x x true true true true false false.
Variant incomparel (x y : T) :
- bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool ->
- T -> T -> T -> T -> Set :=
+ T -> T -> T -> T ->
+ bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> Set :=
| InComparelLt of x < y : incomparel x y
- false false false true false true true true x x y y
+ x x y y false false false true false true true true
| InComparelGt of y < x : incomparel x y
- false false true false true false true true y y x x
+ y y x x false false true false true false true true
| InComparel of x >< y : incomparel x y
- false false false false false false false false
(meet x y) (meet x y) (join x y) (join x y)
+ false false false false false false false false
| InComparelEq of x = y : incomparel x y
- true true true true false false true true x x x x.
+ x x x x true true true true false false true true.
End LatticeDef.
@@ -3218,8 +3218,8 @@ Lemma leU2 x y z t : x <= z -> y <= t -> x `|` y <= z `|` t.
Proof. exact: (@leI2 _ [latticeType of L^d]). Qed.
Lemma lcomparableP x y : incomparel x y
- (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y)
- (y >=< x) (x >=< y) (y `&` x) (x `&` y) (y `|` x) (x `|` y).
+ (y `&` x) (x `&` y) (y `|` x) (x `|` y)
+ (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y) (y >=< x) (x >=< y).
Proof.
by case: (comparableP x) => [hxy|hxy|hxy|->]; do 1?have hxy' := ltW hxy;
rewrite ?(meetxx, joinxx, meetC y, joinC y)
@@ -3228,16 +3228,16 @@ by case: (comparableP x) => [hxy|hxy|hxy|->]; do 1?have hxy' := ltW hxy;
Qed.
Lemma lcomparable_ltgtP x y : x >=< y ->
- comparel x y (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y)
- (y `&` x) (x `&` y) (y `|` x) (x `|` y).
+ comparel x y (y `&` x) (x `&` y) (y `|` x) (x `|` y)
+ (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y).
Proof. by case: (lcomparableP x) => // *; constructor. Qed.
Lemma lcomparable_leP x y : x >=< y ->
- lel_xor_gt x y (x <= y) (y < x) (y `&` x) (x `&` y) (y `|` x) (x `|` y).
+ lel_xor_gt x y (y `&` x) (x `&` y) (y `|` x) (x `|` y) (x <= y) (y < x).
Proof. by move/lcomparable_ltgtP => [/ltW xy|xy|->]; constructor. Qed.
Lemma lcomparable_ltP x y : x >=< y ->
- ltl_xor_ge x y (y <= x) (x < y) (y `&` x) (x `&` y) (y `|` x) (x `|` y).
+ ltl_xor_ge x y (y `&` x) (x `&` y) (y `|` x) (x `|` y) (y <= x) (x < y).
Proof. by move=> /lcomparable_ltgtP [xy|/ltW xy|->]; constructor. Qed.
End LatticeTheoryJoin.
@@ -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 33ea698..02d3cda 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..6dc739e 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -530,6 +530,9 @@ Proof. by elim: s => //= x s IHs; case a_x: (a x). Qed.
Lemma before_find s i : i < find s -> a (nth s i) = false.
Proof. by elim: s i => //= x s IHs; case: ifP => // a'x [|i] // /(IHs i). Qed.
+Lemma hasNfind s : ~~ has s -> find s = size s.
+Proof. by rewrite has_find; case: ltngtP (find_size s). Qed.
+
Lemma filter_cat s1 s2 : filter (s1 ++ s2) = filter s1 ++ filter s2.
Proof. by elim: s1 => //= x s1 ->; case (a x). Qed.
@@ -887,9 +890,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.
@@ -929,6 +930,23 @@ Proof.
by move=> Pnil Pcons; elim=> [|x s IHs] [|y t] //= [eq_sz]; apply/Pcons/IHs.
Qed.
+Section FindSpec.
+Variable (T : Type) (a : {pred T}) (s : seq T).
+
+Variant find_spec : bool -> nat -> Type :=
+| NotFound of ~~ has a s : find_spec false (size s)
+| Found (i : nat) of i < size s & (forall x0, a (nth x0 s i)) &
+ (forall x0 j, j < i -> a (nth x0 s j) = false) : find_spec true i.
+
+Lemma findP : find_spec (has a s) (find a s).
+Proof.
+have [a_s|aNs] := boolP (has a s); last by rewrite hasNfind//; constructor.
+by constructor=> [|x0|x0]; rewrite -?has_find ?nth_find//; apply: before_find.
+Qed.
+
+End FindSpec.
+Arguments findP {T}.
+
Section RotRcons.
Variable T : Type.
@@ -1304,6 +1322,9 @@ Proof. by rewrite /index find_size. Qed.
Lemma index_mem x s : (index x s < size s) = (x \in s).
Proof. by rewrite -has_pred1 has_find. Qed.
+Lemma memNindex x s : x \notin s -> index x s = size s.
+Proof. by rewrite -has_pred1 => /hasNfind. Qed.
+
Lemma nth_index x s : x \in s -> nth s (index x s) = x.
Proof. by rewrite -has_pred1 => /(nth_find x0)/eqP. Qed.
@@ -1736,14 +1757,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 +2432,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 +2443,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.
@@ -2499,6 +2518,9 @@ Variables (R : Type) (f : T2 -> R -> R) (z0 : R).
Lemma foldr_cat s1 s2 : foldr f z0 (s1 ++ s2) = foldr f (foldr f z0 s2) s1.
Proof. by elim: s1 => //= x s1 ->. Qed.
+Lemma foldr_rcons s x : foldr f z0 (rcons s x) = foldr f (f x z0) s.
+Proof. by rewrite -cats1 foldr_cat. Qed.
+
Lemma foldr_map s : foldr f z0 (map h s) = foldr (fun x z => f (h x) z) z0 s.
Proof. by elim: s => //= x s ->. Qed.
@@ -2553,6 +2575,9 @@ Proof.
by rewrite -(revK (s1 ++ s2)) foldl_rev rev_cat foldr_cat -!foldl_rev !revK.
Qed.
+Lemma foldl_rcons z s x : foldl z (rcons s x) = f (foldl z s) x.
+Proof. by rewrite -cats1 foldl_cat. Qed.
+
End FoldLeft.
Section Scan.
@@ -2583,9 +2608,17 @@ Lemma scanl_cat x s1 s2 :
scanl x (s1 ++ s2) = scanl x s1 ++ scanl (foldl g x s1) s2.
Proof. by elim: s1 x => //= y s1 IHs1 x; rewrite IHs1. Qed.
+Lemma scanl_rcons x s1 y :
+ scanl x (rcons s1 y) = rcons (scanl x s1) (foldl g x (rcons s1 y)).
+Proof. by rewrite -!cats1 scanl_cat foldl_cat. Qed.
+
+Lemma nth_cons_scanl s n : n <= size s ->
+ forall x, nth x1 (x :: scanl x s) n = foldl g x (take n s).
+Proof. by elim: s n => [|y s IHs] [|n] Hn x //=; rewrite IHs. Qed.
+
Lemma nth_scanl s n : n < size s ->
forall x, nth x1 (scanl x s) n = foldl g x (take n.+1 s).
-Proof. by elim: s n => [|y s IHs] [|n] Hn x //=; rewrite ?take0 ?IHs. Qed.
+Proof. by move=> n_lt x; rewrite -nth_cons_scanl. Qed.
Lemma scanlK :
(forall x, cancel (g x) (f x)) -> forall x, cancel (scanl x) (pairmap x).
@@ -3393,21 +3426,6 @@ Notation "[ '<->' P0 ; P1 ; .. ; Pn ]" :=
Ltac tfae := do !apply: AllIffConj.
(* Temporary backward compatibility. *)
-Notation perm_eqP := (deprecate perm_eqP permP) (only parsing).
-Notation perm_eqlP := (deprecate perm_eqlP permPl) (only parsing).
-Notation perm_eqrP := (deprecate perm_eqrP permPr) (only parsing).
-Notation perm_eqlE := (deprecate perm_eqlE permEl _ _ _) (only parsing).
-Notation perm_eq_refl := (deprecate perm_eq_refl perm_refl _) (only parsing).
-Notation perm_eq_sym := (deprecate perm_eq_sym perm_sym _) (only parsing).
-Notation "@ 'perm_eq_trans'" := (deprecate perm_eq_trans perm_trans)
- (at level 10, only parsing).
-Notation perm_eq_trans := (@perm_eq_trans _ _ _ _) (only parsing).
-Notation perm_eq_size := (deprecate perm_eq_size perm_size _ _ _)
- (only parsing).
-Notation perm_eq_mem := (deprecate perm_eq_mem perm_mem _ _ _)
- (only parsing).
-Notation perm_eq_uniq := (deprecate perm_eq_uniq perm_uniq _ _ _)
- (only parsing).
Notation perm_eq_rev := (deprecate perm_eq_rev perm_rev _)
(only parsing).
Notation perm_eq_flatten := (deprecate perm_eq_flatten perm_flatten _ _ _)
diff --git a/mathcomp/ssreflect/ssrAC.v b/mathcomp/ssreflect/ssrAC.v
new file mode 100644
index 0000000..8483f71
--- /dev/null
+++ b/mathcomp/ssreflect/ssrAC.v
@@ -0,0 +1,241 @@
+Require Import BinPos BinNat.
+From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq bigop.
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+(************************************************************************)
+(* Small Scale Rewriting using Associatity and Commutativity *)
+(* *)
+(* Rewriting with AC (not modulo AC), using a small scale command. *)
+(* Replaces opA, opC, opAC, opCA, ... and any combinations of them *)
+(* *)
+(* Usage : *)
+(* rewrite [pattern](AC patternshape reordering) *)
+(* rewrite [pattern](ACl reordering) *)
+(* rewrite [pattern](ACof reordering reordering) *)
+(* rewrite [pattern]op.[AC patternshape reordering] *)
+(* rewrite [pattern]op.[ACl reordering] *)
+(* rewrite [pattern]op.[ACof reordering reordering] *)
+(* *)
+(* - if op is specified, the rule is specialized to op *)
+(* otherwise, the head symbol is a generic comm_law *)
+(* and the rewrite might be less efficient *)
+(* NOTE because of a bug in Coq's notations coq/coq#8190 *)
+(* op must not contain any hole. *)
+(* *%R.[AC p s] currently does not work because of that *)
+(* (@GRing.mul R).[AC p s] must be used instead *)
+(* *)
+(* - pattern is optional, as usual, but must be used to select the *)
+(* appropriate operator in case of ambiguity such an operator must *)
+(* have a canonical Monoid.com_law structure *)
+(* (additions, multiplications, conjuction and disjunction do) *)
+(* *)
+(* - patternshape is expressed using the syntax *)
+(* p := n | p * p' *)
+(* where "*" is purely formal *)
+(* and n > 0 is number of left associated symbols *)
+(* examples of pattern shapes: *)
+(* + 4 represents (n * m * p * q) *)
+(* + (1*2) represents (n * (m * p)) *)
+(* *)
+(* - reordering is expressed using the syntax *)
+(* s := n | s * s' *)
+(* where "*" is purely formal and n > 0 is the position in the LHS *)
+(* positions start at 1 ! *)
+(* *)
+(* If the ACl variant is used, the patternshape defaults to the *)
+(* pattern fully associated to the left i.e. n i.e (x * y * ...) *)
+(* *)
+(* Examples of reorderings: *)
+(* - ACl ((1*2)*3) is the identity (and will fail with error message) *)
+(* - opAC == op.[ACl (1*3)*2] == op.[AC 3 ((1*3)*2)] *)
+(* - opCA == op.[AC (2*1) (1*2*3)] *)
+(* - opACA == op.[AC (2*2) ((1*3)*(2*4))] *)
+(* - rewrite opAC -opA == rewrite op.[ACl 1*(3*2)] *)
+(* ... *)
+(************************************************************************)
+
+
+Delimit Scope AC_scope with AC.
+
+Definition change_type ty ty' (x : ty) (strategy : ty = ty') : ty' :=
+ ecast ty ty strategy x.
+Notation simplrefl := (ltac: (simpl; reflexivity)).
+Notation cbvrefl := (ltac: (cbv; reflexivity)).
+Notation vmrefl := (ltac: (vm_compute; reflexivity)).
+
+Module AC.
+
+Canonical positive_eqType := EqType positive
+ (EqMixin (fun _ _ => equivP idP (Pos.eqb_eq _ _))).
+(* Should be replaced by (EqMixin Pos.eqb_spec) for coq >= 8.7 *)
+
+Inductive syntax := Leaf of positive | Op of syntax & syntax.
+Coercion serial := (fix loop (acc : seq positive) (s : syntax) :=
+ match s with
+ | Leaf n => n :: acc
+ | Op s s' => (loop^~ s (loop^~ s' acc))
+ end) [::].
+
+Lemma serial_Op s1 s2 : Op s1 s2 = s1 ++ s2 :> seq _.
+Proof.
+rewrite /serial; set loop := (X in X [::]); rewrite -/loop.
+elim: s1 (loop [::] s2) => [n|s11 IHs1 s12 IHs2] //= l.
+by rewrite IHs1 [in RHS]IHs1 IHs2 catA.
+Qed.
+
+Definition Leaf_of_nat n := Leaf ((pos_of_nat n n) - 1)%positive.
+
+Module Import Syntax.
+Bind Scope AC_scope with syntax.
+Coercion Leaf : positive >-> syntax.
+Coercion Leaf_of_nat : nat >-> syntax.
+Notation "1" := 1%positive : AC_scope.
+Notation "x * y" := (Op x%AC y%AC) : AC_scope.
+End Syntax.
+
+Definition pattern (s : syntax) := ((fix loop n s :=
+ match s with
+ | Leaf 1%positive => (Leaf n, Pos.succ n)
+ | Leaf m => Pos.iter (fun oi => (Op oi.1 (Leaf oi.2), Pos.succ oi.2))
+ (Leaf n, Pos.succ n) (m - 1)%positive
+ | Op s s' => let: (p, n') := loop n s in
+ let: (p', n'') := loop n' s' in
+ (Op p p', n'')
+ end) 1%positive s).1.
+
+Section eval.
+Variables (T : Type) (idx : T) (op : T -> T -> T).
+Inductive env := Empty | ENode of T & env & env.
+Definition pos := fix loop (e : env) p {struct e} :=
+ match e, p with
+ | ENode t _ _, 1%positive => t
+ | ENode t e _, (p~0)%positive => loop e p
+ | ENode t _ e, (p~1)%positive => loop e p
+ | _, _ => idx
+end.
+
+Definition set_pos (f : T -> T) := fix loop e p {struct p} :=
+ match e, p with
+ | ENode t e e', 1%positive => ENode (f t) e e'
+ | ENode t e e', (p~0)%positive => ENode t (loop e p) e'
+ | ENode t e e', (p~1)%positive => ENode t e (loop e' p)
+ | Empty, 1%positive => ENode (f idx) Empty Empty
+ | Empty, (p~0)%positive => ENode idx (loop Empty p) Empty
+ | Empty, (p~1)%positive => ENode idx Empty (loop Empty p)
+ end.
+
+Lemma pos_set_pos (f : T -> T) e (p p' : positive) :
+ pos (set_pos f e p) p' = if p == p' then f (pos e p) else pos e p'.
+Proof. by elim: p e p' => [p IHp|p IHp|] [|???] [?|?|]//=; rewrite IHp. Qed.
+
+Fixpoint unzip z (e : env) : env := match z with
+ | [::] => e
+ | (x, inl e') :: z' => unzip z' (ENode x e' e)
+ | (x, inr e') :: z' => unzip z' (ENode x e e')
+end.
+
+Definition set_pos_trec (f : T -> T) := fix loop z e p {struct p} :=
+ match e, p with
+ | ENode t e e', 1%positive => unzip z (ENode (f t) e e')
+ | ENode t e e', (p~0)%positive => loop ((t, inr e') :: z) e p
+ | ENode t e e', (p~1)%positive => loop ((t, inl e) :: z) e' p
+ | Empty, 1%positive => unzip z (ENode (f idx) Empty Empty)
+ | Empty, (p~0)%positive => loop ((idx, (inr Empty)) :: z) Empty p
+ | Empty, (p~1)%positive => loop ((idx, (inl Empty)) :: z) Empty p
+ end.
+
+Lemma set_pos_trecE f z e p : set_pos_trec f z e p = unzip z (set_pos f e p).
+Proof. by elim: p e z => [p IHp|p IHp|] [|???] [|[??]?] //=; rewrite ?IHp. Qed.
+
+Definition eval (e : env) := fix loop (s : syntax) :=
+match s with
+ | Leaf n => pos e n
+ | Op s s' => op (loop s) (loop s')
+end.
+End eval.
+Arguments Empty {T}.
+
+Definition content := (fix loop (acc : env N) s :=
+ match s with
+ | Leaf n => set_pos_trec 0%num N.succ [::] acc n
+ | Op s s' => loop (loop acc s') s
+ end) Empty.
+
+Lemma count_memE x (t : syntax) : count_mem x t = pos 0%num (content t) x.
+Proof.
+rewrite /content; set loop := (X in X Empty); rewrite -/loop.
+rewrite -[LHS]addn0; have <- : pos 0%num Empty x = 0 :> nat by elim: x.
+elim: t Empty => [n|s IHs s' IHs'] e //=; last first.
+ by rewrite serial_Op count_cat -addnA IHs' IHs.
+rewrite ?addn0 set_pos_trecE pos_set_pos; case: (altP eqP) => [->|] //=.
+by rewrite -N.add_1_l nat_of_add_bin //=.
+Qed.
+
+Definition cforall N T : env N -> (env T -> Type) -> Type := env_rect (@^~ Empty)
+ (fun _ e IHe e' IHe' R => forall x, IHe (fun xe => IHe' (R \o ENode x xe))).
+
+Lemma cforallP N T R : (forall e : env T, R e) -> forall (e : env N), cforall e R.
+Proof.
+move=> Re e; elim: e R Re => [|? e /= IHe e' IHe' ?? x] //=.
+by apply: IHe => ?; apply: IHe' => /=.
+Qed.
+
+Section eq_eval.
+Variables (T : Type) (idx : T) (op : Monoid.com_law idx).
+
+Lemma proof (p s : syntax) : content p = content s ->
+ forall env, eval idx op env p = eval idx op env s.
+Proof.
+suff evalE env t : eval idx op env t = \big[op/idx]_(i <- t) (pos idx env i).
+ move=> cps e; rewrite !evalE; apply: perm_big.
+ by apply/allP => x _ /=; rewrite !count_memE cps.
+elim: t => //= [n|t -> t' ->]; last by rewrite serial_Op big_cat.
+by rewrite big_cons big_nil Monoid.mulm1.
+Qed.
+
+Definition direct p s ps := cforallP (@proof p s ps) (content p).
+
+End eq_eval.
+
+Module Exports.
+Export AC.Syntax.
+End Exports.
+End AC.
+Export AC.Exports.
+
+Notation AC_check_pattern :=
+ (ltac: (match goal with
+ |- AC.content ?pat = AC.content ?ord =>
+ let pat' := fresh "pat" in let pat' := eval compute in pat in
+ tryif unify pat' ord then
+ fail 1 "AC: equality between" pat
+ "and" ord "is trivial, cannot progress"
+ else tryif vm_compute; reflexivity then idtac
+ else fail 2 "AC: mismatch between shape" pat "=" pat' "and reordering" ord
+ | |- ?G => fail 3 "AC: no pattern to check" G
+ end)).
+
+Notation opACof law p s :=
+((fun T idx op assoc lid rid comm => (change_type (@AC.direct T idx
+ (@Monoid.ComLaw _ _ (@Monoid.Law _ idx op assoc lid rid) comm)
+ p%AC s%AC AC_check_pattern) cbvrefl)) _ _ law
+(Monoid.mulmA _) (Monoid.mul1m _) (Monoid.mulm1 _) (Monoid.mulmC _)).
+
+Notation opAC op p s := (opACof op (AC.pattern p%AC) s%AC).
+Notation opACl op s := (opAC op (AC.Leaf_of_nat (size (AC.serial s%AC))) s%AC).
+
+Notation "op .[ 'ACof' p s ]" := (opACof op p s)
+ (at level 2, p at level 1, left associativity).
+Notation "op .[ 'AC' p s ]" := (opAC op p s)
+ (at level 2, p at level 1, left associativity).
+Notation "op .[ 'ACl' s ]" := (opACl op s)
+ (at level 2, left associativity).
+
+Notation AC_strategy :=
+ (ltac: (cbv -[Monoid.com_operator Monoid.operator]; reflexivity)).
+Notation ACof p s := (change_type
+ (@AC.direct _ _ _ p%AC s%AC AC_check_pattern) AC_strategy).
+Notation AC p s := (ACof (AC.pattern p%AC) s%AC).
+Notation ACl s := (AC (AC.Leaf_of_nat (size (AC.serial s%AC))) s%AC).
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index 8ddfccb..fb6a030 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.
diff --git a/mathcomp/test_suite/test_ssrAC.v b/mathcomp/test_suite/test_ssrAC.v
new file mode 100644
index 0000000..92dd101
--- /dev/null
+++ b/mathcomp/test_suite/test_ssrAC.v
@@ -0,0 +1,100 @@
+From mathcomp Require Import all_ssreflect ssralg.
+
+Section Tests.
+Lemma test_orb (a b c d : bool) : (a || b) || (c || d) = (a || c) || (b || d).
+Proof. time by rewrite orbACA. Restart.
+Proof. time by rewrite (AC (2*2) ((1*3)*(2*4))). Restart.
+Proof. time by rewrite orb.[AC (2*2) ((1*3)*(2*4))]. Qed.
+
+Lemma test_addn (a b c d : nat) : a + b + c + d = a + c + b + d.
+Proof. time by rewrite -addnA addnAC addnA addnAC. Restart.
+Proof. time by rewrite (ACl (1*3*2*4)). Restart.
+Proof. time by rewrite addn.[ACl 1*3*2*4]. Qed.
+
+Lemma test_addr (R : comRingType) (a b c d : R) : (a + b + c + d = a + c + b + d)%R.
+Proof. time by rewrite -GRing.addrA GRing.addrAC GRing.addrA GRing.addrAC. Restart.
+Proof. time by rewrite (ACl (1*3*2*4)). Restart.
+Proof. time by rewrite (@GRing.add R).[ACl 1*3*2*4]. Qed.
+
+Local Open Scope ring_scope.
+Import GRing.Theory.
+
+Lemma test_mulr (R : comRingType) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : R)
+ (x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 : R) :
+ (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+ (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19) *
+ (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+ (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19) =
+ (x0 * x2 * x4 * x9) * (x1 * x3 * x5 * x7) * x6 * x8 *
+ (x10 * x12 * x14 * x19) * (x11 * x13 * x15 * x17) * x16 * x18 * (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+ (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19)
+ *(x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+ (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19) *
+ (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *(x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+ (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19) *
+ (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) * (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+ (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19)
+ *(x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+ (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19) *
+ (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *(x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+ (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19) *
+ (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) * (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+ (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19)
+ *(x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+ (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19) *
+ (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *(x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+ (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19) *
+ (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+ (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19) *
+ (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) * (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+ (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19)
+ *(x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+ (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19) *
+ (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *(x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+ (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19) *
+ (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) * (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+ (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19)
+ *(x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+ (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19) *
+ (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *(x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+ (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19) *
+ (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9)*
+ (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19) *
+ (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) * (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+ (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19)
+ *(x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+ (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19) *
+ (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *(x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+ (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19) *
+ (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) * (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+ (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19)
+ *(x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+ (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19) *
+ (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *(x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+ (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19) *
+ (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) .
+Proof.
+pose s := ((2 * 4 * 9 * 1 * 3 * 5 * 7 * 6 * 8 * 20 * 21 * 22 * 23) * 25 * 26 * 27 * 28
+ * (29 * 30 * 31) * 32 * 33 * 34 * 35 * 36 * 37 * 38 * 39 * 40 * 41
+ * (10 * 12 * 14 * 19 * 11 * 13 * 15 * 17 * 16 * 18 * 24)
+ * (42 * 43 * 44 * 45 * 46 * 47 * 48 * 49) * 50
+ * 52 * 53 * 54 * 55 * 56 * 57 * 58 * 59 * 51* 60
+ * 62 * 63 * 64 * 65 * 66 * 67 * 68 * 69 * 61* 70
+ * 72 * 73 * 74 * 75 * 76 * 77 * 78 * 79 * 71 * 80
+ * 82 * 83 * 84 * 85 * 86 * 87 * 88 * 89 * 81* 90
+ * 92 * 93 * 94 * 95 * 96 * 97 * 98 * 99 * 91 * 100 *
+((102 * 104 * 109 * 101 * 103 * 105 * 107 * 106 * 108 * 120 * 121 * 122 * 123) * 125 * 126 * 127 * 128
+ * (129 * 130 * 131) * 132 * 133 * 134 * 135 * 136 * 137 * 138 * 139 * 140 * 141
+ * (110 * 112 * 114 * 119 * 111 * 113 * 115 * 117 * 116 * 118 * 124)
+ * (142 * 143 * 144 * 145 * 146 * 147 * 148 * 149) * 150
+ * 152 * 153 * 154 * 155 * 156 * 157 * 158 * 159 * 151* 160
+ * 162 * 163 * 164 * 165 * 166 * 167 * 168 * 169 * 161* 170
+ * 172 * 173 * 174 * 175 * 176 * 177 * 178 * 179 * 171 * 180
+ * 182 * 183 * 184 * 185 * 186 * 187 * 188 * 189 * 181* 190
+ * 192 * 193 * 194 * 195 * 196 * 197 * 198 * 199 * 191)
+
+)%AC.
+time have := (@GRing.mul R).[ACl s].
+time rewrite (@GRing.mul R).[ACl s].
+Abort.
+End Tests. \ No newline at end of file
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 18:41:23 +0000