Merge pull request #607 from pi8027/distr-suffixes

Switch from long suffixes to short suffixes

1 files changed, 42 insertions, 21 deletions

diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v
index a33788d..e9e9c45 100644
--- a/mathcomp/algebra/poly.v
+++ b/mathcomp/algebra/poly.v
@@ -428,26 +428,25 @@ Lemma coef_sum I (r : seq I) (P : pred I) (F : I -> {poly R}) k :
   (\sum_(i <- r | P i) F i)`_k = \sum_(i <- r | P i) (F i)`_k.
 Proof. exact: (raddf_sum (coefp_additive k)). Qed.
 
-Lemma polyC_add : {morph polyC : a b / a + b}.
+Lemma polyCD : {morph polyC : a b / a + b}.
 Proof. by move=> a b; apply/polyP=> [[|i]]; rewrite coefD !coefC ?addr0. Qed.
 
-Lemma polyC_opp : {morph polyC : c / - c}.
+Lemma polyCN : {morph polyC : c / - c}.
 Proof. by move=> c; apply/polyP=> [[|i]]; rewrite coefN !coefC ?oppr0. Qed.
 
-Lemma polyC_sub : {morph polyC : a b / a - b}.
-Proof. by move=> a b; rewrite polyC_add polyC_opp. Qed.
+Lemma polyCB : {morph polyC : a b / a - b}.
+Proof. by move=> a b; rewrite polyCD polyCN. Qed.
 
-Canonical polyC_additive := Additive polyC_sub.
+Canonical polyC_additive := Additive polyCB.
 
-Lemma polyC_muln n : {morph polyC : c / c *+ n}.
-Proof. exact: raddfMn. Qed.
+Lemma polyCMn n : {morph polyC : c / c *+ n}. Proof. exact: raddfMn. Qed.
 
 Lemma size_opp p : size (- p) = size p.
 Proof.
 by apply/eqP; rewrite eqn_leq -{3}(opprK p) -[-%R]/opp_poly unlock !size_poly.
 Qed.
 
-Lemma lead_coef_opp p : lead_coef (- p) = - lead_coef p.
+Lemma lead_coefN p : lead_coef (- p) = - lead_coef p.
 Proof. by rewrite /lead_coef size_opp coefN. Qed.
 
 Lemma size_add p q : size (p + q) <= maxn (size p) (size q).
@@ -621,15 +620,14 @@ rewrite coefMr big_ord_recl subn0.
 by rewrite big1 => [|j _]; rewrite coefC !simp.
 Qed.
 
-Lemma polyC_mul : {morph polyC : a b / a * b}.
+Lemma polyCM : {morph polyC : a b / a * b}.
 Proof. by move=> a b; apply/polyP=> [[|i]]; rewrite coefCM !coefC ?simp. Qed.
 
 Fact polyC_multiplicative : multiplicative polyC.
-Proof. by split; first apply: polyC_mul. Qed.
+Proof. by split; first apply: polyCM. Qed.
 Canonical polyC_rmorphism := AddRMorphism polyC_multiplicative.
 
-Lemma polyC_exp n : {morph polyC : c / c ^+ n}.
-Proof. exact: rmorphX. Qed.
+Lemma polyC_exp n : {morph polyC : c / c ^+ n}. Proof. exact: rmorphX. Qed.
 
 Lemma size_exp_leq p n : size (p ^+ n) <= ((size p).-1 * n).+1.
 Proof.
@@ -665,7 +663,7 @@ by case: leqP => // le_p_n; rewrite nth_default ?mulr0.
 Qed.
 
 Fact scale_polyA a b p : scale_poly a (scale_poly b p) = scale_poly (a * b) p.
-Proof. by rewrite !scale_polyE mulrA polyC_mul. Qed.
+Proof. by rewrite !scale_polyE mulrA polyCM. Qed.
 
 Fact scale_1poly : left_id 1 scale_poly.
 Proof. by move=> p; rewrite scale_polyE mul1r. Qed.
@@ -761,9 +759,7 @@ by elim: {p}(p : seq R) => //= p c IHp; rewrite cons_poly_def; apply: Kcons.
 Qed.
 
 Lemma polyseqXsubC a : 'X - a%:P = [:: - a; 1] :> seq R.
-Proof.
-by rewrite -['X]mul1r -polyC_opp -cons_poly_def polyseq_cons polyseq1.
-Qed.
+Proof. by rewrite -['X]mul1r -polyCN -cons_poly_def polyseq_cons polyseq1. Qed.
 
 Lemma size_XsubC a : size ('X - a%:P) = 2%N.
 Proof. by rewrite polyseqXsubC. Qed.
@@ -843,7 +839,7 @@ Lemma poly_def n E : \poly_(i < n) E i = \sum_(i < n) E i *: 'X^i.
 Proof.
 rewrite unlock; elim: n => [|n IHn] in E *; first by rewrite big_ord0.
 rewrite big_ord_recl /= cons_poly_def addrC expr0 alg_polyC.
-congr (_ + _); rewrite (iota_addl 1 0) -map_comp IHn big_distrl /=.
+congr (_ + _); rewrite (iotaDl 1 0) -map_comp IHn big_distrl /=.
 by apply: eq_bigr => i _; rewrite -scalerAl exprSr.
 Qed.
 
@@ -1065,7 +1061,7 @@ Proof. by elim/big_rec2: _ => [|i _ p _ <-]; rewrite (horner0, hornerD). Qed.
 Lemma hornerCM a p x : (a%:P * p).[x] = a * p.[x].
 Proof.
 elim/poly_ind: p => [|p c IHp]; first by rewrite !(mulr0, horner0).
-by rewrite mulrDr mulrA -polyC_mul !hornerMXaddC IHp mulrDr mulrA.
+by rewrite mulrDr mulrA -polyCM !hornerMXaddC IHp mulrDr mulrA.
 Qed.
 
 Lemma hornerZ c p x : (c *: p).[x] = c * p.[x].
@@ -1528,7 +1524,7 @@ Proof. by case: n => // n; rewrite derivSn derivC linear0. Qed.
 Lemma derivnD n : {morph derivn n : p q / p + q}.
 Proof. exact: linearD. Qed.
 
-Lemma derivn_sub n : {morph derivn n : p q / p - q}.
+Lemma derivnB n : {morph derivn n : p q / p - q}.
 Proof. exact: linearB. Qed.
 
 Lemma derivnMn n m p : (p *+ m)^`(n) = p^`(n) *+ m.
@@ -2219,7 +2215,7 @@ Definition poly_inv p := if p \in poly_unit then (p`_0)^-1%:P else p.
 Fact poly_mulVp : {in poly_unit, left_inverse 1 poly_inv *%R}.
 Proof.
 move=> p Up; rewrite /poly_inv Up.
-by case/andP: Up => /size_poly1P[c _ ->]; rewrite coefC -polyC_mul => /mulVr->.
+by case/andP: Up => /size_poly1P[c _ ->]; rewrite coefC -polyCM => /mulVr->.
 Qed.
 
 Fact poly_intro_unit p q : q * p = 1 -> p \in poly_unit.
@@ -2264,7 +2260,7 @@ Proof. by []. Qed.
 Lemma poly_invE p : p ^-1 = if p \in GRing.unit then (p`_0)^-1%:P else p.
 Proof. by []. Qed.
 
-Lemma polyC_inv c : c%:P^-1 = (c^-1)%:P.
+Lemma polyCV c : c%:P^-1 = (c^-1)%:P.
 Proof.
 have [/rmorphV-> // | nUc] := boolP (c \in GRing.unit).
 by rewrite !invr_out // poly_unitE coefC (negbTE nUc) andbF.
@@ -2771,3 +2767,28 @@ by rewrite monic_prod => // i; rewrite monicXsubC.
 Qed.
 
 End ClosedField.
+
+Notation "@ 'polyC_add'" :=
+  (deprecate polyC_add polyCD) (at level 10, only parsing) : fun_scope.
+Notation "@ 'polyC_opp'" :=
+  (deprecate polyC_opp polyCN) (at level 10, only parsing) : fun_scope.
+Notation "@ 'polyC_sub'" :=
+  (deprecate polyC_sub polyCB) (at level 10, only parsing) : fun_scope.
+Notation "@ 'polyC_muln'" :=
+  (deprecate polyC_muln polyCMn) (at level 10, only parsing) : fun_scope.
+Notation "@ 'polyC_mul'" :=
+  (deprecate polyC_mul polyCM) (at level 10, only parsing) : fun_scope.
+Notation "@ 'polyC_inv'" :=
+  (deprecate polyC_inv polyCV) (at level 10, only parsing) : fun_scope.
+Notation "@ 'lead_coef_opp'" :=
+  (deprecate lead_coef_opp lead_coefN) (at level 10, only parsing) : fun_scope.
+Notation "@ 'derivn_sub'" :=
+  (deprecate derivn_sub derivnB) (at level 10, only parsing) : fun_scope.
+Notation polyC_add := (@polyC_add _) (only parsing).
+Notation polyC_opp := (@polyC_opp _) (only parsing).
+Notation polyC_sub := (@polyC_sub _) (only parsing).
+Notation polyC_muln := (@polyC_muln _) (only parsing).
+Notation polyC_mul := (@polyC_mul _) (only parsing).
+Notation polyC_inv := (@polyC_inv _) (only parsing).
+Notation lead_coef_opp := (@lead_coef_opp _) (only parsing).
+Notation derivn_sub := (@derivn_sub _) (only parsing).