wip

auxresults.v

@@ -323,9 +323,7 @@ Local Notation "x =p y"  := (perm_eq x y) (at level 70, no associativity).
 
 Lemma perm_eq_nil (s : seq T) : (s =p [::]) = (s == [::]).
 Proof.
-apply/idP/idP ; last by move/eqP ->.
-move => H ; apply/eqP.
-by apply: perm_eq_small.
+by apply/idP/eqP => /perm_nilP.
 Qed.
 
 Lemma rem_cons (s : seq T) (a : T) : rem a (a :: s) = s.
@@ -417,16 +415,7 @@ Qed.
 Lemma rem_undup (x : T) (s : seq T) : 
   rem x (undup s) = undup (filter (predC1 x) s).
 Proof.
-elim: s => // y s /=.
-have [<- | neq_xy] := eqVneq x y.
-  rewrite eqxx fun_if /= eqxx => <-.  
-  have [x_in_s | x_notin_s] := boolP (x \in s) => //.
-  by rewrite rem_id // mem_undup.
-rewrite eq_sym neq_xy /=.
-have [y_in_s | /negbTE y_notin_s] := boolP (y \in s); rewrite mem_filter.
-  by rewrite y_in_s andbT /= eq_sym neq_xy.
-rewrite /= eq_sym ; move/negbTE : neq_xy => ->.
-by rewrite y_notin_s andbF => ->.
+by rewrite rem_filter ?undup_uniq// filter_undup.
 Qed.
 
 Local Open Scope ring_scope. 
@@ -450,7 +439,7 @@ End MoreSeqEqType.
 
 Section MoreFinmap.
 
-Open Local Scope fset_scope.
+Local Open Scope fset_scope.
 
 Lemma finSet_ind (T : choiceType) (P : {fset T} -> Prop) : 
   P fset0 -> (forall s x, P s -> P (x |` s)) -> forall s, P s.
@@ -729,14 +718,14 @@ Variable (K : fieldType).
 Fact modp_sumn (I : Type) (r : seq I) (P : pred I)
                (F : I -> {poly K}) (p : {poly K}) :
                (\sum_(i <- r | P i) F i) %% p = \sum_(i <- r | P i) (F i %% p).
-Proof. by rewrite (big_morph ((@modp _)^~ p) (modp_add _) (mod0p _) _). Qed.
+Proof. by rewrite (big_morph ((@modp _)^~ p) (modpD _) (mod0p _) _). Qed.
 
 Fact modp_mul2 (p q m : {poly K}): ((p %% m) * q) %% m = (p * q) %% m.
 Proof. by rewrite mulrC modp_mul mulrC. Qed.
 
 End AuxiliaryResults.
 
-Module InjMorphism.
+(* Module InjMorphism.
 
 Section ClassDef.
 
@@ -784,7 +773,7 @@ Canonical rmorphism.
 End Exports.
 
 End InjMorphism.
-Include InjMorphism.Exports.
+   Include InjMorphism.Exports. *)
 
 Section InjectiveTheory.
 
@@ -795,7 +784,7 @@ move=> f_inj x y /eqP; rewrite -subr_eq0 -raddfB => /eqP /f_inj /eqP.
 by rewrite subr_eq0 => /eqP.
 Qed.
 
-Variable (R S : ringType) (f : {injmorphism R -> S}).
+(*Variable (R S : ringType) (f : {injmorphism R -> S}).
 
 Lemma rmorph_inj : injective f. Proof. by case: f => [? []]. Qed.
 
@@ -812,9 +801,9 @@ by rewrite !coef_map => /rmorph_inj.
 Qed.
 
 Canonical map_poly_is_injective := InjMorphism map_poly_injective.
-
+ *)
 End InjectiveTheory.
-Hint Resolve rmorph_inj.
+(* Hint Resolve rmorph_inj. 
 
 Canonical polyC_is_injective (R : ringType) := InjMorphism (@polyC_inj R).
 
@@ -826,4 +815,4 @@ Canonical comp_is_injmorphism (R S T : ringType)
 Definition fmorph (F R : Type) (f : F -> R) := f.
 Canonical fmorph_is_injmorphism (F : fieldType) (R : ringType)
   (f : {rmorphism F -> R}) :=
-  InjMorphism (fmorph_inj f : injective (fmorph f)).
+   InjMorphism (fmorph_inj f : injective (fmorph f)). *)

extra_ssr.v

@@ -1,8 +1,8 @@
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp
-Require Import ssrfun ssrbool eqtype ssrnat seq div fintype tuple.
+Require Import ssrfun ssrbool eqtype ssrnat seq div fintype tuple binomial.
 From mathcomp
-Require Import finfun bigop fingroup perm ssralg zmodp matrix mxalgebra.
+Require Import finfun finset bigop fingroup perm ssralg zmodp matrix mxalgebra.
 From mathcomp
 Require Import poly polydiv mxpoly.
 From mathcomp
@@ -33,8 +33,6 @@ End extra_nat.
 
 Section extra_perm.
 
-From mathcomp Require Import fintype finfun finset perm zmodp div binomial.
-
 (* Remark: generalize (D : {set aT}) to (D : pred_class_of aT) in finset.v *)
 (* Meanwhile, we reprove it in this more general case *)
 Notation pred_class_of T := (pred_sort (predPredType T)).
@@ -67,12 +65,12 @@ Qed.
 
 Definition perm_circle n : 'S_n := perm (@perm_circle_proof n).
 
-Lemma pcycle_perm_circle n x : pcycle (perm_circle n) x = setT.
+Lemma porbit_perm_circle n x : porbit (perm_circle n) x = setT.
 Proof.
 apply/setP => y /=; rewrite in_setT.
 wlog le_xy : x y / x <= y => /= [hwlog|].
-  by have /orP[/hwlog//|/hwlog] := leq_total x y; rewrite pcycle_sym.
-suff -> : y = ((perm_circle n) ^+ (y - x))%g x by rewrite mem_pcycle.
+  by have /orP[/hwlog//|/hwlog] := leq_total x y; rewrite porbit_sym.
+suff -> : y = ((perm_circle n) ^+ (y - x))%g x by rewrite mem_porbit.
 rewrite permX; apply: val_inj => /=.
 move: (ltn_ord y); set d := (y - x)%N; rewrite -(subnK le_xy) -/d.
 elim: d => //= d ihd; rewrite addSn => hd.
@@ -87,9 +85,9 @@ by apply/imsetP/eqP => [[//]|->]; last exists a.
 Qed.
 Arguments imset_const {_ _ _} a [x] _.
 
-Lemma pcycles_perm_circle n : pcycles (perm_circle n.+1) = [set setT].
+Lemma porbits_perm_circle n : porbits (perm_circle n.+1) = [set setT].
 Proof.
-rewrite /pcycles /= (pred_class_eq_imset _ (@pcycle_perm_circle n.+1)) /=.
+rewrite /porbits /= (pred_class_eq_imset _ (@porbit_perm_circle n.+1)) /=.
 by apply/setP => /= x; rewrite (imset_const ord0).
 Qed.
 
@@ -98,15 +96,15 @@ Proof. by apply/permP => [[]]. Qed.
 
 Lemma odd_perm_circle n : perm_circle n.+1 = odd n :> bool.
 Proof.
-by rewrite /odd_perm pcycles_perm_circle card_ord cards1 addbT negbK.
+by rewrite /odd_perm porbits_perm_circle card_ord cards1 addbT negbK.
 Qed.
 
 Lemma odd_perm_rev n : @perm_rev n = odd 'C(n, 2) :> bool.
 Proof.
 elim: n => [|/= n ihn]; first by rewrite perm_rev0 odd_perm1.
 suff -> : perm_rev = (perm_circle n.+1 * lift0_perm perm_rev)%g.
   rewrite odd_permM odd_lift_perm /= ihn => {ihn}.
-  by rewrite odd_perm_circle /= binS bin1 odd_add addbC.
+  by rewrite odd_perm_circle /= binS bin1 oddD addbC.
 apply/permP => i /=; apply/val_inj; do !rewrite !permE /=.
 rewrite /lift_perm_fun /= subSS ltnS.
 case: unliftP => /= [j|] /(congr1 val) /=; last first.
@@ -131,20 +129,21 @@ Import ssrint.IntDist.
 
 Lemma bin2D m n : 'C(m + n, 2) = 'C(m, 2) + 'C(n, 2) + m * n.
 Proof.
-case: m => [|m] //=; rewrite bin2 !addSn /= mulnDr -{1}addSn -addnS !mulnDl.
+case: m => [|m] /=; first by rewrite addn0.
+rewrite bin2 !addSn /= mulnDr -{1}addSn -addnS !mulnDl.
 rewrite [n * m]mulnC [X in X + _]addnC addnACA addnn.
-rewrite halfD !odd_double /= doubleK halfD !odd_mul !andNb !add0n addnC.
+rewrite halfD !odd_double /= doubleK halfD !oddM !andNb !add0n addnC.
 by rewrite -!bin2 ['C(n.+1, 2)]binS bin1 mulSn !addnA.
 Qed.
 
 Lemma odd_bin2M2 n : odd 'C(n.*2, 2) = odd n.
 Proof.
-rewrite bin2 -{1}mul2n -mulnA mul2n doubleK odd_mul.
+rewrite bin2 -{1}mul2n -mulnA mul2n doubleK oddM.
 by case: n => //= n; rewrite odd_double andbT.
 Qed.
 
 Lemma odd_bin2D2n k n : odd 'C(k.*2 + n, 2) = (odd k (+) odd 'C(n, 2)).
-Proof. by rewrite bin2D !odd_add odd_bin2M2 -doubleMl odd_double addbF. Qed.
+Proof. by rewrite bin2D !oddD odd_bin2M2 -doubleMl odd_double addbF. Qed.
 
 Lemma bin2DB m n : odd 'C(m + n, 2) = odd (minn m n) (+) odd 'C(`|m - n|, 2).
 Proof.
@@ -229,22 +228,22 @@ Lemma dvdp_lcml (p q : {poly R}) : p %| lcmp p q.
 Proof.
 have [->|p0] := eqVneq p 0; first by rewrite lcm0p.
 rewrite -(@dvdp_mul2l _ (gcdp p q)) ?gcdp_eq0 ?(negPf p0) // mulp_gcd_lcm.
-by rewrite dvdp_scaler ?lc_expn_scalp_neq0 // mulrC dvdp_mul ?dvdp_gcdr.
+by rewrite dvdpZr ?lc_expn_scalp_neq0 // mulrC dvdp_mul ?dvdp_gcdr.
 Qed.
 
 Lemma dvdp_lcmr (p q : {poly R}) : q %| lcmp p q.
 Proof.
 have [->|p0] := eqVneq p 0; first by rewrite lcm0p dvdp0.
 rewrite -(@dvdp_mul2l _ (gcdp p q)) ?gcdp_eq0 ?(negPf p0) // mulp_gcd_lcm.
-by rewrite dvdp_scaler ?lc_expn_scalp_neq0 ?dvdp_mul ?dvdp_gcdl.
+by rewrite dvdpZr ?lc_expn_scalp_neq0 ?dvdp_mul ?dvdp_gcdl.
 Qed.
 
 Lemma dvdp_lcm (p q r : {poly R}) : (lcmp p q %| r) = (p %| r) && (q %| r).
 Proof.
 have [->|p0] := eqVneq p 0; first by rewrite lcm0p dvd0p andb_idr => // /eqP->.
 have [->|q0] := eqVneq q 0; first by rewrite lcmp0 dvd0p andb_idl => // /eqP->.
 rewrite -(@dvdp_mul2l _ (gcdp p q)) ?gcdp_eq0 ?(negPf p0) // mulp_gcd_lcm.
-rewrite dvdp_scalel ?lc_expn_scalp_neq0 // -(eqp_dvdr _ (gcdp_mul2r _ _ _)).
+rewrite dvdpZl ?lc_expn_scalp_neq0 // -(eqp_dvdr _ (gcdp_mul2r _ _ _)).
 by rewrite dvdp_gcd dvdp_mul2l // mulrC dvdp_mul2l // andbC.
 Qed.