[WIP] replace the infrastructure of mpoly with monalg

Author: pi8027

src/monalg.v

@@ -44,7 +44,7 @@ Reserved Notation "<< k >>" (format "<< k >>").
 Reserved Notation "g @_ k"
   (at level 3, k at level 2, left associativity, format "g @_ k").
 Reserved Notation "c %:MP" (format "c %:MP").
-Reserved Notation "''X_{1..' n '}'".
+Reserved Notation "''X_{1..' n '}'" (n at level 2).
 Reserved Notation "'U_(' n )" (format "'U_(' n )").
 Reserved Notation "x ^[ f , g ]" (at level 1, format "x ^[ f , g ]").
 
@@ -72,9 +72,9 @@ Bind Scope type_scope with monomType.
 Notation mone := one.
 Notation mmul := mul.
 
-Local Notation "1" := (@mone _) : monom_scope.
-Local Notation "*%M" := (@mmul _) : function_scope.
-Local Notation "x * y" := (mmul x y) : monom_scope.
+Notation "1" := (@mone _) : monom_scope.
+Notation "*%M" := (@mmul _) : function_scope.
+Notation "x * y" := (mmul x y) : monom_scope.
 
 (* -------------------------------------------------------------------- *)
 HB.mixin Record MonomialDef_isConomialDef V of MonomialDef V := {

src/mpoly.v

@@ -84,7 +84,7 @@ From mathcomp Require Import order fingroup perm ssralg zmodp poly ssrint.
 From mathcomp Require Import matrix vector.
 From mathcomp Require Import bigenough.
 
-Require Import ssrcomplements freeg.
+Require Import xfinmap monalg.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -94,12 +94,6 @@ Import Order.Theory GRing.Theory BigEnough.
 
 Local Open Scope ring_scope.
 
-Declare Scope mpoly_scope.
-Declare Scope multi_scope.
-
-Delimit Scope mpoly_scope with MP.
-Delimit Scope multi_scope with MM.
-
 Local Notation simpm := Monoid.simpm.
 
 Local Infix "@@" := (allpairs pair) (at level 60, right associativity).
@@ -111,14 +105,12 @@ Import Order.DefaultSeqLexiOrder.
 Import Order.DefaultTupleLexiOrder.
 
 (* -------------------------------------------------------------------- *)
-Reserved Notation "''X_{1..' n '}'" (n at level 2).
 Reserved Notation "''X_{1..' n  < b '}'" (n, b at level 2).
 Reserved Notation "''X_{1..' n  < b1 , b2 '}'" (b1, b2 at level 2).
 Reserved Notation "[ 'multinom' s ]" (format "[ 'multinom'  s ]").
 Reserved Notation "[ 'multinom' 'of' s ]" (format "[ 'multinom'  'of'  s ]").
 Reserved Notation "[ 'multinom' F | i < n ]"
-  (i at level 0,
-     format "[ '[hv' 'multinom'  F '/'  |  i  <  n ] ']'").
+  (i at level 0, format "[ '[hv' 'multinom'  F '/'  |  i  <  n ] ']'").
 Reserved Notation "'U_(' n )" (format "'U_(' n )").
 Reserved Notation "{ 'mpoly' T [ n ] }"
   (T at level 2, format "{ 'mpoly'  T [ n ] }").
@@ -127,8 +119,7 @@ Reserved Notation "{ 'ipoly' T [ n ] }"
   (T at level 2, format "{ 'ipoly'  T [ n ] }").
 Reserved Notation "{ 'ipoly' T [ n ] }^p"
   (T at level 2, format "{ 'ipoly'  T [ n ] }^p").
-Reserved Notation "''X_' i"
-  (at level 8, i at level 2, format "''X_' i").
+Reserved Notation "''X_' i" (at level 8, i at level 2, format "''X_' i").
 Reserved Notation "''X_[' i ]" (format "''X_[' i ]").
 Reserved Notation "''X_[' R , i ]" (format "''X_[' R ,  i ]").
 Reserved Notation "c %:MP" (format "c %:MP").
@@ -141,218 +132,157 @@ Reserved Notation "e .@[< x >]" (format "e .@[< x >]").
 Reserved Notation "p \mPo q" (at level 50).
 Reserved Notation "x ^[ f ]" (format "x ^[ f ]").
 Reserved Notation "x ^[ f , g ]" (format "x ^[ f , g ]").
-Reserved Notation "p ^`M ( m )"
-  (at level 8, format "p ^`M ( m )").
-Reserved Notation "p ^`M ( m , n )"
-  (at level 8, format "p ^`M ( m ,  n )").
-Reserved Notation "p ^`M [ m ]"
-  (at level 8, format "p ^`M [ m ]").
-Reserved Notation "''s_' k"
-  (at level 8, k at level 2, format "''s_' k").
+Reserved Notation "p ^`M ( m )" (at level 8, format "p ^`M ( m )").
+Reserved Notation "p ^`M ( m , n )" (at level 8, format "p ^`M ( m ,  n )").
+Reserved Notation "p ^`M [ m ]" (at level 8, format "p ^`M [ m ]").
+Reserved Notation "''s_' k" (at level 8, k at level 2, format "''s_' k").
 Reserved Notation "''s_(' n , k )" (format "''s_(' n ,  k )").
 Reserved Notation "''s_(' K , n , k )" (format "''s_(' K ,  n ,  k )").
 Reserved Notation "+%MM".
 Reserved Notation "-%MM".
 
 (* -------------------------------------------------------------------- *)
-Section MultinomDef.
-Context (n : nat).
-
-Record multinom : predArgType := Multinom { multinom_val :> n.-tuple nat }.
-
-HB.instance Definition _ := [isNew for multinom_val].
-
-Definition fun_of_multinom M := tnth (multinom_val M).
-
-Coercion fun_of_multinom : multinom >-> Funclass.
-
-Lemma multinomE M : Multinom M =1 tnth M.
-Proof. by []. Qed.
-
-End MultinomDef.
 
-Notation "[ 'multinom' s ]" := (@Multinom _ s) : form_scope.
-Notation "[ 'multinom' 'of'  s ]" := [multinom [tuple of s]] : form_scope.
 Notation "[ 'multinom' E | i < n ]" :=
-  [multinom [tuple E%N | i < n]] : form_scope.
+  [cmonom E | i in [fset x in 'I_n]]%M : monom_scope.
 Notation "[ 'multinom' E | i < n ]" :=
-  [multinom [tuple E%N : nat | i < n]] (only parsing) : form_scope.
+  [cmonom E : nat | i in [fset x in 'I_n]]%M (only parsing) : monom_scope.
 
 (* -------------------------------------------------------------------- *)
-Notation "''X_{1..' n '}'" := (multinom n) : type_scope.
-
-HB.instance Definition _ n := [Countable of 'X_{1..n} by <:].
-
-Bind Scope multi_scope with multinom.
-
-(* -------------------------------------------------------------------- *)
-Definition lem n (m1 m2 : 'X_{1..n}) :=
-  [forall i, m1%MM i <= m2%MM i].
-
-Definition ltm n (m1 m2 : 'X_{1..n}) :=
-  (m1 != m2) && (lem m1 m2).
-
-(* -------------------------------------------------------------------- *)
-Section MultinomTheory.
-Context {n : nat}.
-Implicit Types (m : 'X_{1..n}).
+#[deprecated(use=mone)]
+Notation mnm0 := (@mone 'X_{1.._}).
+#[deprecated(use=ucm)]
+Notation mnm1 := (@ucm 'I__).
+#[deprecated(use=mmul)]
+Notation mnm_add := (@mmul 'X_{1.._}).
+#[deprecated(use=divcm)]
+Notation mnm_sub := (@divcm 'I__).
+#[deprecated(use=expmn)]
+Notation mnm_muln := (@expmn 'X_{1.._}).
 
-Lemma mnm_tnth m j : m j = tnth m j.
-Proof. by []. Qed.
-
-Lemma mnm_nth x0 m j : m j = nth x0 m j.
-Proof. by rewrite mnm_tnth (tnth_nth x0). Qed.
-
-Lemma mnmE E j : [multinom E i | i < n] j = E j.
-Proof. by rewrite multinomE tnth_mktuple. Qed.
-
-Lemma mnm_valK t : [multinom t] = t :> n.-tuple nat.
-Proof. by []. Qed.
-
-Lemma mnmP m1 m2 : (m1 = m2) <-> (m1 =1 m2).
-Proof.
-case: m1 m2 => [m1] [m2] /=; split => [->//|h].
-by apply/val_inj/eq_from_tnth => i; rewrite -!multinomE.
-Qed.
-
-End MultinomTheory.
-
-(* -------------------------------------------------------------------- *)
 Section MultinomMonoid.
 Context {n : nat}.
 Implicit Types (m : 'X_{1..n}).
 
-Definition mnm0 := [multinom 0 | _ < n].
-Definition mnm1 (c : 'I_n) := [multinom c == i | i < n].
-Definition mnm_add m1 m2 := [multinom m1 i + m2 i | i < n].
-Definition mnm_sub m1 m2 := [multinom m1 i - m2 i | i < n].
-Definition mnm_muln m i := iterop i mnm_add m mnm0.
+Definition lem m1 m2 := [forall i, m1 i <= m2 i].
+Definition ltm m1 m2 := (m1 != m2) && (lem m1 m2).
+
+Local Notation "*%M" := (@mmul 'X_{1..n}) : function_scope.
+Local Notation "/%M" := (@divcm 'I_n) : function_scope.
 
-Arguments mnm_muln : simpl never.
+Local Notation "1"         := (@mone 'X_{1..n}) : monom_scope.
+Local Notation "'U_(' i )" := (@ucm 'I_n i) : monom_scope.
+Local Notation "m1 * m2"   := ( *%M m1 m2) : monom_scope.
+Local Notation "m1 / m2"   := (/%M m1 m2) : monom_scope.
+Local Notation "x ^+ m"    := (@expmn 'X_{1..n} x m) : monom_scope.
 
-Local Notation "0"         := mnm0 : multi_scope.
-Local Notation "'U_(' n )" := (mnm1 n) : multi_scope.
-Local Notation "m1 + m2"   := (mnm_add m1 m2) : multi_scope.
-Local Notation "m1 - m2"   := (mnm_sub m1 m2) : multi_scope.
-Local Notation "x *+ n"    := (mnm_muln x n) : multi_scope.
+Local Notation "m1 <= m2" := (lem m1 m2) : monom_scope.
+Local Notation "m1 < m2"  := (ltm m1 m2) : monom_scope.
 
-Local Notation "+%MM" := (@mnm_add) : function_scope.
-Local Notation "-%MM" := (@mnm_sub) : function_scope.
+Lemma mnmE (E : 'I_n -> nat) (j : 'I_n) : [multinom E i | i < n]%M j = E j.
+Proof. by rewrite cmE fsfunE inE. Qed.
 
-Local Notation "m1 <= m2" := (lem m1 m2) : multi_scope.
-Local Notation "m1 < m2"  := (ltm m1 m2) : multi_scope.
+Lemma mnmP (m1 m2 : 'X_{1..n}) : (m1 = m2) <-> (m1 =1 m2).
+Proof. by split => [->|/fsfunP/val_inj]. Qed.
 
-Lemma mnm0E i : 0%MM i = 0%N. Proof. exact/mnmE. Qed.
+Lemma mnm0E i : 1%M i = 0%N. Proof. exact: cm1. Qed.
 
-Lemma mnmDE i m1 m2 : (m1 + m2)%MM i = (m1 i + m2 i)%N. Proof. exact/mnmE. Qed.
+Lemma mnmDE i m1 m2 : (m1 * m2)%M i = (m1 i + m2 i)%N. Proof. exact: cmM. Qed.
 
-Lemma mnmBE i m1 m2 : (m1 - m2)%MM i = (m1 i - m2 i)%N. Proof. exact/mnmE. Qed.
+Lemma mnmBE i m1 m2 : (m1 / m2)%M i = (m1 i - m2 i)%N.
+Proof. exact: divcmE. Qed.
 
 Lemma mnm_sumE (I : Type) i (r : seq I) P F :
-  (\big[+%MM/0%MM]_(x <- r | P x) (F x)) i = (\sum_(x <- r | P x) (F x i))%N.
-Proof. by apply/(big_morph (fun m => m i)) => [x y|]; rewrite mnmE. Qed.
+  (\big[*%M/1%M]_(x <- r | P x) (F x)) i = (\sum_(x <- r | P x) (F x i))%N.
+Proof. exact/(big_morph (fun m => m i))/cm1/cmM. Qed.
+
+Lemma mnm1E i j : U_(i)%M j = (i == j). Proof. exact: ucmE. Qed.
 
 (*-------------------------------------------------------------------- *)
-Lemma mnm_lepP {m1 m2} : reflect (forall i, m1 i <= m2 i) (m1 <= m2)%MM.
+Lemma mnm_lepP {m1 m2} : reflect (forall i, m1 i <= m2 i) (m1 <= m2)%M.
 Proof. exact: (iffP forallP). Qed.
 
-Lemma lepm_refl m : (m <= m)%MM. Proof. exact/mnm_lepP. Qed.
+Lemma lepm_refl m : (m <= m)%M. Proof. exact/mnm_lepP. Qed.
 
-Lemma lepm_trans m3 m1 m2 : (m1 <= m2 -> m2 <= m3 -> m1 <= m3)%MM.
+Lemma lepm_trans m3 m1 m2 : (m1 <= m2 -> m2 <= m3 -> m1 <= m3)%M.
 Proof.
 move=> h1 h2; apply/mnm_lepP => i.
 exact: leq_trans (mnm_lepP h1 i) (mnm_lepP h2 i).
 Qed.
 
-Lemma addmC : commutative +%MM.
-Proof. by move=> m1 m2; apply/mnmP=> i; rewrite !mnmE addnC. Qed.
-
-Lemma addmA : associative +%MM.
-Proof. by move=> m1 m2 m3; apply/mnmP=> i; rewrite !mnmE addnA. Qed.
+Lemma addmC : commutative *%M. Proof. exact: mulmC. Qed.
 
-Lemma add0m : left_id 0%MM +%MM.
-Proof. by move=> m; apply/mnmP=> i; rewrite !mnmE add0n. Qed.
+Lemma addmA : associative *%M. Proof. exact: mulmA. Qed.
 
-Lemma addm0 : right_id 0%MM +%MM.
-Proof. by move=> m; rewrite addmC add0m. Qed.
+Lemma add0m : left_id 1%M *%M. Proof. exact: mul1m. Qed.
 
-HB.instance Definition _ := Monoid.isComLaw.Build 'X_{1..n} 0%MM +%MM
-  addmA addmC add0m.
+Lemma addm0 : right_id 1%M *%M. Proof. exact: mulm1. Qed.
 
-Lemma subm0 m : (m - 0)%MM = m.
-Proof. by apply/mnmP=> i; rewrite !mnmE subn0. Qed.
+Lemma subm0 m : (m / 1)%M = m.
+Proof. by apply/mnmP=> i; rewrite divcmE cm1 subn0. Qed.
 
-Lemma sub0m m : (0 - m = 0)%MM.
-Proof. by apply/mnmP=> i; rewrite !mnmE sub0n. Qed.
+Lemma sub0m m : (1 / m = 1)%M.
+Proof. by apply/mnmP=> i; rewrite divcmE cm1 sub0n. Qed.
 
-Lemma addmK m : cancel (+%MM^~ m) (-%MM^~ m).
-Proof. by move=> m' /=; apply/mnmP=> i; rewrite !mnmE addnK. Qed.
+Lemma addmK m : cancel ( *%M^~ m) (/%M^~ m).
+Proof. by move=> m'; apply/mnmP=> i; rewrite divcmE cmM addnK. Qed.
 
-Lemma addIm : left_injective +%MM.
-Proof. by move=> ? ? ? /(can_inj (@addmK _)). Qed.
+Lemma addIm : left_injective *%M.
+Proof. by move=> ? ? ? /(can_inj (addmK _)). Qed.
 
-Lemma addmI : right_injective +%MM.
-Proof. by move=> m ? ?; rewrite ![(m + _)%MM]addmC => /addIm. Qed.
+Lemma addmI : right_injective *%M.
+Proof. by move=> m ? ?; rewrite ![mmul m _]mulmC => /addIm. Qed.
 
-Lemma eqm_add2l m n1 n2 : (m + n1 == m + n2)%MM = (n1 == n2).
+Lemma eqm_add2l m n1 n2 : (m * n1 == m * n2)%M = (n1 == n2).
 Proof. exact/inj_eq/addmI. Qed.
 
-Lemma eqm_add2r m n1 n2 : (n1 + m == n2 + m)%MM = (n1 == n2).
+Lemma eqm_add2r m n1 n2 : (n1 * m == n2 * m)%M = (n1 == n2).
 Proof. exact: (inj_eq (@addIm _)). Qed.
 
-Lemma submK m m' : (m <= m')%MM -> (m' - m + m = m')%MM.
-Proof. by move/mnm_lepP=> h; apply/mnmP=> i; rewrite !mnmE subnK. Qed.
+Lemma submK m m' : (m <= m')%M -> (m' / m * m = m')%M.
+Proof. by move/mnm_lepP=> h; apply/mnmP=> i; rewrite cmM divcmE subnK. Qed.
 
-Lemma addmBA m1 m2 m3 :
-  (m3 <= m2)%MM -> (m1 + (m2 - m3))%MM = (m1 + m2 - m3)%MM.
-Proof. by move/mnm_lepP=> h; apply/mnmP=> i; rewrite !mnmE addnBA. Qed.
+Lemma addmBA m1 m2 m3 : (m3 <= m2)%M -> (m1 * (m2 / m3))%M = (m1 * m2 / m3)%M.
+Proof. by move/mnm_lepP=> h; apply/mnmP=> i; rewrite !(divcmE, cmM) addnBA. Qed.
 
-Lemma submDA m1 m2 m3 : (m1 - m2 - m3)%MM = (m1 - (m2 + m3))%MM.
-Proof. by apply/mnmP=> i; rewrite !mnmE subnDA. Qed.
+Lemma submDA m1 m2 m3 : (m1 / m2 / m3)%M = (m1 / (m2 * m3))%M.
+Proof. by apply/mnmP=> i; rewrite !divcmE cmM subnDA. Qed.
 
-Lemma submBA m1 m2 m3 : (m3 <= m2)%MM -> (m1 - (m2 - m3) = m1 + m3 - m2)%MM.
-Proof. by move/mnm_lepP=> h; apply/mnmP=> i; rewrite !mnmE subnBA. Qed.
+Lemma submBA m1 m2 m3 : (m3 <= m2)%M -> (m1 / (m2 / m3) = m1 * m3 / m2)%M.
+Proof. by move/mnm_lepP=> h; apply/mnmP=> i; rewrite !divcmE cmM subnBA. Qed.
 
-Lemma lem_subr m1 m2 : (m1 - m2 <= m1)%MM.
-Proof. by apply/mnm_lepP=> i; rewrite !mnmE leq_subr. Qed.
+Lemma lem_subr m1 m2 : (m1 / m2 <= m1)%M.
+Proof. by apply/mnm_lepP=> i; rewrite divcmE leq_subr. Qed.
 
-Lemma lem_addr m1 m2 : (m1 <= m1 + m2)%MM.
-Proof. by apply/mnm_lepP=> i; rewrite mnmDE leq_addr. Qed.
+Lemma lem_addr m1 m2 : (m1 <= m1* m2)%M.
+Proof. by apply/mnm_lepP=> i; rewrite cmM leq_addr. Qed.
 
-Lemma lem_addl m1 m2 : (m2 <= m1 + m2)%MM.
-Proof. by apply/mnm_lepP=> i; rewrite mnmDE leq_addl. Qed.
+Lemma lem_addl m1 m2 : (m2 <= m1 * m2)%M.
+Proof. by apply/mnm_lepP=> i; rewrite cmM leq_addl. Qed.
 
 (* -------------------------------------------------------------------- *)
-Lemma mulm0n m : (m *+ 0 = 0)%MM.
-Proof. by []. Qed.
+Lemma mulm0n m : (m ^+ 0 = 1)%M. Proof. by []. Qed.
 
-Lemma mulm1n m : (m *+ 1 = m)%MM.
-Proof. by []. Qed.
+Lemma mulm1n m : (m ^+ 1 = m)%M. Proof. by []. Qed.
 
-Lemma mulmS m i : (m *+ i.+1 = m + m *+ i)%MM.
-Proof. by rewrite /mnm_muln !Monoid.iteropE iterS. Qed.
+Lemma mulmS m i : (m ^+ i.+1 = m * m ^+ i)%M. Proof. exact: expmnS. Qed.
 
-Lemma mulmSr m i : (m *+ i.+1 = m *+ i + m)%MM.
-Proof. by rewrite mulmS addmC. Qed.
+Lemma mulmSr m i : (m ^+ i.+1 = m ^+ i * m)%M. Proof. exact: expmnSr. Qed.
 
-Lemma mulmnE m k i : ((m *+ k) i)%MM = (m i * k)%N.
+Lemma mulmnE m k i : (m ^+ k)%M i = (m i * k)%N.
 Proof.
-elim: k => [|k ih]; first by rewrite muln0 mulm0n !mnmE.
-by rewrite mulmS mulnS mnmDE ih.
+elim: k => [|k ih]; first by rewrite cm1 muln0.
+by rewrite mulmS cmM ih mulnS.
 Qed.
 
-Lemma mnm1E i j : U_(i)%MM j = (i == j). Proof. exact/mnmE. Qed.
-
-Lemma lep1mP i m : (U_(i) <= m)%MM = (m i != 0%N).
+Lemma lep1mP i m : (U_(i) <= m)%M = (m i != 0%N).
 Proof.
 apply/mnm_lepP/idP=> [/(_ i)|]; rewrite -lt0n; first by rewrite mnm1E eqxx.
 by move=> lt0_mi j; rewrite mnm1E; case: eqP=> // <-.
 Qed.
 
 End MultinomMonoid.
 
-Arguments mnm_muln : simpl never.
-
 (* -------------------------------------------------------------------- *)
 Notation "+%MM" := (@mnm_add _).
 Notation "-%MM" := (@mnm_sub _).