Library mathcomp.algebra.ssralg
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq.
From mathcomp Require Import choice fintype finfun bigop prime binomial.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq.
From mathcomp Require Import choice fintype finfun bigop prime binomial.
The base hierarchy of algebraic structures
NB: See CONTRIBUTING.md for an introduction to HB concepts and commands.
Reference: Francois Garillot, Georges Gonthier, Assia Mahboubi, Laurence
Rideau, Packaging mathematical structures, TPHOLs 2009
This file defines the following algebraic structures:
nmodType == additive abelian monoid
The HB class is called Nmodule.
zmodType == additive abelian group (Nmodule with an opposite)
The HB class is called Zmodule.
semiRingType == non-commutative semi rings
(NModule with a multiplication)
The HB class is called SemiRing.
comSemiringType == commutative semi rings
The HB class is called ComSemiRing.
ringType == non-commutative rings (semi rings with an opposite)
The HB class is called Ring.
comRingType == commutative rings
The HB class is called ComRing.
lmodType R == module with left multiplication by external scalars
in the ring R
The HB class is called Lmodule.
lalgType R == left algebra, ring with scaling
that associates on the left
The HB class is called Lalgebra.
algType R == ring with scaling that associates both left and right
The HB class is called Algebra.
comAlgType R == commutative algType
The HB class is called ComAlgebra.
unitRingType == Rings whose units have computable inverses
The HB class is called UnitRing.
comUnitRingType == commutative UnitRing
The HB class is called ComUnitRing.
unitAlgType R == algebra with computable inverses
The HB class is called UnitAlgebra.
comUnitAlgType R == commutative UnitAlgebra
The HB class is called ComUnitAlgebra.
idomainType == integral, commutative, ring with partial inverses
The HB class is called IntegralDomain.
fieldType == commutative fields
The HB class is called Field.
decFieldType == fields with a decidable first order theory
The HB class is called DecidableField.
closedFieldType == algebraically closed fields
The HB class is called ClosedField.
and their joins with subType:
subNmodType V P == join of nmodType and subType (P : pred V) such
that val is semi_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.
subSemiRingType R P == join of semiRingType and subType (P : pred R)
such that val is a semiring morphism
The HB class is called SubSemiRing.
subComSemiRingType R P == join of comSemiRingType and subType (P : pred R)
such that val is a morphism
The HB class is called SubComSemiRing.
subRingType R P == join of ringType and subType (P : pred R)
such that val is a morphism
The HB class is called SubRing.
subComRingType R P == join of comRingType and subType (P : pred R)
such that val is a morphism
The HB class is called SubComRing.
subLmodType R V P == join of lmodType and subType (P : pred V)
such that val is scalable
The HB class is called SubLmodule.
subLalgType R V P == join of lalgType and subType (P : pred V)
such that val is linear
The HB class is called SubLalgebra.
subAlgType R V P == join of algType and subType (P : pred V)
such that val is linear
The HB class is called SubAlgebra.
subUnitRingType R P == join of unitRingType and subType (P : pred R)
such that val is a ring morphism
The HB class is called SubUnitRing.
subComUnitRingType R P == join of comUnitRingType and subType (P : pred R)
such that val is a ring morphism
The HB class is called SubComUnitRing.
subIdomainType R P == join of idomainType and subType (P : pred R)
such that val is a ring morphism
The HB class is called SubIntegralDomain.
subField R P == join of fieldType and subType (P : pred R)
such that val is a ring morphism
The HB class is called SubField.
Morphisms between the above structures:
Additive.type U V == semi additive (resp. additive) functions between
nmodType (resp. zmodType) instances U and V
RMorphism.type R S == semi ring (resp. ring) morphism between
semiRingType (resp. ringType) instances R and S
GRing.Scale.law R V == scaling morphism : R -> V -> V
The HB class is called GRing.Scale.Law.
Linear.type R U V == linear functions : U -> V
LRMorphism.type R A B == linear ring morphisms, i.e., algebra morphisms
Closedness predicates for the algebraic structures:
opprClosed V == predicate closed under opposite on V : zmodType
The HB class is called OppClosed.
addrClosed V == predicate closed under addition on V : nmodType
The HB class is called AddClosed.
zmodClosed V == predicate closed under opposite and addition on V
The HB class is called ZmodClosed.
mulr2Closed R == predicate closed under multiplication on R : semiRingType
The HB class is called Mul2Closed.
mulrClosed R == predicate closed under multiplication and for 1
The HB class is called MulClosed.
smulClosed R == predicate closed under multiplication and for -1
The HB class is called SmulClosed.
semiring2Closed R == predicate closed under addition and multiplication
The HB class is called Semiring2Closed.
semiringClosed R == predicate closed under semiring operations
The HB class is called SemiringClosed.
subringClosed R == predicate closed under ring operations
The HB class is called SubringClosed.
divClosed R == predicate closed under division
The HB class is called DivClosed.
sdivClosed R == predicate closed under division and opposite
The HB class is called SdivClosed.
submodClosed R == predicate closed under lmodType operations
The HB class is called SubmodClosed.
subalgClosed R == predicate closed under lalgType operations
The HB class is called SubalgClosed.
divringClosed R == predicate closed under unitRing operations
The HB class is called DivringClosed.
divalgClosed R S == predicate closed under (S : unitAlg R) operations
The HB class is called DivalgClosed.
Canonical properties of the algebraic structures:
nmodType (additive abelian monoids):
0 == the zero (additive identity) of a Nmodule x + y == the sum of x and y (in a Nmodule) 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 Zmodule (cf bigop.v) e`_i == nth 0 e i, when e : seq M and M has a zmodType structure support f == 0.-support f, i.e., [pred x | f x != 0] addr_closed S <-> collective predicate S is closed under finite sums (0 and x + y in S, for x, y in S) [SubChoice_isSubNmodule of U by <: ] == nmodType mixin for a subType whose base type is a nmodType and whose predicate's is a nmodClosedzmodType (additive abelian groups):
- x == the opposite (additive inverse) of x
SemiRing (non-commutative semirings):
R^c == the converse Ring for R: R^c is convertible to R but when R has a canonical ringType structure R^c has the converse one: if x y : R^c, then x * y = (y : R) * (x : R) 1 == the multiplicative identity element of a Ring n%:R == the ring image of an n in nat; this is just notation for 1 *+ n, so 1%:R is convertible to 1 and 2%:R to 1 + 1 <number> == <number>%:R with <number> a sequence of digits x * y == the ring product of x and y \prod_<range> e == iterated product for a ring (cf bigop.v) x ^+ n == x to the nth power with n in nat (non-negative), i.e., x * (x * .. (x * x)..) (n factors); x ^+ 1 is thus convertible to x, and x ^+ 2 to x * x GRing.comm x y <-> x and y commute, i.e., x * y = y * x GRing.lreg x <-> x if left-regular, i.e., *%R x is injective GRing.rreg x <-> x if right-regular, i.e., *%R x is injective [char R] == the characteristic of R, defined as the set of prime numbers p such that p%:R = 0 in R The set [char R] has at most one element, and is implemented as a pred_nat collective predicate (see prime.v); thus the statement p \in [char R] can be read as `R has characteristic p', while [char R] =i pred0 means `R has characteristic 0' when R is a field. Frobenius_aut chRp == the Frobenius automorphism mapping x in R to x ^+ p, where chRp : p \in [char R] is a proof that R has (non-zero) characteristic p mulr_closed S <-> collective predicate S is closed under finite products (1 and x * y in S for x, y in S) semiring_closed S <-> collective predicate S is closed under semiring operations (0, 1, x + y and x * y in S) [SubNmodule_isSubSemiRing of R by <: ] == [SubChoice_isSubSemiRing of R by <: ] == semiRingType mixin for a subType whose base type is a semiRingType and whose predicate's is a semiringClosedRing (non-commutative rings):
GRing.sign R b := (-1) ^+ b in R : ringType, with b : bool This is a parsing-only helper notation, to be used for defining more specific instances. smulr_closed S <-> collective predicate S is closed under products and opposite (-1 and x * y in S for x, y in S) subring_closed S <-> collective predicate S is closed under ring operations (1, x - y and x * y in S) [SubZmodule_isSubRing of R by <: ] == [SubChoice_isSubRing of R by <: ] == ringType mixin for a subType whose base type is a ringType and whose predicate's is a subringClosedComSemiRing (commutative SemiRings):
[SubNmodule_isSubComSemiRing of R by <: ] == [SubChoice_isSubComSemiRing of R by <: ] == comSemiRingType mixin for a subType whose base type is a comSemiRingType and whose predicate's is a semiringClosedComRing (commutative Rings):
[SubZmodule_isSubComRing of R by <: ] == [SubChoice_isSubComRing of R by <: ] == comRingType mixin for a subType whose base type is a comRingType and whose predicate's is a subringClosedUnitRing (Rings whose units have computable inverses):
x \is a GRing.unit <=> x is a unit (i.e., has an inverse) x^-1 == the ring inverse of x, if x is a unit, else x x / y == x divided by y (notation for x * y^-1) x ^- n := notation for (x ^+ n)^-1, the inverse of x ^+ n invr_closed S <-> collective predicate S is closed under inverse divr_closed S <-> collective predicate S is closed under division (1 and x / y in S) sdivr_closed S <-> collective predicate S is closed under division and opposite (-1 and x / y in S, for x, y in S) divring_closed S <-> collective predicate S is closed under unitRing operations (1, x - y and x / y in S) [SubRing_isSubUnitRing of R by <: ] == [SubChoice_isSubUnitRing of R by <: ] == unitRingType mixin for a subType whose base type is a unitRingType and whose predicate's is a divringClosed and whose ring structure is compatible with the base type'sComUnitRing (commutative rings with computable inverses):
[SubChoice_isSubComUnitRing of R by <: ] == comUnitRingType mixin for a subType whose base type is a comUnitRingType and whose predicate's is a divringClosed and whose ring structure is compatible with the base type'sIntegralDomain (integral, commutative, ring with partial inverses):
[SubComUnitRing_isSubIntegralDomain R by <: ] == [SubChoice_isSubIntegralDomain R by <: ] == mixin axiom for a idomain subTypeField (commutative fields):
GRing.Field.axiom inv == field axiom: x != 0 -> inv x * x = 1 for all x This is equivalent to the property above, but does not require a unitRingType as inv is an explicit argument. [SubIntegralDomain_isSubField of R by <: ] == mixin axiom for a field subTypeDecidableField (fields with a decidable first order theory):
GRing.term R == the type of formal expressions in a unit ring R with formal variables 'X_k, k : nat, and manifest constants x%:T, x : R The notation of all the ring operations is redefined for terms, in scope %T. GRing.formula R == the type of first order formulas over R; the %T scope binds the logical connectives /\, \/, ~, ==>, ==, and != to formulae; GRing.True/False and GRing.Bool b denote constant formulae, and quantifiers are written 'forall/'exists 'X_k, f GRing.Unit x tests for ring units GRing.If p_f t_f e_f emulates if-then-else GRing.Pick p_f t_f e_f emulates fintype.pick foldr GRing.Exists/Forall q_f xs can be used to write iterated quantifiers GRing.eval e t == the value of term t with valuation e : seq R (e maps 'X_i to e`_i) GRing.same_env e1 e2 <-> environments e1 and e2 are extensionally equal GRing.qf_form f == f is quantifier-free GRing.holds e f == the intuitionistic CiC interpretation of the formula f holds with valuation e GRing.qf_eval e f == the value (in bool) of a quantifier-free f GRing.sat e f == valuation e satisfies f (only in a decField) GRing.sol n f == a sequence e of size n such that e satisfies f, if one exists, or [:: ] if there is no such e 'exists 'X_i, u1 == 0 /\ ... /\ u_m == 0 /\ v1 != 0 ... /\ v_n != 0Lmodule (module with left multiplication by external scalars).
a *: v == v scaled by a, when v is in an Lmodule V and a is in the scalar Ring of V scaler_closed S <-> collective predicate S is closed under scaling linear_closed S <-> collective predicate S is closed under linear combinations (a *: u + v in S when u, v in S) submod_closed S <-> collective predicate S is closed under lmodType operations (0 and a *: u + v in S) [SubZmodule_isSubLmodule of V by <: ] == [SubChoice_isSubLmodule of V by <: ] == mixin axiom for a subType of an lmodTypeLalgebra (left algebra, ring with scaling that associates on the left):
R^o == the regular algebra of R: R^o is convertible to R, but when R has a ringType structure then R^o extends it to an lalgType structure by letting R act on itself: if x : R and y : R^o then x *: y = x * (y : R) k%:A == the image of the scalar k in an L-algebra; this is simply notation for k *: 1 subalg_closed S <-> collective predicate S is closed under lalgType operations (1, a *: u + v and u * v in S) [lalgMixin of V by <: ] == mixin axiom for a subType of an lalgType [SubRing_SubLmodule_isSubLalgebra of V by <: ] == [SubChoice_isSubLalgebra of V by <: ] == mixin axiom for a subType of an lalgTypeAlgebra (ring with scaling that associates both left and right):
[SubLalgebra_isSubAlgebra of V by <: ] == [SubChoice_isSubAlgebra of V by <: ] == mixin axiom for a subType of an algTypeUnitAlgebra (algebra with computable inverses):
divalg_closed S <-> collective predicate S is closed under all unitAlgType operations (1, a *: u + v and u / v are in S fo u, v in S) In addition to this structure hierarchy, we also develop a separate, parallel hierarchy for morphisms linking these structures:Additive (semi additive or additive functions):
semi_additive f <-> f of type U -> V is semi additive, 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} additive f <-> f of type U -> V is additive, i.e., f maps the Zmodule structure of U to that of V, 0 to 0,- to - and + to + (equivalently, binary - to -)
RMorphism (semiring or ring morphisms):
multiplicative f <-> f of type R -> S is multiplicative, i.e., f maps 1 and * in R to 1 and * in S, respectively R ans S must have canonical semiRingType instances {rmorphism R -> S} == the interface type for semiring morphisms; both R and S must have semiRingType instances When both R and S have ringType instances, it is a ring morphism.- > If R and S are UnitRings the f also maps units to units and inverses of units to inverses; if R is a field then f is a field isomorphism between R and its image.
- > Additive properties (raddf_suffix, see below) are duplicated and specialised for RMorphism (as rmorph_suffix). This allows more precise rewriting and cleaner chaining: although raddf lemmas will recognize RMorphism functions, the converse will not hold (we cannot add reverse inheritance rules because of incomplete backtracking in the Canonical Projection unification), so one would have to insert a /= every time one switched from additive to multiplicative rules.
Linear (linear functions):
scalable f <-> f of type U -> V is scalable, i.e., f morphs scaling on U to scaling on V, a *: _ to a *: _ U and V must both have lmodType R structures, for the same ringType R. scalable_for s f <-> f is scalable for scaling operator s, i.e., f morphs a *: _ to s a _; the range of f only need to be a zmodType The scaling operator s should be one of *:%R (see scalable, above), *%R or a combination nu \; *%R or nu \; *:%R with nu : {rmorphism _}; otherwise some of the theory (e.g., the linearZ rule) will not apply. linear f <-> f of type U -> V is linear, i.e., f morphs linear combinations a *: u + v in U to similar linear combinations in V; U and V must both have lmodType R structures, for the same ringType R := forall a, {morph f: u v / a *: u + v} scalar f <-> f of type U -> R is a scalar function, i.e., f (a *: u + v) = a * f u + f v linear_for s f <-> f is linear for the scaling operator s, i.e., f (a *: u + v) = s a (f u) + f v The range of f only needs to be a zmodType, but s MUST be of the form described in the scalable_for paragraph above for this predicate to type check. lmorphism f <-> f is both additive and scalable This is in fact equivalent to linear f, although somewhat less convenient to prove. lmorphism_for s f <-> f is both additive and scalable for s {linear U -> V} == the interface type for linear functions, i.e., a Structure that encapsulates the linear property for functions f : U -> V; both U and V must have lmodType R structures, for the same R {scalar U} == the interface type for scalar functions, of type U -> R where U has an lmodType R structure {linear U -> V | s} == the interface type for functions linear for s (a *: u)%Rlin == transient forms that simplify to a *: u, a * u, (a * u)%Rlin nu a *: u, and nu a * u, respectively, and are (a *:^nu u)%Rlin created by rewriting with the linearZ lemma (a *^nu u)%Rlin The forms allows the RHS of linearZ to be matched reliably, using the GRing.Scale.law structure.- > Similarly to Ring morphisms, additive properties are specialized for linear functions.
- > Although {scalar U} is convertible to {linear U -> R^o}, it does not actually use R^o, so that rewriting preserves the canonical structure of the range of scalar functions.
- > The generic linearZ lemma uses a set of bespoke interface structures to ensure that both left-to-right and right-to-left rewriting work even in the presence of scaling functions that simplify non-trivially (e.g., idfun \; *%R). Because most of the canonical instances and projections are coercions the machinery will be mostly invisible (with only the {linear ...} structure and %Rlin notations showing), but users should beware that in (a *: f u)%Rlin, a actually occurs in the f u subterm.
- > The simpler linear_LR, or more specialized linearZZ and scalarZ rules should be used instead of linearZ if there are complexity issues, as well as for explicit forward and backward application, as the main parameter of linearZ is a proper sub-interface of {linear fUV | s}.
LRMorphism (linear ring morphisms, i.e., algebra morphisms):
lrmorphism f <-> f of type A -> B is a linear Ring (Algebra) morphism: f is both additive, multiplicative and scalable; A and B must both have lalgType R canonical structures, for the same ringType R lrmorphism_for s f <-> f a linear Ring morphism for the scaling operator s: f is additive, multiplicative and scalable for s; A must be an lalgType R, but B only needs to have a ringType structure {lrmorphism A -> B} == the interface type for linear morphisms, i.e., a Structure that encapsulates the lrmorphism property for functions f : A -> B; both A and B must have lalgType R structures, for the same R {lrmorphism A -> B | s} == the interface type for morphisms linear for s- > Linear and rmorphism properties do not need to be specialized for as we supply inheritance join instances in both directions.
Set Implicit Arguments.
Declare Scope ring_scope.
Declare Scope term_scope.
Declare Scope linear_ring_scope.
Reserved Notation "+%R" (at level 0).
Reserved Notation "-%R" (at level 0).
Reserved Notation "*%R" (at level 0, format " *%R").
Reserved Notation "*:%R" (at level 0, format " *:%R").
Reserved Notation "n %:R" (at level 2, left associativity, format "n %:R").
Reserved Notation "k %:A" (at level 2, left associativity, format "k %:A").
Reserved Notation "[ 'char' F ]" (at level 0, format "[ 'char' F ]").
Reserved Notation "x %:T" (at level 2, left associativity, format "x %:T").
Reserved Notation "''X_' i" (at level 8, i at level 2, format "''X_' i").
Patch for recurring Coq parser bug: Coq seg faults when a level 200
notation is used as a pattern.
Reserved Notation "''exists' ''X_' i , f"
(at level 199, i at level 2, right associativity,
format "'[hv' ''exists' ''X_' i , '/ ' f ']'").
Reserved Notation "''forall' ''X_' i , f"
(at level 199, i at level 2, right associativity,
format "'[hv' ''forall' ''X_' i , '/ ' f ']'").
Reserved Notation "x ^f" (at level 2, left associativity, format "x ^f").
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 "a \*o f" (at level 40).
Reserved Notation "a \o* f" (at level 40).
Reserved Notation "a \*: f" (at level 40).
Reserved Notation "f \* g" (at level 40, left associativity).
Reserved Notation "'{' 'additive' U '->' V '}'"
(at level 0, U at level 98, V at level 99,
format "{ 'additive' U -> V }").
Reserved Notation "'{' 'rmorphism' U '->' V '}'"
(at level 0, U at level 98, V at level 99,
format "{ 'rmorphism' U -> V }").
Reserved Notation "'{' 'lrmorphism' U '->' V '|' s '}'"
(at level 0, U at level 98, V at level 99,
format "{ 'lrmorphism' U -> V | s }").
Reserved Notation "'{' 'lrmorphism' U '->' V '}'"
(at level 0, U at level 98, V at level 99,
format "{ 'lrmorphism' U -> V }").
Reserved Notation "'{' 'linear' U '->' V '|' s '}'"
(at level 0, U at level 98, V at level 99,
format "{ 'linear' U -> V | s }").
Reserved Notation "'{' 'linear' U '->' V '}'"
(at level 0, U at level 98, V at level 99,
format "{ 'linear' U -> V }").
Declare Scope ring_scope.
Delimit Scope ring_scope with R.
Declare Scope term_scope.
Delimit Scope term_scope with T.
Local Open Scope ring_scope.
Module Import GRing.
Import Monoid.Theory.
#[short(type="nmodType")]
HB.structure Definition Nmodule := {V of isNmodule V & Choice V}.
Module NmodExports.
Bind Scope ring_scope with Nmodule.sort.
#[deprecated(since="mathcomp 2.0.0",
note="Use GRing.Nmodule.clone instead.")]
Notation "[ 'nmodType' 'of' T 'for' cT ]" := (Nmodule.clone T cT)
(at level 0, format "[ 'nmodType' 'of' T 'for' cT ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0",
note="Use GRing.Nmodule.clone instead.")]
Notation "[ 'nmodType' 'of' T ]" := (Nmodule.clone T _)
(at level 0, format "[ 'nmodType' 'of' T ]") : form_scope.
End NmodExports.
Definition natmul V x n := nosimpl iterop _ n +%R x (@zero V).
Section NmoduleTheory.
Variable V : nmodType.
Implicit Types x y : V.
Lemma addr0 : @right_id V V 0 +%R.
#[export]
HB.instance Definition _ := Monoid.isComLaw.Build V 0 +%R addrA addrC add0r.
Lemma addrCA : @left_commutative V V +%R.
Lemma addrAC : @right_commutative V V +%R.
Lemma addrACA : @interchange V +%R +%R.
Lemma mulr0n x : x *+ 0 = 0.
Lemma mulr1n x : x *+ 1 = x.
Lemma mulr2n x : x *+ 2 = x + x.
Lemma mulrS x n : x *+ n.+1 = x + x *+ n.
Lemma mulrSr x n : x *+ n.+1 = x *+ n + x.
Lemma mulrb x (b : bool) : x *+ b = (if b then x else 0).
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).
Section ClosedPredicates.
Variable S : {pred V}.
Definition addr_closed := 0 \in S ∧ {in S &, ∀ u v, u + v \in S}.
End ClosedPredicates.
End NmoduleTheory.
#[short(type="zmodType")]
HB.structure Definition Zmodule := {V of Nmodule_isZmodule V & Nmodule V}.
Module ZmodExports.
Bind Scope ring_scope with Zmodule.sort.
#[deprecated(since="mathcomp 2.0.0", note="use GRing.isZmodule.Build instead")]
Notation ZmodMixin V := (isZmodule.Build V).
#[deprecated(since="mathcomp 2.0.0", note="Use GRing.Zmodule.clone instead.")]
Notation "[ 'zmodType' 'of' T 'for' cT ]" := (Zmodule.clone T cT)
(at level 0, format "[ 'zmodType' 'of' T 'for' cT ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use GRing.Zmodule.clone instead.")]
Notation "[ 'zmodType' 'of' T ]" := (Zmodule.clone T _)
(at level 0, format "[ 'zmodType' 'of' T ]") : form_scope.
End ZmodExports.
Section ZmoduleTheory.
Variable V : zmodType.
Implicit Types x y : V.
Lemma addrN : @right_inverse V V V 0 -%R +%R.
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}.
Definition oppr_closed := {in S, ∀ u, - u \in S}.
Definition subr_2closed := {in S &, ∀ u v, u - v \in S}.
Definition zmod_closed := 0 \in S ∧ subr_2closed.
Lemma zmod_closedN : zmod_closed → oppr_closed.
Lemma zmod_closedD : zmod_closed → addr_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].
Arguments telescope_sumr_eq {V n m} f u.
#[short(type="semiRingType")]
HB.structure Definition SemiRing := { R of Nmodule_isSemiRing R & Nmodule R }.
Module SemiRingExports.
Bind Scope ring_scope with SemiRing.sort.
#[deprecated(since="mathcomp 2.0.0", note="Use GRing.SemiRing.clone instead.")]
Notation "[ 'semiRingType' 'of' T 'for' cT ]" := (SemiRing.clone T cT)
(at level 0, format "[ 'semiRingType' 'of' T 'for' cT ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use GRing.SemiRing.clone instead.")]
Notation "[ 'semiRingType' 'of' T ]" := (SemiRing.clone T _)
(at level 0, format "[ 'semiRingType' 'of' T ]") : form_scope.
End SemiRingExports.
Definition exp R x n := nosimpl iterop _ n (@mul R) x (@one R).
Definition comm R x y := @mul R x y = mul y x.
Definition lreg R x := injective (@mul R x).
Definition rreg R x := injective ((@mul R)^~ x).
(at level 199, i at level 2, right associativity,
format "'[hv' ''exists' ''X_' i , '/ ' f ']'").
Reserved Notation "''forall' ''X_' i , f"
(at level 199, i at level 2, right associativity,
format "'[hv' ''forall' ''X_' i , '/ ' f ']'").
Reserved Notation "x ^f" (at level 2, left associativity, format "x ^f").
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 "a \*o f" (at level 40).
Reserved Notation "a \o* f" (at level 40).
Reserved Notation "a \*: f" (at level 40).
Reserved Notation "f \* g" (at level 40, left associativity).
Reserved Notation "'{' 'additive' U '->' V '}'"
(at level 0, U at level 98, V at level 99,
format "{ 'additive' U -> V }").
Reserved Notation "'{' 'rmorphism' U '->' V '}'"
(at level 0, U at level 98, V at level 99,
format "{ 'rmorphism' U -> V }").
Reserved Notation "'{' 'lrmorphism' U '->' V '|' s '}'"
(at level 0, U at level 98, V at level 99,
format "{ 'lrmorphism' U -> V | s }").
Reserved Notation "'{' 'lrmorphism' U '->' V '}'"
(at level 0, U at level 98, V at level 99,
format "{ 'lrmorphism' U -> V }").
Reserved Notation "'{' 'linear' U '->' V '|' s '}'"
(at level 0, U at level 98, V at level 99,
format "{ 'linear' U -> V | s }").
Reserved Notation "'{' 'linear' U '->' V '}'"
(at level 0, U at level 98, V at level 99,
format "{ 'linear' U -> V }").
Declare Scope ring_scope.
Delimit Scope ring_scope with R.
Declare Scope term_scope.
Delimit Scope term_scope with T.
Local Open Scope ring_scope.
Module Import GRing.
Import Monoid.Theory.
#[short(type="nmodType")]
HB.structure Definition Nmodule := {V of isNmodule V & Choice V}.
Module NmodExports.
Bind Scope ring_scope with Nmodule.sort.
#[deprecated(since="mathcomp 2.0.0",
note="Use GRing.Nmodule.clone instead.")]
Notation "[ 'nmodType' 'of' T 'for' cT ]" := (Nmodule.clone T cT)
(at level 0, format "[ 'nmodType' 'of' T 'for' cT ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0",
note="Use GRing.Nmodule.clone instead.")]
Notation "[ 'nmodType' 'of' T ]" := (Nmodule.clone T _)
(at level 0, format "[ 'nmodType' 'of' T ]") : form_scope.
End NmodExports.
Definition natmul V x n := nosimpl iterop _ n +%R x (@zero V).
Section NmoduleTheory.
Variable V : nmodType.
Implicit Types x y : V.
Lemma addr0 : @right_id V V 0 +%R.
#[export]
HB.instance Definition _ := Monoid.isComLaw.Build V 0 +%R addrA addrC add0r.
Lemma addrCA : @left_commutative V V +%R.
Lemma addrAC : @right_commutative V V +%R.
Lemma addrACA : @interchange V +%R +%R.
Lemma mulr0n x : x *+ 0 = 0.
Lemma mulr1n x : x *+ 1 = x.
Lemma mulr2n x : x *+ 2 = x + x.
Lemma mulrS x n : x *+ n.+1 = x + x *+ n.
Lemma mulrSr x n : x *+ n.+1 = x *+ n + x.
Lemma mulrb x (b : bool) : x *+ b = (if b then x else 0).
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).
Section ClosedPredicates.
Variable S : {pred V}.
Definition addr_closed := 0 \in S ∧ {in S &, ∀ u v, u + v \in S}.
End ClosedPredicates.
End NmoduleTheory.
#[short(type="zmodType")]
HB.structure Definition Zmodule := {V of Nmodule_isZmodule V & Nmodule V}.
Module ZmodExports.
Bind Scope ring_scope with Zmodule.sort.
#[deprecated(since="mathcomp 2.0.0", note="use GRing.isZmodule.Build instead")]
Notation ZmodMixin V := (isZmodule.Build V).
#[deprecated(since="mathcomp 2.0.0", note="Use GRing.Zmodule.clone instead.")]
Notation "[ 'zmodType' 'of' T 'for' cT ]" := (Zmodule.clone T cT)
(at level 0, format "[ 'zmodType' 'of' T 'for' cT ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use GRing.Zmodule.clone instead.")]
Notation "[ 'zmodType' 'of' T ]" := (Zmodule.clone T _)
(at level 0, format "[ 'zmodType' 'of' T ]") : form_scope.
End ZmodExports.
Section ZmoduleTheory.
Variable V : zmodType.
Implicit Types x y : V.
Lemma addrN : @right_inverse V V V 0 -%R +%R.
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}.
Definition oppr_closed := {in S, ∀ u, - u \in S}.
Definition subr_2closed := {in S &, ∀ u v, u - v \in S}.
Definition zmod_closed := 0 \in S ∧ subr_2closed.
Lemma zmod_closedN : zmod_closed → oppr_closed.
Lemma zmod_closedD : zmod_closed → addr_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].
Arguments telescope_sumr_eq {V n m} f u.
#[short(type="semiRingType")]
HB.structure Definition SemiRing := { R of Nmodule_isSemiRing R & Nmodule R }.
Module SemiRingExports.
Bind Scope ring_scope with SemiRing.sort.
#[deprecated(since="mathcomp 2.0.0", note="Use GRing.SemiRing.clone instead.")]
Notation "[ 'semiRingType' 'of' T 'for' cT ]" := (SemiRing.clone T cT)
(at level 0, format "[ 'semiRingType' 'of' T 'for' cT ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use GRing.SemiRing.clone instead.")]
Notation "[ 'semiRingType' 'of' T ]" := (SemiRing.clone T _)
(at level 0, format "[ 'semiRingType' 'of' T ]") : form_scope.
End SemiRingExports.
Definition exp R x n := nosimpl iterop _ n (@mul R) x (@one R).
Definition comm R x y := @mul R x y = mul y x.
Definition lreg R x := injective (@mul R x).
Definition rreg R x := injective ((@mul R)^~ x).
The ``field'' characteristic; the definition, and many of the theorems,
has to apply to rings as well; indeed, we need the Frobenius automorphism
results for a non commutative ring in the proof of Gorenstein 2.6.3.
Converse ring tag.
Definition converse R : Type := R.
Section SemiRingTheory.
Variable R : semiRingType.
Implicit Types x y : R.
Lemma oner_eq0 : (1 == 0 :> R) = false.
#[export]
HB.instance Definition _ := Monoid.isLaw.Build R 1 *%R mulrA mul1r mulr1.
#[export]
HB.instance Definition _ := Monoid.isMulLaw.Build R 0 *%R mul0r mulr0.
#[export]
HB.instance Definition _ := Monoid.isAddLaw.Build R *%R +%R mulrDl mulrDr.
Lemma mulr_suml I r P (F : I → R) x :
(\sum_(i <- r | P i) F i) × x = \sum_(i <- r | P i) F i × x.
Lemma mulr_sumr I r P (F : I → R) x :
x × (\sum_(i <- r | P i) F i) = \sum_(i <- r | P i) x × F i.
Lemma mulrnAl x y n : (x *+ n) × y = (x × y) *+ n.
Lemma mulrnAr x y n : x × (y *+ n) = (x × y) *+ n.
Lemma mulr_natl x n : n%:R × x = x *+ n.
Lemma mulr_natr x n : x × n%:R = x *+ n.
Lemma natrD m n : (m + n)%:R = m%:R + n%:R :> R.
Lemma natr1 n : n%:R + 1 = n.+1%:R :> R.
Lemma nat1r n : 1 + n%:R = n.+1%:R :> R.
Definition natr_sum := big_morph (natmul 1) natrD (mulr0n 1).
Lemma natrM m n : (m × n)%:R = m%:R × n%:R :> R.
Lemma expr0 x : x ^+ 0 = 1.
Lemma expr1 x : x ^+ 1 = x.
Lemma expr2 x : x ^+ 2 = x × x.
Lemma exprS x n : x ^+ n.+1 = x × x ^+ n.
Lemma expr0n n : 0 ^+ n = (n == 0%N)%:R :> R.
Lemma expr1n n : 1 ^+ n = 1 :> R.
Lemma exprD x m n : x ^+ (m + n) = x ^+ m × x ^+ n.
Lemma exprSr x n : x ^+ n.+1 = x ^+ n × x.
Lemma expr_sum x (I : Type) (s : seq I) (P : pred I) F :
x ^+ (\sum_(i <- s | P i) F i) = \prod_(i <- s | P i) x ^+ F i :> R.
Lemma commr_sym x y : comm x y → comm y x.
Lemma commr_refl x : comm x x.
Lemma commr0 x : comm x 0.
Lemma commr1 x : comm x 1.
Lemma commrD x y z : comm x y → comm x z → comm x (y + z).
Lemma commr_sum (I : Type) (s : seq I) (P : pred I) (F : I → R) x :
(∀ i, P i → comm x (F i)) → comm x (\sum_(i <- s | P i) F i).
Lemma commrMn x y n : comm x y → comm x (y *+ n).
Lemma commrM x y z : comm x y → comm x z → comm x (y × z).
Lemma commr_prod (I : Type) (s : seq I) (P : pred I) (F : I → R) x :
(∀ i, P i → comm x (F i)) → comm x (\prod_(i <- s | P i) F i).
Lemma commr_nat x n : comm x n%:R.
Lemma commrX x y n : comm x y → comm x (y ^+ n).
Lemma exprMn_comm x y n : comm x y → (x × y) ^+ n = x ^+ n × y ^+ n.
Lemma exprMn_n x m n : (x *+ m) ^+ n = x ^+ n *+ (m ^ n) :> R.
Lemma exprM x m n : x ^+ (m × n) = x ^+ m ^+ n.
Lemma exprAC x m n : (x ^+ m) ^+ n = (x ^+ n) ^+ m.
Lemma expr_mod n x i : x ^+ n = 1 → x ^+ (i %% n) = x ^+ i.
Lemma expr_dvd n x i : x ^+ n = 1 → n %| i → x ^+ i = 1.
Lemma natrX n k : (n ^ k)%:R = n%:R ^+ k :> R.
Lemma lastr_eq0 (s : seq R) x : x != 0 → (last x s == 0) = (last 1 s == 0).
Lemma mulrI_eq0 x y : lreg x → (x × y == 0) = (y == 0).
Lemma lreg_neq0 x : lreg x → x != 0.
Lemma lreg1 : lreg (1 : R).
Lemma lregM x y : lreg x → lreg y → lreg (x × y).
Lemma lregMl (a b: R) : lreg (a × b) → lreg b.
Lemma rregMr (a b: R) : rreg (a × b) → rreg a.
Lemma lregX x n : lreg x → lreg (x ^+ n).
Lemma iter_mulr n x y : iter n ( *%R x) y = x ^+ n × y.
Lemma iter_mulr_1 n x : iter n ( *%R x) 1 = x ^+ n.
Lemma prodr_const (I : finType) (A : pred I) x : \prod_(i in A) x = x ^+ #|A|.
Lemma prodr_const_nat n m x : \prod_(n ≤ i < m) x = x ^+ (m - n).
Lemma prodrXr x I r P (F : I → nat) :
\prod_(i <- r | P i) x ^+ F i = x ^+ (\sum_(i <- r | P i) F i).
Lemma prodrMn (I : Type) (s : seq I) (P : pred I) (F : I → R) (g : I → nat) :
\prod_(i <- s | P i) (F i *+ g i) =
\prod_(i <- s | P i) (F i) *+ \prod_(i <- s | P i) g i.
Lemma prodrMn_const n (I : finType) (A : pred I) (F : I → R) :
\prod_(i in A) (F i *+ n) = \prod_(i in A) F i *+ n ^ #|A|.
Lemma natr_prod I r P (F : I → nat) :
(\prod_(i <- r | P i) F i)%:R = \prod_(i <- r | P i) (F i)%:R :> R.
Lemma exprDn_comm x y n (cxy : comm x y) :
(x + y) ^+ n = \sum_(i < n.+1) (x ^+ (n - i) × y ^+ i) *+ 'C(n, i).
Lemma exprD1n x n : (x + 1) ^+ n = \sum_(i < n.+1) x ^+ i *+ 'C(n, i).
Lemma sqrrD1 x : (x + 1) ^+ 2 = x ^+ 2 + x *+ 2 + 1.
Definition Frobenius_aut p of p \in char R := fun x ⇒ x ^+ p.
Section FrobeniusAutomorphism.
Variable p : nat.
Hypothesis charFp : p \in char R.
Lemma charf0 : p%:R = 0 :> R.
Lemma charf_prime : prime p.
Hint Resolve charf_prime : core.
Lemma mulrn_char x : x *+ p = 0.
Lemma natr_mod_char n : (n %% p)%:R = n%:R :> R.
Lemma dvdn_charf n : (p %| n)%N = (n%:R == 0 :> R).
Lemma charf_eq : char R =i (p : nat_pred).
Lemma bin_lt_charf_0 k : 0 < k < p → 'C(p, k)%:R = 0 :> R.
Lemma Frobenius_autE x : x^f = x ^+ p.
Lemma Frobenius_aut0 : 0^f = 0.
Lemma Frobenius_aut1 : 1^f = 1.
Lemma Frobenius_autD_comm x y (cxy : comm x y) : (x + y)^f = x^f + y^f.
Lemma Frobenius_autMn x n : (x *+ n)^f = x^f *+ n.
Lemma Frobenius_aut_nat n : (n%:R)^f = n%:R.
Lemma Frobenius_autM_comm x y : comm x y → (x × y)^f = x^f × y^f.
Lemma Frobenius_autX x n : (x ^+ n)^f = x^f ^+ n.
End FrobeniusAutomorphism.
Section Char2.
Hypothesis charR2 : 2 \in char R.
Lemma addrr_char2 x : x + x = 0.
End Char2.
Section ClosedPredicates.
Variable S : {pred R}.
Definition mulr_2closed := {in S &, ∀ u v, u × v \in S}.
Definition mulr_closed := 1 \in S ∧ mulr_2closed.
Definition semiring_closed := addr_closed S ∧ mulr_closed.
Lemma semiring_closedD : semiring_closed → addr_closed S.
Lemma semiring_closedM : semiring_closed → mulr_closed.
End ClosedPredicates.
End SemiRingTheory.
#[short(type="ringType")]
HB.structure Definition Ring := { R of SemiRing R & Zmodule R }.
Lemma mul0r : @left_zero R R 0 mul.
Lemma mulr0 : @right_zero R R 0 mul.
Module RingExports.
Bind Scope ring_scope with Ring.sort.
#[deprecated(since="mathcomp 2.0.0", note="Use GRing.Ring.clone instead.")]
Notation "[ 'ringType' 'of' T 'for' cT ]" := (Ring.clone T cT)
(at level 0, format "[ 'ringType' 'of' T 'for' cT ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use GRing.Ring.clone instead.")]
Notation "[ 'ringType' 'of' T ]" := (Ring.clone T _)
(at level 0, format "[ 'ringType' 'of' T ]") : form_scope.
End RingExports.
Notation sign R b := (exp (- @one R) (nat_of_bool b)) (only parsing).
Section RingTheory.
Variable R : ringType.
Implicit Types x y : R.
Lemma mulrN x y : x × (- y) = - (x × y).
Lemma mulNr x y : (- x) × y = - (x × y).
Lemma mulrNN x y : (- x) × (- y) = x × y.
Lemma mulN1r x : -1 × x = - x.
Lemma mulrN1 x : x × -1 = - x.
Lemma mulrBl x y z : (y - z) × x = y × x - z × x.
Lemma mulrBr x y z : x × (y - z) = x × y - x × z.
Lemma natrB m n : n ≤ m → (m - n)%:R = m%:R - n%:R :> R.
Lemma commrN x y : comm x y → comm x (- y).
Lemma commrN1 x : comm x (-1).
Lemma commrB x y z : comm x y → comm x z → comm x (y - z).
Lemma commr_sign x n : comm x ((-1) ^+ n).
Lemma signr_odd n : (-1) ^+ (odd n) = (-1) ^+ n :> R.
Lemma signr_eq0 n : ((-1) ^+ n == 0 :> R) = false.
Lemma mulr_sign (b : bool) x : (-1) ^+ b × x = (if b then - x else x).
Lemma signr_addb b1 b2 : (-1) ^+ (b1 (+) b2) = (-1) ^+ b1 × (-1) ^+ b2 :> R.
Lemma signrE (b : bool) : (-1) ^+ b = 1 - b.*2%:R :> R.
Lemma signrN b : (-1) ^+ (~~ b) = - (-1) ^+ b :> R.
Lemma mulr_signM (b1 b2 : bool) x1 x2 :
((-1) ^+ b1 × x1) × ((-1) ^+ b2 × x2) = (-1) ^+ (b1 (+) b2) × (x1 × x2).
Lemma exprNn x n : (- x) ^+ n = (-1) ^+ n × x ^+ n :> R.
Lemma sqrrN x : (- x) ^+ 2 = x ^+ 2.
Lemma sqrr_sign n : ((-1) ^+ n) ^+ 2 = 1 :> R.
Lemma signrMK n : @involutive R ( *%R ((-1) ^+ n)).
Lemma mulrI0_lreg x : (∀ y, x × y = 0 → y = 0) → lreg x.
Lemma lregN x : lreg x → lreg (- x).
Lemma lreg_sign n : lreg ((-1) ^+ n : R).
Lemma prodrN (I : finType) (A : pred I) (F : I → R) :
\prod_(i in A) - F i = (- 1) ^+ #|A| × \prod_(i in A) F i.
Lemma exprBn_comm x y n (cxy : comm x y) :
(x - y) ^+ n =
\sum_(i < n.+1) ((-1) ^+ i × x ^+ (n - i) × y ^+ i) *+ 'C(n, i).
Lemma subrXX_comm x y n (cxy : comm x y) :
x ^+ n - y ^+ n = (x - y) × (\sum_(i < n) x ^+ (n.-1 - i) × y ^+ i).
Lemma subrX1 x n : x ^+ n - 1 = (x - 1) × (\sum_(i < n) x ^+ i).
Lemma sqrrB1 x : (x - 1) ^+ 2 = x ^+ 2 - x *+ 2 + 1.
Lemma subr_sqr_1 x : x ^+ 2 - 1 = (x - 1) × (x + 1).
Section FrobeniusAutomorphism.
Variable p : nat.
Hypothesis charFp : p \in char R.
Hint Resolve charf_prime : core.
Lemma Frobenius_autN x : (- x)^f = - x^f.
Lemma Frobenius_autB_comm x y : comm x y → (x - y)^f = x^f - y^f.
End FrobeniusAutomorphism.
Lemma exprNn_char x n : (char R).-nat n → (- x) ^+ n = - (x ^+ n).
Section Char2.
Hypothesis charR2 : 2 \in char R.
Lemma oppr_char2 x : - x = x.
Lemma subr_char2 x y : x - y = x + y.
Lemma addrK_char2 x : involutive (+%R^~ x).
Lemma addKr_char2 x : involutive (+%R x).
End Char2.
Section ClosedPredicates.
Variable S : {pred R}.
Definition smulr_closed := -1 \in S ∧ mulr_2closed S.
Definition subring_closed := [/\ 1 \in S, subr_2closed S & mulr_2closed S].
Lemma smulr_closedM : smulr_closed → mulr_closed S.
Lemma smulr_closedN : smulr_closed → oppr_closed S.
Lemma subring_closedB : subring_closed → zmod_closed S.
Lemma subring_closedM : subring_closed → smulr_closed.
Lemma subring_closed_semi : subring_closed → semiring_closed S.
End ClosedPredicates.
End RingTheory.
Module ConverseRingExports.
End ConverseRingExports.
Section SemiRightRegular.
Variable R : semiRingType.
Implicit Types x y : R.
Lemma mulIr_eq0 x y : rreg x → (y × x == 0) = (y == 0).
Lemma rreg_neq0 x : rreg x → x != 0.
Lemma rreg1 : rreg (1 : R).
Lemma rregM x y : rreg x → rreg y → rreg (x × y).
Lemma revrX x n : (x : R^c) ^+ n = (x : R) ^+ n.
Lemma rregX x n : rreg x → rreg (x ^+ n).
End SemiRightRegular.
Section RightRegular.
Variable R : ringType.
Implicit Types x y : R.
Lemma mulIr0_rreg x : (∀ y, y × x = 0 → y = 0) → rreg x.
Lemma rregN x : rreg x → rreg (- x).
End RightRegular.
#[short(type="lmodType")]
HB.structure Definition Lmodule (R : ringType) :=
{M of Zmodule M & Zmodule_isLmodule R M}.
Section SemiRingTheory.
Variable R : semiRingType.
Implicit Types x y : R.
Lemma oner_eq0 : (1 == 0 :> R) = false.
#[export]
HB.instance Definition _ := Monoid.isLaw.Build R 1 *%R mulrA mul1r mulr1.
#[export]
HB.instance Definition _ := Monoid.isMulLaw.Build R 0 *%R mul0r mulr0.
#[export]
HB.instance Definition _ := Monoid.isAddLaw.Build R *%R +%R mulrDl mulrDr.
Lemma mulr_suml I r P (F : I → R) x :
(\sum_(i <- r | P i) F i) × x = \sum_(i <- r | P i) F i × x.
Lemma mulr_sumr I r P (F : I → R) x :
x × (\sum_(i <- r | P i) F i) = \sum_(i <- r | P i) x × F i.
Lemma mulrnAl x y n : (x *+ n) × y = (x × y) *+ n.
Lemma mulrnAr x y n : x × (y *+ n) = (x × y) *+ n.
Lemma mulr_natl x n : n%:R × x = x *+ n.
Lemma mulr_natr x n : x × n%:R = x *+ n.
Lemma natrD m n : (m + n)%:R = m%:R + n%:R :> R.
Lemma natr1 n : n%:R + 1 = n.+1%:R :> R.
Lemma nat1r n : 1 + n%:R = n.+1%:R :> R.
Definition natr_sum := big_morph (natmul 1) natrD (mulr0n 1).
Lemma natrM m n : (m × n)%:R = m%:R × n%:R :> R.
Lemma expr0 x : x ^+ 0 = 1.
Lemma expr1 x : x ^+ 1 = x.
Lemma expr2 x : x ^+ 2 = x × x.
Lemma exprS x n : x ^+ n.+1 = x × x ^+ n.
Lemma expr0n n : 0 ^+ n = (n == 0%N)%:R :> R.
Lemma expr1n n : 1 ^+ n = 1 :> R.
Lemma exprD x m n : x ^+ (m + n) = x ^+ m × x ^+ n.
Lemma exprSr x n : x ^+ n.+1 = x ^+ n × x.
Lemma expr_sum x (I : Type) (s : seq I) (P : pred I) F :
x ^+ (\sum_(i <- s | P i) F i) = \prod_(i <- s | P i) x ^+ F i :> R.
Lemma commr_sym x y : comm x y → comm y x.
Lemma commr_refl x : comm x x.
Lemma commr0 x : comm x 0.
Lemma commr1 x : comm x 1.
Lemma commrD x y z : comm x y → comm x z → comm x (y + z).
Lemma commr_sum (I : Type) (s : seq I) (P : pred I) (F : I → R) x :
(∀ i, P i → comm x (F i)) → comm x (\sum_(i <- s | P i) F i).
Lemma commrMn x y n : comm x y → comm x (y *+ n).
Lemma commrM x y z : comm x y → comm x z → comm x (y × z).
Lemma commr_prod (I : Type) (s : seq I) (P : pred I) (F : I → R) x :
(∀ i, P i → comm x (F i)) → comm x (\prod_(i <- s | P i) F i).
Lemma commr_nat x n : comm x n%:R.
Lemma commrX x y n : comm x y → comm x (y ^+ n).
Lemma exprMn_comm x y n : comm x y → (x × y) ^+ n = x ^+ n × y ^+ n.
Lemma exprMn_n x m n : (x *+ m) ^+ n = x ^+ n *+ (m ^ n) :> R.
Lemma exprM x m n : x ^+ (m × n) = x ^+ m ^+ n.
Lemma exprAC x m n : (x ^+ m) ^+ n = (x ^+ n) ^+ m.
Lemma expr_mod n x i : x ^+ n = 1 → x ^+ (i %% n) = x ^+ i.
Lemma expr_dvd n x i : x ^+ n = 1 → n %| i → x ^+ i = 1.
Lemma natrX n k : (n ^ k)%:R = n%:R ^+ k :> R.
Lemma lastr_eq0 (s : seq R) x : x != 0 → (last x s == 0) = (last 1 s == 0).
Lemma mulrI_eq0 x y : lreg x → (x × y == 0) = (y == 0).
Lemma lreg_neq0 x : lreg x → x != 0.
Lemma lreg1 : lreg (1 : R).
Lemma lregM x y : lreg x → lreg y → lreg (x × y).
Lemma lregMl (a b: R) : lreg (a × b) → lreg b.
Lemma rregMr (a b: R) : rreg (a × b) → rreg a.
Lemma lregX x n : lreg x → lreg (x ^+ n).
Lemma iter_mulr n x y : iter n ( *%R x) y = x ^+ n × y.
Lemma iter_mulr_1 n x : iter n ( *%R x) 1 = x ^+ n.
Lemma prodr_const (I : finType) (A : pred I) x : \prod_(i in A) x = x ^+ #|A|.
Lemma prodr_const_nat n m x : \prod_(n ≤ i < m) x = x ^+ (m - n).
Lemma prodrXr x I r P (F : I → nat) :
\prod_(i <- r | P i) x ^+ F i = x ^+ (\sum_(i <- r | P i) F i).
Lemma prodrMn (I : Type) (s : seq I) (P : pred I) (F : I → R) (g : I → nat) :
\prod_(i <- s | P i) (F i *+ g i) =
\prod_(i <- s | P i) (F i) *+ \prod_(i <- s | P i) g i.
Lemma prodrMn_const n (I : finType) (A : pred I) (F : I → R) :
\prod_(i in A) (F i *+ n) = \prod_(i in A) F i *+ n ^ #|A|.
Lemma natr_prod I r P (F : I → nat) :
(\prod_(i <- r | P i) F i)%:R = \prod_(i <- r | P i) (F i)%:R :> R.
Lemma exprDn_comm x y n (cxy : comm x y) :
(x + y) ^+ n = \sum_(i < n.+1) (x ^+ (n - i) × y ^+ i) *+ 'C(n, i).
Lemma exprD1n x n : (x + 1) ^+ n = \sum_(i < n.+1) x ^+ i *+ 'C(n, i).
Lemma sqrrD1 x : (x + 1) ^+ 2 = x ^+ 2 + x *+ 2 + 1.
Definition Frobenius_aut p of p \in char R := fun x ⇒ x ^+ p.
Section FrobeniusAutomorphism.
Variable p : nat.
Hypothesis charFp : p \in char R.
Lemma charf0 : p%:R = 0 :> R.
Lemma charf_prime : prime p.
Hint Resolve charf_prime : core.
Lemma mulrn_char x : x *+ p = 0.
Lemma natr_mod_char n : (n %% p)%:R = n%:R :> R.
Lemma dvdn_charf n : (p %| n)%N = (n%:R == 0 :> R).
Lemma charf_eq : char R =i (p : nat_pred).
Lemma bin_lt_charf_0 k : 0 < k < p → 'C(p, k)%:R = 0 :> R.
Lemma Frobenius_autE x : x^f = x ^+ p.
Lemma Frobenius_aut0 : 0^f = 0.
Lemma Frobenius_aut1 : 1^f = 1.
Lemma Frobenius_autD_comm x y (cxy : comm x y) : (x + y)^f = x^f + y^f.
Lemma Frobenius_autMn x n : (x *+ n)^f = x^f *+ n.
Lemma Frobenius_aut_nat n : (n%:R)^f = n%:R.
Lemma Frobenius_autM_comm x y : comm x y → (x × y)^f = x^f × y^f.
Lemma Frobenius_autX x n : (x ^+ n)^f = x^f ^+ n.
End FrobeniusAutomorphism.
Section Char2.
Hypothesis charR2 : 2 \in char R.
Lemma addrr_char2 x : x + x = 0.
End Char2.
Section ClosedPredicates.
Variable S : {pred R}.
Definition mulr_2closed := {in S &, ∀ u v, u × v \in S}.
Definition mulr_closed := 1 \in S ∧ mulr_2closed.
Definition semiring_closed := addr_closed S ∧ mulr_closed.
Lemma semiring_closedD : semiring_closed → addr_closed S.
Lemma semiring_closedM : semiring_closed → mulr_closed.
End ClosedPredicates.
End SemiRingTheory.
#[short(type="ringType")]
HB.structure Definition Ring := { R of SemiRing R & Zmodule R }.
Lemma mul0r : @left_zero R R 0 mul.
Lemma mulr0 : @right_zero R R 0 mul.
Module RingExports.
Bind Scope ring_scope with Ring.sort.
#[deprecated(since="mathcomp 2.0.0", note="Use GRing.Ring.clone instead.")]
Notation "[ 'ringType' 'of' T 'for' cT ]" := (Ring.clone T cT)
(at level 0, format "[ 'ringType' 'of' T 'for' cT ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use GRing.Ring.clone instead.")]
Notation "[ 'ringType' 'of' T ]" := (Ring.clone T _)
(at level 0, format "[ 'ringType' 'of' T ]") : form_scope.
End RingExports.
Notation sign R b := (exp (- @one R) (nat_of_bool b)) (only parsing).
Section RingTheory.
Variable R : ringType.
Implicit Types x y : R.
Lemma mulrN x y : x × (- y) = - (x × y).
Lemma mulNr x y : (- x) × y = - (x × y).
Lemma mulrNN x y : (- x) × (- y) = x × y.
Lemma mulN1r x : -1 × x = - x.
Lemma mulrN1 x : x × -1 = - x.
Lemma mulrBl x y z : (y - z) × x = y × x - z × x.
Lemma mulrBr x y z : x × (y - z) = x × y - x × z.
Lemma natrB m n : n ≤ m → (m - n)%:R = m%:R - n%:R :> R.
Lemma commrN x y : comm x y → comm x (- y).
Lemma commrN1 x : comm x (-1).
Lemma commrB x y z : comm x y → comm x z → comm x (y - z).
Lemma commr_sign x n : comm x ((-1) ^+ n).
Lemma signr_odd n : (-1) ^+ (odd n) = (-1) ^+ n :> R.
Lemma signr_eq0 n : ((-1) ^+ n == 0 :> R) = false.
Lemma mulr_sign (b : bool) x : (-1) ^+ b × x = (if b then - x else x).
Lemma signr_addb b1 b2 : (-1) ^+ (b1 (+) b2) = (-1) ^+ b1 × (-1) ^+ b2 :> R.
Lemma signrE (b : bool) : (-1) ^+ b = 1 - b.*2%:R :> R.
Lemma signrN b : (-1) ^+ (~~ b) = - (-1) ^+ b :> R.
Lemma mulr_signM (b1 b2 : bool) x1 x2 :
((-1) ^+ b1 × x1) × ((-1) ^+ b2 × x2) = (-1) ^+ (b1 (+) b2) × (x1 × x2).
Lemma exprNn x n : (- x) ^+ n = (-1) ^+ n × x ^+ n :> R.
Lemma sqrrN x : (- x) ^+ 2 = x ^+ 2.
Lemma sqrr_sign n : ((-1) ^+ n) ^+ 2 = 1 :> R.
Lemma signrMK n : @involutive R ( *%R ((-1) ^+ n)).
Lemma mulrI0_lreg x : (∀ y, x × y = 0 → y = 0) → lreg x.
Lemma lregN x : lreg x → lreg (- x).
Lemma lreg_sign n : lreg ((-1) ^+ n : R).
Lemma prodrN (I : finType) (A : pred I) (F : I → R) :
\prod_(i in A) - F i = (- 1) ^+ #|A| × \prod_(i in A) F i.
Lemma exprBn_comm x y n (cxy : comm x y) :
(x - y) ^+ n =
\sum_(i < n.+1) ((-1) ^+ i × x ^+ (n - i) × y ^+ i) *+ 'C(n, i).
Lemma subrXX_comm x y n (cxy : comm x y) :
x ^+ n - y ^+ n = (x - y) × (\sum_(i < n) x ^+ (n.-1 - i) × y ^+ i).
Lemma subrX1 x n : x ^+ n - 1 = (x - 1) × (\sum_(i < n) x ^+ i).
Lemma sqrrB1 x : (x - 1) ^+ 2 = x ^+ 2 - x *+ 2 + 1.
Lemma subr_sqr_1 x : x ^+ 2 - 1 = (x - 1) × (x + 1).
Section FrobeniusAutomorphism.
Variable p : nat.
Hypothesis charFp : p \in char R.
Hint Resolve charf_prime : core.
Lemma Frobenius_autN x : (- x)^f = - x^f.
Lemma Frobenius_autB_comm x y : comm x y → (x - y)^f = x^f - y^f.
End FrobeniusAutomorphism.
Lemma exprNn_char x n : (char R).-nat n → (- x) ^+ n = - (x ^+ n).
Section Char2.
Hypothesis charR2 : 2 \in char R.
Lemma oppr_char2 x : - x = x.
Lemma subr_char2 x y : x - y = x + y.
Lemma addrK_char2 x : involutive (+%R^~ x).
Lemma addKr_char2 x : involutive (+%R x).
End Char2.
Section ClosedPredicates.
Variable S : {pred R}.
Definition smulr_closed := -1 \in S ∧ mulr_2closed S.
Definition subring_closed := [/\ 1 \in S, subr_2closed S & mulr_2closed S].
Lemma smulr_closedM : smulr_closed → mulr_closed S.
Lemma smulr_closedN : smulr_closed → oppr_closed S.
Lemma subring_closedB : subring_closed → zmod_closed S.
Lemma subring_closedM : subring_closed → smulr_closed.
Lemma subring_closed_semi : subring_closed → semiring_closed S.
End ClosedPredicates.
End RingTheory.
Module ConverseRingExports.
End ConverseRingExports.
Section SemiRightRegular.
Variable R : semiRingType.
Implicit Types x y : R.
Lemma mulIr_eq0 x y : rreg x → (y × x == 0) = (y == 0).
Lemma rreg_neq0 x : rreg x → x != 0.
Lemma rreg1 : rreg (1 : R).
Lemma rregM x y : rreg x → rreg y → rreg (x × y).
Lemma revrX x n : (x : R^c) ^+ n = (x : R) ^+ n.
Lemma rregX x n : rreg x → rreg (x ^+ n).
End SemiRightRegular.
Section RightRegular.
Variable R : ringType.
Implicit Types x y : R.
Lemma mulIr0_rreg x : (∀ y, y × x = 0 → y = 0) → rreg x.
Lemma rregN x : rreg x → rreg (- x).
End RightRegular.
#[short(type="lmodType")]
HB.structure Definition Lmodule (R : ringType) :=
{M of Zmodule M & Zmodule_isLmodule R M}.
FIXME: see #1126 and #1127
Arguments scalerA [R s] (a b)%ring_scope v.
Module LmodExports.
Bind Scope ring_scope with Lmodule.sort.
#[deprecated(since="mathcomp 2.0.0", note="Use GRing.Lmodule.clone instead.")]
Notation "[ 'lmodType' R 'of' T 'for' cT ]" := (Lmodule.clone R T%type cT)
(at level 0, format "[ 'lmodType' R 'of' T 'for' cT ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use GRing.Lmodule.clone instead.")]
Notation "[ 'lmodType' R 'of' T ]" := (Lmodule.clone R T%type _)
(at level 0, format "[ 'lmodType' R 'of' T ]") : form_scope.
End LmodExports.
Section LmoduleTheory.
Variables (R : ringType) (V : lmodType R).
Implicit Types (a b c : R) (u v : V).
Lemma scale0r v : 0 *: v = 0.
Lemma scaler0 a : a *: 0 = 0 :> V.
Lemma scaleNr a v : - a *: v = - (a *: v).
Lemma scaleN1r v : (- 1) *: v = - v.
Lemma scalerN a v : a *: (- v) = - (a *: v).
Lemma scalerBl a b v : (a - b) *: v = a *: v - b *: v.
Lemma scalerBr a u v : a *: (u - v) = a *: u - a *: v.
Lemma scaler_nat n v : n%:R *: v = v *+ n.
Lemma scaler_sign (b : bool) v: (-1) ^+ b *: v = (if b then - v else v).
Lemma signrZK n : @involutive V ( *:%R ((-1) ^+ n)).
Lemma scalerMnl a v n : a *: v *+ n = (a *+ n) *: v.
Lemma scalerMnr a v n : a *: v *+ n = a *: (v *+ n).
Lemma scaler_suml v I r (P : pred I) F :
(\sum_(i <- r | P i) F i) *: v = \sum_(i <- r | P i) F i *: v.
Lemma scaler_sumr a I r (P : pred I) (F : I → V) :
a *: (\sum_(i <- r | P i) F i) = \sum_(i <- r | P i) a *: F i.
Section ClosedPredicates.
Variable S : {pred V}.
Definition scaler_closed := ∀ a, {in S, ∀ v, a *: v \in S}.
Definition linear_closed := ∀ a, {in S &, ∀ u v, a *: u + v \in S}.
Definition submod_closed := 0 \in S ∧ linear_closed.
Lemma linear_closedB : linear_closed → subr_2closed S.
Lemma submod_closedB : submod_closed → zmod_closed S.
Lemma submod_closedZ : submod_closed → scaler_closed.
End ClosedPredicates.
End LmoduleTheory.
#[short(type="lalgType")]
HB.structure Definition Lalgebra R :=
{A of Lmodule_isLalgebra R A & Ring A & Lmodule R A}.
Module LalgExports.
Bind Scope ring_scope with Lalgebra.sort.
#[deprecated(since="mathcomp 2.0.0", note="Use GRing.Lalgebra.clone instead.")]
Notation "[ 'lalgType' R 'of' T 'for' cT ]" := (Lalgebra.clone R T%type cT)
(at level 0, format "[ 'lalgType' R 'of' T 'for' cT ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use GRing.Lalgebra.clone instead.")]
Notation "[ 'lalgType' R 'of' T ]" := (Lalgebra.clone R T%type _)
(at level 0, format "[ 'lalgType' R 'of' T ]") : form_scope.
End LalgExports.
Module LmodExports.
Bind Scope ring_scope with Lmodule.sort.
#[deprecated(since="mathcomp 2.0.0", note="Use GRing.Lmodule.clone instead.")]
Notation "[ 'lmodType' R 'of' T 'for' cT ]" := (Lmodule.clone R T%type cT)
(at level 0, format "[ 'lmodType' R 'of' T 'for' cT ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use GRing.Lmodule.clone instead.")]
Notation "[ 'lmodType' R 'of' T ]" := (Lmodule.clone R T%type _)
(at level 0, format "[ 'lmodType' R 'of' T ]") : form_scope.
End LmodExports.
Section LmoduleTheory.
Variables (R : ringType) (V : lmodType R).
Implicit Types (a b c : R) (u v : V).
Lemma scale0r v : 0 *: v = 0.
Lemma scaler0 a : a *: 0 = 0 :> V.
Lemma scaleNr a v : - a *: v = - (a *: v).
Lemma scaleN1r v : (- 1) *: v = - v.
Lemma scalerN a v : a *: (- v) = - (a *: v).
Lemma scalerBl a b v : (a - b) *: v = a *: v - b *: v.
Lemma scalerBr a u v : a *: (u - v) = a *: u - a *: v.
Lemma scaler_nat n v : n%:R *: v = v *+ n.
Lemma scaler_sign (b : bool) v: (-1) ^+ b *: v = (if b then - v else v).
Lemma signrZK n : @involutive V ( *:%R ((-1) ^+ n)).
Lemma scalerMnl a v n : a *: v *+ n = (a *+ n) *: v.
Lemma scalerMnr a v n : a *: v *+ n = a *: (v *+ n).
Lemma scaler_suml v I r (P : pred I) F :
(\sum_(i <- r | P i) F i) *: v = \sum_(i <- r | P i) F i *: v.
Lemma scaler_sumr a I r (P : pred I) (F : I → V) :
a *: (\sum_(i <- r | P i) F i) = \sum_(i <- r | P i) a *: F i.
Section ClosedPredicates.
Variable S : {pred V}.
Definition scaler_closed := ∀ a, {in S, ∀ v, a *: v \in S}.
Definition linear_closed := ∀ a, {in S &, ∀ u v, a *: u + v \in S}.
Definition submod_closed := 0 \in S ∧ linear_closed.
Lemma linear_closedB : linear_closed → subr_2closed S.
Lemma submod_closedB : submod_closed → zmod_closed S.
Lemma submod_closedZ : submod_closed → scaler_closed.
End ClosedPredicates.
End LmoduleTheory.
#[short(type="lalgType")]
HB.structure Definition Lalgebra R :=
{A of Lmodule_isLalgebra R A & Ring A & Lmodule R A}.
Module LalgExports.
Bind Scope ring_scope with Lalgebra.sort.
#[deprecated(since="mathcomp 2.0.0", note="Use GRing.Lalgebra.clone instead.")]
Notation "[ 'lalgType' R 'of' T 'for' cT ]" := (Lalgebra.clone R T%type cT)
(at level 0, format "[ 'lalgType' R 'of' T 'for' cT ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use GRing.Lalgebra.clone instead.")]
Notation "[ 'lalgType' R 'of' T ]" := (Lalgebra.clone R T%type _)
(at level 0, format "[ 'lalgType' R 'of' T ]") : form_scope.
End LalgExports.
Scalar injection (see the definition of in_alg A below).
Regular ring algebra tag.
Definition regular R : Type := R.
Module RegularLalgExports.
Section LalgebraTheory.
Variables (R : ringType) (A : lalgType R).
End LalgebraTheory.
End RegularLalgExports.
Section LalgebraTheory.
Variables (R : ringType) (A : lalgType R).
Implicit Types x y : A.
Lemma mulr_algl a x : (a *: 1) × x = a *: x.
Section ClosedPredicates.
Variable S : {pred A}.
Definition subalg_closed := [/\ 1 \in S, linear_closed S & mulr_2closed S].
Lemma subalg_closedZ : subalg_closed → submod_closed S.
Lemma subalg_closedBM : subalg_closed → subring_closed S.
End ClosedPredicates.
End LalgebraTheory.
Module RegularLalgExports.
Section LalgebraTheory.
Variables (R : ringType) (A : lalgType R).
End LalgebraTheory.
End RegularLalgExports.
Section LalgebraTheory.
Variables (R : ringType) (A : lalgType R).
Implicit Types x y : A.
Lemma mulr_algl a x : (a *: 1) × x = a *: x.
Section ClosedPredicates.
Variable S : {pred A}.
Definition subalg_closed := [/\ 1 \in S, linear_closed S & mulr_2closed S].
Lemma subalg_closedZ : subalg_closed → submod_closed S.
Lemma subalg_closedBM : subalg_closed → subring_closed S.
End ClosedPredicates.
End LalgebraTheory.
Morphism hierarchy.
Definition semi_additive (U V : nmodType) (f : U → V) : Prop :=
(f 0 = 0) × {morph f : x y / x + y}.
#[mathcomp(axiom="semi_additive")]
HB.structure Definition Additive (U V : nmodType) :=
{f of isSemiAdditive U V f}.
Definition additive (U V : zmodType) (f : U → V) := {morph f : x y / x - y}.
Module AdditiveExports.
Module Additive.
Definition apply_deprecated (U V : nmodType) (phUV : phant (U → V)) :=
@Additive.sort U V.
#[deprecated(since="mathcomp 2.0", note="Use Additive.sort instead.")]
Notation apply := apply_deprecated.
End Additive.
Notation "{ 'additive' U -> V }" := (Additive.type U%type V%type) : type_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use GRing.Additive.clone instead.")]
Notation "[ 'additive' 'of' f 'as' g ]" := (Additive.clone _ _ f%function g)
(at level 0, format "[ 'additive' 'of' f 'as' g ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use GRing.Additive.clone instead.")]
Notation "[ 'additive' 'of' f ]" := (Additive.clone _ _ f%function _)
(at level 0, format "[ 'additive' 'of' f ]") : form_scope.
End AdditiveExports.
Lifted additive operations.
Section LiftedNmod.
Variables (U : Type) (V : nmodType).
Definition null_fun of U : V := 0.
Definition add_fun (f g : U → V) x := f x + g x.
End LiftedNmod.
Section LiftedZmod.
Variables (U : Type) (V : zmodType).
Definition sub_fun (f g : U → V) x := f x - g x.
Definition opp_fun (f : U → V) x := - f x.
End LiftedZmod.
Variables (U : Type) (V : nmodType).
Definition null_fun of U : V := 0.
Definition add_fun (f g : U → V) x := f x + g x.
End LiftedNmod.
Section LiftedZmod.
Variables (U : Type) (V : zmodType).
Definition sub_fun (f g : U → V) x := f x - g x.
Definition opp_fun (f : U → V) x := - f x.
End LiftedZmod.
Lifted multiplication.
Section LiftedSemiRing.
Variables (R : semiRingType) (T : Type).
Implicit Type f : T → R.
Definition mull_fun a f x := a × f x.
Definition mulr_fun a f x := f x × a.
Definition mul_fun f g x := f x × g x.
End LiftedSemiRing.
Variables (R : semiRingType) (T : Type).
Implicit Type f : T → R.
Definition mull_fun a f x := a × f x.
Definition mulr_fun a f x := f x × a.
Definition mul_fun f g x := f x × g x.
End LiftedSemiRing.
Lifted linear operations.
Section LiftedScale.
Variables (R : ringType) (U : Type) (V : lmodType R) (A : lalgType R).
Definition scale_fun a (f : U → V) x := a *: f x.
Definition in_alg_head k : A := k%:A.
End LiftedScale.
Variables (R : ringType) (U : Type) (V : lmodType R) (A : lalgType R).
Definition scale_fun a (f : U → V) x := a *: f x.
Definition in_alg_head k : A := k%:A.
End LiftedScale.
The real in_alg notation is declared after GRing.Theory so that at least
in Coq 8.2 it gets precedence when GRing.Theory is not imported.
Arguments null_fun {_} V _ /.
Arguments in_alg_head {_} A _ /.
Arguments add_fun {_ _} f g _ /.
Arguments sub_fun {_ _} f g _ /.
Arguments opp_fun {_ _} f _ /.
Arguments mull_fun {_ _} a f _ /.
Arguments mulr_fun {_ _} a f _ /.
Arguments scale_fun {_ _ _} a f _ /.
Arguments mul_fun {_ _} f g _ /.
Section AdditiveTheory.
Section Properties.
Variables (U V : nmodType) (k : unit) (f : {additive U → V}).
Lemma raddf0 : f 0 = 0.
Lemma raddf_eq0 x : injective f → (f x == 0) = (x == 0).
Lemma raddfD : {morph f : x y / x + y}.
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_semi_additive f' : cancel f f' → cancel f' f → semi_additive f'.
End Properties.
Section SemiRingProperties.
Variables (R S : semiRingType) (f : {additive R → S}).
Lemma raddfMnat n x : f (n%:R × x) = n%:R × f x.
End SemiRingProperties.
Section AddFun.
Variables (U V W : nmodType).
Variables (f g : {additive V → W}) (h : {additive U → V}).
Fact idfun_is_semi_additive : semi_additive (@idfun U).
#[export]
HB.instance Definition _ := isSemiAdditive.Build U U idfun
idfun_is_semi_additive.
Fact comp_is_semi_additive : semi_additive (f \o h).
#[export]
HB.instance Definition _ := isSemiAdditive.Build U W (f \o h)
comp_is_semi_additive.
Fact null_fun_is_semi_additive : semi_additive (\0 : U → V).
#[export]
HB.instance Definition _ := isSemiAdditive.Build U V \0
null_fun_is_semi_additive.
Fact add_fun_is_semi_additive : semi_additive (f \+ g).
#[export]
HB.instance Definition _ := isSemiAdditive.Build V W (f \+ g)
add_fun_is_semi_additive.
End AddFun.
Section MulFun.
Variables (R : semiRingType) (U : nmodType) (a : R) (f : {additive U → R}).
Fact mull_fun_is_semi_additive : semi_additive (a \*o f).
#[export]
HB.instance Definition _ := isSemiAdditive.Build U R (a \*o f)
mull_fun_is_semi_additive.
Fact mulr_fun_is_semi_additive : semi_additive (a \o× f).
#[export]
HB.instance Definition _ := isSemiAdditive.Build U R (a \o× f)
mulr_fun_is_semi_additive.
End MulFun.
Section Properties.
Variables (U V : zmodType) (k : unit) (f : {additive U → V}).
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_additive f' : cancel f f' → cancel f' f → additive f'.
End Properties.
Section RingProperties.
Variables (R S : ringType) (f : {additive R → S}).
Lemma raddfMsign n x : f ((-1) ^+ n × x) = (-1) ^+ n × f x.
Variables (U : lmodType R) (V : lmodType S) (h : {additive U → V}).
Lemma raddfZnat n u : h (n%:R *: u) = n%:R *: h u.
Lemma raddfZsign n u : h ((-1) ^+ n *: u) = (-1) ^+ n *: h u.
End RingProperties.
Section AddFun.
Variables (U V W : zmodType) (f g : {additive V → W}) (h : {additive U → V}).
Fact opp_is_additive : additive (-%R : U → U).
#[export]
HB.instance Definition _ := isAdditive.Build U U -%R opp_is_additive.
Fact sub_fun_is_additive : additive (f \- g).
#[export]
HB.instance Definition _ := isAdditive.Build V W (f \- g) sub_fun_is_additive.
Fact opp_fun_is_additive : additive (\- g).
#[export]
HB.instance Definition _ := isAdditive.Build V W (\- g) opp_fun_is_additive.
End AddFun.
Section ScaleFun.
Variables (R : ringType) (U : zmodType) (V : lmodType R).
Variables (a : R) (f : {additive U → V}).
#[export]
HB.instance Definition _ := isAdditive.Build V V ( *:%R a) (@scalerBr R V a).
#[export]
HB.instance Definition _ := Additive.copy (a \*: f) (f \; *:%R a).
End ScaleFun.
End AdditiveTheory.
Definition multiplicative (R S : semiRingType) (f : R → S) : Prop :=
{morph f : x y / x × y}%R × (f 1 = 1).
FIXME: remove the @ once
https://github.com/math-comp/hierarchy-builder/issues/319 is fixed
Module RMorphismExports.
Notation "{ 'rmorphism' U -> V }" := (RMorphism.type U%type V%type)
: type_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use GRing.RMorphism.clone instead.")]
Notation "[ 'rmorphism' 'of' f 'as' g ]" := (RMorphism.clone _ _ f%function g)
(at level 0, format "[ 'rmorphism' 'of' f 'as' g ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0",
note="Use GRing.RMorphism.clone instead.")]
Notation "[ 'rmorphism' 'of' f ]" := (RMorphism.clone _ _ f%function _)
(at level 0, format "[ 'rmorphism' 'of' f ]") : form_scope.
End RMorphismExports.
Section RmorphismTheory.
Section Properties.
Variables (R S : semiRingType) (k : unit) (f : {rmorphism R → S}).
Lemma rmorph0 : f 0 = 0.
Lemma rmorphD : {morph f : x y / x + y}.
Lemma rmorphMn n : {morph f : x / x *+ n}.
Lemma rmorph_sum I r (P : pred I) E :
f (\sum_(i <- r | P i) E i) = \sum_(i <- r | P i) f (E i).
Lemma rmorphismMP : multiplicative f.
Lemma rmorph1 : f 1 = 1.
Lemma rmorphM : {morph f: x y / x × y}.
Lemma rmorph_prod I r (P : pred I) E :
f (\prod_(i <- r | P i) E i) = \prod_(i <- r | P i) f (E i).
Lemma rmorphXn n : {morph f : x / x ^+ n}.
Lemma rmorph_nat n : f n%:R = n%:R.
Lemma rmorph_char p : p \in char R → p \in char S.
Lemma rmorph_eq_nat x n : injective f → (f x == n%:R) = (x == n%:R).
Lemma rmorph_eq1 x : injective f → (f x == 1) = (x == 1).
Lemma can2_rmorphism f' : cancel f f' → cancel f' f → multiplicative f'.
End Properties.
Section Projections.
Variables (R S T : semiRingType).
Variables (f : {rmorphism S → T}) (g : {rmorphism R → S}).
Fact idfun_is_multiplicative : multiplicative (@idfun R).
#[export]
HB.instance Definition _ := isMultiplicative.Build R R idfun
idfun_is_multiplicative.
Fact comp_is_multiplicative : multiplicative (f \o g).
#[export]
HB.instance Definition _ := isMultiplicative.Build R T (f \o g)
comp_is_multiplicative.
End Projections.
Section Properties.
Variables (R S : ringType) (k : unit) (f : {rmorphism R → S}).
Lemma rmorphN : {morph f : x / - x}.
Lemma rmorphB : {morph f: x y / x - y}.
Lemma rmorphMNn n : {morph f : x / x *- n}.
Lemma rmorphMsign n : {morph f : x / (- 1) ^+ n × x}.
Lemma rmorphN1 : f (- 1) = (- 1).
Lemma rmorph_sign n : f ((- 1) ^+ n) = (- 1) ^+ n.
End Properties.
Section InAlgebra.
Variables (R : ringType) (A : lalgType R).
Fact in_alg_is_additive : additive (in_alg_loc A).
#[export]
HB.instance Definition _ := isAdditive.Build R A (in_alg_loc A)
in_alg_is_additive.
Fact in_alg_is_rmorphism : multiplicative (in_alg_loc A).
#[export]
HB.instance Definition _ := isMultiplicative.Build R A (in_alg_loc A)
in_alg_is_rmorphism.
Lemma in_algE a : in_alg_loc A a = a%:A.
End InAlgebra.
End RmorphismTheory.
Module Scale.
#[export]
HB.structure Definition Law R V := {op of isLaw R V op}.
Definition law := Law.type.
Section ScaleLaw.
Variables (R : ringType) (V : zmodType) (s_law : law R V).
Lemma N1op : s_law (-1) =1 -%R.
Fact opB a : additive (s_law a).
Variables (aR : ringType) (nu : {rmorphism aR → R}).
Fact compN1op : (nu \; s_law) (-1) =1 -%R.
End ScaleLaw.
Module Exports. End Exports.
End Scale.
Export Scale.Exports.
#[export]
HB.instance Definition _ (R : ringType) := Scale.isLaw.Build R R *%R
(@mulN1r R) (@mulrBr R).
#[export]
HB.instance Definition _ (R : ringType) (U : lmodType R) :=
Scale.isLaw.Build R U *:%R (@scaleN1r R U) (@scalerBr R U).
#[export]
HB.instance Definition _ (R : ringType) (V : zmodType) (s : Scale.law R V)
(aR : ringType) (nu : {rmorphism aR → R}) :=
Scale.isLaw.Build aR V (nu \; s)
(@Scale.compN1op _ _ s _ nu) (fun a ⇒ Scale.opB _ _).
#[export, non_forgetful_inheritance]
HB.instance Definition _ (R : ringType) (V : zmodType) (s : Scale.law R V) a :=
isAdditive.Build V V (s a) (Scale.opB s a).
Definition scalable_for (R : ringType) (U : lmodType R) (V : zmodType)
(s : R → V → V) (f : U → V) :=
∀ a, {morph f : u / a *: u >-> s a u}.
Definition linear_for (R : ringType) (U : lmodType R) (V : zmodType)
(s : R → V → V) (f : U → V) :=
∀ a, {morph f : u v / a *: u + v >-> s a u + v}.
Lemma additive_linear (R : ringType) (U : lmodType R) V
(s : Scale.law R V) (f : U → V) : linear_for s f → additive f.
Lemma scalable_linear (R : ringType) (U : lmodType R) V
(s : Scale.law R V) (f : U → V) : linear_for s f → scalable_for s f.
Module LinearExports.
Notation scalable f := (scalable_for *:%R f).
Notation linear f := (linear_for *:%R f).
Notation scalar f := (linear_for *%R f).
Module Linear.
Section Linear.
Variables (R : ringType) (U : lmodType R) (V : zmodType) (s : R → V → V).
Definition apply_deprecated (phUV : phant (U → V)) := @Linear.sort R U V s.
#[deprecated(since="mathcomp 2.0", note="Use Linear.sort instead.")]
Notation apply := apply_deprecated.
Support for right-to-left rewriting with the generic linearZ rule.
Definition map_class := mapUV.
Definition map_at (a : R) := mapUV.
Structure map_for a s_a := MapFor {map_for_map : mapUV; _ : s a = s_a}.
Definition unify_map_at a (f : map_at a) := MapFor f (erefl (s a)).
Structure wrapped := Wrap {unwrap : mapUV}.
Definition wrap (f : map_class) := Wrap f.
End Linear.
End Linear.
Notation "{ 'linear' U -> V | s }" := (@Linear.type _ U%type V%type s)
: type_scope.
Notation "{ 'linear' U -> V }" := {linear U%type → V%type | *:%R}
: type_scope.
Notation "{ 'scalar' U }" := {linear U → _ | *%R}
(at level 0, format "{ 'scalar' U }") : type_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use GRing.Linear.clone instead.")]
Notation "[ 'linear' 'of' f 'as' g ]" := (Linear.clone _ _ _ _ f%function g)
(at level 0, format "[ 'linear' 'of' f 'as' g ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use GRing.Linear.clone instead.")]
Notation "[ 'linear' 'of' f ]" := (Linear.clone _ _ _ _ f%function _)
(at level 0, format "[ 'linear' 'of' f ]") : form_scope.
Definition map_at (a : R) := mapUV.
Structure map_for a s_a := MapFor {map_for_map : mapUV; _ : s a = s_a}.
Definition unify_map_at a (f : map_at a) := MapFor f (erefl (s a)).
Structure wrapped := Wrap {unwrap : mapUV}.
Definition wrap (f : map_class) := Wrap f.
End Linear.
End Linear.
Notation "{ 'linear' U -> V | s }" := (@Linear.type _ U%type V%type s)
: type_scope.
Notation "{ 'linear' U -> V }" := {linear U%type → V%type | *:%R}
: type_scope.
Notation "{ 'scalar' U }" := {linear U → _ | *%R}
(at level 0, format "{ 'scalar' U }") : type_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use GRing.Linear.clone instead.")]
Notation "[ 'linear' 'of' f 'as' g ]" := (Linear.clone _ _ _ _ f%function g)
(at level 0, format "[ 'linear' 'of' f 'as' g ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use GRing.Linear.clone instead.")]
Notation "[ 'linear' 'of' f ]" := (Linear.clone _ _ _ _ f%function _)
(at level 0, format "[ 'linear' 'of' f ]") : form_scope.
Support for right-to-left rewriting with the generic linearZ rule.
Coercion Linear.map_for_map : Linear.map_for >-> Linear.type.
Coercion Linear.unify_map_at : Linear.map_at >-> Linear.map_for.
Canonical Linear.unify_map_at.
Coercion Linear.unwrap : Linear.wrapped >-> Linear.type.
Coercion Linear.wrap : Linear.map_class >-> Linear.wrapped.
Canonical Linear.wrap.
End LinearExports.
Section LinearTheory.
Variable R : ringType.
Section GenericProperties.
Variables (U : lmodType R) (V : zmodType) (s : R → V → V) (k : unit).
Variable f : {linear U → V | s}.
Lemma linear0 : f 0 = 0.
Lemma linearN : {morph f : x / - x}.
Lemma linearD : {morph f : x y / x + y}.
Lemma linearB : {morph f : x y / x - y}.
Lemma linearMn n : {morph f : x / x *+ n}.
Lemma linearMNn n : {morph f : x / x *- n}.
Lemma linear_sum I r (P : pred I) E :
f (\sum_(i <- r | P i) E i) = \sum_(i <- r | P i) f (E i).
Lemma linearZ_LR : scalable_for s f.
Lemma linearP a : {morph f : u v / a *: u + v >-> s a u + v}.
End GenericProperties.
Section BidirectionalLinearZ.
Variables (U : lmodType R) (V : zmodType) (s : R → V → V).
Coercion Linear.unify_map_at : Linear.map_at >-> Linear.map_for.
Canonical Linear.unify_map_at.
Coercion Linear.unwrap : Linear.wrapped >-> Linear.type.
Coercion Linear.wrap : Linear.map_class >-> Linear.wrapped.
Canonical Linear.wrap.
End LinearExports.
Section LinearTheory.
Variable R : ringType.
Section GenericProperties.
Variables (U : lmodType R) (V : zmodType) (s : R → V → V) (k : unit).
Variable f : {linear U → V | s}.
Lemma linear0 : f 0 = 0.
Lemma linearN : {morph f : x / - x}.
Lemma linearD : {morph f : x y / x + y}.
Lemma linearB : {morph f : x y / x - y}.
Lemma linearMn n : {morph f : x / x *+ n}.
Lemma linearMNn n : {morph f : x / x *- n}.
Lemma linear_sum I r (P : pred I) E :
f (\sum_(i <- r | P i) E i) = \sum_(i <- r | P i) f (E i).
Lemma linearZ_LR : scalable_for s f.
Lemma linearP a : {morph f : u v / a *: u + v >-> s a u + v}.
End GenericProperties.
Section BidirectionalLinearZ.
Variables (U : lmodType R) (V : zmodType) (s : R → V → V).
The general form of the linearZ lemma uses some bespoke interfaces to
allow right-to-left rewriting when a composite scaling operation such as
conjC \; *%R has been expanded, say in a^* * f u. This redex is matched
by using the Scale.law interface to recognize a "head" scaling operation
h (here *%R), stow away its "scalar" c, then reconcile h c and s a, once
s is known, that is, once the Linear.map structure for f has been found.
In general, s and a need not be equal to h and c; indeed they need not
have the same type! The unification is performed by the unify_map_at
default instance for the Linear.map_for U s a h_c sub-interface of
Linear.map; the h_c pattern uses the Scale.law structure to insure it is
inferred when rewriting right-to-left.
The wrap on the rhs allows rewriting f (a *: b *: u) into a *: b *: f u
with rewrite !linearZ /= instead of rewrite linearZ /= linearZ /=.
Without it, the first rewrite linearZ would produce
(a *: apply (map_for_map (@check_map_at .. a f)) (b *: u)%R)%Rlin
and matching the second rewrite LHS would bypass the unify_map_at default
instance for b, reuse the one for a, and subsequently fail to match the
b *: u argument. The extra wrap / unwrap ensures that this can't happen.
In the RL direction, the wrap / unwrap will be inserted on the redex side
as needed, without causing unnecessary delta-expansion: using an explicit
identity function would have Coq normalize the redex to head normal, then
reduce the identity to expose the map_for_map projection, and the
expanded Linear.map structure would then be exposed in the result.
Most of this machinery will be invisible to a casual user, because all
the projections and default instances involved are declared as coercions.
Variables (S : ringType) (h : Scale.law S V).
Lemma linearZ c a (h_c := h c) (f : Linear.map_for U s a h_c) u :
f (a *: u) = h_c (Linear.wrap f u).
End BidirectionalLinearZ.
Section LmodProperties.
Variables (U V : lmodType R) (f : {linear U → V}).
Lemma linearZZ : scalable f.
Lemma linearPZ : linear f.
Lemma can2_scalable f' : cancel f f' → cancel f' f → scalable f'.
Lemma can2_linear f' : cancel f f' → cancel f' f → linear f'.
End LmodProperties.
Section ScalarProperties.
Variable (U : lmodType R) (f : {scalar U}).
Lemma scalarZ : scalable_for *%R f.
Lemma scalarP : scalar f.
End ScalarProperties.
Section LinearLmod.
Variables (W U : lmodType R) (V : zmodType).
Section Plain.
Variable (s : R → V → V).
Variables (f : {linear U → V | s}) (h : {linear W → U}).
Lemma idfun_is_scalable : scalable (@idfun U).
#[export]
HB.instance Definition _ := isScalable.Build R U U *:%R idfun idfun_is_scalable.
Lemma opp_is_scalable : scalable (-%R : U → U).
#[export]
HB.instance Definition _ := isScalable.Build R U U *:%R -%R opp_is_scalable.
Lemma comp_is_scalable : scalable_for s (f \o h).
#[export]
HB.instance Definition _ := isScalable.Build R W V s (f \o h) comp_is_scalable.
End Plain.
Section Scale.
Variable (s : Scale.law R V).
Variables (f : {linear U → V | s}) (g : {linear U → V | s}).
Lemma null_fun_is_scalable : scalable_for s (\0 : U → V).
#[export]
HB.instance Definition _ := isScalable.Build R U V s \0 null_fun_is_scalable.
Lemma add_fun_is_scalable : scalable_for s (f \+ g).
#[export]
HB.instance Definition _ := isScalable.Build R U V s (f \+ g) add_fun_is_scalable.
Lemma sub_fun_is_scalable : scalable_for s (f \- g).
#[export]
HB.instance Definition _ := isScalable.Build R U V s (f \- g) sub_fun_is_scalable.
Lemma opp_fun_is_scalable : scalable_for s (\- g).
#[export]
HB.instance Definition _ := isScalable.Build R U V s (\- g) opp_fun_is_scalable.
End Scale.
End LinearLmod.
Section LinearLalg.
Variables (A : lalgType R) (U : lmodType R).
Variables (a : A) (f : {linear U → A}).
Fact mulr_fun_is_scalable : scalable (a \o× f).
#[export]
HB.instance Definition _ := isScalable.Build R U A *:%R (a \o× f)
mulr_fun_is_scalable.
End LinearLalg.
End LinearTheory.
FIXME: remove the @ once
https://github.com/math-comp/hierarchy-builder/issues/319 is fixed
Module LRMorphismExports.
Module LRMorphism.
Definition apply_deprecated (R : ringType) (A : lalgType R) (B : ringType)
(s : R → B → B) (phAB : phant (A → B)) := @LRMorphism.sort R A B s.
#[deprecated(since="mathcomp 2.0", note="Use LRMorphism.sort instead.")]
Notation apply := apply_deprecated.
End LRMorphism.
Notation "{ 'lrmorphism' A -> B | s }" := (@LRMorphism.type _ A%type B%type s)
: type_scope.
Notation "{ 'lrmorphism' A -> B }" := {lrmorphism A%type → B%type | *:%R}
: type_scope.
#[deprecated(since="mathcomp 2.0.0",
note="Use GRing.LRMorphism.clone instead.")]
Notation "[ 'lrmorphism' 'of' f ]" := (LRMorphism.clone _ _ _ _ f%function _)
(at level 0, format "[ 'lrmorphism' 'of' f ]") : form_scope.
End LRMorphismExports.
Section LRMorphismTheory.
Variables (R : ringType) (A B : lalgType R) (C : ringType) (s : R → C → C).
Variables (k : unit) (f : {lrmorphism A → B}) (g : {lrmorphism B → C | s}).
#[export] HB.instance Definition _ := RMorphism.on (@idfun A).
#[export] HB.instance Definition _ := RMorphism.on (g \o f).
Lemma rmorph_alg a : f a%:A = a%:A.
End LRMorphismTheory.
#[short(type="comSemiRingType")]
HB.structure Definition ComSemiRing :=
{R of SemiRing R & SemiRing_hasCommutativeMul R}.
Module ComSemiRingExports.
Bind Scope ring_scope with ComSemiRing.sort.
#[deprecated(since="mathcomp 2.0.0",
note="Use GRing.ComSemiRing.clone instead.")]
Notation "[ 'comSemiRingType' 'of' T 'for' cT ]" := (ComSemiRing.clone T cT)
(at level 0, format "[ 'comSemiRingType' 'of' T 'for' cT ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0",
note="Use GRing.ComSemiRing.clone instead.")]
Notation "[ 'comSemiRingType' 'of' T ]" := (ComSemiRing.clone T _)
(at level 0, format "[ 'comSemiRingType' 'of' T ]") : form_scope.
End ComSemiRingExports.
Definition mulr1 := Monoid.mulC_id mulrC mul1r.
Definition mulrDr := Monoid.mulC_dist mulrC mulrDl.
Lemma mulr0 : right_zero zero mul.
Section ComSemiRingTheory.
Variable R : comSemiRingType.
Implicit Types x y : R.
#[export]
HB.instance Definition _ := SemiGroup.isCommutativeLaw.Build R *%R mulrC.
Lemma mulrCA : @left_commutative R R *%R.
Lemma mulrAC : @right_commutative R R *%R.
Lemma mulrACA : @interchange R *%R *%R.
Lemma exprMn n : {morph (fun x ⇒ x ^+ n) : x y / x × y}.
Lemma prodrXl n I r (P : pred I) (F : I → R) :
\prod_(i <- r | P i) F i ^+ n = (\prod_(i <- r | P i) F i) ^+ n.
Lemma prodr_undup_exp_count (I : eqType) r (P : pred I) (F : I → R) :
\prod_(i <- undup r | P i) F i ^+ count_mem i r = \prod_(i <- r | P i) F i.
Lemma exprDn x y n :
(x + y) ^+ n = \sum_(i < n.+1) (x ^+ (n - i) × y ^+ i) *+ 'C(n, i).
Lemma sqrrD x y : (x + y) ^+ 2 = x ^+ 2 + x × y *+ 2 + y ^+ 2.
End ComSemiRingTheory.
#[short(type="comRingType")]
HB.structure Definition ComRing := {R of Ring R & ComSemiRing R}.
Definition mulr1 := Monoid.mulC_id mulrC mul1r.
Definition mulrDr := Monoid.mulC_dist mulrC mulrDl.
Module ComRingExports.
Bind Scope ring_scope with ComRing.sort.
#[deprecated(since="mathcomp 2.0.0",
note="Use GRing.ComSemiRing.clone instead.")]
Notation "[ 'comRingType' 'of' T 'for' cT ]" := (ComRing.clone T%type cT)
(at level 0, format "[ 'comRingType' 'of' T 'for' cT ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0",
note="Use GRing.ComSemiRing.clone instead.")]
Notation "[ 'comRingType' 'of' T ]" := (ComRing.clone T%type _)
(at level 0, format "[ 'comRingType' 'of' T ]") : form_scope.
End ComRingExports.
Section ComRingTheory.
Variable R : comRingType.
Implicit Types x y : R.
Lemma exprBn x y n :
(x - y) ^+ n =
\sum_(i < n.+1) ((-1) ^+ i × x ^+ (n - i) × y ^+ i) *+ 'C(n, i).
Lemma subrXX x y n :
x ^+ n - y ^+ n = (x - y) × (\sum_(i < n) x ^+ (n.-1 - i) × y ^+ i).
Lemma sqrrB x y : (x - y) ^+ 2 = x ^+ 2 - x × y *+ 2 + y ^+ 2.
Lemma subr_sqr x y : x ^+ 2 - y ^+ 2 = (x - y) × (x + y).
Lemma subr_sqrDB x y : (x + y) ^+ 2 - (x - y) ^+ 2 = x × y *+ 4.
Section FrobeniusAutomorphism.
Variables (p : nat) (charRp : p \in char R).
Lemma Frobenius_aut_is_additive : additive (Frobenius_aut charRp).
Lemma Frobenius_aut_is_multiplicative : multiplicative (Frobenius_aut charRp).
#[export]
HB.instance Definition _ := isAdditive.Build R R (Frobenius_aut charRp)
Frobenius_aut_is_additive.
#[export]
HB.instance Definition _ := isMultiplicative.Build R R (Frobenius_aut charRp)
Frobenius_aut_is_multiplicative.
End FrobeniusAutomorphism.
Lemma exprDn_char x y n : (char R).-nat n → (x + y) ^+ n = x ^+ n + y ^+ n.
Lemma rmorph_comm (S : ringType) (f : {rmorphism R → S}) x y :
comm (f x) (f y).
Section ScaleLinear.
Variables (U V : lmodType R) (b : R) (f : {linear U → V}).
Lemma scale_is_scalable : scalable ( *:%R b : V → V).
#[export]
HB.instance Definition _ := isScalable.Build R V V *:%R ( *:%R b)
scale_is_scalable.
Lemma scale_fun_is_scalable : scalable (b \*: f).
#[export]
HB.instance Definition _ := isScalable.Build R U V *:%R (b \*: f)
scale_fun_is_scalable.
End ScaleLinear.
End ComRingTheory.
#[short(type="algType")]
HB.structure Definition Algebra (R : ringType) :=
{A of Lalgebra_isAlgebra R A & Lalgebra R A}.
Module AlgExports.
Bind Scope ring_scope with Algebra.sort.
#[deprecated(since="mathcomp 2.0.0", note="Use GRing.Algebra.clone instead.")]
Notation "[ 'algType' R 'of' T 'for' cT ]" := (Algebra.clone R T%type cT)
(at level 0, format "[ 'algType' R 'of' T 'for' cT ]")
: form_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use GRing.Algebra.clone instead.")]
Notation "[ 'algType' R 'of' T ]" := (Algebra.clone R T%type _)
(at level 0, format "[ 'algType' R 'of' T ]") : form_scope.
End AlgExports.
Lemma scalarAr k (x y : V) : k *: (x × y) = x × (k *: y).
#[short(type="comAlgType")]
HB.structure Definition ComAlgebra R := {V of ComRing V & Algebra R V}.
Module ComAlgExports.
Bind Scope ring_scope with ComAlgebra.sort.
#[deprecated(since="mathcomp 2.0.0",
note="Use GRing.ComAlgebra.clone instead.")]
Notation "[ 'comAlgType' R 'of' T ]" := (ComAlgebra.clone R T%type _)
(at level 0, format "[ 'comAlgType' R 'of' T ]") : form_scope.
End ComAlgExports.
Section AlgebraTheory.
Variables (R : comRingType).
#[export]
HB.instance Definition _ :=
SemiRing_hasCommutativeMul.Build R^c (fun _ _ ⇒ mulrC _ _).
#[export]
HB.instance Definition _ := ComSemiRing.on R^o.
#[export]
HB.instance Definition _ := Lalgebra_isComAlgebra.Build R R^o.
End AlgebraTheory.
Section AlgebraTheory.
TODO: MC-1 port (R has been changed from comRingType to ringType)
Variables (R : ringType) (A : algType R).
Implicit Types (k : R) (x y : A).
Lemma scalerCA k x y : k *: x × y = x × (k *: y).
Lemma mulr_algr a x : x × a%:A = a *: x.
Lemma comm_alg a x : comm a%:A x.
Lemma exprZn k x n : (k *: x) ^+ n = k ^+ n *: x ^+ n.
Lemma scaler_prod I r (P : pred I) (F : I → R) (G : I → A) :
\prod_(i <- r | P i) (F i *: G i) =
\prod_(i <- r | P i) F i *: \prod_(i <- r | P i) G i.
Lemma scaler_prodl (I : finType) (S : pred I) (F : I → A) k :
\prod_(i in S) (k *: F i) = k ^+ #|S| *: \prod_(i in S) F i.
Lemma scaler_prodr (I : finType) (S : pred I) (F : I → R) x :
\prod_(i in S) (F i *: x) = \prod_(i in S) F i *: x ^+ #|S|.
Variables (U : lmodType R) (a : A) (f : {linear U → A}).
Lemma mull_fun_is_scalable : scalable (a \*o f).
#[export]
HB.instance Definition _ := isScalable.Build R U A *:%R (a \*o f)
mull_fun_is_scalable.
End AlgebraTheory.
#[short(type="unitRingType")]
HB.structure Definition UnitRing := {R of Ring_hasMulInverse R & Ring R}.
Module UnitRingExports.
Bind Scope ring_scope with UnitRing.sort.
#[deprecated(since="mathcomp 2.0.0", note="Use GRing.UnitRing.clone instead.")]
Notation "[ 'unitRingType' 'of' T 'for' cT ]" := (UnitRing.clone T%type cT)
(at level 0, format "[ 'unitRingType' 'of' T 'for' cT ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use GRing.UnitRing.clone instead.")]
Notation "[ 'unitRingType' 'of' T ]" := (UnitRing.clone T%type _)
(at level 0, format "[ 'unitRingType' 'of' T ]") : form_scope.
End UnitRingExports.
Definition unit_pred {R : unitRingType} :=
Eval cbv [ unit_subdef Ring_hasMulInverse.unit_subdef ] in
(fun u : R ⇒ unit_subdef u).
Arguments unit_pred _ _ /.
Definition unit {R : unitRingType} := [qualify a u : R | unit_pred u].
Section UnitRingTheory.
Variable R : unitRingType.
Implicit Types x y : R.
Lemma divrr : {in unit, right_inverse 1 (@inv R) *%R}.
Definition mulrV := divrr.
Lemma mulVr : {in unit, left_inverse 1 (@inv R) *%R}.
Lemma invr_out x : x \isn't a unit → x^-1 = x.
Lemma unitrP x : reflect (∃ y, y × x = 1 ∧ x × y = 1) (x \is a unit).
Lemma mulKr : {in unit, left_loop (@inv R) *%R}.
Lemma mulVKr : {in unit, rev_left_loop (@inv R) *%R}.
Lemma mulrK : {in unit, right_loop (@inv R) *%R}.
Lemma mulrVK : {in unit, rev_right_loop (@inv R) *%R}.
Definition divrK := mulrVK.
Lemma mulrI : {in @unit R, right_injective *%R}.
Lemma mulIr : {in @unit R, left_injective *%R}.
Implicit Types (k : R) (x y : A).
Lemma scalerCA k x y : k *: x × y = x × (k *: y).
Lemma mulr_algr a x : x × a%:A = a *: x.
Lemma comm_alg a x : comm a%:A x.
Lemma exprZn k x n : (k *: x) ^+ n = k ^+ n *: x ^+ n.
Lemma scaler_prod I r (P : pred I) (F : I → R) (G : I → A) :
\prod_(i <- r | P i) (F i *: G i) =
\prod_(i <- r | P i) F i *: \prod_(i <- r | P i) G i.
Lemma scaler_prodl (I : finType) (S : pred I) (F : I → A) k :
\prod_(i in S) (k *: F i) = k ^+ #|S| *: \prod_(i in S) F i.
Lemma scaler_prodr (I : finType) (S : pred I) (F : I → R) x :
\prod_(i in S) (F i *: x) = \prod_(i in S) F i *: x ^+ #|S|.
Variables (U : lmodType R) (a : A) (f : {linear U → A}).
Lemma mull_fun_is_scalable : scalable (a \*o f).
#[export]
HB.instance Definition _ := isScalable.Build R U A *:%R (a \*o f)
mull_fun_is_scalable.
End AlgebraTheory.
#[short(type="unitRingType")]
HB.structure Definition UnitRing := {R of Ring_hasMulInverse R & Ring R}.
Module UnitRingExports.
Bind Scope ring_scope with UnitRing.sort.
#[deprecated(since="mathcomp 2.0.0", note="Use GRing.UnitRing.clone instead.")]
Notation "[ 'unitRingType' 'of' T 'for' cT ]" := (UnitRing.clone T%type cT)
(at level 0, format "[ 'unitRingType' 'of' T 'for' cT ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use GRing.UnitRing.clone instead.")]
Notation "[ 'unitRingType' 'of' T ]" := (UnitRing.clone T%type _)
(at level 0, format "[ 'unitRingType' 'of' T ]") : form_scope.
End UnitRingExports.
Definition unit_pred {R : unitRingType} :=
Eval cbv [ unit_subdef Ring_hasMulInverse.unit_subdef ] in
(fun u : R ⇒ unit_subdef u).
Arguments unit_pred _ _ /.
Definition unit {R : unitRingType} := [qualify a u : R | unit_pred u].
Section UnitRingTheory.
Variable R : unitRingType.
Implicit Types x y : R.
Lemma divrr : {in unit, right_inverse 1 (@inv R) *%R}.
Definition mulrV := divrr.
Lemma mulVr : {in unit, left_inverse 1 (@inv R) *%R}.
Lemma invr_out x : x \isn't a unit → x^-1 = x.
Lemma unitrP x : reflect (∃ y, y × x = 1 ∧ x × y = 1) (x \is a unit).
Lemma mulKr : {in unit, left_loop (@inv R) *%R}.
Lemma mulVKr : {in unit, rev_left_loop (@inv R) *%R}.
Lemma mulrK : {in unit, right_loop (@inv R) *%R}.
Lemma mulrVK : {in unit, rev_right_loop (@inv R) *%R}.
Definition divrK := mulrVK.
Lemma mulrI : {in @unit R, right_injective *%R}.
Lemma mulIr : {in @unit R, left_injective *%R}.
Due to noncommutativity, fractions are inverted.
Lemma telescope_prodr n m (f : nat → R) :
(∀ k, n < k < m → f k \is a unit) → n < m →
\prod_(n ≤ k < m) (f k / f k.+1) = f n / f m.
Lemma telescope_prodr_eq n m (f u : nat → R) : n < m →
(∀ k, n < k < m → f k \is a unit) →
(∀ k, (n ≤ k < m)%N → u k = f k / f k.+1) →
\prod_(n ≤ k < m) u k = f n / f m.
Lemma commrV x y : comm x y → comm x y^-1.
Lemma unitrE x : (x \is a unit) = (x / x == 1).
Lemma invrK : involutive (@inv R).
Lemma invr_inj : injective (@inv R).
Lemma unitrV x : (x^-1 \in unit) = (x \in unit).
Lemma unitr1 : 1 \in @unit R.
Lemma invr1 : 1^-1 = 1 :> R.
Lemma div1r x : 1 / x = x^-1.
Lemma divr1 x : x / 1 = x.
Lemma natr_div m d :
d %| m → d%:R \is a @unit R → (m %/ d)%:R = m%:R / d%:R :> R.
Lemma divrI : {in unit, right_injective (fun x y ⇒ x / y)}.
Lemma divIr : {in unit, left_injective (fun x y ⇒ x / y)}.
Lemma unitr0 : (0 \is a @unit R) = false.
Lemma invr0 : 0^-1 = 0 :> R.
Lemma unitrN1 : -1 \is a @unit R.
Lemma invrN1 : (-1)^-1 = -1 :> R.
Lemma invr_sign n : ((-1) ^- n) = (-1) ^+ n :> R.
Lemma unitrMl x y : y \is a unit → (x × y \is a unit) = (x \is a unit).
Lemma unitrMr x y : x \is a unit → (x × y \is a unit) = (y \is a unit).
Lemma invrM : {in unit &, ∀ x y, (x × y)^-1 = y^-1 × x^-1}.
Lemma unitrM_comm x y :
comm x y → (x × y \is a unit) = (x \is a unit) && (y \is a unit).
Lemma unitrX x n : x \is a unit → x ^+ n \is a unit.
Lemma unitrX_pos x n : n > 0 → (x ^+ n \in unit) = (x \in unit).
Lemma exprVn x n : x^-1 ^+ n = x ^- n.
Lemma exprB m n x : n ≤ m → x \is a unit → x ^+ (m - n) = x ^+ m / x ^+ n.
Lemma invr_neq0 x : x != 0 → x^-1 != 0.
Lemma invr_eq0 x : (x^-1 == 0) = (x == 0).
Lemma invr_eq1 x : (x^-1 == 1) = (x == 1).
Lemma rev_unitrP (x y : R^c) : y × x = 1 ∧ x × y = 1 → x \is a unit.
End UnitRingTheory.
Arguments invrK {R}.
Arguments invr_inj {R} [x1 x2].
Arguments telescope_prodr_eq {R n m} f u.
Module RegularConverseUnitRingExports.
Section UnitRingTheory.
Variable R : unitRingType.
Implicit Types x y : R.
End UnitRingTheory.
End RegularConverseUnitRingExports.
Section UnitRingClosedPredicates.
Variable R : unitRingType.
Implicit Types x y : R.
Variables S : {pred R}.
Definition invr_closed := {in S, ∀ x, x^-1 \in S}.
Definition divr_2closed := {in S &, ∀ x y, x / y \in S}.
Definition divr_closed := 1 \in S ∧ divr_2closed.
Definition sdivr_closed := -1 \in S ∧ divr_2closed.
Definition divring_closed := [/\ 1 \in S, subr_2closed S & divr_2closed].
Lemma divr_closedV : divr_closed → invr_closed.
Lemma divr_closedM : divr_closed → mulr_closed S.
Lemma sdivr_closed_div : sdivr_closed → divr_closed.
Lemma sdivr_closedM : sdivr_closed → smulr_closed S.
Lemma divring_closedBM : divring_closed → subring_closed S.
Lemma divring_closed_div : divring_closed → sdivr_closed.
End UnitRingClosedPredicates.
Section UnitRingMorphism.
Variables (R S : unitRingType) (f : {rmorphism R → S}).
Lemma rmorph_unit x : x \in unit → f x \in unit.
Lemma rmorphV : {in unit, {morph f: x / x^-1}}.
Lemma rmorph_div x y : y \in unit → f (x / y) = f x / f y.
End UnitRingMorphism.
#[short(type="comUnitRingType")]
HB.structure Definition ComUnitRing := {R of ComRing R & UnitRing R}.
Module ComUnitRingExports.
Bind Scope ring_scope with ComUnitRing.sort.
#[deprecated(since="mathcomp 2.0.0",
note="Use GRing.ComUnitRing.clone instead.")]
Notation "[ 'comUnitRingType' 'of' T ]" := (ComUnitRing.clone T%type _)
(at level 0, format "[ 'comUnitRingType' 'of' T ]") : form_scope.
End ComUnitRingExports.
(∀ k, n < k < m → f k \is a unit) → n < m →
\prod_(n ≤ k < m) (f k / f k.+1) = f n / f m.
Lemma telescope_prodr_eq n m (f u : nat → R) : n < m →
(∀ k, n < k < m → f k \is a unit) →
(∀ k, (n ≤ k < m)%N → u k = f k / f k.+1) →
\prod_(n ≤ k < m) u k = f n / f m.
Lemma commrV x y : comm x y → comm x y^-1.
Lemma unitrE x : (x \is a unit) = (x / x == 1).
Lemma invrK : involutive (@inv R).
Lemma invr_inj : injective (@inv R).
Lemma unitrV x : (x^-1 \in unit) = (x \in unit).
Lemma unitr1 : 1 \in @unit R.
Lemma invr1 : 1^-1 = 1 :> R.
Lemma div1r x : 1 / x = x^-1.
Lemma divr1 x : x / 1 = x.
Lemma natr_div m d :
d %| m → d%:R \is a @unit R → (m %/ d)%:R = m%:R / d%:R :> R.
Lemma divrI : {in unit, right_injective (fun x y ⇒ x / y)}.
Lemma divIr : {in unit, left_injective (fun x y ⇒ x / y)}.
Lemma unitr0 : (0 \is a @unit R) = false.
Lemma invr0 : 0^-1 = 0 :> R.
Lemma unitrN1 : -1 \is a @unit R.
Lemma invrN1 : (-1)^-1 = -1 :> R.
Lemma invr_sign n : ((-1) ^- n) = (-1) ^+ n :> R.
Lemma unitrMl x y : y \is a unit → (x × y \is a unit) = (x \is a unit).
Lemma unitrMr x y : x \is a unit → (x × y \is a unit) = (y \is a unit).
Lemma invrM : {in unit &, ∀ x y, (x × y)^-1 = y^-1 × x^-1}.
Lemma unitrM_comm x y :
comm x y → (x × y \is a unit) = (x \is a unit) && (y \is a unit).
Lemma unitrX x n : x \is a unit → x ^+ n \is a unit.
Lemma unitrX_pos x n : n > 0 → (x ^+ n \in unit) = (x \in unit).
Lemma exprVn x n : x^-1 ^+ n = x ^- n.
Lemma exprB m n x : n ≤ m → x \is a unit → x ^+ (m - n) = x ^+ m / x ^+ n.
Lemma invr_neq0 x : x != 0 → x^-1 != 0.
Lemma invr_eq0 x : (x^-1 == 0) = (x == 0).
Lemma invr_eq1 x : (x^-1 == 1) = (x == 1).
Lemma rev_unitrP (x y : R^c) : y × x = 1 ∧ x × y = 1 → x \is a unit.
End UnitRingTheory.
Arguments invrK {R}.
Arguments invr_inj {R} [x1 x2].
Arguments telescope_prodr_eq {R n m} f u.
Module RegularConverseUnitRingExports.
Section UnitRingTheory.
Variable R : unitRingType.
Implicit Types x y : R.
End UnitRingTheory.
End RegularConverseUnitRingExports.
Section UnitRingClosedPredicates.
Variable R : unitRingType.
Implicit Types x y : R.
Variables S : {pred R}.
Definition invr_closed := {in S, ∀ x, x^-1 \in S}.
Definition divr_2closed := {in S &, ∀ x y, x / y \in S}.
Definition divr_closed := 1 \in S ∧ divr_2closed.
Definition sdivr_closed := -1 \in S ∧ divr_2closed.
Definition divring_closed := [/\ 1 \in S, subr_2closed S & divr_2closed].
Lemma divr_closedV : divr_closed → invr_closed.
Lemma divr_closedM : divr_closed → mulr_closed S.
Lemma sdivr_closed_div : sdivr_closed → divr_closed.
Lemma sdivr_closedM : sdivr_closed → smulr_closed S.
Lemma divring_closedBM : divring_closed → subring_closed S.
Lemma divring_closed_div : divring_closed → sdivr_closed.
End UnitRingClosedPredicates.
Section UnitRingMorphism.
Variables (R S : unitRingType) (f : {rmorphism R → S}).
Lemma rmorph_unit x : x \in unit → f x \in unit.
Lemma rmorphV : {in unit, {morph f: x / x^-1}}.
Lemma rmorph_div x y : y \in unit → f (x / y) = f x / f y.
End UnitRingMorphism.
#[short(type="comUnitRingType")]
HB.structure Definition ComUnitRing := {R of ComRing R & UnitRing R}.
Module ComUnitRingExports.
Bind Scope ring_scope with ComUnitRing.sort.
#[deprecated(since="mathcomp 2.0.0",
note="Use GRing.ComUnitRing.clone instead.")]
Notation "[ 'comUnitRingType' 'of' T ]" := (ComUnitRing.clone T%type _)
(at level 0, format "[ 'comUnitRingType' 'of' T ]") : form_scope.
End ComUnitRingExports.
TODO_HB: fix the name (was ComUnitRingMixin)
Fact mulC_mulrV : {in unit, right_inverse 1 inv *%R}.
Fact mulC_unitP x y : y × x = 1 ∧ x × y = 1 → unit x.
#[short(type="unitAlgType")]
HB.structure Definition UnitAlgebra R := {V of Algebra R V & UnitRing V}.
Module UnitAlgebraExports.
Bind Scope ring_scope with UnitAlgebra.sort.
#[deprecated(since="mathcomp 2.0.0",
note="Use GRing.UnitAlgebra.clone instead.")]
Notation "[ 'unitAlgType' R 'of' T ]" := (UnitAlgebra.clone R T%type _)
(at level 0, format "[ 'unitAlgType' R 'of' T ]") : form_scope.
End UnitAlgebraExports.
#[short(type="comUnitAlgType")]
HB.structure Definition ComUnitAlgebra R := {V of ComAlgebra R V & UnitRing V}.
Module ComUnitAlgebraExports.
Bind Scope ring_scope with UnitAlgebra.sort.
#[deprecated(since="mathcomp 2.0.0",
note="Use GRing.ComUnitAlgebra.clone instead.")]
Notation "[ 'comUnitAlgType' R 'of' T ]" := (ComUnitAlgebra.clone R T%type _)
(at level 0, format "[ 'comUnitAlgType' R 'of' T ]") : form_scope.
End ComUnitAlgebraExports.
Section ComUnitRingTheory.
Variable R : comUnitRingType.
Implicit Types x y : R.
Lemma unitrM x y : (x × y \in unit) = (x \in unit) && (y \in unit).
Lemma unitrPr x : reflect (∃ y, x × y = 1) (x \in unit).
Lemma mulr1_eq x y : x × y = 1 → x^-1 = y.
Lemma divr1_eq x y : x / y = 1 → x = y.
Lemma divKr x : x \is a unit → {in unit, involutive (fun y ⇒ x / y)}.
Lemma expr_div_n x y n : (x / y) ^+ n = x ^+ n / y ^+ n.
End ComUnitRingTheory.
Module RegularConverseComUnitRingExports.
Section ComUnitRingTheory.
Variable R : comUnitRingType.
Implicit Types x y : R.
TODO: HB.recover_all_instances (R^o).
End ComUnitRingTheory.
End RegularConverseComUnitRingExports.
Section UnitAlgebraTheory.
Variable (R : comUnitRingType) (A : unitAlgType R).
Implicit Types (k : R) (x y : A).
Lemma scaler_injl : {in unit, @right_injective R A A *:%R}.
Lemma scaler_unit k x : k \in unit → (k *: x \in unit) = (x \in unit).
Lemma invrZ k x : k \in unit → x \in unit → (k *: x)^-1 = k^-1 *: x^-1.
Section ClosedPredicates.
Variables S : {pred A}.
Definition divalg_closed := [/\ 1 \in S, linear_closed S & divr_2closed S].
Lemma divalg_closedBdiv : divalg_closed → divring_closed S.
Lemma divalg_closedZ : divalg_closed → subalg_closed S.
End ClosedPredicates.
End UnitAlgebraTheory.
Module ClosedExports.
Notation oppr_closed := oppr_closed.
Notation addr_closed := addr_closed.
Notation mulr_closed := mulr_closed.
Notation zmod_closed := zmod_closed.
Notation smulr_closed := smulr_closed.
Notation invr_closed := invr_closed.
Notation divr_closed := divr_closed.
Notation scaler_closed := scaler_closed.
Notation linear_closed := linear_closed.
Notation submod_closed := submod_closed.
Notation semiring_closed := semiring_closed.
Notation subring_closed := subring_closed.
Notation sdivr_closed := sdivr_closed.
Notation subalg_closed := subalg_closed.
Notation divring_closed := divring_closed.
Notation divalg_closed := divalg_closed.
Coercion zmod_closedD : zmod_closed >-> addr_closed.
Coercion zmod_closedN : zmod_closed >-> oppr_closed.
Coercion smulr_closedN : smulr_closed >-> oppr_closed.
Coercion smulr_closedM : smulr_closed >-> mulr_closed.
Coercion divr_closedV : divr_closed >-> invr_closed.
Coercion divr_closedM : divr_closed >-> mulr_closed.
Coercion submod_closedZ : submod_closed >-> scaler_closed.
Coercion submod_closedB : submod_closed >-> zmod_closed.
Coercion semiring_closedD : semiring_closed >-> addr_closed.
Coercion semiring_closedM : semiring_closed >-> mulr_closed.
Coercion subring_closedB : subring_closed >-> zmod_closed.
Coercion subring_closedM : subring_closed >-> smulr_closed.
Coercion subring_closed_semi : subring_closed >-> semiring_closed.
Coercion sdivr_closedM : sdivr_closed >-> smulr_closed.
Coercion sdivr_closed_div : sdivr_closed >-> divr_closed.
Coercion subalg_closedZ : subalg_closed >-> submod_closed.
Coercion subalg_closedBM : subalg_closed >-> subring_closed.
Coercion divring_closedBM : divring_closed >-> subring_closed.
Coercion divring_closed_div : divring_closed >-> sdivr_closed.
Coercion divalg_closedZ : divalg_closed >-> subalg_closed.
Coercion divalg_closedBdiv : divalg_closed >-> divring_closed.
End ClosedExports.
End RegularConverseComUnitRingExports.
Section UnitAlgebraTheory.
Variable (R : comUnitRingType) (A : unitAlgType R).
Implicit Types (k : R) (x y : A).
Lemma scaler_injl : {in unit, @right_injective R A A *:%R}.
Lemma scaler_unit k x : k \in unit → (k *: x \in unit) = (x \in unit).
Lemma invrZ k x : k \in unit → x \in unit → (k *: x)^-1 = k^-1 *: x^-1.
Section ClosedPredicates.
Variables S : {pred A}.
Definition divalg_closed := [/\ 1 \in S, linear_closed S & divr_2closed S].
Lemma divalg_closedBdiv : divalg_closed → divring_closed S.
Lemma divalg_closedZ : divalg_closed → subalg_closed S.
End ClosedPredicates.
End UnitAlgebraTheory.
Module ClosedExports.
Notation oppr_closed := oppr_closed.
Notation addr_closed := addr_closed.
Notation mulr_closed := mulr_closed.
Notation zmod_closed := zmod_closed.
Notation smulr_closed := smulr_closed.
Notation invr_closed := invr_closed.
Notation divr_closed := divr_closed.
Notation scaler_closed := scaler_closed.
Notation linear_closed := linear_closed.
Notation submod_closed := submod_closed.
Notation semiring_closed := semiring_closed.
Notation subring_closed := subring_closed.
Notation sdivr_closed := sdivr_closed.
Notation subalg_closed := subalg_closed.
Notation divring_closed := divring_closed.
Notation divalg_closed := divalg_closed.
Coercion zmod_closedD : zmod_closed >-> addr_closed.
Coercion zmod_closedN : zmod_closed >-> oppr_closed.
Coercion smulr_closedN : smulr_closed >-> oppr_closed.
Coercion smulr_closedM : smulr_closed >-> mulr_closed.
Coercion divr_closedV : divr_closed >-> invr_closed.
Coercion divr_closedM : divr_closed >-> mulr_closed.
Coercion submod_closedZ : submod_closed >-> scaler_closed.
Coercion submod_closedB : submod_closed >-> zmod_closed.
Coercion semiring_closedD : semiring_closed >-> addr_closed.
Coercion semiring_closedM : semiring_closed >-> mulr_closed.
Coercion subring_closedB : subring_closed >-> zmod_closed.
Coercion subring_closedM : subring_closed >-> smulr_closed.
Coercion subring_closed_semi : subring_closed >-> semiring_closed.
Coercion sdivr_closedM : sdivr_closed >-> smulr_closed.
Coercion sdivr_closed_div : sdivr_closed >-> divr_closed.
Coercion subalg_closedZ : subalg_closed >-> submod_closed.
Coercion subalg_closedBM : subalg_closed >-> subring_closed.
Coercion divring_closedBM : divring_closed >-> subring_closed.
Coercion divring_closed_div : divring_closed >-> sdivr_closed.
Coercion divalg_closedZ : divalg_closed >-> subalg_closed.
Coercion divalg_closedBdiv : divalg_closed >-> divring_closed.
End ClosedExports.
Reification of the theory of rings with units, in named style
Section TermDef.
Variable R : Type.
Inductive term : Type :=
| Var of nat
| Const of R
| NatConst of nat
| Add of term & term
| Opp of term
| NatMul of term & nat
| Mul of term & term
| Inv of term
| Exp of term & nat.
Inductive formula : Type :=
| Bool of bool
| Equal of term & term
| Unit of term
| And of formula & formula
| Or of formula & formula
| Implies of formula & formula
| Not of formula
| Exists of nat & formula
| Forall of nat & formula.
End TermDef.
Bind Scope term_scope with term.
Bind Scope term_scope with formula.
Arguments Add {R} t1%T t2%T.
Arguments Opp {R} t1%T.
Arguments NatMul {R} t1%T n%N.
Arguments Mul {R} t1%T t2%T.
Arguments Inv {R} t1%T.
Arguments Exp {R} t1%T n%N.
Arguments Equal {R} t1%T t2%T.
Arguments Unit {R} t1%T.
Arguments And {R} f1%T f2%T.
Arguments Or {R} f1%T f2%T.
Arguments Implies {R} f1%T f2%T.
Arguments Not {R} f1%T.
Arguments Exists {R} i%N f1%T.
Arguments Forall {R} i%N f1%T.
Arguments Bool {R} b.
Arguments Const {R} x.
Notation True := (Bool true).
Notation False := (Bool false).
Section Substitution.
Variable R : Type.
Fixpoint tsubst (t : term R) (s : nat × term R) :=
match t with
| 'X_i ⇒ if i == s.1 then s.2 else t
| _%:T | _%:R ⇒ t
| t1 + t2 ⇒ tsubst t1 s + tsubst t2 s
| - t1 ⇒ - tsubst t1 s
| t1 *+ n ⇒ tsubst t1 s *+ n
| t1 × t2 ⇒ tsubst t1 s × tsubst t2 s
| t1^-1 ⇒ (tsubst t1 s)^-1
| t1 ^+ n ⇒ tsubst t1 s ^+ n
end%T.
Fixpoint fsubst (f : formula R) (s : nat × term R) :=
match f with
| Bool _ ⇒ f
| t1 == t2 ⇒ tsubst t1 s == tsubst t2 s
| Unit t1 ⇒ Unit (tsubst t1 s)
| f1 ∧ f2 ⇒ fsubst f1 s ∧ fsubst f2 s
| f1 ∨ f2 ⇒ fsubst f1 s ∨ fsubst f2 s
| f1 ==> f2 ⇒ fsubst f1 s ==> fsubst f2 s
| ¬ f1 ⇒ ¬ fsubst f1 s
| ('∃ 'X_i, f1) ⇒ '∃ 'X_i, if i == s.1 then f1 else fsubst f1 s
| ('∀ 'X_i, f1) ⇒ '∀ 'X_i, if i == s.1 then f1 else fsubst f1 s
end%T.
End Substitution.
Section EvalTerm.
Variable R : unitRingType.
Variable R : Type.
Inductive term : Type :=
| Var of nat
| Const of R
| NatConst of nat
| Add of term & term
| Opp of term
| NatMul of term & nat
| Mul of term & term
| Inv of term
| Exp of term & nat.
Inductive formula : Type :=
| Bool of bool
| Equal of term & term
| Unit of term
| And of formula & formula
| Or of formula & formula
| Implies of formula & formula
| Not of formula
| Exists of nat & formula
| Forall of nat & formula.
End TermDef.
Bind Scope term_scope with term.
Bind Scope term_scope with formula.
Arguments Add {R} t1%T t2%T.
Arguments Opp {R} t1%T.
Arguments NatMul {R} t1%T n%N.
Arguments Mul {R} t1%T t2%T.
Arguments Inv {R} t1%T.
Arguments Exp {R} t1%T n%N.
Arguments Equal {R} t1%T t2%T.
Arguments Unit {R} t1%T.
Arguments And {R} f1%T f2%T.
Arguments Or {R} f1%T f2%T.
Arguments Implies {R} f1%T f2%T.
Arguments Not {R} f1%T.
Arguments Exists {R} i%N f1%T.
Arguments Forall {R} i%N f1%T.
Arguments Bool {R} b.
Arguments Const {R} x.
Notation True := (Bool true).
Notation False := (Bool false).
Section Substitution.
Variable R : Type.
Fixpoint tsubst (t : term R) (s : nat × term R) :=
match t with
| 'X_i ⇒ if i == s.1 then s.2 else t
| _%:T | _%:R ⇒ t
| t1 + t2 ⇒ tsubst t1 s + tsubst t2 s
| - t1 ⇒ - tsubst t1 s
| t1 *+ n ⇒ tsubst t1 s *+ n
| t1 × t2 ⇒ tsubst t1 s × tsubst t2 s
| t1^-1 ⇒ (tsubst t1 s)^-1
| t1 ^+ n ⇒ tsubst t1 s ^+ n
end%T.
Fixpoint fsubst (f : formula R) (s : nat × term R) :=
match f with
| Bool _ ⇒ f
| t1 == t2 ⇒ tsubst t1 s == tsubst t2 s
| Unit t1 ⇒ Unit (tsubst t1 s)
| f1 ∧ f2 ⇒ fsubst f1 s ∧ fsubst f2 s
| f1 ∨ f2 ⇒ fsubst f1 s ∨ fsubst f2 s
| f1 ==> f2 ⇒ fsubst f1 s ==> fsubst f2 s
| ¬ f1 ⇒ ¬ fsubst f1 s
| ('∃ 'X_i, f1) ⇒ '∃ 'X_i, if i == s.1 then f1 else fsubst f1 s
| ('∀ 'X_i, f1) ⇒ '∀ 'X_i, if i == s.1 then f1 else fsubst f1 s
end%T.
End Substitution.
Section EvalTerm.
Variable R : unitRingType.
Evaluation of a reified term into R a ring with units
Fixpoint eval (e : seq R) (t : term R) {struct t} : R :=
match t with
| ('X_i)%T ⇒ e`_i
| (x%:T)%T ⇒ x
| (n%:R)%T ⇒ n%:R
| (t1 + t2)%T ⇒ eval e t1 + eval e t2
| (- t1)%T ⇒ - eval e t1
| (t1 *+ n)%T ⇒ eval e t1 *+ n
| (t1 × t2)%T ⇒ eval e t1 × eval e t2
| t1^-1%T ⇒ (eval e t1)^-1
| (t1 ^+ n)%T ⇒ eval e t1 ^+ n
end.
Definition same_env (e e' : seq R) := nth 0 e =1 nth 0 e'.
Lemma eq_eval e e' t : same_env e e' → eval e t = eval e' t.
Lemma eval_tsubst e t s :
eval e (tsubst t s) = eval (set_nth 0 e s.1 (eval e s.2)) t.
match t with
| ('X_i)%T ⇒ e`_i
| (x%:T)%T ⇒ x
| (n%:R)%T ⇒ n%:R
| (t1 + t2)%T ⇒ eval e t1 + eval e t2
| (- t1)%T ⇒ - eval e t1
| (t1 *+ n)%T ⇒ eval e t1 *+ n
| (t1 × t2)%T ⇒ eval e t1 × eval e t2
| t1^-1%T ⇒ (eval e t1)^-1
| (t1 ^+ n)%T ⇒ eval e t1 ^+ n
end.
Definition same_env (e e' : seq R) := nth 0 e =1 nth 0 e'.
Lemma eq_eval e e' t : same_env e e' → eval e t = eval e' t.
Lemma eval_tsubst e t s :
eval e (tsubst t s) = eval (set_nth 0 e s.1 (eval e s.2)) t.
Evaluation of a reified formula
Fixpoint holds (e : seq R) (f : formula R) {struct f} : Prop :=
match f with
| Bool b ⇒ b
| (t1 == t2)%T ⇒ eval e t1 = eval e t2
| Unit t1 ⇒ eval e t1 \in unit
| (f1 ∧ f2)%T ⇒ holds e f1 ∧ holds e f2
| (f1 ∨ f2)%T ⇒ holds e f1 ∨ holds e f2
| (f1 ==> f2)%T ⇒ holds e f1 → holds e f2
| (¬ f1)%T ⇒ ¬ holds e f1
| ('∃ 'X_i, f1)%T ⇒ ∃ x, holds (set_nth 0 e i x) f1
| ('∀ 'X_i, f1)%T ⇒ ∀ x, holds (set_nth 0 e i x) f1
end.
Lemma same_env_sym e e' : same_env e e' → same_env e' e.
match f with
| Bool b ⇒ b
| (t1 == t2)%T ⇒ eval e t1 = eval e t2
| Unit t1 ⇒ eval e t1 \in unit
| (f1 ∧ f2)%T ⇒ holds e f1 ∧ holds e f2
| (f1 ∨ f2)%T ⇒ holds e f1 ∨ holds e f2
| (f1 ==> f2)%T ⇒ holds e f1 → holds e f2
| (¬ f1)%T ⇒ ¬ holds e f1
| ('∃ 'X_i, f1)%T ⇒ ∃ x, holds (set_nth 0 e i x) f1
| ('∀ 'X_i, f1)%T ⇒ ∀ x, holds (set_nth 0 e i x) f1
end.
Lemma same_env_sym e e' : same_env e e' → same_env e' e.
Extensionality of formula evaluation
Evaluation and substitution by a constant
Boolean test selecting terms in the language of rings
Fixpoint rterm (t : term R) :=
match t with
| _^-1 ⇒ false
| t1 + t2 | t1 × t2 ⇒ rterm t1 && rterm t2
| - t1 | t1 *+ _ | t1 ^+ _ ⇒ rterm t1
| _ ⇒ true
end%T.
match t with
| _^-1 ⇒ false
| t1 + t2 | t1 × t2 ⇒ rterm t1 && rterm t2
| - t1 | t1 *+ _ | t1 ^+ _ ⇒ rterm t1
| _ ⇒ true
end%T.
Boolean test selecting formulas in the theory of rings
Fixpoint rformula (f : formula R) :=
match f with
| Bool _ ⇒ true
| t1 == t2 ⇒ rterm t1 && rterm t2
| Unit t1 ⇒ false
| f1 ∧ f2 | f1 ∨ f2 | f1 ==> f2 ⇒ rformula f1 && rformula f2
| ¬ f1 | ('∃ 'X__, f1) | ('∀ 'X__, f1) ⇒ rformula f1
end%T.
match f with
| Bool _ ⇒ true
| t1 == t2 ⇒ rterm t1 && rterm t2
| Unit t1 ⇒ false
| f1 ∧ f2 | f1 ∨ f2 | f1 ==> f2 ⇒ rformula f1 && rformula f2
| ¬ f1 | ('∃ 'X__, f1) | ('∀ 'X__, f1) ⇒ rformula f1
end%T.
Upper bound of the names used in a term
Fixpoint ub_var (t : term R) :=
match t with
| 'X_i ⇒ i.+1
| t1 + t2 | t1 × t2 ⇒ maxn (ub_var t1) (ub_var t2)
| - t1 | t1 *+ _ | t1 ^+ _ | t1^-1 ⇒ ub_var t1
| _ ⇒ 0%N
end%T.
match t with
| 'X_i ⇒ i.+1
| t1 + t2 | t1 × t2 ⇒ maxn (ub_var t1) (ub_var t2)
| - t1 | t1 *+ _ | t1 ^+ _ | t1^-1 ⇒ ub_var t1
| _ ⇒ 0%N
end%T.
Replaces inverses in the term t by fresh variables, accumulating the
substitution.
Fixpoint to_rterm (t : term R) (r : seq (term R)) (n : nat) {struct t} :=
match t with
| t1^-1 ⇒
let: (t1', r1) := to_rterm t1 r n in
('X_(n + size r1), rcons r1 t1')
| t1 + t2 ⇒
let: (t1', r1) := to_rterm t1 r n in
let: (t2', r2) := to_rterm t2 r1 n in
(t1' + t2', r2)
| - t1 ⇒
let: (t1', r1) := to_rterm t1 r n in
(- t1', r1)
| t1 *+ m ⇒
let: (t1', r1) := to_rterm t1 r n in
(t1' *+ m, r1)
| t1 × t2 ⇒
let: (t1', r1) := to_rterm t1 r n in
let: (t2', r2) := to_rterm t2 r1 n in
(Mul t1' t2', r2)
| t1 ^+ m ⇒
let: (t1', r1) := to_rterm t1 r n in
(t1' ^+ m, r1)
| _ ⇒ (t, r)
end%T.
Lemma to_rterm_id t r n : rterm t → to_rterm t r n = (t, r).
match t with
| t1^-1 ⇒
let: (t1', r1) := to_rterm t1 r n in
('X_(n + size r1), rcons r1 t1')
| t1 + t2 ⇒
let: (t1', r1) := to_rterm t1 r n in
let: (t2', r2) := to_rterm t2 r1 n in
(t1' + t2', r2)
| - t1 ⇒
let: (t1', r1) := to_rterm t1 r n in
(- t1', r1)
| t1 *+ m ⇒
let: (t1', r1) := to_rterm t1 r n in
(t1' *+ m, r1)
| t1 × t2 ⇒
let: (t1', r1) := to_rterm t1 r n in
let: (t2', r2) := to_rterm t2 r1 n in
(Mul t1' t2', r2)
| t1 ^+ m ⇒
let: (t1', r1) := to_rterm t1 r n in
(t1' ^+ m, r1)
| _ ⇒ (t, r)
end%T.
Lemma to_rterm_id t r n : rterm t → to_rterm t r n = (t, r).
A ring formula stating that t1 is equal to 0 in the ring theory.
Also applies to non commutative rings.
Definition eq0_rform t1 :=
let m := ub_var t1 in
let: (t1', r1) := to_rterm t1 [::] m in
let fix loop r i := match r with
| [::] ⇒ t1' == 0
| t :: r' ⇒
let f := 'X_i × t == 1 ∧ t × 'X_i == 1 in
'∀ 'X_i, (f ∨ 'X_i == t ∧ ¬ ('∃ 'X_i, f)) ==> loop r' i.+1
end%T
in loop r1 m.
let m := ub_var t1 in
let: (t1', r1) := to_rterm t1 [::] m in
let fix loop r i := match r with
| [::] ⇒ t1' == 0
| t :: r' ⇒
let f := 'X_i × t == 1 ∧ t × 'X_i == 1 in
'∀ 'X_i, (f ∨ 'X_i == t ∧ ¬ ('∃ 'X_i, f)) ==> loop r' i.+1
end%T
in loop r1 m.
Transformation of a formula in the theory of rings with units into an
equivalent formula in the sub-theory of rings.
Fixpoint to_rform f :=
match f with
| Bool b ⇒ f
| t1 == t2 ⇒ eq0_rform (t1 - t2)
| Unit t1 ⇒ eq0_rform (t1 × t1^-1 - 1)
| f1 ∧ f2 ⇒ to_rform f1 ∧ to_rform f2
| f1 ∨ f2 ⇒ to_rform f1 ∨ to_rform f2
| f1 ==> f2 ⇒ to_rform f1 ==> to_rform f2
| ¬ f1 ⇒ ¬ to_rform f1
| ('∃ 'X_i, f1) ⇒ '∃ 'X_i, to_rform f1
| ('∀ 'X_i, f1) ⇒ '∀ 'X_i, to_rform f1
end%T.
match f with
| Bool b ⇒ f
| t1 == t2 ⇒ eq0_rform (t1 - t2)
| Unit t1 ⇒ eq0_rform (t1 × t1^-1 - 1)
| f1 ∧ f2 ⇒ to_rform f1 ∧ to_rform f2
| f1 ∨ f2 ⇒ to_rform f1 ∨ to_rform f2
| f1 ==> f2 ⇒ to_rform f1 ==> to_rform f2
| ¬ f1 ⇒ ¬ to_rform f1
| ('∃ 'X_i, f1) ⇒ '∃ 'X_i, to_rform f1
| ('∀ 'X_i, f1) ⇒ '∀ 'X_i, to_rform f1
end%T.
The transformation gives a ring formula.
Correctness of the transformation.
Boolean test selecting formulas which describe a constructible set,
i.e. formulas without quantifiers.
The quantifier elimination check.
Fixpoint qf_form (f : formula R) :=
match f with
| Bool _ | _ == _ | Unit _ ⇒ true
| f1 ∧ f2 | f1 ∨ f2 | f1 ==> f2 ⇒ qf_form f1 && qf_form f2
| ¬ f1 ⇒ qf_form f1
| _ ⇒ false
end%T.
match f with
| Bool _ | _ == _ | Unit _ ⇒ true
| f1 ∧ f2 | f1 ∨ f2 | f1 ==> f2 ⇒ qf_form f1 && qf_form f2
| ¬ f1 ⇒ qf_form f1
| _ ⇒ false
end%T.
Boolean holds predicate for quantifier free formulas
Definition qf_eval e := fix loop (f : formula R) : bool :=
match f with
| Bool b ⇒ b
| t1 == t2 ⇒ (eval e t1 == eval e t2)%bool
| Unit t1 ⇒ eval e t1 \in unit
| f1 ∧ f2 ⇒ loop f1 && loop f2
| f1 ∨ f2 ⇒ loop f1 || loop f2
| f1 ==> f2 ⇒ (loop f1 ==> loop f2)%bool
| ¬ f1 ⇒ ~~ loop f1
|_ ⇒ false
end%T.
match f with
| Bool b ⇒ b
| t1 == t2 ⇒ (eval e t1 == eval e t2)%bool
| Unit t1 ⇒ eval e t1 \in unit
| f1 ∧ f2 ⇒ loop f1 && loop f2
| f1 ∨ f2 ⇒ loop f1 || loop f2
| f1 ==> f2 ⇒ (loop f1 ==> loop f2)%bool
| ¬ f1 ⇒ ~~ loop f1
|_ ⇒ false
end%T.
qf_eval is equivalent to holds
Lemma qf_evalP e f : qf_form f → reflect (holds e f) (qf_eval e f).
Implicit Type bc : seq (term R) × seq (term R).
Implicit Type bc : seq (term R) × seq (term R).
Quantifier-free formula are normalized into DNF. A DNF is
represented by the type seq (seq (term R) * seq (term R)), where we
separate positive and negative literals
DNF preserving conjunction
Definition and_dnf bcs1 bcs2 :=
\big[cat/nil]_(bc1 <- bcs1)
map (fun bc2 ⇒ (bc1.1 ++ bc2.1, bc1.2 ++ bc2.2)) bcs2.
\big[cat/nil]_(bc1 <- bcs1)
map (fun bc2 ⇒ (bc1.1 ++ bc2.1, bc1.2 ++ bc2.2)) bcs2.
Computes a DNF from a qf ring formula
Fixpoint qf_to_dnf (f : formula R) (neg : bool) {struct f} :=
match f with
| Bool b ⇒ if b (+) neg then [:: ([::], [::])] else [::]
| t1 == t2 ⇒ [:: if neg then ([::], [:: t1 - t2]) else ([:: t1 - t2], [::])]
| f1 ∧ f2 ⇒ (if neg then cat else and_dnf) [rec f1, neg] [rec f2, neg]
| f1 ∨ f2 ⇒ (if neg then and_dnf else cat) [rec f1, neg] [rec f2, neg]
| f1 ==> f2 ⇒ (if neg then and_dnf else cat) [rec f1, ~~ neg] [rec f2, neg]
| ¬ f1 ⇒ [rec f1, ~~ neg]
| _ ⇒ if neg then [:: ([::], [::])] else [::]
end%T where "[ 'rec' f , neg ]" := (qf_to_dnf f neg).
match f with
| Bool b ⇒ if b (+) neg then [:: ([::], [::])] else [::]
| t1 == t2 ⇒ [:: if neg then ([::], [:: t1 - t2]) else ([:: t1 - t2], [::])]
| f1 ∧ f2 ⇒ (if neg then cat else and_dnf) [rec f1, neg] [rec f2, neg]
| f1 ∨ f2 ⇒ (if neg then and_dnf else cat) [rec f1, neg] [rec f2, neg]
| f1 ==> f2 ⇒ (if neg then and_dnf else cat) [rec f1, ~~ neg] [rec f2, neg]
| ¬ f1 ⇒ [rec f1, ~~ neg]
| _ ⇒ if neg then [:: ([::], [::])] else [::]
end%T where "[ 'rec' f , neg ]" := (qf_to_dnf f neg).
Conversely, transforms a DNF into a formula
Definition dnf_to_form :=
let pos_lit t := And (t == 0) in let neg_lit t := And (t != 0) in
let cls bc := Or (foldr pos_lit True bc.1 ∧ foldr neg_lit True bc.2) in
foldr cls False.
let pos_lit t := And (t == 0) in let neg_lit t := And (t != 0) in
let cls bc := Or (foldr pos_lit True bc.1 ∧ foldr neg_lit True bc.2) in
foldr cls False.
Catenation of dnf is the Or of formulas
Lemma cat_dnfP e bcs1 bcs2 :
qf_eval e (dnf_to_form (bcs1 ++ bcs2))
= qf_eval e (dnf_to_form bcs1 ∨ dnf_to_form bcs2).
qf_eval e (dnf_to_form (bcs1 ++ bcs2))
= qf_eval e (dnf_to_form bcs1 ∨ dnf_to_form bcs2).
and_dnf is the And of formulas
Lemma and_dnfP e bcs1 bcs2 :
qf_eval e (dnf_to_form (and_dnf bcs1 bcs2))
= qf_eval e (dnf_to_form bcs1 ∧ dnf_to_form bcs2).
Lemma qf_to_dnfP e :
let qev f b := qf_eval e (dnf_to_form (qf_to_dnf f b)) in
∀ f, qf_form f && rformula f → qev f false = qf_eval e f.
Lemma dnf_to_form_qf bcs : qf_form (dnf_to_form bcs).
Definition dnf_rterm cl := all rterm cl.1 && all rterm cl.2.
Lemma qf_to_dnf_rterm f b : rformula f → all dnf_rterm (qf_to_dnf f b).
Lemma dnf_to_rform bcs : rformula (dnf_to_form bcs) = all dnf_rterm bcs.
Section If.
Variables (pred_f then_f else_f : formula R).
Definition If := (pred_f ∧ then_f ∨ ¬ pred_f ∧ else_f)%T.
Lemma If_form_qf :
qf_form pred_f → qf_form then_f → qf_form else_f → qf_form If.
Lemma If_form_rf :
rformula pred_f → rformula then_f → rformula else_f → rformula If.
Lemma eval_If e :
let ev := qf_eval e in ev If = (if ev pred_f then ev then_f else ev else_f).
End If.
Section Pick.
Variables (I : finType) (pred_f then_f : I → formula R) (else_f : formula R).
Definition Pick :=
\big[Or/False]_(p : {ffun pred I})
((\big[And/True]_i (if p i then pred_f i else ¬ pred_f i))
∧ (if pick p is Some i then then_f i else else_f))%T.
Lemma Pick_form_qf :
(∀ i, qf_form (pred_f i)) →
(∀ i, qf_form (then_f i)) →
qf_form else_f →
qf_form Pick.
Lemma eval_Pick e (qev := qf_eval e) :
let P i := qev (pred_f i) in
qev Pick = (if pick P is Some i then qev (then_f i) else qev else_f).
End Pick.
Section MultiQuant.
Variable f : formula R.
Implicit Types (I : seq nat) (e : seq R).
Lemma foldExistsP I e :
(exists2 e', {in [predC I], same_env e e'} & holds e' f)
↔ holds e (foldr Exists f I).
Lemma foldForallP I e :
(∀ e', {in [predC I], same_env e e'} → holds e' f)
↔ holds e (foldr Forall f I).
End MultiQuant.
End EvalTerm.
Definition integral_domain_axiom (R : ringType) :=
∀ x y : R, x × y = 0 → (x == 0) || (y == 0).
#[mathcomp(axiom="integral_domain_axiom"), short(type="idomainType")]
HB.structure Definition IntegralDomain :=
{R of ComUnitRing_isIntegral R & ComUnitRing R}.
Module IntegralDomainExports.
Bind Scope ring_scope with IntegralDomain.sort.
#[deprecated(since="mathcomp 2.0.0",
note="Use GRing.IntegralDomain.clone instead.")]
Notation "[ 'idomainType' 'of' T 'for' cT ]" := (IntegralDomain.clone T%type cT)
(at level 0, format "[ 'idomainType' 'of' T 'for' cT ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0",
note="Use GRing.IntegralDomain.clone instead.")]
Notation "[ 'idomainType' 'of' T ]" := (IntegralDomain.clone T%type _)
(at level 0, format "[ 'idomainType' 'of' T ]") : form_scope.
End IntegralDomainExports.
Section IntegralDomainTheory.
Variable R : idomainType.
Implicit Types x y : R.
Lemma mulf_eq0 x y : (x × y == 0) = (x == 0) || (y == 0).
Lemma prodf_eq0 (I : finType) (P : pred I) (F : I → R) :
reflect (exists2 i, P i & (F i == 0)) (\prod_(i | P i) F i == 0).
Lemma prodf_seq_eq0 I r (P : pred I) (F : I → R) :
(\prod_(i <- r | P i) F i == 0) = has (fun i ⇒ P i && (F i == 0)) r.
Lemma mulf_neq0 x y : x != 0 → y != 0 → x × y != 0.
Lemma prodf_neq0 (I : finType) (P : pred I) (F : I → R) :
reflect (∀ i, P i → (F i != 0)) (\prod_(i | P i) F i != 0).
Lemma prodf_seq_neq0 I r (P : pred I) (F : I → R) :
(\prod_(i <- r | P i) F i != 0) = all (fun i ⇒ P i ==> (F i != 0)) r.
Lemma expf_eq0 x n : (x ^+ n == 0) = (n > 0) && (x == 0).
Lemma sqrf_eq0 x : (x ^+ 2 == 0) = (x == 0).
Lemma expf_neq0 x m : x != 0 → x ^+ m != 0.
Lemma natf_neq0 n : (n%:R != 0 :> R) = (char R)^'.-nat n.
Lemma natf0_char n : n > 0 → n%:R == 0 :> R → ∃ p, p \in char R.
Lemma charf'_nat n : (char R)^'.-nat n = (n%:R != 0 :> R).
Lemma charf0P : char R =i pred0 ↔ (∀ n, (n%:R == 0 :> R) = (n == 0)%N).
Lemma eqf_sqr x y : (x ^+ 2 == y ^+ 2) = (x == y) || (x == - y).
Lemma mulfI x : x != 0 → injective ( *%R x).
Lemma mulIf x : x != 0 → injective ( *%R^~ x).
Lemma divfI x : x != 0 → injective (fun y ⇒ x / y).
Lemma divIf y : y != 0 → injective (fun x ⇒ x / y).
Lemma sqrf_eq1 x : (x ^+ 2 == 1) = (x == 1) || (x == -1).
Lemma expfS_eq1 x n :
(x ^+ n.+1 == 1) = (x == 1) || (\sum_(i < n.+1) x ^+ i == 0).
Lemma lregP x : reflect (lreg x) (x != 0).
Lemma rregP x : reflect (rreg x) (x != 0).
End IntegralDomainTheory.
Module RegularIdomainExports.
End RegularIdomainExports.
Arguments lregP {R x}.
Arguments rregP {R x}.
Definition field_axiom (R : unitRingType) := ∀ x : R, x != 0 → x \in unit.
#[mathcomp(axiom="field_axiom"), short(type="fieldType")]
HB.structure Definition Field := { R of IntegralDomain R & UnitRing_isField R }.
Module FieldExports.
Bind Scope ring_scope with Field.sort.
#[deprecated(since="mathcomp 2.0.0", note="Use GRing.Field.clone instead.")]
Notation "[ 'fieldType' 'of' T 'for' cT ]" := (Field.clone T%type cT)
(at level 0, format "[ 'fieldType' 'of' T 'for' cT ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use GRing.Field.clone instead.")]
Notation "[ 'fieldType' 'of' T ]" := (Field.clone T%type _)
(at level 0, format "[ 'fieldType' 'of' T ]") : form_scope.
End FieldExports.
#[export] HB.instance Definition regular_field (F : fieldType) := Field.on F^o.
Lemma IdomainMixin (R : unitRingType): Field.axiom R → IntegralDomain.axiom R.
Fact intro_unit (x y : R) : y × x = 1 → x != 0.
Fact inv_out : {in predC (predC1 0), inv =1 id}.
Section FieldTheory.
Variable F : fieldType.
Implicit Types x y : F.
Lemma unitfE x : (x \in unit) = (x != 0).
Lemma mulVf x : x != 0 → x^-1 × x = 1.
Lemma divff x : x != 0 → x / x = 1.
Definition mulfV := divff.
Lemma mulKf x : x != 0 → cancel ( *%R x) ( *%R x^-1).
Lemma mulVKf x : x != 0 → cancel ( *%R x^-1) ( *%R x).
Lemma mulfK x : x != 0 → cancel ( *%R^~ x) ( *%R^~ x^-1).
Lemma mulfVK x : x != 0 → cancel ( *%R^~ x^-1) ( *%R^~ x).
Definition divfK := mulfVK.
Lemma invfM : {morph @inv F : x y / x × y}.
Lemma invf_div x y : (x / y)^-1 = y / x.
Lemma divKf x : x != 0 → involutive (fun y ⇒ x / y).
Lemma expfB_cond m n x : (x == 0) + n ≤ m → x ^+ (m - n) = x ^+ m / x ^+ n.
Lemma expfB m n x : n < m → x ^+ (m - n) = x ^+ m / x ^+ n.
Lemma prodfV I r (P : pred I) (E : I → F) :
\prod_(i <- r | P i) (E i)^-1 = (\prod_(i <- r | P i) E i)^-1.
Lemma prodf_div I r (P : pred I) (E D : I → F) :
\prod_(i <- r | P i) (E i / D i) =
\prod_(i <- r | P i) E i / \prod_(i <- r | P i) D i.
Lemma telescope_prodf n m (f : nat → F) :
(∀ k, n < k < m → f k != 0) → n < m →
\prod_(n ≤ k < m) (f k.+1 / f k) = f m / f n.
Lemma telescope_prodf_eq n m (f u : nat → F) :
(∀ k, n < k < m → f k != 0) → n < m →
(∀ k, n ≤ k < m → u k = f k.+1 / f k) →
\prod_(n ≤ k < m) u k = f m / f n.
Lemma addf_div x1 y1 x2 y2 :
y1 != 0 → y2 != 0 → x1 / y1 + x2 / y2 = (x1 × y2 + x2 × y1) / (y1 × y2).
Lemma mulf_div x1 y1 x2 y2 : (x1 / y1) × (x2 / y2) = (x1 × x2) / (y1 × y2).
Lemma eqr_div x y z t : y != 0 → t != 0 → (x / y == z / t) = (x × t == z × y).
Lemma eqr_sum_div I r P (f : I → F) c a : c != 0 →
\big[+%R/0]_(x <- r | P x) (f x / c) == a
= (\big[+%R/0]_(x <- r | P x) f x == a × c).
Lemma char0_natf_div :
char F =i pred0 → ∀ m d, d %| m → (m %/ d)%:R = m%:R / d%:R :> F.
Section FieldMorphismInj.
Variables (R : ringType) (f : {rmorphism F → R}).
Lemma fmorph_eq0 x : (f x == 0) = (x == 0).
Lemma fmorph_inj : injective f.
Lemma fmorph_eq : {mono f : x y / x == y}.
Lemma fmorph_eq1 x : (f x == 1) = (x == 1).
Lemma fmorph_char : char R =i char F.
End FieldMorphismInj.
Section FieldMorphismInv.
Variables (R : unitRingType) (f : {rmorphism F → R}).
Lemma fmorph_unit x : (f x \in unit) = (x != 0).
Lemma fmorphV : {morph f: x / x^-1}.
Lemma fmorph_div : {morph f : x y / x / y}.
End FieldMorphismInv.
Section ModuleTheory.
Variable V : lmodType F.
Implicit Types (a : F) (v : V).
Lemma scalerK a : a != 0 → cancel ( *:%R a : V → V) ( *:%R a^-1).
Lemma scalerKV a : a != 0 → cancel ( *:%R a^-1 : V → V) ( *:%R a).
Lemma scalerI a : a != 0 → injective ( *:%R a : V → V).
Lemma scaler_eq0 a v : (a *: v == 0) = (a == 0) || (v == 0).
End ModuleTheory.
Lemma char_lalg (A : lalgType F) : char A =i char F.
End FieldTheory.
Arguments fmorph_inj {F R} f [x1 x2].
Arguments telescope_prodf_eq {F n m} f u.
Definition decidable_field_axiom (R : unitRingType)
(s : seq R → pred (formula R)) :=
∀ e f, reflect (holds e f) (s e f).
#[mathcomp(axiom="decidable_field_axiom"), short(type="decFieldType")]
HB.structure Definition DecidableField := { F of Field F & Field_isDecField F }.
Module DecFieldExports.
Bind Scope ring_scope with DecidableField.sort.
#[deprecated(since="mathcomp 2.0.0",
note="Use GRing.DecidableField.clone instead.")]
Notation "[ 'decFieldType' 'of' T 'for' cT ]" := (DecidableField.clone T%type cT)
(at level 0, format "[ 'decFieldType' 'of' T 'for' cT ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0",
note="Use GRing.DecidableField.clone instead.")]
Notation "[ 'decFieldType' 'of' T ]" := (DecidableField.clone T%type _)
(at level 0, format "[ 'decFieldType' 'of' T ]") : form_scope.
End DecFieldExports.
Section DecidableFieldTheory.
Variable F : decFieldType.
Implicit Type f : formula F.
Fact sol_subproof n f :
reflect (∃ s, (size s == n) && sat s f)
(sat [::] (foldr Exists f (iota 0 n))).
Definition sol n f :=
if sol_subproof n f is ReflectT sP then xchoose sP else nseq n 0.
Lemma size_sol n f : size (sol n f) = n.
Lemma solP n f : reflect (exists2 s, size s = n & holds s f) (sat (sol n f) f).
Lemma eq_sat f1 f2 :
(∀ e, holds e f1 ↔ holds e f2) → sat^~ f1 =1 sat^~ f2.
Lemma eq_sol f1 f2 :
(∀ e, holds e f1 ↔ holds e f2) → sol^~ f1 =1 sol^~ f2.
End DecidableFieldTheory.
Arguments satP {F e f} : rename.
Arguments solP {F n f} : rename.
Section QE_Mixin.
Variable F : Field.type.
Implicit Type f : formula F.
Variable proj : nat → seq (term F) × seq (term F) → formula F.
qf_eval e (dnf_to_form (and_dnf bcs1 bcs2))
= qf_eval e (dnf_to_form bcs1 ∧ dnf_to_form bcs2).
Lemma qf_to_dnfP e :
let qev f b := qf_eval e (dnf_to_form (qf_to_dnf f b)) in
∀ f, qf_form f && rformula f → qev f false = qf_eval e f.
Lemma dnf_to_form_qf bcs : qf_form (dnf_to_form bcs).
Definition dnf_rterm cl := all rterm cl.1 && all rterm cl.2.
Lemma qf_to_dnf_rterm f b : rformula f → all dnf_rterm (qf_to_dnf f b).
Lemma dnf_to_rform bcs : rformula (dnf_to_form bcs) = all dnf_rterm bcs.
Section If.
Variables (pred_f then_f else_f : formula R).
Definition If := (pred_f ∧ then_f ∨ ¬ pred_f ∧ else_f)%T.
Lemma If_form_qf :
qf_form pred_f → qf_form then_f → qf_form else_f → qf_form If.
Lemma If_form_rf :
rformula pred_f → rformula then_f → rformula else_f → rformula If.
Lemma eval_If e :
let ev := qf_eval e in ev If = (if ev pred_f then ev then_f else ev else_f).
End If.
Section Pick.
Variables (I : finType) (pred_f then_f : I → formula R) (else_f : formula R).
Definition Pick :=
\big[Or/False]_(p : {ffun pred I})
((\big[And/True]_i (if p i then pred_f i else ¬ pred_f i))
∧ (if pick p is Some i then then_f i else else_f))%T.
Lemma Pick_form_qf :
(∀ i, qf_form (pred_f i)) →
(∀ i, qf_form (then_f i)) →
qf_form else_f →
qf_form Pick.
Lemma eval_Pick e (qev := qf_eval e) :
let P i := qev (pred_f i) in
qev Pick = (if pick P is Some i then qev (then_f i) else qev else_f).
End Pick.
Section MultiQuant.
Variable f : formula R.
Implicit Types (I : seq nat) (e : seq R).
Lemma foldExistsP I e :
(exists2 e', {in [predC I], same_env e e'} & holds e' f)
↔ holds e (foldr Exists f I).
Lemma foldForallP I e :
(∀ e', {in [predC I], same_env e e'} → holds e' f)
↔ holds e (foldr Forall f I).
End MultiQuant.
End EvalTerm.
Definition integral_domain_axiom (R : ringType) :=
∀ x y : R, x × y = 0 → (x == 0) || (y == 0).
#[mathcomp(axiom="integral_domain_axiom"), short(type="idomainType")]
HB.structure Definition IntegralDomain :=
{R of ComUnitRing_isIntegral R & ComUnitRing R}.
Module IntegralDomainExports.
Bind Scope ring_scope with IntegralDomain.sort.
#[deprecated(since="mathcomp 2.0.0",
note="Use GRing.IntegralDomain.clone instead.")]
Notation "[ 'idomainType' 'of' T 'for' cT ]" := (IntegralDomain.clone T%type cT)
(at level 0, format "[ 'idomainType' 'of' T 'for' cT ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0",
note="Use GRing.IntegralDomain.clone instead.")]
Notation "[ 'idomainType' 'of' T ]" := (IntegralDomain.clone T%type _)
(at level 0, format "[ 'idomainType' 'of' T ]") : form_scope.
End IntegralDomainExports.
Section IntegralDomainTheory.
Variable R : idomainType.
Implicit Types x y : R.
Lemma mulf_eq0 x y : (x × y == 0) = (x == 0) || (y == 0).
Lemma prodf_eq0 (I : finType) (P : pred I) (F : I → R) :
reflect (exists2 i, P i & (F i == 0)) (\prod_(i | P i) F i == 0).
Lemma prodf_seq_eq0 I r (P : pred I) (F : I → R) :
(\prod_(i <- r | P i) F i == 0) = has (fun i ⇒ P i && (F i == 0)) r.
Lemma mulf_neq0 x y : x != 0 → y != 0 → x × y != 0.
Lemma prodf_neq0 (I : finType) (P : pred I) (F : I → R) :
reflect (∀ i, P i → (F i != 0)) (\prod_(i | P i) F i != 0).
Lemma prodf_seq_neq0 I r (P : pred I) (F : I → R) :
(\prod_(i <- r | P i) F i != 0) = all (fun i ⇒ P i ==> (F i != 0)) r.
Lemma expf_eq0 x n : (x ^+ n == 0) = (n > 0) && (x == 0).
Lemma sqrf_eq0 x : (x ^+ 2 == 0) = (x == 0).
Lemma expf_neq0 x m : x != 0 → x ^+ m != 0.
Lemma natf_neq0 n : (n%:R != 0 :> R) = (char R)^'.-nat n.
Lemma natf0_char n : n > 0 → n%:R == 0 :> R → ∃ p, p \in char R.
Lemma charf'_nat n : (char R)^'.-nat n = (n%:R != 0 :> R).
Lemma charf0P : char R =i pred0 ↔ (∀ n, (n%:R == 0 :> R) = (n == 0)%N).
Lemma eqf_sqr x y : (x ^+ 2 == y ^+ 2) = (x == y) || (x == - y).
Lemma mulfI x : x != 0 → injective ( *%R x).
Lemma mulIf x : x != 0 → injective ( *%R^~ x).
Lemma divfI x : x != 0 → injective (fun y ⇒ x / y).
Lemma divIf y : y != 0 → injective (fun x ⇒ x / y).
Lemma sqrf_eq1 x : (x ^+ 2 == 1) = (x == 1) || (x == -1).
Lemma expfS_eq1 x n :
(x ^+ n.+1 == 1) = (x == 1) || (\sum_(i < n.+1) x ^+ i == 0).
Lemma lregP x : reflect (lreg x) (x != 0).
Lemma rregP x : reflect (rreg x) (x != 0).
End IntegralDomainTheory.
Module RegularIdomainExports.
End RegularIdomainExports.
Arguments lregP {R x}.
Arguments rregP {R x}.
Definition field_axiom (R : unitRingType) := ∀ x : R, x != 0 → x \in unit.
#[mathcomp(axiom="field_axiom"), short(type="fieldType")]
HB.structure Definition Field := { R of IntegralDomain R & UnitRing_isField R }.
Module FieldExports.
Bind Scope ring_scope with Field.sort.
#[deprecated(since="mathcomp 2.0.0", note="Use GRing.Field.clone instead.")]
Notation "[ 'fieldType' 'of' T 'for' cT ]" := (Field.clone T%type cT)
(at level 0, format "[ 'fieldType' 'of' T 'for' cT ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use GRing.Field.clone instead.")]
Notation "[ 'fieldType' 'of' T ]" := (Field.clone T%type _)
(at level 0, format "[ 'fieldType' 'of' T ]") : form_scope.
End FieldExports.
#[export] HB.instance Definition regular_field (F : fieldType) := Field.on F^o.
Lemma IdomainMixin (R : unitRingType): Field.axiom R → IntegralDomain.axiom R.
Fact intro_unit (x y : R) : y × x = 1 → x != 0.
Fact inv_out : {in predC (predC1 0), inv =1 id}.
Section FieldTheory.
Variable F : fieldType.
Implicit Types x y : F.
Lemma unitfE x : (x \in unit) = (x != 0).
Lemma mulVf x : x != 0 → x^-1 × x = 1.
Lemma divff x : x != 0 → x / x = 1.
Definition mulfV := divff.
Lemma mulKf x : x != 0 → cancel ( *%R x) ( *%R x^-1).
Lemma mulVKf x : x != 0 → cancel ( *%R x^-1) ( *%R x).
Lemma mulfK x : x != 0 → cancel ( *%R^~ x) ( *%R^~ x^-1).
Lemma mulfVK x : x != 0 → cancel ( *%R^~ x^-1) ( *%R^~ x).
Definition divfK := mulfVK.
Lemma invfM : {morph @inv F : x y / x × y}.
Lemma invf_div x y : (x / y)^-1 = y / x.
Lemma divKf x : x != 0 → involutive (fun y ⇒ x / y).
Lemma expfB_cond m n x : (x == 0) + n ≤ m → x ^+ (m - n) = x ^+ m / x ^+ n.
Lemma expfB m n x : n < m → x ^+ (m - n) = x ^+ m / x ^+ n.
Lemma prodfV I r (P : pred I) (E : I → F) :
\prod_(i <- r | P i) (E i)^-1 = (\prod_(i <- r | P i) E i)^-1.
Lemma prodf_div I r (P : pred I) (E D : I → F) :
\prod_(i <- r | P i) (E i / D i) =
\prod_(i <- r | P i) E i / \prod_(i <- r | P i) D i.
Lemma telescope_prodf n m (f : nat → F) :
(∀ k, n < k < m → f k != 0) → n < m →
\prod_(n ≤ k < m) (f k.+1 / f k) = f m / f n.
Lemma telescope_prodf_eq n m (f u : nat → F) :
(∀ k, n < k < m → f k != 0) → n < m →
(∀ k, n ≤ k < m → u k = f k.+1 / f k) →
\prod_(n ≤ k < m) u k = f m / f n.
Lemma addf_div x1 y1 x2 y2 :
y1 != 0 → y2 != 0 → x1 / y1 + x2 / y2 = (x1 × y2 + x2 × y1) / (y1 × y2).
Lemma mulf_div x1 y1 x2 y2 : (x1 / y1) × (x2 / y2) = (x1 × x2) / (y1 × y2).
Lemma eqr_div x y z t : y != 0 → t != 0 → (x / y == z / t) = (x × t == z × y).
Lemma eqr_sum_div I r P (f : I → F) c a : c != 0 →
\big[+%R/0]_(x <- r | P x) (f x / c) == a
= (\big[+%R/0]_(x <- r | P x) f x == a × c).
Lemma char0_natf_div :
char F =i pred0 → ∀ m d, d %| m → (m %/ d)%:R = m%:R / d%:R :> F.
Section FieldMorphismInj.
Variables (R : ringType) (f : {rmorphism F → R}).
Lemma fmorph_eq0 x : (f x == 0) = (x == 0).
Lemma fmorph_inj : injective f.
Lemma fmorph_eq : {mono f : x y / x == y}.
Lemma fmorph_eq1 x : (f x == 1) = (x == 1).
Lemma fmorph_char : char R =i char F.
End FieldMorphismInj.
Section FieldMorphismInv.
Variables (R : unitRingType) (f : {rmorphism F → R}).
Lemma fmorph_unit x : (f x \in unit) = (x != 0).
Lemma fmorphV : {morph f: x / x^-1}.
Lemma fmorph_div : {morph f : x y / x / y}.
End FieldMorphismInv.
Section ModuleTheory.
Variable V : lmodType F.
Implicit Types (a : F) (v : V).
Lemma scalerK a : a != 0 → cancel ( *:%R a : V → V) ( *:%R a^-1).
Lemma scalerKV a : a != 0 → cancel ( *:%R a^-1 : V → V) ( *:%R a).
Lemma scalerI a : a != 0 → injective ( *:%R a : V → V).
Lemma scaler_eq0 a v : (a *: v == 0) = (a == 0) || (v == 0).
End ModuleTheory.
Lemma char_lalg (A : lalgType F) : char A =i char F.
End FieldTheory.
Arguments fmorph_inj {F R} f [x1 x2].
Arguments telescope_prodf_eq {F n m} f u.
Definition decidable_field_axiom (R : unitRingType)
(s : seq R → pred (formula R)) :=
∀ e f, reflect (holds e f) (s e f).
#[mathcomp(axiom="decidable_field_axiom"), short(type="decFieldType")]
HB.structure Definition DecidableField := { F of Field F & Field_isDecField F }.
Module DecFieldExports.
Bind Scope ring_scope with DecidableField.sort.
#[deprecated(since="mathcomp 2.0.0",
note="Use GRing.DecidableField.clone instead.")]
Notation "[ 'decFieldType' 'of' T 'for' cT ]" := (DecidableField.clone T%type cT)
(at level 0, format "[ 'decFieldType' 'of' T 'for' cT ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0",
note="Use GRing.DecidableField.clone instead.")]
Notation "[ 'decFieldType' 'of' T ]" := (DecidableField.clone T%type _)
(at level 0, format "[ 'decFieldType' 'of' T ]") : form_scope.
End DecFieldExports.
Section DecidableFieldTheory.
Variable F : decFieldType.
Implicit Type f : formula F.
Fact sol_subproof n f :
reflect (∃ s, (size s == n) && sat s f)
(sat [::] (foldr Exists f (iota 0 n))).
Definition sol n f :=
if sol_subproof n f is ReflectT sP then xchoose sP else nseq n 0.
Lemma size_sol n f : size (sol n f) = n.
Lemma solP n f : reflect (exists2 s, size s = n & holds s f) (sat (sol n f) f).
Lemma eq_sat f1 f2 :
(∀ e, holds e f1 ↔ holds e f2) → sat^~ f1 =1 sat^~ f2.
Lemma eq_sol f1 f2 :
(∀ e, holds e f1 ↔ holds e f2) → sol^~ f1 =1 sol^~ f2.
End DecidableFieldTheory.
Arguments satP {F e f} : rename.
Arguments solP {F n f} : rename.
Section QE_Mixin.
Variable F : Field.type.
Implicit Type f : formula F.
Variable proj : nat → seq (term F) × seq (term F) → formula F.
proj is the elimination of a single existential quantifier
The elimination projector is well_formed.
The elimination projector is valid
Definition valid_QE_proj :=
∀ i bc (ex_i_bc := ('∃ 'X_i, dnf_to_form [:: bc])%T) e,
dnf_rterm bc → reflect (holds e ex_i_bc) (qf_eval e (proj i bc)).
Hypotheses (wf_proj : wf_QE_proj) (ok_proj : valid_QE_proj).
Let elim_aux f n := foldr Or False (map (proj n) (qf_to_dnf f false)).
Fixpoint quantifier_elim f :=
match f with
| f1 ∧ f2 ⇒ (quantifier_elim f1) ∧ (quantifier_elim f2)
| f1 ∨ f2 ⇒ (quantifier_elim f1) ∨ (quantifier_elim f2)
| f1 ==> f2 ⇒ (¬ quantifier_elim f1) ∨ (quantifier_elim f2)
| ¬ f ⇒ ¬ quantifier_elim f
| ('∃ 'X_n, f) ⇒ elim_aux (quantifier_elim f) n
| ('∀ 'X_n, f) ⇒ ¬ elim_aux (¬ quantifier_elim f) n
| _ ⇒ f
end%T.
Lemma quantifier_elim_wf f :
let qf := quantifier_elim f in rformula f → qf_form qf && rformula qf.
Lemma quantifier_elim_rformP e f :
rformula f → reflect (holds e f) (qf_eval e (quantifier_elim f)).
Definition proj_sat e f := qf_eval e (quantifier_elim (to_rform f)).
Lemma proj_satP : DecidableField.axiom proj_sat.
End QE_Mixin.
∀ i bc (ex_i_bc := ('∃ 'X_i, dnf_to_form [:: bc])%T) e,
dnf_rterm bc → reflect (holds e ex_i_bc) (qf_eval e (proj i bc)).
Hypotheses (wf_proj : wf_QE_proj) (ok_proj : valid_QE_proj).
Let elim_aux f n := foldr Or False (map (proj n) (qf_to_dnf f false)).
Fixpoint quantifier_elim f :=
match f with
| f1 ∧ f2 ⇒ (quantifier_elim f1) ∧ (quantifier_elim f2)
| f1 ∨ f2 ⇒ (quantifier_elim f1) ∨ (quantifier_elim f2)
| f1 ==> f2 ⇒ (¬ quantifier_elim f1) ∨ (quantifier_elim f2)
| ¬ f ⇒ ¬ quantifier_elim f
| ('∃ 'X_n, f) ⇒ elim_aux (quantifier_elim f) n
| ('∀ 'X_n, f) ⇒ ¬ elim_aux (¬ quantifier_elim f) n
| _ ⇒ f
end%T.
Lemma quantifier_elim_wf f :
let qf := quantifier_elim f in rformula f → qf_form qf && rformula qf.
Lemma quantifier_elim_rformP e f :
rformula f → reflect (holds e f) (qf_eval e (quantifier_elim f)).
Definition proj_sat e f := qf_eval e (quantifier_elim (to_rform f)).
Lemma proj_satP : DecidableField.axiom proj_sat.
End QE_Mixin.
Axiom == all non-constant monic polynomials have a root
Definition closed_field_axiom (R : ringType) :=
∀ n (P : nat → R), n > 0 →
∃ x : R, x ^+ n = \sum_(i < n) P i × (x ^+ i).
#[mathcomp(axiom="closed_field_axiom"), short(type="closedFieldType")]
HB.structure Definition ClosedField :=
{ F of DecidableField F & DecField_isAlgClosed F }.
Module ClosedFieldExports.
Bind Scope ring_scope with ClosedField.sort.
#[deprecated(since="mathcomp 2.0.0",
note="Use GRing.ClosedField.clone instead.")]
Notation "[ 'closedFieldType' 'of' T 'for' cT ]" := (ClosedField.clone T%type cT)
(at level 0, format "[ 'closedFieldType' 'of' T 'for' cT ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0",
note="Use GRing.ClosedField.clone instead.")]
Notation "[ 'closedFieldType' 'of' T ]" := (ClosedField.clone T%type _)
(at level 0, format "[ 'closedFieldType' 'of' T ]") : form_scope.
End ClosedFieldExports.
Section ClosedFieldTheory.
Variable F : closedFieldType.
Lemma imaginary_exists : {i : F | i ^+ 2 = -1}.
End ClosedFieldTheory.
Lemma lalgMixin (R : ringType) (A : lalgType R) (B : lmodType R) (f : B → A) :
phant B → injective f → scalable f →
∀ mulB, {morph f : x y / mulB x y >-> x × y} →
∀ a u v, a *: (mulB u v) = mulB (a *: u) v.
Lemma comRingMixin (R : comRingType) (T : ringType) (f : T → R) :
phant T → injective f → {morph f : x y / x × y} → commutative (@mul T).
Lemma algMixin (R : ringType) (A : algType R) (B : lalgType R) (f : B → A) :
phant B → injective f → {morph f : x y / x × y} → scalable f →
∀ k (x y : B), k *: (x × y) = x × (k *: y).
∀ n (P : nat → R), n > 0 →
∃ x : R, x ^+ n = \sum_(i < n) P i × (x ^+ i).
#[mathcomp(axiom="closed_field_axiom"), short(type="closedFieldType")]
HB.structure Definition ClosedField :=
{ F of DecidableField F & DecField_isAlgClosed F }.
Module ClosedFieldExports.
Bind Scope ring_scope with ClosedField.sort.
#[deprecated(since="mathcomp 2.0.0",
note="Use GRing.ClosedField.clone instead.")]
Notation "[ 'closedFieldType' 'of' T 'for' cT ]" := (ClosedField.clone T%type cT)
(at level 0, format "[ 'closedFieldType' 'of' T 'for' cT ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0",
note="Use GRing.ClosedField.clone instead.")]
Notation "[ 'closedFieldType' 'of' T ]" := (ClosedField.clone T%type _)
(at level 0, format "[ 'closedFieldType' 'of' T ]") : form_scope.
End ClosedFieldExports.
Section ClosedFieldTheory.
Variable F : closedFieldType.
Lemma imaginary_exists : {i : F | i ^+ 2 = -1}.
End ClosedFieldTheory.
Lemma lalgMixin (R : ringType) (A : lalgType R) (B : lmodType R) (f : B → A) :
phant B → injective f → scalable f →
∀ mulB, {morph f : x y / mulB x y >-> x × y} →
∀ a u v, a *: (mulB u v) = mulB (a *: u) v.
Lemma comRingMixin (R : comRingType) (T : ringType) (f : T → R) :
phant T → injective f → {morph f : x y / x × y} → commutative (@mul T).
Lemma algMixin (R : ringType) (A : algType R) (B : lalgType R) (f : B → A) :
phant B → injective f → {morph f : x y / x × y} → scalable f →
∀ k (x y : B), k *: (x × y) = x × (k *: y).
Mixins for stability properties
Structures for stability properties
#[short(type="opprClosed")]
HB.structure Definition OppClosed V := {S of isOppClosed V S}.
#[short(type="addrClosed")]
HB.structure Definition AddClosed V := {S of isAddClosed V S}.
#[short(type="zmodClosed")]
HB.structure Definition ZmodClosed V := {S of OppClosed V S & AddClosed V S}.
#[short(type="mulr2Closed")]
HB.structure Definition Mul2Closed R := {S of isMul2Closed R S}.
#[short(type="mulrClosed")]
HB.structure Definition MulClosed R := {S of Mul2Closed R S & isMul1Closed R S}.
#[short(type="smulClosed")]
HB.structure Definition SmulClosed (R : ringType) :=
{S of OppClosed R S & MulClosed R S}.
#[short(type="semiring2Closed")]
HB.structure Definition Semiring2Closed (R : semiRingType) :=
{S of AddClosed R S & Mul2Closed R S}.
#[short(type="semiringClosed")]
HB.structure Definition SemiringClosed (R : semiRingType) :=
{S of AddClosed R S & MulClosed R S}.
#[short(type="subringClosed")]
HB.structure Definition SubringClosed (R : ringType) :=
{S of ZmodClosed R S & MulClosed R S}.
#[short(type="divClosed")]
HB.structure Definition DivClosed (R : unitRingType) :=
{S of MulClosed R S & isInvClosed R S}.
#[short(type="sdivClosed")]
HB.structure Definition SdivClosed (R : unitRingType) :=
{S of SmulClosed R S & isInvClosed R S}.
#[short(type="submodClosed")]
HB.structure Definition SubmodClosed (R : ringType) (V : lmodType R) :=
{S of ZmodClosed V S & isScaleClosed R V S}.
#[short(type="subalgClosed")]
HB.structure Definition SubalgClosed (R : ringType) (A : lalgType R) :=
{S of SubringClosed A S & isScaleClosed R A S}.
#[short(type="divringClosed")]
HB.structure Definition DivringClosed (R : unitRingType) :=
{S of SubringClosed R S & isInvClosed R S}.
#[short(type="divalgClosed")]
HB.structure Definition DivalgClosed (R : ringType) (A : unitAlgType R) :=
{S of DivringClosed A S & isScaleClosed R A S}.
Factories for stability properties
Section NmodulePred.
Variables (V : nmodType).
Section Add.
Variable S : addrClosed V.
Lemma rpred0 : 0 \in S.
Lemma rpredD : {in S &, ∀ u v, u + v \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.
Lemma rpredMn n : {in S, ∀ u, u *+ n \in S}.
End Add.
End NmodulePred.
Section ZmodulePred.
Variables (V : zmodType).
Section Opp.
Variable S : opprClosed V.
Lemma rpredN : {mono -%R: u / u \in S}.
End Opp.
Section Sub.
Variable S : zmodClosed V.
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 Sub.
End ZmodulePred.
Section SemiRingPred.
Variables (R : semiRingType).
Section Mul.
Variable S : mulrClosed R.
Lemma rpred1M : mulr_closed S.
Lemma rpred_prod I r (P : pred I) F :
(∀ i, P i → F i \in S) → \prod_(i <- r | P i) F i \in S.
Lemma rpredX n : {in S, ∀ u, u ^+ n \in S}.
End Mul.
Lemma rpred_nat (S : semiringClosed R) n : n%:R \in S.
Lemma semiringClosedP (rngS : semiringClosed R) : semiring_closed rngS.
End SemiRingPred.
Section RingPred.
Variables (R : ringType).
Lemma rpredMsign (S : opprClosed R) n x : ((-1) ^+ n × x \in S) = (x \in S).
Lemma rpredN1 (S : smulClosed R) : -1 \in S.
Lemma rpred_sign (S : smulClosed R) n : (-1) ^+ n \in S.
Lemma subringClosedP (rngS : subringClosed R) : subring_closed rngS.
End RingPred.
Section LmodPred.
Variables (R : ringType) (V : lmodType R).
Lemma rpredZsign (S : opprClosed V) n u : ((-1) ^+ n *: u \in S) = (u \in S).
Lemma rpredZnat (S : addrClosed V) n : {in S, ∀ u, n%:R *: u \in S}.
Lemma submodClosedP (modS : submodClosed V) : submod_closed modS.
End LmodPred.
Section LalgPred.
Variables (R : ringType) (A : lalgType R).
Lemma subalgClosedP (algS : subalgClosed A) : subalg_closed algS.
End LalgPred.
Section UnitRingPred.
Variable R : unitRingType.
Section Div.
Variable S : divClosed R.
Lemma rpredV x : (x^-1 \in S) = (x \in S).
Lemma rpred_div : {in S &, ∀ x y, x / y \in S}.
Lemma rpredXN n : {in S, ∀ x, x ^- n \in S}.
Lemma rpredMl x y : x \in S → x \is a unit→ (x × y \in S) = (y \in S).
Lemma rpredMr x y : x \in S → x \is a unit → (y × x \in S) = (y \in S).
Lemma rpred_divr x y : x \in S → x \is a unit → (y / x \in S) = (y \in S).
Lemma rpred_divl x y : x \in S → x \is a unit → (x / y \in S) = (y \in S).
End Div.
Lemma divringClosedP (divS : divringClosed R) : divring_closed divS.
Fact unitr_sdivr_closed : @sdivr_closed R unit.
#[export]
HB.instance Definition _ := isSdivClosed.Build R unit_pred unitr_sdivr_closed.
Implicit Type x : R.
Lemma unitrN x : (- x \is a unit) = (x \is a unit).
Lemma invrN x : (- x)^-1 = - x^-1.
Lemma divrNN x y : (- x) / (- y) = x / y.
Lemma divrN x y : x / (- y) = - (x / y).
Lemma invr_signM n x : ((-1) ^+ n × x)^-1 = (-1) ^+ n × x^-1.
Lemma divr_signM (b1 b2 : bool) x1 x2:
((-1) ^+ b1 × x1) / ((-1) ^+ b2 × x2) = (-1) ^+ (b1 (+) b2) × (x1 / x2).
End UnitRingPred.
Section FieldPred.
Variable F : fieldType.
Implicit Types x y : F.
Section ModuleTheory.
Variable V : lmodType F.
Implicit Types (a : F) (v : V).
Lemma rpredZeq (S : submodClosed V) a v :
(a *: v \in S) = (a == 0) || (v \in S).
End ModuleTheory.
Section Predicates.
Context (S : divClosed F).
Lemma fpredMl x y : x \in S → x != 0 → (x × y \in S) = (y \in S).
Lemma fpredMr x y : x \in S → x != 0 → (y × x \in S) = (y \in S).
Lemma fpred_divl x y : x \in S → x != 0 → (x / y \in S) = (y \in S).
Lemma fpred_divr x y : x \in S → x != 0 → (y / x \in S) = (y \in S).
End Predicates.
End FieldPred.
#[short(type="subNmodType")]
HB.structure Definition SubNmodule (V : nmodType) S :=
{ U of SubChoice V S U & Nmodule U & isSubNmodule V S U }.
Section additive.
Context (V : nmodType) (S : pred V) (U : SubNmodule.type S).
Notation val := (val : U → V).
#[export]
HB.instance Definition _ := isSemiAdditive.Build U V val valD_subproof.
Lemma valD : {morph val : x y / x + y}.
Lemma val0 : val 0 = 0.
End additive.
Let inU v Sv : U := Sub v Sv.
Let zeroU := inU (rpred0 (AddClosed.clone V S _)).
Let addU (u1 u2 : U) := inU (rpredD (valP u1) (valP u2)).
Lemma addUA : associative addU.
Lemma addUC : commutative addU.
Lemma add0U : left_id zeroU addU.
Lemma val0 : (val : U → V) 0 = 0.
Lemma valD : semi_additive (val : U → V).
Implicit Type V : zmodType.
#[short(type="subZmodType")]
HB.structure Definition SubZmodule V S :=
{ U of SubNmodule V S U & Zmodule U & isSubZmodule V S U }.
Section additive.
Context V (S : pred V) (U : SubZmodule.type S).
Notation val := (val : U → V).
#[export]
HB.instance Definition _ := isAdditive.Build U V val valB_subproof.
Lemma valB : {morph val : x y / x - y}.
Lemma valN : {morph val : x / - x}.
End additive.
Let inU v Sv : U := Sub v Sv.
Let zeroU := inU (rpred0 (AddClosed.clone V S _)).
Let oppU (u : U) := inU (rpredNr _ (valP u)).
Let addU (u1 u2 : U) := inU (rpredD (valP u1) (valP u2)).
Lemma addNr : left_inverse zeroU oppU addU.
Lemma valD : semi_additive (val : U → V).
Lemma valB : additive (val : U → V).
#[short(type="subSemiRingType")]
HB.structure Definition SubSemiRing (R : semiRingType) (S : pred R) :=
{ U of SubNmodule R S U & SemiRing U & isSubSemiRing R S U }.
Section multiplicative.
Context (R : semiRingType) (S : pred R) (U : SubSemiRing.type S).
Notation val := (val : U → R).
#[export]
HB.instance Definition _ := isMultiplicative.Build U R val valM_subproof.
Lemma val1 : val 1 = 1.
Lemma valM : {morph val : x y / x × y}.
Lemma valM1 : multiplicative val.
End multiplicative.
Let inU v Sv : U := Sub v Sv.
Let oneU : U := inU (@rpred1 _ (MulClosed.clone R S _)).
Let mulU (u1 u2 : U) := inU (rpredM _ _ (valP u1) (valP u2)).
Lemma mulrA : associative mulU.
Lemma mul1r : left_id oneU mulU.
Lemma mulr1 : right_id oneU mulU.
Lemma mulrDl : left_distributive mulU +%R.
Lemma mulrDr : right_distributive mulU +%R.
Lemma mul0r : left_zero 0%R mulU.
Lemma mulr0 : right_zero 0%R mulU.
Lemma oner_neq0 : oneU != 0.
Lemma valM : multiplicative (val : U → R).
#[short(type="subComSemiRingType")]
HB.structure Definition SubComSemiRing (R : semiRingType) S :=
{U of SubSemiRing R S U & ComSemiRing U}.
Lemma mulrC : @commutative U U *%R.
#[short(type="subRingType")]
HB.structure Definition SubRing (R : ringType) (S : pred R) :=
{ U of SubSemiRing R S U & Ring U & isSubZmodule R S U }.
Let inU v Sv : U := Sub v Sv.
Let oneU : U := inU (@rpred1 _ (MulClosed.clone R S _)).
Let mulU (u1 u2 : U) := inU (rpredM _ _ (valP u1) (valP u2)).
#[short(type="subComRingType")]
HB.structure Definition SubComRing (R : ringType) S :=
{U of SubRing R S U & ComRing U}.
Lemma mulrC : @commutative U U *%R.
#[short(type="subLmodType")]
HB.structure Definition SubLmodule (R : ringType) (V : lmodType R)
(S : pred V) :=
{ W of SubZmodule V S W & Zmodule_isLmodule R W & isSubLmodule R V S W}.
Section linear.
Context (R : ringType) (V : lmodType R) (S : pred V) (W : SubLmodule.type S).
Notation val := (val : W → V).
#[export]
HB.instance Definition _ := isScalable.Build R W V *:%R val valZ.
End linear.
Let inW v Sv : W := Sub v Sv.
Let scaleW a (w : W) := inW (rpredZ a _ (valP w)).
Lemma scalerA' a b v : scaleW a (scaleW b v) = scaleW (a × b) v.
Lemma scale1r : left_id 1 scaleW.
Lemma scalerDr : right_distributive scaleW +%R.
Lemma scalerDl v : {morph scaleW^~ v : a b / a + b}.
Fact valZ : scalable (val : W → _).
#[short(type="subLalgType")]
HB.structure Definition SubLalgebra (R : ringType) (V : lalgType R) S :=
{W of SubRing V S W & @SubLmodule R V S W & Lalgebra R W}.
Lemma scalerAl (a : R) (u v : W) : a *: (u × v) = a *: u × v.
#[short(type="subAlgType")]
HB.structure Definition SubAlgebra (R : ringType) (V : algType R) S :=
{W of @SubLalgebra R V S W & Algebra R W}.
Lemma scalerAr (k : R) (x y : W) : k *: (x × y) = x × (k *: y).
#[short(type="subUnitRingType")]
HB.structure Definition SubUnitRing (R : ringType) (S : pred R) :=
{U of SubRing R S U & UnitRing U}.
Let inU v Sv : U := Sub v Sv.
Let invU (u : U) := inU (rpredVr _ (valP u)).
Lemma mulVr : {in [pred x | val x \is a unit], left_inverse 1 invU *%R}.
Lemma divrr : {in [pred x | val x \is a unit], right_inverse 1 invU *%R}.
Lemma unitrP (x y : U) : y × x = 1 ∧ x × y = 1 → val x \is a unit.
Lemma invr_out : {in [pred x | val x \isn't a unit], invU =1 id}.
#[short(type="subComUnitRingType")]
HB.structure Definition SubComUnitRing (R : comUnitRingType) (S : pred R) :=
{U of SubComRing R S U & SubUnitRing R S U}.
#[short(type="subIdomainType")]
HB.structure Definition SubIntegralDomain (R : idomainType) (S : pred R) :=
{U of SubComRing R S U & IntegralDomain U}.
Lemma id : IntegralDomain.axiom U.
#[short(type="subFieldType")]
HB.structure Definition SubField (F : fieldType) (S : pred F) :=
{U of SubIntegralDomain F S U & Field U}.
Lemma fieldP : Field.axiom 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 "[ 'SubChoice_isSubZmodule' 'of' U 'by' <: ]" :=
(SubChoice_isSubZmodule.Build _ _ U (zmodClosedP _))
(at level 0, format "[ 'SubChoice_isSubZmodule' 'of' U 'by' <: ]")
: form_scope.
Notation "[ 'SubNmodule_isSubSemiRing' 'of' U 'by' <: ]" :=
(SubNmodule_isSubSemiRing.Build _ _ U (@rpred1M _ _))
(at level 0, format "[ 'SubNmodule_isSubSemiRing' 'of' U 'by' <: ]")
: form_scope.
Notation "[ 'SubChoice_isSubSemiRing' 'of' U 'by' <: ]" :=
(SubChoice_isSubSemiRing.Build _ _ U (semiringClosedP _))
(at level 0, format "[ 'SubChoice_isSubSemiRing' 'of' U 'by' <: ]")
: form_scope.
Notation "[ 'SubSemiRing_isSubComSemiRing' 'of' U 'by' <: ]" :=
(SubSemiRing_isSubComSemiRing.Build _ _ U)
(at level 0, format "[ 'SubSemiRing_isSubComSemiRing' 'of' U 'by' <: ]")
: form_scope.
Notation "[ 'SubChoice_isSubComSemiRing' 'of' U 'by' <: ]" :=
(SubChoice_isSubComSemiRing.Build _ _ U (semiringClosedP _))
(at level 0, format "[ 'SubChoice_isSubComSemiRing' 'of' U 'by' <: ]")
: form_scope.
Notation "[ 'SubZmodule_isSubRing' 'of' U 'by' <: ]" :=
(SubZmodule_isSubRing.Build _ _ U (subringClosedP _))
(at level 0, format "[ 'SubZmodule_isSubRing' 'of' U 'by' <: ]")
: form_scope.
Notation "[ 'SubChoice_isSubRing' 'of' U 'by' <: ]" :=
(SubChoice_isSubRing.Build _ _ U (subringClosedP _))
(at level 0, format "[ 'SubChoice_isSubRing' 'of' U 'by' <: ]")
: form_scope.
Notation "[ 'SubRing_isSubComRing' 'of' U 'by' <: ]" :=
(SubRing_isSubComRing.Build _ _ U)
(at level 0, format "[ 'SubRing_isSubComRing' 'of' U 'by' <: ]")
: form_scope.
Notation "[ 'SubChoice_isSubComRing' 'of' U 'by' <: ]" :=
(SubChoice_isSubComRing.Build _ _ U (subringClosedP _))
(at level 0, format "[ 'SubChoice_isSubComRing' 'of' U 'by' <: ]")
: form_scope.
Notation "[ 'SubZmodule_isSubLmodule' 'of' U 'by' <: ]" :=
(SubZmodule_isSubLmodule.Build _ _ _ U (submodClosedP _))
(at level 0, format "[ 'SubZmodule_isSubLmodule' 'of' U 'by' <: ]")
: form_scope.
Notation "[ 'SubChoice_isSubLmodule' 'of' U 'by' <: ]" :=
(SubChoice_isSubLmodule.Build _ _ _ U (submodClosedP _))
(at level 0, format "[ 'SubChoice_isSubLmodule' 'of' U 'by' <: ]")
: form_scope.
Notation "[ 'SubRing_SubLmodule_isSubLalgebra' 'of' U 'by' <: ]" :=
(SubRing_SubLmodule_isSubLalgebra.Build _ _ _ U)
(at level 0, format "[ 'SubRing_SubLmodule_isSubLalgebra' 'of' U 'by' <: ]")
: form_scope.
Notation "[ 'SubChoice_isSubLalgebra' 'of' U 'by' <: ]" :=
(SubChoice_isSubLalgebra.Build _ _ _ U (subalgClosedP _))
(at level 0, format "[ 'SubChoice_isSubLalgebra' 'of' U 'by' <: ]")
: form_scope.
Notation "[ 'SubLalgebra_isSubAlgebra' 'of' U 'by' <: ]" :=
(SubLalgebra_isSubAlgebra.Build _ _ _ U)
(at level 0, format "[ 'SubLalgebra_isSubAlgebra' 'of' U 'by' <: ]")
: form_scope.
Notation "[ 'SubChoice_isSubAlgebra' 'of' U 'by' <: ]" :=
(SubChoice_isSubAlgebra.Build _ _ _ U (subalgClosedP _))
(at level 0, format "[ 'SubChoice_isSubAlgebra' 'of' U 'by' <: ]")
: form_scope.
Notation "[ 'SubRing_isSubUnitRing' 'of' U 'by' <: ]" :=
(SubRing_isSubUnitRing.Build _ _ U (divringClosedP _))
(at level 0, format "[ 'SubRing_isSubUnitRing' 'of' U 'by' <: ]")
: form_scope.
Notation "[ 'SubChoice_isSubUnitRing' 'of' U 'by' <: ]" :=
(SubChoice_isSubUnitRing.Build _ _ U (divringClosedP _))
(at level 0, format "[ 'SubChoice_isSubUnitRing' 'of' U 'by' <: ]")
: form_scope.
Notation "[ 'SubChoice_isSubComUnitRing' 'of' U 'by' <: ]" :=
(SubChoice_isSubComUnitRing.Build _ _ U (divringClosedP _))
(at level 0, format "[ 'SubChoice_isSubComUnitRing' 'of' U 'by' <: ]")
: form_scope.
Notation "[ 'SubComUnitRing_isSubIntegralDomain' 'of' U 'by' <: ]" :=
(SubComUnitRing_isSubIntegralDomain.Build _ _ U)
(at level 0, format "[ 'SubComUnitRing_isSubIntegralDomain' 'of' U 'by' <: ]")
: form_scope.
Notation "[ 'SubChoice_isSubIntegralDomain' 'of' U 'by' <: ]" :=
(SubChoice_isSubIntegralDomain.Build _ _ U (divringClosedP _))
(at level 0, format "[ 'SubChoice_isSubIntegralDomain' 'of' U 'by' <: ]")
: form_scope.
Notation "[ 'SubIntegralDomain_isSubField' 'of' U 'by' <: ]" :=
(SubIntegralDomain_isSubField.Build _ _ U (frefl _))
(at level 0, format "[ 'SubIntegralDomain_isSubField' 'of' U 'by' <: ]")
: form_scope.
End SubExports.
Module Theory.
Definition addrA := @addrA.
Definition addrC := @addrC.
Definition add0r := @add0r.
Definition addNr := @addNr.
Definition addr0 := addr0.
Definition addrN := addrN.
Definition subrr := subrr.
Definition addrCA := addrCA.
Definition addrAC := addrAC.
Definition addrACA := addrACA.
Definition addKr := addKr.
Definition addNKr := addNKr.
Definition addrK := addrK.
Definition addrNK := addrNK.
Definition subrK := subrK.
Definition subKr := subKr.
Definition addrI := @addrI.
Definition addIr := @addIr.
Definition subrI := @subrI.
Definition subIr := @subIr.
Arguments addrI {V} y [x1 x2].
Arguments addIr {V} x [x1 x2].
Arguments subrI {V} y [x1 x2].
Arguments subIr {V} x [x1 x2].
Definition opprK := @opprK.
Arguments opprK {V}.
Definition oppr_inj := @oppr_inj.
Arguments oppr_inj {V} [x1 x2].
Definition oppr0 := oppr0.
Definition oppr_eq0 := oppr_eq0.
Definition opprD := opprD.
Definition opprB := opprB.
Definition addrKA := addrKA.
Definition subrKA := subrKA.
Definition subr0 := subr0.
Definition sub0r := sub0r.
Definition subr_eq := subr_eq.
Definition addr0_eq := addr0_eq.
Definition subr0_eq := subr0_eq.
Definition subr_eq0 := subr_eq0.
Definition addr_eq0 := addr_eq0.
Definition eqr_opp := eqr_opp.
Definition eqr_oppLR := eqr_oppLR.
Definition sumrN := sumrN.
Definition sumrB := sumrB.
Definition sumrMnl := sumrMnl.
Definition sumrMnr := sumrMnr.
Definition sumr_const := sumr_const.
Definition sumr_const_nat := sumr_const_nat.
Definition telescope_sumr := telescope_sumr.
Definition telescope_sumr_eq := @telescope_sumr_eq.
Arguments telescope_sumr_eq {V n m} f u.
Definition mulr0n := mulr0n.
Definition mulr1n := mulr1n.
Definition mulr2n := mulr2n.
Definition mulrS := mulrS.
Definition mulrSr := mulrSr.
Definition mulrb := mulrb.
Definition mul0rn := mul0rn.
Definition mulNrn := mulNrn.
Definition mulrnDl := mulrnDl.
Definition mulrnDr := mulrnDr.
Definition mulrnBl := mulrnBl.
Definition mulrnBr := mulrnBr.
Definition mulrnA := mulrnA.
Definition mulrnAC := mulrnAC.
Definition iter_addr := iter_addr.
Definition iter_addr_0 := iter_addr_0.
Definition mulrA := @mulrA.
Definition mul1r := @mul1r.
Definition mulr1 := @mulr1.
Definition mulrDl := @mulrDl.
Definition mulrDr := @mulrDr.
Definition oner_neq0 := @oner_neq0.
Definition oner_eq0 := oner_eq0.
Definition mul0r := @mul0r.
Definition mulr0 := @mulr0.
Definition mulrN := mulrN.
Definition mulNr := mulNr.
Definition mulrNN := mulrNN.
Definition mulN1r := mulN1r.
Definition mulrN1 := mulrN1.
Definition mulr_suml := mulr_suml.
Definition mulr_sumr := mulr_sumr.
Definition mulrBl := mulrBl.
Definition mulrBr := mulrBr.
Definition mulrnAl := mulrnAl.
Definition mulrnAr := mulrnAr.
Definition mulr_natl := mulr_natl.
Definition mulr_natr := mulr_natr.
Definition natrD := natrD.
Definition nat1r := nat1r.
Definition natr1 := natr1.
Arguments natr1 {R} n.
Arguments nat1r {R} n.
Definition natrB := natrB.
Definition natr_sum := natr_sum.
Definition natrM := natrM.
Definition natrX := natrX.
Definition expr0 := expr0.
Definition exprS := exprS.
Definition expr1 := expr1.
Definition expr2 := expr2.
Definition expr0n := expr0n.
Definition expr1n := expr1n.
Definition exprD := exprD.
Definition exprSr := exprSr.
Definition expr_sum := expr_sum.
Definition commr_sym := commr_sym.
Definition commr_refl := commr_refl.
Definition commr0 := commr0.
Definition commr1 := commr1.
Definition commrN := commrN.
Definition commrN1 := commrN1.
Definition commrD := commrD.
Definition commrB := commrB.
Definition commr_sum := commr_sum.
Definition commr_prod := commr_prod.
Definition commrMn := commrMn.
Definition commrM := commrM.
Definition commr_nat := commr_nat.
Definition commrX := commrX.
Definition exprMn_comm := exprMn_comm.
Definition commr_sign := commr_sign.
Definition exprMn_n := exprMn_n.
Definition exprM := exprM.
Definition exprAC := exprAC.
Definition expr_mod := expr_mod.
Definition expr_dvd := expr_dvd.
Definition signr_odd := signr_odd.
Definition signr_eq0 := signr_eq0.
Definition mulr_sign := mulr_sign.
Definition signr_addb := signr_addb.
Definition signrN := signrN.
Definition signrE := signrE.
Definition mulr_signM := mulr_signM.
Definition exprNn := exprNn.
Definition sqrrN := sqrrN.
Definition sqrr_sign := sqrr_sign.
Definition signrMK := signrMK.
Definition mulrI_eq0 := mulrI_eq0.
Definition lreg_neq0 := lreg_neq0.
Definition mulrI0_lreg := mulrI0_lreg.
Definition lregN := lregN.
Definition lreg1 := lreg1.
Definition lregM := lregM.
Definition lregX := lregX.
Definition lreg_sign := lreg_sign.
Definition lregP {R x} := @lregP R x.
Definition mulIr_eq0 := mulIr_eq0.
Definition mulIr0_rreg := mulIr0_rreg.
Definition rreg_neq0 := rreg_neq0.
Definition rregN := rregN.
Definition rreg1 := rreg1.
Definition rregM := rregM.
Definition revrX := revrX.
Definition rregX := rregX.
Definition rregP {R x} := @rregP R x.
Definition exprDn_comm := exprDn_comm.
Definition exprBn_comm := exprBn_comm.
Definition subrXX_comm := subrXX_comm.
Definition exprD1n := exprD1n.
Definition subrX1 := subrX1.
Definition sqrrD1 := sqrrD1.
Definition sqrrB1 := sqrrB1.
Definition subr_sqr_1 := subr_sqr_1.
Definition charf0 := charf0.
Definition charf_prime := charf_prime.
Definition mulrn_char := mulrn_char.
Definition dvdn_charf := dvdn_charf.
Definition charf_eq := charf_eq.
Definition bin_lt_charf_0 := bin_lt_charf_0.
Definition Frobenius_autE := Frobenius_autE.
Definition Frobenius_aut0 := Frobenius_aut0.
Definition Frobenius_aut1 := Frobenius_aut1.
Definition Frobenius_autD_comm := Frobenius_autD_comm.
Definition Frobenius_autMn := Frobenius_autMn.
Definition Frobenius_aut_nat := Frobenius_aut_nat.
Definition Frobenius_autM_comm := Frobenius_autM_comm.
Definition Frobenius_autX := Frobenius_autX.
Definition Frobenius_autN := Frobenius_autN.
Definition Frobenius_autB_comm := Frobenius_autB_comm.
Definition exprNn_char := exprNn_char.
Definition addrr_char2 := addrr_char2.
Definition oppr_char2 := oppr_char2.
Definition addrK_char2 := addrK_char2.
Definition addKr_char2 := addKr_char2.
Definition iter_mulr := iter_mulr.
Definition iter_mulr_1 := iter_mulr_1.
Definition prodr_const := prodr_const.
Definition prodr_const_nat := prodr_const_nat.
Definition mulrC := @mulrC.
Definition mulrCA := mulrCA.
Definition mulrAC := mulrAC.
Definition mulrACA := mulrACA.
Definition exprMn := exprMn.
Definition prodrXl := prodrXl.
Definition prodrXr := prodrXr.
Definition prodrN := prodrN.
Definition prodrMn_const := prodrMn_const.
Definition prodrMn := prodrMn.
Definition natr_prod := natr_prod.
Definition prodr_undup_exp_count := prodr_undup_exp_count.
Definition exprDn := exprDn.
Definition exprBn := exprBn.
Definition subrXX := subrXX.
Definition sqrrD := sqrrD.
Definition sqrrB := sqrrB.
Definition subr_sqr := subr_sqr.
Definition subr_sqrDB := subr_sqrDB.
Definition exprDn_char := exprDn_char.
Definition mulrV := mulrV.
Definition divrr := divrr.
Definition mulVr := mulVr.
Definition invr_out := invr_out.
Definition unitrP {R x} := @unitrP R x.
Definition mulKr := mulKr.
Definition mulVKr := mulVKr.
Definition mulrK := mulrK.
Definition mulrVK := mulrVK.
Definition divrK := divrK.
Definition mulrI := mulrI.
Definition mulIr := mulIr.
Definition divrI := divrI.
Definition divIr := divIr.
Definition telescope_prodr := telescope_prodr.
Definition telescope_prodr_eq := @telescope_prodr_eq.
Arguments telescope_prodr_eq {R n m} f u.
Definition commrV := commrV.
Definition unitrE := unitrE.
Definition invrK := @invrK.
Arguments invrK {R}.
Definition invr_inj := @invr_inj.
Arguments invr_inj {R} [x1 x2].
Definition unitrV := unitrV.
Definition unitr1 := unitr1.
Definition invr1 := invr1.
Definition divr1 := divr1.
Definition div1r := div1r.
Definition natr_div := natr_div.
Definition unitr0 := unitr0.
Definition invr0 := invr0.
Definition unitrN1 := unitrN1.
Definition unitrN := unitrN.
Definition invrN1 := invrN1.
Definition invrN := invrN.
Definition divrNN := divrNN.
Definition divrN := divrN.
Definition invr_sign := invr_sign.
Definition unitrMl := unitrMl.
Definition unitrMr := unitrMr.
Definition invrM := invrM.
Definition invr_eq0 := invr_eq0.
Definition invr_eq1 := invr_eq1.
Definition invr_neq0 := invr_neq0.
Definition unitrM_comm := unitrM_comm.
Definition unitrX := unitrX.
Definition unitrX_pos := unitrX_pos.
Definition exprVn := exprVn.
Definition exprB := exprB.
Definition invr_signM := invr_signM.
Definition divr_signM := divr_signM.
Definition rpred0D := @rpred0D.
Definition rpred0 := rpred0.
Definition rpredD := rpredD.
Definition rpredNr := @rpredNr.
Definition rpred_sum := rpred_sum.
Definition rpredMn := rpredMn.
Definition rpredN := rpredN.
Definition rpredB := rpredB.
Definition rpredBC := rpredBC.
Definition rpredMNn := rpredMNn.
Definition rpredDr := rpredDr.
Definition rpredDl := rpredDl.
Definition rpredBr := rpredBr.
Definition rpredBl := rpredBl.
Definition zmodClosedP := zmodClosedP.
Definition rpredMsign := rpredMsign.
Definition rpred1M := @rpred1M.
Definition rpred1 := @rpred1.
Definition rpredM := @rpredM.
Definition rpred_prod := rpred_prod.
Definition rpredX := rpredX.
Definition rpred_nat := rpred_nat.
Definition rpredN1 := rpredN1.
Definition rpred_sign := rpred_sign.
Definition semiringClosedP := semiringClosedP.
Definition subringClosedP := subringClosedP.
Definition rpredZsign := rpredZsign.
Definition rpredZnat := rpredZnat.
Definition submodClosedP := submodClosedP.
Definition subalgClosedP := subalgClosedP.
Definition rpredZ := @rpredZ.
Definition rpredVr := @rpredVr.
Definition rpredV := rpredV.
Definition rpred_div := rpred_div.
Definition rpredXN := rpredXN.
Definition rpredZeq := rpredZeq.
Definition char_lalg := char_lalg.
Definition rpredMr := rpredMr.
Definition rpredMl := rpredMl.
Definition rpred_divr := rpred_divr.
Definition rpred_divl := rpred_divl.
Definition divringClosedP := divringClosedP.
Definition eq_eval := eq_eval.
Definition eval_tsubst := eval_tsubst.
Definition eq_holds := eq_holds.
Definition holds_fsubst := holds_fsubst.
Definition unitrM := unitrM.
Definition unitrPr {R x} := @unitrPr R x.
Definition expr_div_n := expr_div_n.
Definition mulr1_eq := mulr1_eq.
Definition divr1_eq := divr1_eq.
Definition divKr := divKr.
Definition mulf_eq0 := mulf_eq0.
Definition prodf_eq0 := prodf_eq0.
Definition prodf_seq_eq0 := prodf_seq_eq0.
Definition mulf_neq0 := mulf_neq0.
Definition prodf_neq0 := prodf_neq0.
Definition prodf_seq_neq0 := prodf_seq_neq0.
Definition expf_eq0 := expf_eq0.
Definition sqrf_eq0 := sqrf_eq0.
Definition expf_neq0 := expf_neq0.
Definition natf_neq0 := natf_neq0.
Definition natf0_char := natf0_char.
Definition charf'_nat := charf'_nat.
Definition charf0P := charf0P.
Definition eqf_sqr := eqf_sqr.
Definition mulfI := mulfI.
Definition mulIf := mulIf.
Definition divfI := divfI.
Definition divIf := divIf.
Definition sqrf_eq1 := sqrf_eq1.
Definition expfS_eq1 := expfS_eq1.
Definition fieldP := @fieldP.
Definition unitfE := unitfE.
Definition mulVf := mulVf.
Definition mulfV := mulfV.
Definition divff := divff.
Definition mulKf := mulKf.
Definition mulVKf := mulVKf.
Definition mulfK := mulfK.
Definition mulfVK := mulfVK.
Definition divfK := divfK.
Definition divKf := divKf.
Definition invfM := invfM.
Definition invf_div := invf_div.
Definition expfB_cond := expfB_cond.
Definition expfB := expfB.
Definition prodfV := prodfV.
Definition prodf_div := prodf_div.
Definition telescope_prodf := telescope_prodf.
Definition telescope_prodf_eq := @telescope_prodf_eq.
Arguments telescope_prodf_eq {F n m} f u.
Definition addf_div := addf_div.
Definition mulf_div := mulf_div.
Definition eqr_div := eqr_div.
Definition eqr_sum_div := eqr_sum_div.
Definition char0_natf_div := char0_natf_div.
Definition fpredMr := fpredMr.
Definition fpredMl := fpredMl.
Definition fpred_divr := fpred_divr.
Definition fpred_divl := fpred_divl.
Definition satP {F e f} := @satP F e f.
Definition eq_sat := eq_sat.
Definition solP {F n f} := @solP F n f.
Definition eq_sol := eq_sol.
Definition size_sol := size_sol.
Definition solve_monicpoly := @solve_monicpoly.
Definition semi_additive := semi_additive.
Definition additive := additive.
Definition raddf0 := raddf0.
Definition raddf_eq0 := raddf_eq0.
Definition raddf_inj := raddf_inj.
Definition raddfN := raddfN.
Definition raddfD := raddfD.
Definition raddfB := raddfB.
Definition raddf_sum := raddf_sum.
Definition raddfMn := raddfMn.
Definition raddfMNn := raddfMNn.
Definition raddfMnat := raddfMnat.
Definition raddfMsign := raddfMsign.
Definition can2_semi_additive := can2_semi_additive.
Definition can2_additive := can2_additive.
Definition multiplicative := multiplicative.
Definition rmorph0 := rmorph0.
Definition rmorphN := rmorphN.
Definition rmorphD := rmorphD.
Definition rmorphB := rmorphB.
Definition rmorph_sum := rmorph_sum.
Definition rmorphMn := rmorphMn.
Definition rmorphMNn := rmorphMNn.
Definition rmorphismMP := rmorphismMP.
Definition rmorph1 := rmorph1.
Definition rmorph_eq1 := rmorph_eq1.
Definition rmorphM := rmorphM.
Definition rmorphMsign := rmorphMsign.
Definition rmorph_nat := rmorph_nat.
Definition rmorph_eq_nat := rmorph_eq_nat.
Definition rmorph_prod := rmorph_prod.
Definition rmorphXn := rmorphXn.
#[deprecated(since="mathcomp 1.17.0", note="Use rmorphXn instead.")]
Notation rmorphX := rmorphXn.
Definition rmorphN1 := rmorphN1.
Definition rmorph_sign := rmorph_sign.
Definition rmorph_char := rmorph_char.
Definition can2_rmorphism := can2_rmorphism.
Definition rmorph_comm := rmorph_comm.
Definition rmorph_unit := rmorph_unit.
Definition rmorphV := rmorphV.
Definition rmorph_div := rmorph_div.
Definition fmorph_eq0 := fmorph_eq0.
Definition fmorph_inj := @fmorph_inj.
Arguments fmorph_inj {F R} f [x1 x2].
Definition fmorph_eq := fmorph_eq.
Definition fmorph_eq1 := fmorph_eq1.
Definition fmorph_char := fmorph_char.
Definition fmorph_unit := fmorph_unit.
Definition fmorphV := fmorphV.
Definition fmorph_div := fmorph_div.
Definition scalerA := scalerA.
Definition scale1r := @scale1r.
Definition scalerDr := @scalerDr.
Definition scalerDl := @scalerDl.
Definition scaler0 := scaler0.
Definition scale0r := scale0r.
Definition scaleNr := scaleNr.
Definition scaleN1r := scaleN1r.
Definition scalerN := scalerN.
Definition scalerBl := scalerBl.
Definition scalerBr := scalerBr.
Definition scaler_nat := scaler_nat.
Definition scalerMnl := scalerMnl.
Definition scalerMnr := scalerMnr.
Definition scaler_suml := scaler_suml.
Definition scaler_sumr := scaler_sumr.
Definition scaler_eq0 := scaler_eq0.
Definition scalerK := scalerK.
Definition scalerKV := scalerKV.
Definition scalerI := scalerI.
Definition scalerAl := @scalerAl.
Definition mulr_algl := mulr_algl.
Definition scaler_sign := scaler_sign.
Definition signrZK := signrZK.
Definition scalerCA := scalerCA.
Definition scalerAr := @scalerAr.
Definition mulr_algr := mulr_algr.
Definition comm_alg := comm_alg.
Definition exprZn := exprZn.
Definition scaler_prodl := scaler_prodl.
Definition scaler_prodr := scaler_prodr.
Definition scaler_prod := scaler_prod.
Definition scaler_injl := scaler_injl.
Definition scaler_unit := scaler_unit.
Definition invrZ := invrZ.
Definition raddfZnat := raddfZnat.
Definition raddfZsign := raddfZsign.
Definition in_algE := in_algE.
Definition scalable_for := scalable_for.
Definition linear_for := linear_for.
Definition additive_linear := additive_linear.
Definition scalable_linear := scalable_linear.
Definition linear0 := linear0.
Definition linearN := linearN.
Definition linearD := linearD.
Definition linearB := linearB.
Definition linear_sum := linear_sum.
Definition linearMn := linearMn.
Definition linearMNn := linearMNn.
Definition linearP := linearP.
Definition linearZ_LR := linearZ_LR.
Definition linearZ := linearZ.
Definition linearPZ := linearPZ.
Definition linearZZ := linearZZ.
Definition scalarP := scalarP.
Definition scalarZ := scalarZ.
Definition can2_scalable := can2_scalable.
Definition can2_linear := can2_linear.
Definition rmorph_alg := rmorph_alg.
Definition imaginary_exists := imaginary_exists.
Definition raddf := (raddf0, raddfN, raddfD, raddfMn).
Definition rmorphE :=
(rmorphD, rmorph0, rmorphB, rmorphN, rmorphMNn, rmorphMn, rmorph1, rmorphXn).
Definition linearE :=
(linearD, linear0, linearB, linearMNn, linearMn, linearZ).
Notation null_fun V := (null_fun V) (only parsing).
Notation in_alg A := (in_alg_loc A).
End Theory.
Notation in_alg A := (in_alg_loc A).
Module AllExports. End AllExports.
End GRing.
Export AllExports.
Export Scale.Exports.
Export ClosedExports.
Variant Ione := IOne : Ione.
Inductive Inatmul :=
| INatmul : Ione → nat → Inatmul
| IOpp : Inatmul → Inatmul.
Variant Idummy_placeholder :=.
Definition parse (x : Number.int) : Inatmul :=
match x with
| Number.IntDecimal (Decimal.Pos u) ⇒ INatmul IOne (Nat.of_uint u)
| Number.IntDecimal (Decimal.Neg u) ⇒ IOpp (INatmul IOne (Nat.of_uint u))
| Number.IntHexadecimal (Hexadecimal.Pos u) ⇒
INatmul IOne (Nat.of_hex_uint u)
| Number.IntHexadecimal (Hexadecimal.Neg u) ⇒
IOpp (INatmul IOne (Nat.of_hex_uint u))
end.
Definition print (x : Inatmul) : option Number.int :=
match x with
| INatmul IOne n ⇒
Some (Number.IntDecimal (Decimal.Pos (Nat.to_uint n)))
| IOpp (INatmul IOne n) ⇒
Some (Number.IntDecimal (Decimal.Neg (Nat.to_uint n)))
| _ ⇒ None
end.
Arguments GRing.one {_}.
Arguments GRing.one : clear implicits.
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.
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.
Arguments GRing.char R%type.
Notation "[ 'char' R ]" := (GRing.char R) : ring_scope.
Notation Frobenius_aut chRp := (Frobenius_aut chRp).
Notation "*%R" := (@mul _) : function_scope.
Notation "x * y" := (mul x y) : ring_scope.
Notation "x ^+ n" := (exp x n) : ring_scope.
Notation "x ^-1" := (inv x) : ring_scope.
Notation "x ^- n" := (inv (x ^+ n)) : ring_scope.
Notation "x / y" := (mul x y^-1) : ring_scope.
Notation "*:%R" := (@scale _ _) : function_scope.
Notation "a *: m" := (scale a m) : ring_scope.
Notation "k %:A" := (scale k 1) : ring_scope.
Notation "\0" := (null_fun _) : ring_scope.
Notation "f \+ g" := (add_fun f g) : ring_scope.
Notation "f \- g" := (sub_fun f g) : ring_scope.
Notation "\- f" := (opp_fun f) : ring_scope.
Notation "a \*: f" := (scale_fun a f) : ring_scope.
Notation "x \*o f" := (mull_fun x f) : ring_scope.
Notation "x \o* f" := (mulr_fun x f) : ring_scope.
Notation "f \* g" := (mul_fun f g) : ring_scope.
Arguments null_fun {_} V _ /.
Arguments in_alg_head {_} A _ /.
Arguments add_fun {_ _} f g _ /.
Arguments sub_fun {_ _} f g _ /.
Arguments opp_fun {_ _} f _ /.
Arguments mull_fun {_ _} a f _ /.
Arguments mulr_fun {_ _} a f _ /.
Arguments scale_fun {_ _ _} a f _ /.
Arguments mul_fun {_ _} f g _ /.
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.
Notation "\prod_ ( i <- r | P ) F" :=
(\big[*%R/1%R]_(i <- r | P%B) F%R) : ring_scope.
Notation "\prod_ ( i <- r ) F" :=
(\big[*%R/1%R]_(i <- r) F%R) : ring_scope.
Notation "\prod_ ( m <= i < n | P ) F" :=
(\big[*%R/1%R]_(m ≤ i < n | P%B) F%R) : ring_scope.
Notation "\prod_ ( m <= i < n ) F" :=
(\big[*%R/1%R]_(m ≤ i < n) F%R) : ring_scope.
Notation "\prod_ ( i | P ) F" :=
(\big[*%R/1%R]_(i | P%B) F%R) : ring_scope.
Notation "\prod_ i F" :=
(\big[*%R/1%R]_i F%R) : ring_scope.
Notation "\prod_ ( i : t | P ) F" :=
(\big[*%R/1%R]_(i : t | P%B) F%R) (only parsing) : ring_scope.
Notation "\prod_ ( i : t ) F" :=
(\big[*%R/1%R]_(i : t) F%R) (only parsing) : ring_scope.
Notation "\prod_ ( i < n | P ) F" :=
(\big[*%R/1%R]_(i < n | P%B) F%R) : ring_scope.
Notation "\prod_ ( i < n ) F" :=
(\big[*%R/1%R]_(i < n) F%R) : ring_scope.
Notation "\prod_ ( i 'in' A | P ) F" :=
(\big[*%R/1%R]_(i in A | P%B) F%R) : ring_scope.
Notation "\prod_ ( i 'in' A ) F" :=
(\big[*%R/1%R]_(i in A) F%R) : ring_scope.
Notation "R ^c" := (converse R) (at level 2, format "R ^c") : type_scope.
Notation "R ^o" := (regular R) (at level 2, format "R ^o") : type_scope.
Bind Scope term_scope with term.
Bind Scope term_scope with formula.
Notation "''X_' i" := (Var _ i) : term_scope.
Notation "n %:R" := (NatConst _ n) : term_scope.
Notation "0" := 0%:R%T : term_scope.
Notation "1" := 1%:R%T : term_scope.
Notation "x %:T" := (Const x) : term_scope.
Infix "+" := Add : term_scope.
Notation "- t" := (Opp t) : term_scope.
Notation "t - u" := (Add t (- u)) : term_scope.
Infix "×" := Mul : term_scope.
Infix "*+" := NatMul : term_scope.
Notation "t ^-1" := (Inv t) : term_scope.
Notation "t / u" := (Mul t u^-1) : term_scope.
Infix "^+" := Exp : term_scope.
Infix "==" := Equal : term_scope.
Notation "x != y" := (GRing.Not (x == y)) : term_scope.
Infix "∧" := And : term_scope.
Infix "∨" := Or : term_scope.
Infix "==>" := Implies : term_scope.
Notation "~ f" := (Not f) : term_scope.
Notation "''exists' ''X_' i , f" := (Exists i f) : term_scope.
Notation "''forall' ''X_' i , f" := (Forall i f) : term_scope.
Lifting Structure from the codomain of finfuns.
Section FinFunNmod.
Variable (aT : finType) (rT : nmodType).
Implicit Types f g : {ffun aT → rT}.
Definition ffun_zero := [ffun a : aT ⇒ (0 : rT)].
Definition ffun_add f g := [ffun a ⇒ f a + g a].
Fact ffun_addA : associative ffun_add.
Fact ffun_addC : commutative ffun_add.
Fact ffun_add0 : left_id ffun_zero ffun_add.
#[export]
HB.instance Definition _ := isNmodule.Build {ffun aT → rT}
ffun_addA ffun_addC ffun_add0.
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.
Lemma ffunMnE f n x : (f *+ n) x = f x *+ n.
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_addN : left_inverse (@ffun_zero _ _) ffun_opp (@ffun_add _ _).
#[export]
HB.instance Definition _ := Nmodule_isZmodule.Build {ffun aT → rT}
ffun_addN.
End FinFunZmod.
Section FinFunSemiRing.
Variable (aT : finType) (rT : nmodType).
Implicit Types f g : {ffun aT → rT}.
Definition ffun_zero := [ffun a : aT ⇒ (0 : rT)].
Definition ffun_add f g := [ffun a ⇒ f a + g a].
Fact ffun_addA : associative ffun_add.
Fact ffun_addC : commutative ffun_add.
Fact ffun_add0 : left_id ffun_zero ffun_add.
#[export]
HB.instance Definition _ := isNmodule.Build {ffun aT → rT}
ffun_addA ffun_addC ffun_add0.
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.
Lemma ffunMnE f n x : (f *+ n) x = f x *+ n.
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_addN : left_inverse (@ffun_zero _ _) ffun_opp (@ffun_add _ _).
#[export]
HB.instance Definition _ := Nmodule_isZmodule.Build {ffun aT → rT}
ffun_addN.
End FinFunZmod.
Section FinFunSemiRing.
As rings require 1 != 0 in order to lift a ring structure over finfuns
we need evidence that the domain is non-empty.
Variable (aT : finType) (R : semiRingType) (a : aT).
Definition ffun_one : {ffun aT → R} := [ffun ⇒ 1].
Definition ffun_mul (f g : {ffun aT → R}) := [ffun x ⇒ f x × g x].
Fact ffun_mulA : associative ffun_mul.
Fact ffun_mul_1l : left_id ffun_one ffun_mul.
Fact ffun_mul_1r : right_id ffun_one ffun_mul.
Fact ffun_mul_addl : left_distributive ffun_mul (@ffun_add _ _).
Fact ffun_mul_addr : right_distributive ffun_mul (@ffun_add _ _).
Fact ffun_mul_0l : left_zero (@ffun_zero _ _) ffun_mul.
Fact ffun_mul_0r : right_zero (@ffun_zero _ _) ffun_mul.
Fact ffun1_nonzero : ffun_one != 0.
TODO_HB uncomment once ffun_ring below is fixed
# [export]
HB.instance Definition _ := Nmodule_isSemiRing.Build {ffun aT -> R}
ffun_mulA ffun_mul_1l ffun_mul_1r ffun_mul_addl ffun_mul_addr
ffun_mul_0l ffun_mul_0r ffun1_nonzero.
Definition ffun_semiring : semiRingType := {ffun aT -> R}.
As rings require 1 != 0 in order to lift a ring structure over finfuns
we need evidence that the domain is non-empty.
TODO_HB: doesn't work in combination with ffun_semiring above
TODO_HB do FinFunComSemiRing once above is fixed
Section FinFunComRing.
Variable (aT : finType) (R : comRingType) (a : aT).
Fact ffun_mulC : commutative (@ffun_mul aT R).
Variable (aT : finType) (R : comRingType) (a : aT).
Fact ffun_mulC : commutative (@ffun_mul aT R).
TODO_HB
# [export]
HB.instance Definition _ :=
Ring_hasCommutativeMul.Build (ffun_ring _ a) ffun_mulC.
End FinFunComRing.
Section FinFunLmod.
Variable (R : ringType) (aT : finType) (rT : lmodType R).
Implicit Types f g : {ffun aT → rT}.
Definition ffun_scale k f := [ffun a ⇒ k *: f a].
Fact ffun_scaleA k1 k2 f :
ffun_scale k1 (ffun_scale k2 f) = ffun_scale (k1 × k2) f.
Fact ffun_scale1 : left_id 1 ffun_scale.
Fact ffun_scale_addr k : {morph (ffun_scale k) : x y / x + y}.
Fact ffun_scale_addl u : {morph (ffun_scale)^~ u : k1 k2 / k1 + k2}.
#[export]
HB.instance Definition _ := Zmodule_isLmodule.Build R {ffun aT → rT}
ffun_scaleA ffun_scale1 ffun_scale_addr ffun_scale_addl.
End FinFunLmod.
External direct product.
Section PairNmod.
Variables U V : nmodType.
Definition add_pair (x y : U × V) := (x.1 + y.1, x.2 + y.2).
Fact pair_addA : associative add_pair.
Fact pair_addC : commutative add_pair.
Fact pair_add0 : left_id (0, 0) add_pair.
#[export]
HB.instance Definition _ := isNmodule.Build (U × V)%type
pair_addA pair_addC pair_add0.
Fact fst_is_semi_additive : semi_additive fst.
#[export]
HB.instance Definition _ := isSemiAdditive.Build (U × V)%type U fst
fst_is_semi_additive.
Fact snd_is_semi_additive : semi_additive snd.
#[export]
HB.instance Definition _ := isSemiAdditive.Build (U × V)%type V snd
snd_is_semi_additive.
End PairNmod.
Section PairZmod.
Variables U V : zmodType.
Definition opp_pair (x : U × V) := (- x.1, - x.2).
Fact pair_addN : left_inverse (0, 0) opp_pair (@add_pair U V).
#[export]
HB.instance Definition _ := Nmodule_isZmodule.Build (U × V)%type pair_addN.
End PairZmod.
Section PairSemiRing.
Variables R1 R2 : semiRingType.
Definition mul_pair (x y : R1 × R2) := (x.1 × y.1, x.2 × y.2).
Fact pair_mulA : associative mul_pair.
Fact pair_mul1l : left_id (1, 1) mul_pair.
Fact pair_mul1r : right_id (1, 1) mul_pair.
Fact pair_mulDl : left_distributive mul_pair +%R.
Fact pair_mulDr : right_distributive mul_pair +%R.
Fact pair_mul0r : left_zero 0 mul_pair.
Fact pair_mulr0 : right_zero 0 mul_pair.
Fact pair_one_neq0 : (1, 1) != 0 :> R1 × R2.
#[export]
HB.instance Definition _ := Nmodule_isSemiRing.Build (R1 × R2)%type
pair_mulA pair_mul1l pair_mul1r pair_mulDl pair_mulDr pair_mul0r pair_mulr0
pair_one_neq0.
Fact fst_is_multiplicative : multiplicative fst.
#[export]
HB.instance Definition _ := isMultiplicative.Build (R1 × R2)%type R1 fst
fst_is_multiplicative.
Fact snd_is_multiplicative : multiplicative snd.
#[export]
HB.instance Definition _ := isMultiplicative.Build (R1 × R2)%type R2 snd
snd_is_multiplicative.
End PairSemiRing.
Section PairComSemiRing.
Variables R1 R2 : comSemiRingType.
Fact pair_mulC : commutative (@mul_pair R1 R2).
#[export]
HB.instance Definition _ := SemiRing_hasCommutativeMul.Build (R1 × R2)%type
pair_mulC.
End PairComSemiRing.
#[export]
HB.instance Definition _ (R1 R2 : ringType) :=
SemiRing.copy (R1 × R1)%type (R1 × R1)%type.
#[export]
HB.instance Definition _ (R1 R2 : comRingType) :=
SemiRing.copy (R1 × R1)%type (R1 × R1)%type.
Section PairLmod.
Variables (R : ringType) (V1 V2 : lmodType R).
Definition scale_pair a (v : V1 × V2) : V1 × V2 := (a *: v.1, a *: v.2).
Fact pair_scaleA a b u : scale_pair a (scale_pair b u) = scale_pair (a × b) u.
Fact pair_scale1 u : scale_pair 1 u = u.
Fact pair_scaleDr : right_distributive scale_pair +%R.
Fact pair_scaleDl u : {morph scale_pair^~ u: a b / a + b}.
#[export]
HB.instance Definition _ := Zmodule_isLmodule.Build R (V1 × V2)%type
pair_scaleA pair_scale1 pair_scaleDr pair_scaleDl.
Fact fst_is_scalable : scalable fst.
#[export]
HB.instance Definition _ := isScalable.Build R (V1 × V2)%type V1 *:%R fst
fst_is_scalable.
Fact snd_is_scalable : scalable snd.
#[export]
HB.instance Definition _ := isScalable.Build R (V1 × V2)%type V2 *:%R snd
snd_is_scalable.
End PairLmod.
Section PairLalg.
Variables (R : ringType) (A1 A2 : lalgType R).
Fact pair_scaleAl a (u v : A1 × A2) : a *: (u × v) = (a *: u) × v.
#[export]
HB.instance Definition _ := Lmodule_isLalgebra.Build R (A1 × A2)%type
pair_scaleAl.
#[export]
HB.instance Definition _ := RMorphism.on (@fst A1 A2).
#[export]
HB.instance Definition _ := RMorphism.on (@snd A1 A2).
End PairLalg.
Section PairAlg.
Variables U V : nmodType.
Definition add_pair (x y : U × V) := (x.1 + y.1, x.2 + y.2).
Fact pair_addA : associative add_pair.
Fact pair_addC : commutative add_pair.
Fact pair_add0 : left_id (0, 0) add_pair.
#[export]
HB.instance Definition _ := isNmodule.Build (U × V)%type
pair_addA pair_addC pair_add0.
Fact fst_is_semi_additive : semi_additive fst.
#[export]
HB.instance Definition _ := isSemiAdditive.Build (U × V)%type U fst
fst_is_semi_additive.
Fact snd_is_semi_additive : semi_additive snd.
#[export]
HB.instance Definition _ := isSemiAdditive.Build (U × V)%type V snd
snd_is_semi_additive.
End PairNmod.
Section PairZmod.
Variables U V : zmodType.
Definition opp_pair (x : U × V) := (- x.1, - x.2).
Fact pair_addN : left_inverse (0, 0) opp_pair (@add_pair U V).
#[export]
HB.instance Definition _ := Nmodule_isZmodule.Build (U × V)%type pair_addN.
End PairZmod.
Section PairSemiRing.
Variables R1 R2 : semiRingType.
Definition mul_pair (x y : R1 × R2) := (x.1 × y.1, x.2 × y.2).
Fact pair_mulA : associative mul_pair.
Fact pair_mul1l : left_id (1, 1) mul_pair.
Fact pair_mul1r : right_id (1, 1) mul_pair.
Fact pair_mulDl : left_distributive mul_pair +%R.
Fact pair_mulDr : right_distributive mul_pair +%R.
Fact pair_mul0r : left_zero 0 mul_pair.
Fact pair_mulr0 : right_zero 0 mul_pair.
Fact pair_one_neq0 : (1, 1) != 0 :> R1 × R2.
#[export]
HB.instance Definition _ := Nmodule_isSemiRing.Build (R1 × R2)%type
pair_mulA pair_mul1l pair_mul1r pair_mulDl pair_mulDr pair_mul0r pair_mulr0
pair_one_neq0.
Fact fst_is_multiplicative : multiplicative fst.
#[export]
HB.instance Definition _ := isMultiplicative.Build (R1 × R2)%type R1 fst
fst_is_multiplicative.
Fact snd_is_multiplicative : multiplicative snd.
#[export]
HB.instance Definition _ := isMultiplicative.Build (R1 × R2)%type R2 snd
snd_is_multiplicative.
End PairSemiRing.
Section PairComSemiRing.
Variables R1 R2 : comSemiRingType.
Fact pair_mulC : commutative (@mul_pair R1 R2).
#[export]
HB.instance Definition _ := SemiRing_hasCommutativeMul.Build (R1 × R2)%type
pair_mulC.
End PairComSemiRing.
#[export]
HB.instance Definition _ (R1 R2 : ringType) :=
SemiRing.copy (R1 × R1)%type (R1 × R1)%type.
#[export]
HB.instance Definition _ (R1 R2 : comRingType) :=
SemiRing.copy (R1 × R1)%type (R1 × R1)%type.
Section PairLmod.
Variables (R : ringType) (V1 V2 : lmodType R).
Definition scale_pair a (v : V1 × V2) : V1 × V2 := (a *: v.1, a *: v.2).
Fact pair_scaleA a b u : scale_pair a (scale_pair b u) = scale_pair (a × b) u.
Fact pair_scale1 u : scale_pair 1 u = u.
Fact pair_scaleDr : right_distributive scale_pair +%R.
Fact pair_scaleDl u : {morph scale_pair^~ u: a b / a + b}.
#[export]
HB.instance Definition _ := Zmodule_isLmodule.Build R (V1 × V2)%type
pair_scaleA pair_scale1 pair_scaleDr pair_scaleDl.
Fact fst_is_scalable : scalable fst.
#[export]
HB.instance Definition _ := isScalable.Build R (V1 × V2)%type V1 *:%R fst
fst_is_scalable.
Fact snd_is_scalable : scalable snd.
#[export]
HB.instance Definition _ := isScalable.Build R (V1 × V2)%type V2 *:%R snd
snd_is_scalable.
End PairLmod.
Section PairLalg.
Variables (R : ringType) (A1 A2 : lalgType R).
Fact pair_scaleAl a (u v : A1 × A2) : a *: (u × v) = (a *: u) × v.
#[export]
HB.instance Definition _ := Lmodule_isLalgebra.Build R (A1 × A2)%type
pair_scaleAl.
#[export]
HB.instance Definition _ := RMorphism.on (@fst A1 A2).
#[export]
HB.instance Definition _ := RMorphism.on (@snd A1 A2).
End PairLalg.
Section PairAlg.
TODO: MC-1 port (R has been changed from comRingType to ringType)
Variables (R : ringType) (A1 A2 : algType R).
Fact pair_scaleAr a (u v : A1 × A2) : a *: (u × v) = u × (a *: v).
#[export]
HB.instance Definition _ := Lalgebra_isAlgebra.Build R (A1 × A2)%type
pair_scaleAr.
End PairAlg.
Section PairUnitRing.
Variables R1 R2 : unitRingType.
Definition pair_unitr :=
[qualify a x : R1 × R2 | (x.1 \is a GRing.unit) && (x.2 \is a GRing.unit)].
Definition pair_invr x :=
if x \is a pair_unitr then (x.1^-1, x.2^-1) else x.
Lemma pair_mulVl : {in pair_unitr, left_inverse 1 pair_invr *%R}.
Lemma pair_mulVr : {in pair_unitr, right_inverse 1 pair_invr *%R}.
Lemma pair_unitP x y : y × x = 1 ∧ x × y = 1 → x \is a pair_unitr.
Lemma pair_invr_out : {in [predC pair_unitr], pair_invr =1 id}.
#[export]
HB.instance Definition _ := Ring_hasMulInverse.Build (R1 × R2)%type
pair_mulVl pair_mulVr pair_unitP pair_invr_out.
End PairUnitRing.
Fact pair_scaleAr a (u v : A1 × A2) : a *: (u × v) = u × (a *: v).
#[export]
HB.instance Definition _ := Lalgebra_isAlgebra.Build R (A1 × A2)%type
pair_scaleAr.
End PairAlg.
Section PairUnitRing.
Variables R1 R2 : unitRingType.
Definition pair_unitr :=
[qualify a x : R1 × R2 | (x.1 \is a GRing.unit) && (x.2 \is a GRing.unit)].
Definition pair_invr x :=
if x \is a pair_unitr then (x.1^-1, x.2^-1) else x.
Lemma pair_mulVl : {in pair_unitr, left_inverse 1 pair_invr *%R}.
Lemma pair_mulVr : {in pair_unitr, right_inverse 1 pair_invr *%R}.
Lemma pair_unitP x y : y × x = 1 ∧ x × y = 1 → x \is a pair_unitr.
Lemma pair_invr_out : {in [predC pair_unitr], pair_invr =1 id}.
#[export]
HB.instance Definition _ := Ring_hasMulInverse.Build (R1 × R2)%type
pair_mulVl pair_mulVr pair_unitP pair_invr_out.
End PairUnitRing.
TODO
HB FEATURE: (hard) complete graph using parameters,...
HB FEATURE: (easy) types/defs/anything can be a factory
HB.saturate (R1 R2 : comUnitRingType) (R1 * R2)%type
#[export]
HB.instance Definition _ (R1 R2 : comUnitRingType) :=
UnitRing.on (R1 × R2)%type.
#[export]
HB.instance Definition _ (R : comUnitRingType) (A1 A2 : unitAlgType R) :=
UnitRing.on (A1 × A2)%type.
Lemma pairMnE (M1 M2 : zmodType) (x : M1 × M2) n :
x *+ n = (x.1 *+ n, x.2 *+ n).
HB.instance Definition _ (R1 R2 : comUnitRingType) :=
UnitRing.on (R1 × R2)%type.
#[export]
HB.instance Definition _ (R : comUnitRingType) (A1 A2 : unitAlgType R) :=
UnitRing.on (A1 × A2)%type.
Lemma pairMnE (M1 M2 : zmodType) (x : M1 × M2) n :
x *+ n = (x.1 *+ n, x.2 *+ n).
Algebraic structure of bool
Fact mulVb (b : bool) : b != 0 → b × b = 1.
Fact invb_out (x y : bool) : y × x = 1 → x != 0.
Lemma bool_fieldP : Field.axiom bool.
Algebraic structure of nat