Module 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 div.
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:
addrClosed V == predicate closed under addition on V : basAddUMagmaType
The HB class is called AddClosed.
opprClosed V == predicate closed under opposite on V : baseZmodType
The HB class is called OppClosed.
zmodClosed V == predicate closed under addition and opposite and
containing 0 on V : baseZmodType
The HB class is called ZmodClosed.
The rpred* lemmas ensure that the set S remains stable under the specified
operations, provided the corresponding closedness predicate is satisfied.
This stability is crucial for constructing and reasoning about
substructures within algebraic hierarchies. For example:
- rpred0: Concludes 0 \in S if S is addrClosed.
- rpredD: Concludes x + y \in S if x \in S and y \in S and S is addrClosed.
- rpredN: Concludes -x \in S if x \in S and S is opprClosed.
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_morphism 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.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
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.
HB.mixin Record hasAdd V := {
add : V -> V -> V
}.
#[short(type="baseAddMagmaType")]
HB.structure Definition BaseAddMagma := {V of hasAdd V}.
Module BaseAddMagmaExports.
Bind Scope ring_scope with BaseAddMagma.sort.
End BaseAddMagmaExports.
HB.export BaseAddMagmaExports.
HB.structure Definition ChoiceBaseAddMagma := {V of BaseAddMagma V & Choice V}.
Module ChoiceBaseAddMagmaExports.
Bind Scope ring_scope with ChoiceBaseAddMagma.sort.
End ChoiceBaseAddMagmaExports.
HB.export 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).
#[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 &, forall u v, u + v \in S}.
End ClosedPredicates.
End BaseAddMagmaTheory.
HB.mixin Record BaseAddMagma_isAddMagma V & BaseAddMagma V := {
addrC : commutative (@add V)
}.
#[short(type="addMagmaType")]
HB.structure Definition AddMagma :=
{V of BaseAddMagma_isAddMagma V & ChoiceBaseAddMagma V}.
HB.factory Record isAddMagma V & Choice V := {
add : V -> V -> V;
addrC : commutative add
}.
HB.builders Context V & isAddMagma V.
HB.instance Definition _ := hasAdd.Build V add.
HB.instance Definition _ := BaseAddMagma_isAddMagma.Build V addrC.
HB.end.
Module AddMagmaExports.
Bind Scope ring_scope with AddMagma.sort.
End AddMagmaExports.
HB.export AddMagmaExports.
Section AddMagmaTheory.
Variables V : addMagmaType.
Lemma commuteT x y : @commute (to_multiplicative V) x y.
Proof.
exact/addrC. Qed.
End AddMagmaTheory.
HB.mixin Record AddMagma_isAddSemigroup V & AddMagma V := {
addrA : associative (@add V)
}.
#[short(type="addSemigroupType")]
HB.structure Definition AddSemigroup :=
{V of AddMagma_isAddSemigroup V & AddMagma V}.
HB.factory Record isAddSemigroup V & Choice V := {
add : V -> V -> V;
addrC : commutative add;
addrA : associative add
}.
HB.builders Context V & isAddSemigroup V.
HB.instance Definition _ := isAddMagma.Build V addrC.
HB.instance Definition _ := AddMagma_isAddSemigroup.Build V addrA.
HB.end.
Module AddSemigroupExports.
Bind Scope ring_scope with AddSemigroup.sort.
End AddSemigroupExports.
HB.export AddSemigroupExports.
#[export]
HB.instance Definition _ (V : addSemigroupType) :=
Magma_isSemigroup.Build (to_multiplicative V) addrA.
Section AddSemigroupTheory.
Variables V : addSemigroupType.
#[export]
HB.instance Definition _ := SemiGroup.isComLaw.Build V +%R addrA addrC.
Lemma addrCA : @left_commutative V V +%R
Lemma addrAC : @right_commutative V V +%R
Lemma addrACA : @interchange V +%R +%R
End AddSemigroupTheory.
HB.mixin Record hasZero V := {
zero : V
}.
#[short(type="baseAddUMagmaType")]
HB.structure Definition BaseAddUMagma :=
{V of hasZero V & BaseAddMagma V}.
Module BaseAddUMagmaExports.
Bind Scope ring_scope with BaseAddUMagma.sort.
End BaseAddUMagmaExports.
HB.export BaseAddUMagmaExports.
HB.structure Definition ChoiceBaseAddUMagma :=
{V of BaseAddUMagma V & Choice V}.
Module ChoiceBaseAddUMagmaExports.
Bind Scope ring_scope with ChoiceBaseAddUMagma.sort.
End ChoiceBaseAddUMagmaExports.
HB.export 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).
#[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
Proof.
by []. Qed.
Proof.
by []. Qed.
Proof.
by []. Qed.
Proof.
Proof.
by []. Qed.
Section ClosedPredicates.
Variable S : {pred V}.
Definition addumagma_closed := 0 \in S /\ addr_closed S.
End ClosedPredicates.
End BaseAddUMagmaTheory.
HB.mixin Record BaseAddUMagma_isAddUMagma V & BaseAddUMagma V := {
add0r : left_id zero (@add V)
}.
HB.factory Record isAddUMagma V & Choice V := {
add : V -> V -> V;
zero : V;
addrC : commutative add;
add0r : left_id zero add
}.
HB.builders Context V & isAddUMagma V.
HB.instance Definition _ := isAddMagma.Build V addrC.
HB.instance Definition _ := hasZero.Build V zero.
#[warning="-HB.no-new-instance"]
HB.instance Definition _ := BaseAddUMagma_isAddUMagma.Build V add0r.
HB.end.
#[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).
#[export]
HB.instance Definition _ (V : addUMagmaType) :=
Magma_isUMagma.Build (to_multiplicative V) add0r (@addr0 V).
HB.factory Record isNmodule V & Choice V := {
zero : V;
add : V -> V -> V;
addrA : associative add;
addrC : commutative add;
add0r : left_id zero add
}.
HB.builders Context V & isNmodule V.
HB.instance Definition _ := isAddUMagma.Build V addrC add0r.
HB.instance Definition _ := AddMagma_isAddSemigroup.Build V addrA.
HB.end.
Module AddUMagmaExports.
Bind Scope ring_scope with AddUMagma.sort.
End AddUMagmaExports.
HB.export 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.
HB.export NmoduleExports.
#[export]
HB.instance Definition _ (V : nmodType) :=
UMagma_isMonoid.Build (to_multiplicative V) addrA.
#[export]
HB.instance Definition _ (V : nmodType) :=
Monoid.isMonoidLaw.Build V 0%R +%R add0r (@addr0 V).
Section NmoduleTheory.
Variable V : nmodType.
Implicit Types x y : V.
Let G := to_multiplicative V.
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.
Proof.
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).
Proof.
End NmoduleTheory.
Notation nmod_closed := addumagma_closed.
HB.mixin Record hasOpp V := {
opp : V -> V
}.
#[short(type="baseZmodType")]
HB.structure Definition BaseZmodule := {V of hasOpp V & BaseAddUMagma V}.
Module BaseZmodExports.
Bind Scope ring_scope with BaseZmodule.sort.
End BaseZmodExports.
HB.export 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, forall u, - u \in S}.
Definition subr_closed := {in S &, forall u v, u - v \in S}.
End ClosedPredicates.
HB.mixin Record BaseZmoduleNmodule_isZmodule V & BaseZmodule V := {
addNr : left_inverse zero opp (@add V)
}.
#[short(type="zmodType")]
HB.structure Definition Zmodule :=
{V of BaseZmoduleNmodule_isZmodule V & BaseZmodule V & Nmodule V}.
HB.factory Record Nmodule_isZmodule V & Nmodule V := {
opp : V -> V;
addNr : left_inverse zero opp add
}.
HB.builders Context V & Nmodule_isZmodule V.
HB.instance Definition _ := hasOpp.Build V opp.
HB.instance Definition _ := BaseZmoduleNmodule_isZmodule.Build V addNr.
HB.end.
HB.factory Record isZmodule V & Choice V := {
zero : V;
opp : V -> V;
add : V -> V -> V;
addrA : associative add;
addrC : commutative add;
add0r : left_id zero add;
addNr : left_inverse zero opp add
}.
HB.builders Context V & isZmodule V.
HB.instance Definition _ := isNmodule.Build V addrA addrC add0r.
HB.instance Definition _ := Nmodule_isZmodule.Build V addNr.
HB.end.
Module ZmoduleExports.
Bind Scope ring_scope with Zmodule.sort.
End ZmoduleExports.
HB.export 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 subrKC x y : x + (y - x) = y.
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.
Proof.
Lemma telescope_sumr_eq n m (f u : nat -> V) : n <= m ->
(forall k, (n <= k < m)%N -> u k = f k.+1 - f k) ->
\sum_(n <= k < m) u k = f m - f n.
Proof.
Section ClosedPredicates.
Variable (S : {pred V}).
Definition zmod_closed := 0 \in S /\ subr_closed S.
Lemma zmod_closedN : zmod_closed -> oppr_closed S.
Proof.
Lemma zmod_closedD : zmod_closed -> addr_closed S.
Proof.
Lemma zmod_closed0D : zmod_closed -> nmod_closed S.
Proof.
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].
Arguments telescope_sumr_eq {V n m} f u.
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", use=nmod_morphism)]
Definition semi_additive := nmod_morphism.
HB.mixin Record isNmodMorphism (U V : baseAddUMagmaType) (apply : U -> V) := {
nmod_morphism_subproof : nmod_morphism apply;
}.
Module isSemiAdditive.
#[deprecated(since="mathcomp 2.5.0", use=isNmodMorphism.Build)]
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", use=zmod_morphism)]
Definition additive := zmod_morphism.
HB.factory Record isZmodMorphism (U V : zmodType) (apply : U -> V) := {
zmod_morphism_subproof : zmod_morphism apply;
}.
Module isAdditive.
#[deprecated(since="mathcomp 2.5.0", use=isZmodMorphism.Build)]
Notation Build U V apply := (isZmodMorphism.Build U V apply) (only parsing).
End isAdditive.
HB.builders Context U V apply & isZmodMorphism U V apply.
Local Lemma raddf0 : apply 0 = 0.
Proof.
Local Lemma raddfD : {morph apply : x y / x + y}.
Proof.
HB.instance Definition _ := isNmodMorphism.Build U V apply (conj raddf0 raddfD).
HB.end.
Module AdditiveExports.
Notation "{ 'additive' U -> V }" := (Additive.type U%type V%type) : type_scope.
End AdditiveExports.
HB.export AdditiveExports.
Section AdditiveTheory.
Variables (U V : baseAddUMagmaType) (f : {additive U -> V}).
Lemma raddf0 : f 0 = 0.
Proof.
Lemma raddfD :
{morph f : x y / x + y}.
Proof.
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 & 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).
Proof.
Lemma can2_nmod_morphism f' : cancel f f' -> cancel f' f -> nmod_morphism f'.
Proof.
#[deprecated(since="mathcomp 2.5.0", use=can2_nmod_morphism)]
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 : (forall 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'.
#[deprecated(since="mathcomp 2.5.0", use=can2_zmod_morphism)]
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 (f \+ g).
#[export]
HB.instance Definition _ f g :=
isNmodMorphism.Build U V (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).
Proof.
by []. Qed.
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).
Fact null_fun_is_nmod_morphism : nmod_morphism (\0 : U -> V).
Proof.
HB.instance Definition _ :=
isNmodMorphism.Build U V (\0 : U -> V) null_fun_is_nmod_morphism.
End AddFun.
Section AddVFun.
Variables (U : baseAddUMagmaType) (V : zmodType).
Fact opp_is_zmod_morphism : zmod_morphism (-%R : V -> V).
Proof.
HB.instance Definition _ := isZmodMorphism.Build V V -%R opp_is_zmod_morphism.
#[export]
HB.instance Definition _ (f : {additive U -> V}) :=
Additive.copy (\- f) (-%R \o f).
#[export]
HB.instance Definition _ (f g : {additive U -> V}) :=
Additive.copy (f \- g) (f \+ (\- g)).
End AddVFun.
End AdditiveTheory.
HB.mixin Record isAddClosed (V : baseAddUMagmaType) (S : {pred V}) := {
nmod_closed_subproof : addumagma_closed S
}.
HB.mixin Record isOppClosed (V : baseZmodType) (S : {pred V}) := {
oppr_closed_subproof : oppr_closed S
}.
#[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}.
HB.factory Record isZmodClosed (V : zmodType) (S : V -> bool) := {
zmod_closed_subproof : zmod_closed S
}.
HB.builders Context V S & isZmodClosed V S.
HB.instance Definition _ := isOppClosed.Build V S
(zmod_closedN zmod_closed_subproof).
HB.instance Definition _ := isAddClosed.Build V S
(zmod_closed0D zmod_closed_subproof).
HB.end.
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.
#[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.
Proof.
Proof.
Lemma rpred0D : addumagma_closed S.
Proof.
Lemma rpredMn n : {in S, forall u, u *+ n \in S}.
Proof.
Lemma rpred_sum I r (P : pred I) F :
(forall 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, forall u, - u \in S}.
Proof.
Lemma rpredN : {mono -%R: u / u \in S}.
Proof.
End Opp.
Section Zmod.
Variables S : zmodClosed V.
Let T := to_pmultiplicative S.
Lemma rpredB : {in S &, forall u v, u - v \in S}.
Lemma rpredBC u v : (u - v \in S) = (v - u \in S).
Lemma rpredMNn n: {in S, forall 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.
HB.mixin Record isSubBaseAddUMagma (V : baseAddUMagmaType) (S : pred V) U
& SubType V S U & BaseAddUMagma U := {
valD0_subproof : nmod_morphism (val : U -> V)
}.
#[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}
Proof.
Proof.
HB.factory Record SubChoice_isSubAddUMagma (V : addUMagmaType) S U
& SubChoice V S U := {
addumagma_closed_subproof : addumagma_closed S
}.
HB.builders Context V S U & SubChoice_isSubAddUMagma V S U.
HB.instance Definition _ := isAddClosed.Build V S addumagma_closed_subproof.
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.
HB.instance Definition _ := isAddUMagma.Build U addrC add0r.
Lemma valD0 : nmod_morphism (val : U -> V).
Proof.
HB.instance Definition _ := isSubBaseAddUMagma.Build V S U valD0.
HB.end.
HB.factory Record SubChoice_isSubNmodule (V : nmodType) S U
& SubChoice V S U := {
nmod_closed_subproof : nmod_closed S
}.
HB.builders Context V S U & SubChoice_isSubNmodule V S U.
HB.instance Definition _ :=
SubChoice_isSubAddUMagma.Build V S U nmod_closed_subproof.
Lemma addrA : associative (@add U).
HB.instance Definition _ := AddMagma_isAddSemigroup.Build U addrA.
HB.end.
#[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}
Proof.
Proof.
HB.factory Record isSubZmodule (V : zmodType) S U
& SubChoice V S U & Zmodule U := {
valB_subproof : zmod_morphism (val : U -> V)
}.
HB.builders Context V S U & isSubZmodule V S U.
Fact valD0 : nmod_morphism (val : U -> V).
Proof.
HB.instance Definition _ := isSubBaseAddUMagma.Build V S U valD0.
HB.end.
HB.factory Record SubNmodule_isSubZmodule (V : zmodType) S U
& SubNmodule V S U := {
oppr_closed_subproof : oppr_closed S
}.
HB.builders Context V S U & SubNmodule_isSubZmodule V S U.
HB.instance Definition _ := isOppClosed.Build V S oppr_closed_subproof.
Let inU v Sv : U := Sub v Sv.
Let oppU (u : U) := inU (rpredNr (valP u)).
HB.instance Definition _ := hasOpp.Build U oppU.
Lemma addNr : left_inverse 0 oppU (@add U).
HB.instance Definition _ := Nmodule_isZmodule.Build U addNr.
HB.end.
HB.factory Record SubChoice_isSubZmodule (V : zmodType) S U
& SubChoice V S U := {
zmod_closed_subproof : zmod_closed S
}.
HB.builders Context V S U & SubChoice_isSubZmodule V S U.
HB.instance Definition _ := isZmodClosed.Build V S zmod_closed_subproof.
HB.instance Definition _ :=
SubChoice_isSubNmodule.Build V S U nmod_closed_subproof.
HB.instance Definition _ :=
SubNmodule_isSubZmodule.Build V S U (@rpredNr _ _).
HB.end.
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.
HB.export SubExports.
Module AllExports. HB.reexport. 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].
HB.instance Definition _ := hasAdd.Build {ffun aT -> rT} ffun_add.
End FinFunBaseAddMagma.
Section FinFunAddMagma.
Variable (aT : finType) (rT : addMagmaType).
Implicit Types f g : {ffun aT -> rT}.
Fact ffun_addrC : commutative (@ffun_add aT rT).
HB.instance Definition _ :=
BaseAddMagma_isAddMagma.Build {ffun aT -> rT} ffun_addrC.
End FinFunAddMagma.
Section FinFunAddSemigroup.
Variable (aT : finType) (rT : addSemigroupType).
Implicit Types f g : {ffun aT -> rT}.
Fact ffun_addrA : associative (@ffun_add aT rT).
HB.instance Definition _ :=
AddMagma_isAddSemigroup.Build {ffun aT -> rT} ffun_addrA.
End FinFunAddSemigroup.
Section FinFunBaseAddUMagma.
Variable (aT : finType) (rT : baseAddUMagmaType).
Implicit Types f g : {ffun aT -> rT}.
Definition ffun_zero := [ffun a : aT => (0 : rT)].
HB.instance Definition _ := hasZero.Build {ffun aT -> rT} ffun_zero.
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).
HB.instance Definition _ :=
BaseAddUMagma_isAddUMagma.Build {ffun aT -> rT} ffun_add0r.
End FinFunAddUMagma.
HB.instance Definition _ (aT : finType) (rT : ChoiceBaseAddMagma.type) :=
BaseAddMagma.on {ffun aT -> rT}.
HB.instance Definition _ (aT : finType) (rT : ChoiceBaseAddUMagma.type) :=
BaseAddMagma.on {ffun aT -> rT}.
Section FinFunNmod.
Variable (aT : finType) (rT : nmodType).
Implicit Types f g : {ffun aT -> rT}.
HB.instance Definition _ := AddSemigroup.on {ffun aT -> rT}.
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].
HB.instance Definition _ := hasOpp.Build {ffun aT -> rT} ffun_opp.
Fact ffun_addNr : left_inverse 0 ffun_opp +%R.
HB.instance Definition _ := Nmodule_isZmodule.Build {ffun aT -> rT} ffun_addNr.
End FinFunZmod.
Section PairBaseAddMagma.
Variables U V : baseAddMagmaType.
Definition add_pair (a b : U * V) := (a.1 + b.1, a.2 + b.2).
HB.instance Definition _ := hasAdd.Build (U * V)%type add_pair.
End PairBaseAddMagma.
Section PairAddMagma.
Variables U V : addMagmaType.
Fact pair_addrC : commutative (@add_pair U V).
HB.instance Definition _ :=
BaseAddMagma_isAddMagma.Build (U * V)%type pair_addrC.
End PairAddMagma.
Section PairAddSemigroup.
Variables U V : addSemigroupType.
Fact pair_addrA : associative (@add_pair U V).
HB.instance Definition _ :=
AddMagma_isAddSemigroup.Build (U * V)%type pair_addrA.
End PairAddSemigroup.
Section PairBaseAddUMagma.
Variables U V : baseAddUMagmaType.
Definition pair_zero : U * V := (0, 0).
HB.instance Definition _ := hasZero.Build (U * V)%type pair_zero.
Fact fst_is_zmod_morphism : nmod_morphism (@fst U V)
Proof.
by []. Qed.
Proof.
by []. Qed.
HB.instance Definition _ :=
isNmodMorphism.Build _ _ (@fst U V) fst_is_zmod_morphism.
HB.instance Definition _ :=
isNmodMorphism.Build _ _ (@snd U V) snd_is_zmod_morphism.
End PairBaseAddUMagma.
Section PairAddUMagma.
Variables U V : addUMagmaType.
Fact pair_add0r : left_id (@pair_zero U V) (@add_pair U V).
HB.instance Definition _ :=
BaseAddUMagma_isAddUMagma.Build (U * V)%type pair_add0r.
End PairAddUMagma.
HB.instance Definition _ (U V : ChoiceBaseAddMagma.type) :=
BaseAddMagma.on (U * V)%type.
HB.instance Definition _ (U V : ChoiceBaseAddUMagma.type) :=
BaseAddMagma.on (U * V)%type.
HB.instance Definition _ (U V : nmodType) := AddSemigroup.on (U * V)%type.
Section PairZmodule.
Variables U V : zmodType.
Definition pair_opp (a : U * V) := (- a.1, - a.2).
HB.instance Definition _ := hasOpp.Build (U * V)%type pair_opp.
Fact pair_addNr : left_inverse 0 pair_opp +%R.
HB.instance Definition _ := Nmodule_isZmodule.Build (U * V)%type pair_addNr.
End PairZmodule.
HB.instance Definition _ := isZmodule.Build bool addbA addbC addFb addbb.
HB.instance Definition _ := isNmodule.Build nat addnA addnC add0n.
HB.instance Definition _ (V : nmodType) (x : V) :=
isNmodMorphism.Build nat V (natmul x) (mulr0n x, mulrnDr x).
Lemma natr0E : 0 = 0%N
Proof.
by []. Qed.
Proof.
by []. Qed.
HB.instance Definition _ p :=
isZmodule.Build 'I_p.+1 (@Zp_addA _) (@Zp_addC _) (@Zp_add0z _) (@Zp_addNz _).
Lemma ord1 : all_equal_to (0 : 'I_1).
Proof.
Lemma lshift0 m n : lshift m (0 : 'I_n.+1) = (0 : 'I_(n + m).+1).
Proof.
Lemma rshift1 n : @rshift 1 n =1 lift (0 : 'I_n.+1).
Proof.
Lemma split1 n i :
split (i : 'I_(1 + n)) = oapp (@inr _ _) (inl _ 0) (unlift 0 i).