Library mathcomp.boot.nmodule

From HB Require Import structures.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype choice ssrnat seq.
From mathcomp Require Import bigop fintype finfun monoid.

Additive group-like structures NB: See CONTRIBUTING.md for an introduction to HB concepts and commands. This file defines the following algebraic structures: baseAddMagmaType == type with an addition operator The HB class is called BaseAddMagma. ChoiceBaseAddMagma.type == join of baseAddMagmaType and choiceType The HB class is called ChoiceBaseAddMagma. addMagmaType == additive magma The HB class is called AddMagma. addSemigroupType == additive semigroup The HB class is called AddSemigroup. baseAddUMagmaType == pointed additive magma The HB class is called BaseAddUMagma. ChoiceBaseAddUMagma.type == join of baseAddUMagmaType and choiceType The HB class is called ChoiceBaseUMagma. addUmagmaType == additive unitary magma The HB class is called AddUMagma. nmodType == additive monoid The HB class is called Nmodule. baseZmodType == pointed additive magma with an opposite operator The HB class is called BaseZmodule. zmodType == abelian group The HB class is called Group. and their joins with subType: subBaseAddUMagmaType V P == join of baseAddUMagmaType and subType (P : pred V) such that val is additive The HB class is called SubBaseAddUMagma. subAddUMagmaType V P == join of addUMagmaType and subType (P : pred V) such that val is additive The HB class is called SubAddUMagma. subNmodType V P == join of nmodType and subType (P : pred V) such that val is additive The HB class is called SubNmodule. subZmodType V P == join of zmodType and subType (P : pred V) such that val is additive The HB class is called SubZmodule. Morphisms between the above structures (see below for details): {additive U -> V} == nmod (resp. zmod) morphism between nmodType (resp. zmodType) instances U and V. The HB class is called Additive. Closedness predicates for the algebraic structures: mulgClosed V == predicate closed under multiplication on G : magmaType The HB class is called MulClosed. umagmaClosed V == predicate closed under multiplication and containing 1 on G : baseUMagmaType The HB class is called UMagmaClosed. invgClosed V == predicate closed under inversion on G : baseGroupType The HB class is called InvClosed. groupClosed V == predicate closed under multiplication and inversion and containing 1 on G : baseGroupType The HB class is called InvClosed. Canonical properties of the algebraic structures:

addMagmaType (additive magmas):

x + y == the addition of x and y addr_closed S <-> collective predicate S is closed under addition

baseAddUMagmaType (pointed additive magmas):

0 == the zero of a unitary additive magma x *+ n == n times x, with n in nat (non-negative), i.e. x + (x + .. (x + x)..) (n terms); x *+ 1 is thus convertible to x, and x *+ 2 to x + x \sum_<range> e == iterated sum for a baseAddUMagmaType (cf bigop.v) e`_i == nth 0 e i, when e : seq M and M has an addUMagmaType structure support f == 0.-support f, i.e., [pred x | f x != 0] addumagma_closed S <-> collective predicate S is closed under addition and contains 0

nmodType (abelian monoids):

nmod_closed S := addumagma_closed S

baseZmodType (pointed additive magmas with an opposite operator):

x == the opposite of x

x - y == x + (- y) x *- n == - (x *+ n) oppr_closed S <-> collective predicate S is closed under opposite subr_closed S <-> collective predicate S is closed under subtraction zmod_closed S <-> collective predicate S is closed under subtraction and contains 1 In addition to this structure hierarchy, we also develop a separate, parallel hierarchy for morphisms linking these structures:

Additive (nmod or zmod morphisms):

nmod_morphism f <-> f of type U -> V is an nmod morphism, i.e., f maps the Nmodule structure of U to that of V, 0 to 0 and + to + := (f 0 = 0) * {morph f : x y / x + y} zmod_morphisme f <-> f of type U -> V is a zmod morphism, i.e., f maps the Zmodule structure of U to that of V, 0 to 0, - to - and + to + (equivalently, binary - to -) := {morph f : u v / u - v} {additive U -> V} == the interface type for a Structure (keyed on a function f : U -> V) that encapsulates the nmod_morphism property; both U and V must have canonical baseAddUMagmaType instances When both U and V have zmodType instances, it is a zmod morphism. := Algebra.Additive.type U V Notations are defined in scope ring_scope (delimiter %R) This library also extends the conventional suffixes described in library ssrbool.v with the following: 0 -- unitary additive magma 0, as in addr0 : x + 0 = x D -- additive magma addition, as in mulrnDr : x *+ (m + n) = x *+ m + x *+ n B -- z-module subtraction, as in opprB : - (x - y) = y - x Mn -- ring by nat multiplication, as in raddfMn : f (x *+ n) = f x *+ n N -- z-module opposite, as in mulNr : (- x) * y = - (x * y) The operator suffixes D, B are also used for the corresponding operations on nat, as in mulrDr : x *+ (m + n) = x *+ m + x *+ n.

Set Implicit Arguments.

Declare Scope ring_scope.
Delimit Scope ring_scope with R.
Local Open Scope ring_scope.

Reserved Notation "+%R" (at level 0).
Reserved Notation "-%R" (at level 0).
Reserved Notation "n %:R" (at level 1, left associativity, format "n %:R").
Reserved Notation "\0" (at level 0).
Reserved Notation "f \+ g" (at level 50, left associativity).
Reserved Notation "f \- g" (at level 50, left associativity).
Reserved Notation "\- f" (at level 35, f at level 35).

Reserved Notation "'{' 'additive' U '->' V '}'"
  (at level 0, U at level 98, V at level 99,
   format "{ 'additive' U -> V }").

Module Import Algebra.

#[short (type ="baseAddMagmaType")]
HB.structure Definition BaseAddMagma := {V of hasAdd V }.

Module BaseAddMagmaExports.
Bind Scope ring_scope with BaseAddMagma.sort.
End BaseAddMagmaExports.

Module ChoiceBaseAddMagmaExports.
Bind Scope ring_scope with ChoiceBaseAddMagma.sort.
End ChoiceBaseAddMagmaExports.

Local Notation "+%R" := (@add _) : function_scope.
Local Notation "x + y" := (add x y) : ring_scope.

Definition to_multiplicative := @id Type.

#[export ]
HB.instance Definition _ (V : choiceType ) := Choice.on (to_multiplicative V ).
#[export ]
HB.instance Definition _ (V : baseAddMagmaType ) :=
  hasMul.Build (to_multiplicative V ) (@add V ).

FIXME: HB.saturate

#[export ]
HB.instance Definition _ (V : ChoiceBaseAddMagma.type ) :=
  Magma.on (to_multiplicative V ).

Section BaseAddMagmaTheory.
Variables V : baseAddMagmaType.

Section ClosedPredicates.

Variable S : {pred V }.

Definition addr_closed := {in S &, ∀ u v, u + v \in S }.

End ClosedPredicates.
End BaseAddMagmaTheory.

#[short (type ="addMagmaType")]
HB.structure Definition AddMagma :=
  {V of BaseAddMagma_isAddMagma V & ChoiceBaseAddMagma V }.

Module AddMagmaExports.
Bind Scope ring_scope with AddMagma.sort.
End AddMagmaExports.

Section AddMagmaTheory.
Variables V : addMagmaType.

Lemma commuteT x y : @commute (to_multiplicative V) x y.

End AddMagmaTheory.

#[short (type ="addSemigroupType")]
HB.structure Definition AddSemigroup :=
  {V of AddMagma_isAddSemigroup V & AddMagma V }.

Module AddSemigroupExports.
Bind Scope ring_scope with AddSemigroup.sort.
End AddSemigroupExports.

#[export ]
HB.instance Definition _ (V : addSemigroupType ) :=
  Magma_isSemigroup.Build (to_multiplicative V ) addrA.

Section AddSemigroupTheory.
Variables V : addSemigroupType.

Lemma addrCA : @left_commutative V V +%R.

Lemma addrAC : @right_commutative V V +%R.

Lemma addrACA : @interchange V +%R +%R.

End AddSemigroupTheory.

#[short (type ="baseAddUMagmaType")]
HB.structure Definition BaseAddUMagma :=
  {V of hasZero V & BaseAddMagma V }.

Module BaseAddUMagmaExports.
Bind Scope ring_scope with BaseAddUMagma.sort.
End BaseAddUMagmaExports.

Module ChoiceBaseAddUMagmaExports.
Bind Scope ring_scope with ChoiceBaseAddUMagma.sort.
End ChoiceBaseAddUMagmaExports.

Local Notation "0" := (@zero _) : ring_scope.

Definition natmul (V : baseAddUMagmaType) (x : V) n : V := iterop n +%R x 0.
Arguments natmul : simpl never.

Local Notation "x *+ n" := (natmul x n) : ring_scope.

#[export ]
HB.instance Definition _ (V : baseAddUMagmaType ) :=
  hasOne.Build (to_multiplicative V ) (@zero V ).

FIXME: HB.saturate

#[export ]
HB.instance Definition _ (V : ChoiceBaseAddUMagma.type ) :=
  BaseUMagma.on (to_multiplicative V ).

Section BaseAddUMagmaTheory.
Variable V : baseAddUMagmaType.
Implicit Types x : V.

Lemma mulr0n x : x *+ 0 = 0.
Lemma mulr1n x : x *+ 1 = x.
Lemma mulr2n x : x *+ 2 = x + x.
Lemma mulrb x (b : bool) : x *+ b = (if b then x else 0).
Lemma mulrSS x n : x *+ n .+2 = x + x *+ n .+1.

Section ClosedPredicates.

Variable S : {pred V }.

Definition addumagma_closed := 0 \in S ∧ addr_closed S.

End ClosedPredicates.

End BaseAddUMagmaTheory.

#[warning ="-HB.no-new-instance"]
HB.instance Definition _ := BaseAddUMagma_isAddUMagma.Build V add0r.

#[short (type ="addUMagmaType")]
HB.structure Definition AddUMagma := {V of isAddUMagma V & Choice V }.

Lemma addr0 (V : addUMagmaType) : right_id (@zero V) add.

Local Notation "\sum_ ( i <- r | P ) F" := (\big [+%R /0]_(i <- r | P) F).
Local Notation "\sum_ ( m <= i < n ) F" := (\big [+%R /0]_(m ≤ i < n) F).
Local Notation "\sum_ ( i < n ) F" := (\big [+%R /0]_(i < n) F).
Local Notation "\sum_ ( i 'in' A ) F" := (\big [+%R /0]_(i in A) F).

Import Monoid.Theory.

#[export ]
HB.instance Definition _ (V : addUMagmaType ) :=
  Magma_isUMagma.Build (to_multiplicative V ) add0r (@addr0 V ).

Module AddUMagmaExports.
Bind Scope ring_scope with AddUMagma.sort.
End AddUMagmaExports.

#[short (type ="nmodType")]
HB.structure Definition Nmodule := {V of isNmodule V & Choice V }.

Module NmoduleExports.
Bind Scope ring_scope with Nmodule.sort.
End NmoduleExports.

#[export ]
HB.instance Definition _ (V : nmodType ) :=
  UMagma_isMonoid.Build (to_multiplicative V ) addrA.

#[export ]
HB.instance Definition _ (V : nmodType ) :=
  Monoid.isComLaw.Build V 0%R +%R addrA addrC add0r.

Section NmoduleTheory.

Variable V : nmodType.
Implicit Types x y : V.

Let G := to_multiplicative V.

addrA, addrC and add0r in the structure addr0 proved above

Lemma mulrS x n : x *+ n .+1 = x + (x *+ n ).

Lemma mulrSr x n : x *+ n .+1 = x *+ n + x.

Lemma mul0rn n : 0 *+ n = 0 :> V.

Lemma mulrnDl n : {morph (fun x ⇒ x *+ n ) : x y / x + y }.

Lemma mulrnDr x m n : x *+ (m + n ) = x *+ m + x *+ n.

Lemma mulrnA x m n : x *+ (m × n ) = x *+ m *+ n.

Lemma mulrnAC x m n : x *+ m *+ n = x *+ n *+ m.

Lemma iter_addr n x y : iter n (+%R x) y = x *+ n + y.

Lemma iter_addr_0 n x : iter n (+%R x) 0 = x *+ n.

Lemma sumrMnl I r P (F : I → V) n :
  \sum_(i <- r | P i ) F i *+ n = (\sum_(i <- r | P i ) F i ) *+ n.

Lemma sumrMnr x I r P (F : I → nat) :
  \sum_(i <- r | P i ) x *+ F i = x *+ (\sum_(i <- r | P i ) F i ).

Lemma sumr_const (I : finType) (A : pred I) x : \sum_(i in A ) x = x *+ #|A |.

Lemma sumr_const_nat m n x : \sum_(n ≤ i < m ) x = x *+ (m - n ).

End NmoduleTheory.
Notation nmod_closed := addumagma_closed.

#[short (type ="baseZmodType")]
HB.structure Definition BaseZmodule := {V of hasOpp V & BaseAddUMagma V }.

Module BaseZmodExports.
Bind Scope ring_scope with BaseZmodule.sort.
End BaseZmodExports.

Local Notation "-%R" := (@opp _) : ring_scope.
Local Notation "- x" := (opp x) : ring_scope.
Local Notation "x - y" := (x + - y) : ring_scope.
Local Notation "x *- n" := (- (x *+ n)) : ring_scope.

Section ClosedPredicates.

Variable (U : baseZmodType) (S : {pred U }).

Definition oppr_closed := {in S , ∀ u, - u \in S }.
Definition subr_closed := {in S &, ∀ u v, u - v \in S }.
Definition zmod_closed := 0 \in S ∧ subr_closed.

End ClosedPredicates.

#[short (type ="zmodType")]
HB.structure Definition Zmodule :=
  {V of BaseZmoduleNmodule_isZmodule V & BaseZmodule V & Nmodule V }.

Module ZmoduleExports.
Bind Scope ring_scope with Zmodule.sort.
End ZmoduleExports.

Lemma addrN (V : zmodType) : @right_inverse V V V 0 -%R +%R.

#[export ]
HB.instance Definition _ (V : baseZmodType ) :=
  hasInv.Build (to_multiplicative V ) (@opp V ).
#[export ]
HB.instance Definition _ (V : zmodType ) :=
  Monoid_isGroup.Build (to_multiplicative V ) addNr (@addrN V ).

Section ZmoduleTheory.

Variable V : zmodType.
Implicit Types x y : V.

Let G := to_multiplicative V.

Definition subrr := addrN.

Lemma addKr : @left_loop V V -%R +%R.
Lemma addNKr : @rev_left_loop V V -%R +%R.
Lemma addrK : @right_loop V V -%R +%R.
Lemma addrNK : @rev_right_loop V V -%R +%R.
Definition subrK := addrNK.
Lemma subKr x : involutive (fun y ⇒ x - y).
Lemma addrI : @right_injective V V V +%R.
Lemma addIr : @left_injective V V V +%R.
Lemma subrI : right_injective (fun x y ⇒ x - y).
Lemma subIr : left_injective (fun x y ⇒ x - y).
Lemma opprK : @involutive V -%R.
Lemma oppr_inj : @injective V V -%R.
Lemma oppr0 : -0 = 0 :> V.
Lemma oppr_eq0 x : (- x == 0) = (x == 0).

Lemma subr0 x : x - 0 = x.
Lemma sub0r x : 0 - x = - x.

Lemma opprB x y : - (x - y ) = y - x.

Lemma opprD : {morph -%R : x y / x + y : V }.

Lemma addrKA z x y : (x + z ) - (z + y ) = x - y.

Lemma subrKA z x y : (x - z ) + (z + y ) = x + y.

Lemma addr0_eq x y : x + y = 0 → - x = y.

Lemma subr0_eq x y : x - y = 0 → x = y.

Lemma subr_eq x y z : (x - z == y ) = (x == y + z ).

Lemma subr_eq0 x y : (x - y == 0) = (x == y ).

Lemma addr_eq0 x y : (x + y == 0) = (x == - y ).

Lemma eqr_opp x y : (- x == - y ) = (x == y ).

Lemma eqr_oppLR x y : (- x == y ) = (x == - y ).

Lemma mulNrn x n : (- x ) *+ n = x *- n.

Lemma mulrnBl n : {morph (fun x ⇒ x *+ n ) : x y / x - y }.

Lemma mulrnBr x m n : n ≤ m → x *+ (m - n ) = x *+ m - x *+ n.

Lemma sumrN I r P (F : I → V) :
  (\sum_(i <- r | P i ) - F i = - (\sum_(i <- r | P i ) F i )).

Lemma sumrB I r (P : pred I) (F1 F2 : I → V) :
  \sum_(i <- r | P i ) (F1 i - F2 i )
     = \sum_(i <- r | P i ) F1 i - \sum_(i <- r | P i ) F2 i.

Lemma telescope_sumr n m (f : nat → V) : n ≤ m →
  \sum_(n ≤ k < m ) (f k .+1 - f k ) = f m - f n.

Lemma telescope_sumr_eq n m (f u : nat → V) : n ≤ m →
    (∀ k, (n ≤ k < m)%N → u k = f k .+1 - f k ) →
  \sum_(n ≤ k < m ) u k = f m - f n.

Section ClosedPredicates.

Variable (S : {pred V }).

Lemma zmod_closedN : zmod_closed S → oppr_closed S.

Lemma zmod_closedD : zmod_closed S → addr_closed S.

Lemma zmod_closed0D : zmod_closed S → nmod_closed S.

End ClosedPredicates.

End ZmoduleTheory.

Arguments addrI {V} y [x1 x2].
Arguments addIr {V} x [x1 x2].
Arguments opprK {V}.
Arguments oppr_inj {V} [x1 x2].

Definition nmod_morphism (U V : baseAddUMagmaType) (f : U → V) : Prop :=
  (f 0 = 0) × {morph f : x y / x + y }.
#[deprecated(since="mathcomp 2.5.0", note="use `nmod_morphism` instead")]
Definition semi_additive := nmod_morphism.

Module isSemiAdditive.
#[deprecated(since="mathcomp 2.5.0",
             note="Use isNmodMorphism.Build instead.")]
Notation Build U V apply := (isNmodMorphism.Build U V apply) (only parsing).
End isSemiAdditive.

#[mathcomp (axiom ="nmod_morphism")]
HB.structure Definition Additive (U V : baseAddUMagmaType ) :=
  {f of isNmodMorphism U V f }.

Definition zmod_morphism (U V : zmodType) (f : U → V) :=
  {morph f : x y / x - y }.

#[deprecated(since="mathcomp 2.5.0", note="use `zmod_morphism` instead")]
Definition additive := zmod_morphism.

Module isAdditive.
#[deprecated(since="mathcomp 2.5.0",
             note="Use isZmodMorphism.Build instead.")]
Notation Build U V apply := (isZmodMorphism.Build U V apply) (only parsing).
End isAdditive.

Local Lemma raddf0 : apply 0 = 0.

Local Lemma raddfD : {morph apply : x y / x + y }.

Module AdditiveExports.
Notation "{ 'additive' U -> V }" := (Additive.type U%type V%type) : type_scope.
End AdditiveExports.

Section AdditiveTheory.
Variables (U V : baseAddUMagmaType) (f : {additive U → V }).

Lemma raddf0 : f 0 = 0.

Lemma raddfD :
  {morph f : x y / x + y }.

End AdditiveTheory.

Definition to_fmultiplicative U V :=
  @id (to_multiplicative U → to_multiplicative V ).

#[export ]
HB.instance Definition _ U V (f : {additive U → V }) :=
  isMultiplicative.Build (to_multiplicative U ) (to_multiplicative V )
    (to_fmultiplicative f ) (@raddfD _ _ f ).
#[export ]
HB.instance Definition _ (U V : baseAddUMagmaType ) (f : {additive U → V }) :=
  Multiplicative_isUMagmaMorphism.Build
    (to_multiplicative U ) (to_multiplicative V ) (to_fmultiplicative f )
    (@raddf0 _ _ f ).

Section LiftedAddMagma.
Variables (U : Type) (V : baseAddMagmaType).
Definition add_fun (f g : U → V) x := f x + g x.
End LiftedAddMagma.
Section LiftedNmod.
Variables (U : Type) (V : baseAddUMagmaType).
Definition null_fun of U : V := 0.
End LiftedNmod.
Section LiftedZmod.
Variables (U : Type) (V : baseZmodType).
Definition opp_fun (f : U → V) x := - f x.
Definition sub_fun (f g : U → V) x := f x - g x.
End LiftedZmod.

Arguments null_fun {_} V _ /.
Arguments add_fun {_ _} f g _ /.
Arguments opp_fun {_ _} f _ /.
Arguments sub_fun {_ _} f g _ /.

Local Notation "\0" := (null_fun _) : function_scope.
Local Notation "f \+ g" := (add_fun f g) : function_scope.
Local Notation "\- f" := (opp_fun f) : function_scope.
Local Notation "f \- g" := (sub_fun f g) : function_scope.

Section Nmod.
Variables (U V : addUMagmaType) (f : {additive U → V }).
Let g := to_fmultiplicative f.

Lemma raddf_eq0 x : injective f → (f x == 0) = (x == 0).

Lemma raddfMn n : {morph f : x / x *+ n }.

Lemma raddf_sum I r (P : pred I) E :
  f (\sum_(i <- r | P i ) E i) = \sum_(i <- r | P i ) f (E i).

Lemma can2_nmod_morphism f' : cancel f f' → cancel f' f → nmod_morphism f'.

#[deprecated(since="mathcomp 2.5.0", note="use `can2_nmod_morphism` instead")]
Definition can2_semi_additive := can2_nmod_morphism.

End Nmod.

Section Zmod.
Variables (U V : zmodType) (f : {additive U → V }).
Let g := to_fmultiplicative f.

Lemma raddfN : {morph f : x / - x }.

Lemma raddfB : {morph f : x y / x - y }.

Lemma raddf_inj : (∀ x, f x = 0 → x = 0) → injective f.

Lemma raddfMNn n : {morph f : x / x *- n }.

Lemma can2_zmod_morphism f' : cancel f f' → cancel f' f → zmod_morphism f'.

#[warning="-deprecated-since-mathcomp-2.5.0",
    deprecated(since="mathcomp 2.5.0", note="use `can2_zmod_morphism` instead")]
Definition can2_additive := can2_zmod_morphism.
End Zmod.

Section AdditiveTheory.
Section AddCFun.
Variables (U : baseAddUMagmaType) (V : nmodType).
Implicit Types (f g : {additive U → V }).

Fact add_fun_nmod_morphism f g : nmod_morphism (add_fun f g).
#[export ]
HB.instance Definition _ f g :=
  isNmodMorphism.Build U V (add_fun f g ) (add_fun_nmod_morphism f g ).

End AddCFun.

Section AddFun.
Variables (U V W : baseAddUMagmaType).
Variables (f : {additive V → W }) (g : {additive U → V }).

Fact idfun_is_nmod_morphism : nmod_morphism (@idfun U).
#[export ]
HB.instance Definition _ := isNmodMorphism.Build U U idfun
  idfun_is_nmod_morphism.

Fact comp_is_nmod_morphism : nmod_morphism (f \o g).
#[export ]
HB.instance Definition _ := isNmodMorphism.Build U W (f \o g )
  comp_is_nmod_morphism.

End AddFun.
Section AddFun.
Variables (U : baseAddUMagmaType) (V : addUMagmaType) (W : nmodType).
Variables (f g : {additive U → W }).

Fact null_fun_is_nmod_morphism : nmod_morphism (\0 : U → V).
#[export ]
HB.instance Definition _ :=
  isNmodMorphism.Build U V (\0 : U → V )
    null_fun_is_nmod_morphism.

End AddFun.

Section AddVFun.
Variables (U : baseAddUMagmaType) (V : zmodType).
Variables (f g : {additive U → V }).

Fact opp_is_zmod_morphism : zmod_morphism (-%R : V → V).
#[export ]
HB.instance Definition _ :=
  isZmodMorphism.Build V V -%R opp_is_zmod_morphism.

Fact opp_fun_is_zmod_morphism : nmod_morphism (\- f).
#[export ]
HB.instance Definition _ :=
  isNmodMorphism.Build U V (opp_fun f ) opp_fun_is_zmod_morphism.

Fact sub_fun_is_zmod_morphism :
  nmod_morphism (f \- g).
#[export ]
HB.instance Definition _ :=
  isNmodMorphism.Build U V (f \- g ) sub_fun_is_zmod_morphism.

End AddVFun.
End AdditiveTheory.

Mixins for stability properties

Structures for stability properties

#[short (type ="addrClosed")]
HB.structure Definition AddClosed V := {S of isAddClosed V S }.

#[short (type ="opprClosed")]
HB.structure Definition OppClosed V := {S of isOppClosed V S }.

#[short (type ="zmodClosed")]
HB.structure Definition ZmodClosed V := {S of OppClosed V S & AddClosed V S }.

Factories for stability properties

Definition to_pmultiplicative (T : Type) := @id {pred to_multiplicative T }.

#[export ]
HB.instance Definition _ (U : baseAddUMagmaType ) (S : addrClosed U ) :=
  isMulClosed.Build (to_multiplicative U ) (to_pmultiplicative S )
    (snd nmod_closed_subproof ).
#[export ]
HB.instance Definition _ (U : baseAddUMagmaType ) (S : addrClosed U ) :=
  isMul1Closed.Build (to_multiplicative U ) (to_pmultiplicative S )
    (fst nmod_closed_subproof ).
#[export ]
HB.instance Definition _ (U : zmodType ) (S : opprClosed U ) :=
  isInvClosed.Build (to_multiplicative U ) (to_pmultiplicative S )
    oppr_closed_subproof.

FIXME: HB.saturate

#[export ]
HB.instance Definition _ (U : zmodType ) (S : zmodClosed U ) :=
  InvClosed.on (to_pmultiplicative S ).

Section BaseAddUMagmaPred.
Variables (V : baseAddUMagmaType).

Section BaseAddUMagmaPred.
Variables S : addrClosed V.

Lemma rpred0 : 0 \in S.
Lemma rpredD : {in S &, ∀ u v, u + v \in S }.

Lemma rpred0D : addumagma_closed S.

Lemma rpredMn n : {in S , ∀ u, u *+ n \in S }.

Lemma rpred_sum I r (P : pred I) F :
  (∀ i, P i → F i \in S ) → \sum_(i <- r | P i ) F i \in S.

End BaseAddUMagmaPred.
End BaseAddUMagmaPred.

Section ZmodPred.
Variables (V : zmodType).

Section Opp.

Variable S : opprClosed V.

Lemma rpredNr : {in S , ∀ u, - u \in S }.

Lemma rpredN : {mono -%R : u / u \in S }.

End Opp.

Section Zmod.
Variables S : zmodClosed V.
Let T := to_pmultiplicative S.

Lemma rpredB : {in S &, ∀ u v, u - v \in S }.

Lemma rpredBC u v : u - v \in S = (v - u \in S ).

Lemma rpredMNn n: {in S , ∀ u, u *- n \in S }.

Lemma rpredDr x y : x \in S → (y + x \in S ) = (y \in S ).

Lemma rpredDl x y : x \in S → (x + y \in S ) = (y \in S ).

Lemma rpredBr x y : x \in S → (y - x \in S ) = (y \in S ).

Lemma rpredBl x y : x \in S → (x - y \in S ) = (y \in S ).

Lemma zmodClosedP : zmod_closed S.
End Zmod.
End ZmodPred.

#[short (type ="subBaseAddUMagma")]
HB.structure Definition SubBaseAddUMagma (V : baseAddUMagmaType ) S :=
  { U of SubChoice V S U & BaseAddUMagma U & isSubBaseAddUMagma V S U }.

#[short (type ="subAddUMagma")]
HB.structure Definition SubAddUMagma (V : addUMagmaType ) S :=
  { U of SubChoice V S U & AddUMagma U & isSubBaseAddUMagma V S U }.

#[short (type ="subNmodType")]
HB.structure Definition SubNmodule (V : nmodType ) S :=
  { U of SubChoice V S U & Nmodule U & isSubBaseAddUMagma V S U }.

Section subBaseAddUMagma.
Context (V : baseAddUMagmaType) (S : pred V) (U : subBaseAddUMagma S).
Notation val := (val : U → V).
#[export ]
HB.instance Definition _ := isNmodMorphism.Build U V val valD0_subproof.
Lemma valD : {morph val : x y / x + y }.
Lemma val0 : val 0 = 0.
End subBaseAddUMagma.

Let inU v Sv : U := Sub v Sv.
Let addU (u1 u2 : U) := inU (rpredD (valP u1) (valP u2)).
Let oneU := inU (fst addumagma_closed_subproof).

Lemma addrC : commutative addU.

Lemma add0r : left_id oneU addU.

Lemma valD0 : nmod_morphism (val : U → V).

Lemma addrA : associative (@add U).

#[short (type ="subZmodType")]
HB.structure Definition SubZmodule (V : zmodType ) S :=
  { U of SubChoice V S U & Zmodule U & isSubBaseAddUMagma V S U }.

Section zmod_morphism.
Context (V : zmodType) (S : pred V) (U : SubZmodule.type S).
Notation val := (val : U → V).
Lemma valB : {morph val : x y / x - y }.
Lemma valN : {morph val : x / - x }.
End zmod_morphism.

Fact valD0 : nmod_morphism (val : U → V).

Let inU v Sv : U := Sub v Sv.
Let oppU (u : U) := inU (rpredNr (valP u)).

Lemma addNr : left_inverse 0 oppU (@add U).

Module SubExports.

Notation "[ 'SubChoice_isSubNmodule' 'of' U 'by' <: ]" :=
  (SubChoice_isSubNmodule.Build _ _ U rpred0D)
  (at level 0, format "[ 'SubChoice_isSubNmodule' 'of' U 'by' <: ]")
  : form_scope.
Notation "[ 'SubNmodule_isSubZmodule' 'of' U 'by' <: ]" :=
  (SubNmodule_isSubZmodule.Build _ _ U (@rpredNr _ _))
  (at level 0, format "[ 'SubNmodule_isSubZmodule' 'of' U 'by' <: ]")
  : form_scope.
Notation "[ 'SubChoice_isSubZmodule' 'of' U 'by' <: ]" :=
  (SubChoice_isSubZmodule.Build _ _ U (zmodClosedP _))
  (at level 0, format "[ 'SubChoice_isSubZmodule' 'of' U 'by' <: ]")
  : form_scope.

End SubExports.

Module AllExports. End AllExports.

End Algebra.

Export AllExports.

Notation "0" := (@zero _) : ring_scope.
Notation "-%R" := (@opp _) : ring_scope.
Notation "- x" := (opp x) : ring_scope.
Notation "+%R" := (@add _) : function_scope.
Notation "x + y" := (add x y) : ring_scope.
Notation "x - y" := (add x (- y)) : ring_scope.
Arguments natmul : simpl never.
Notation "x *+ n" := (natmul x n) : ring_scope.
Notation "x *- n" := (opp (x *+ n)) : ring_scope.
Notation "s `_ i" := (seq.nth 0%R s%R i) : ring_scope.
Notation support := 0.-support.

Notation "1" := (@one _) : ring_scope.
Notation "- 1" := (opp 1) : ring_scope.

Notation "n %:R" := (natmul 1 n) : ring_scope.

Notation "\sum_ ( i <- r | P ) F" :=
  (\big [+%R /0%R]_(i <- r | P%B) F%R) : ring_scope.
Notation "\sum_ ( i <- r ) F" :=
  (\big [+%R /0%R]_(i <- r) F%R) : ring_scope.
Notation "\sum_ ( m <= i < n | P ) F" :=
  (\big [+%R /0%R]_(m ≤ i < n | P%B) F%R) : ring_scope.
Notation "\sum_ ( m <= i < n ) F" :=
  (\big [+%R /0%R]_(m ≤ i < n) F%R) : ring_scope.
Notation "\sum_ ( i | P ) F" :=
  (\big [+%R /0%R]_(i | P%B) F%R) : ring_scope.
Notation "\sum_ i F" :=
  (\big [+%R /0%R]_i F%R) : ring_scope.
Notation "\sum_ ( i : t | P ) F" :=
  (\big [+%R /0%R]_(i : t | P%B) F%R) (only parsing) : ring_scope.
Notation "\sum_ ( i : t ) F" :=
  (\big [+%R /0%R]_(i : t) F%R) (only parsing) : ring_scope.
Notation "\sum_ ( i < n | P ) F" :=
  (\big [+%R /0%R]_(i < n | P%B) F%R) : ring_scope.
Notation "\sum_ ( i < n ) F" :=
  (\big [+%R /0%R]_(i < n) F%R) : ring_scope.
Notation "\sum_ ( i 'in' A | P ) F" :=
  (\big [+%R /0%R]_(i in A | P%B) F%R) : ring_scope.
Notation "\sum_ ( i 'in' A ) F" :=
  (\big [+%R /0%R]_(i in A) F%R) : ring_scope.

Section FinFunBaseAddMagma.
Variable (aT : finType) (rT : baseAddMagmaType).
Implicit Types f g : {ffun aT → rT }.

Definition ffun_add f g := [ffun a ⇒ f a + g a ].

End FinFunBaseAddMagma.

Section FinFunAddMagma.
Variable (aT : finType) (rT : addMagmaType).
Implicit Types f g : {ffun aT → rT }.

Fact ffun_addrC : commutative (@ffun_add aT rT).

End FinFunAddMagma.

Section FinFunAddSemigroup.
Variable (aT : finType) (rT : addSemigroupType).
Implicit Types f g : {ffun aT → rT }.

Fact ffun_addrA : associative (@ffun_add aT rT).

End FinFunAddSemigroup.

Section FinFunBaseAddUMagma.
Variable (aT : finType) (rT : baseAddUMagmaType).
Implicit Types f g : {ffun aT → rT }.

Definition ffun_zero := [ffun a : aT ⇒ (0 : rT )].

End FinFunBaseAddUMagma.

Section FinFunAddUMagma.
Variable (aT : finType) (rT : addUMagmaType).
Implicit Types f g : {ffun aT → rT }.

Fact ffun_add0r : left_id (@ffun_zero aT rT) (@ffun_add aT rT).

End FinFunAddUMagma.

FIXME: HB.saturate

Section FinFunNmod.
Variable (aT : finType) (rT : nmodType).
Implicit Types f g : {ffun aT → rT }.

FIXME: HB.saturate

Lemma ffunMnE f n x : (f *+ n ) x = f x *+ n.

Section Sum.

Variables (I : Type) (r : seq I) (P : pred I) (F : I → {ffun aT → rT }).

Lemma sum_ffunE x : (\sum_(i <- r | P i ) F i ) x = \sum_(i <- r | P i ) F i x.

Lemma sum_ffun :
\sum_(i <- r | P i ) F i = [ffun x ⇒ \sum_(i <- r | P i ) F i x ].

End Sum.

End FinFunNmod.

Section FinFunZmod.

Variable (aT : finType) (rT : zmodType).
Implicit Types f g : {ffun aT → rT }.

Definition ffun_opp f := [ffun a ⇒ - f a ].

Fact ffun_addNr : left_inverse 0 ffun_opp +%R.

End FinFunZmod.

Section PairBaseAddMagma.
Variables U V : baseAddMagmaType.

Definition add_pair (a b : U × V) := (a .1 + b .1 , a .2 + b .2 ).

End PairBaseAddMagma.

Section PairAddMagma.
Variables U V : addMagmaType.

Fact pair_addrC : commutative (@add_pair U V).

End PairAddMagma.

Section PairAddSemigroup.
Variables U V : addSemigroupType.

Fact pair_addrA : associative (@add_pair U V).

End PairAddSemigroup.

Section PairBaseAddUMagma.
Variables U V : baseAddUMagmaType.

Definition pair_zero : U × V := (0, 0).

Fact fst_is_zmod_morphism : nmod_morphism (@fst U V).
Fact snd_is_zmod_morphism : nmod_morphism (@snd U V).

End PairBaseAddUMagma.

Section PairAddUMagma.
Variables U V : addUMagmaType.

Fact pair_add0r : left_id (@pair_zero U V) (@add_pair U V).

End PairAddUMagma.

FIXME: HB.saturate

/FIXME

Section PairZmodule.
Variables U V : zmodType.

Definition pair_opp (a : U × V) := (- a .1 , - a .2 ).

Fact pair_addNr : left_inverse 0 pair_opp +%R.

End PairZmodule.

zmodType structure on bool

nmodType structure on nat

Lemma natr0E : 0 = 0%N.
Lemma natrDE n m : n + m = (n + m)%N.
Definition natrE := (natr0E , natrDE ).