- -

Library mathcomp.algebra.ssralg

- -

-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- Distributed under the terms of CeCILL-B. *)
- -
-

- -

- The algebraic part of the Algebraic Hierarchy, as described in - ``Packaging mathematical structures'', TPHOLs09, by - Francois Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau - -

- - This file defines for each Structure (Zmodule, Ring, etc ...) its type, - its packers and its canonical properties : - -

- -

Zmodule (additive abelian groups):

- - zmodType == interface type for Zmodule structure. - ZmodMixin addA addC add0x addNx == builds the mixin for a Zmodule from the - algebraic properties of its operations. - ZmodType V m == packs the mixin m to build a Zmodule of type - zmodType. The carrier type V must have a - choiceType canonical structure. - [zmodType of V for S] == V-clone of the zmodType structure S: a copy of S - where the sort carrier has been replaced by V, - and which is therefore a zmodType structure on V. - The sort carrier for S must be convertible to V. - [zmodType of V] == clone of a canonical zmodType structure on V. - Similar to the above, except S is inferred, but - possibly with a syntactically different carrier. - 0 == the zero (additive identity) of a Zmodule. - x + y == the sum of x and y (in a Zmodule). -

x == the opposite (additive inverse) of x. - -

- x - y == the difference of x and y; this is only notation - for x + (- y). - 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. - x *- n == notation for - (x *+ n), the opposite of x *+ n. - \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]. - oppr_closed S <-> collective predicate S is closed under opposite. - addr_closed S <-> collective predicate S is closed under finite - sums (0 and x + y in S, for x, y in S). - zmod_closed S <-> collective predicate S is closed under zmodType - operations (0 and x - y in S, for x, y in S). - This property coerces to oppr_pred and addr_pred. - OpprPred oppS == packs oppS : oppr_closed S into an opprPred S - interface structure associating this property to - the canonical pred_key S, i.e. the k for which S - has a Canonical keyed_pred k structure (see file - ssrbool.v). - AddrPred addS == packs addS : addr_closed S into an addrPred S - interface structure associating this property to - the canonical pred_key S (see above). - ZmodPred oppS == packs oppS : oppr_closed S into an zmodPred S - interface structure associating the zmod_closed - property to the canonical pred_key S (see above), - which must already be an addrPred. - [zmodMixin of M by <: ] == zmodType mixin for a subType whose base type is - a zmodType and whose predicate's canonical - pred_key is a zmodPred. -> Coq can be made to behave as if all predicates had canonical zmodPred - keys by executing Import DefaultKeying GRing.DefaultPred. The required - oppr_closed and addr_closed assumptions will be either abstracted, - resolved or issued as separate proof obligations by the ssreflect - plugin abstraction and Prop-irrelevance functions. -
Ring (non-commutative rings):
- - ringType == interface type for a Ring structure. - RingMixin mulA mul1x mulx1 mulDx mulxD == builds the mixin for a Ring from - the algebraic properties of its multiplicative - operators; the carrier type must have a zmodType - structure. - RingType R m == packs the ring mixin m into a ringType. - 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). - [ringType of R for S] == R-clone of the ringType structure S. - [ringType of R] == clone of a canonical ringType structure on 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. - 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.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. - 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 p] has a 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). - smulr_closed S <-> collective predicate S is closed under products - and opposite (-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). - subring_closed S <-> collective predicate S is closed under ring - operations (1, x - y and x * y in S). - MulrPred mulS == packs mulS : mulr_closed S into a mulrPred S, - SmulrPred mulS smulrPred S, semiringPred S, or subringPred S - SemiringPred mulS interface structure, corresponding to the above - SubRingPred mulS properties, respectively, provided S already has - the supplementary zmodType closure properties. - The properties above coerce to subproperties so, - e.g., ringS : subring_closed S can be used for - the proof obligations of all prerequisites. - [ringMixin of R by <: ] == ringType mixin for a subType whose base type is - a ringType and whose predicate's canonical key - is a SubringPred. -> As for zmodType predicates, Import DefaultKeying GRing.DefaultPred - turns unresolved GRing.Pred unification constraints into proof - obligations for basic closure assumptions. - -

- -

ComRing (commutative Rings):

- - comRingType == interface type for commutative ring structure. - ComRingType R mulC == packs mulC into a comRingType; the carrier type - R must have a ringType canonical structure. - ComRingMixin mulA mulC mul1x mulDx == builds the mixin for a Ring (i.e., a - *non commutative* ring), using the commutativity - to reduce the number of proof obligations. - [comRingType of R for S] == R-clone of the comRingType structure S. - [comRingType of R] == clone of a canonical comRingType structure on R. - [comRingMixin of R by <: ] == comutativity mixin axiom for R when it is a - subType of a commutative ring. - -

- -

UnitRing (Rings whose units have computable inverses):

- - unitRingType == interface type for the UnitRing structure. - UnitRingMixin mulVr mulrV unitP inv0id == builds the mixin for a UnitRing - from the properties of the inverse operation and - the boolean test for being a unit (invertible). - The inverse of a non-unit x is constrained to be - x itself (property inv0id). The carrier type - must have a ringType canonical structure. - UnitRingType R m == packs the unit ring mixin m into a unitRingType. - WARNING: while it is possible to omit R for most of the - XxxType functions, R MUST be explicitly given - when UnitRingType is used with a mixin produced - by ComUnitRingMixin, in a Canonical definition, - otherwise the resulting structure will have the - WRONG sort key and will NOT BE USED during type - inference. - [unitRingType of R for S] == R-clone of the unitRingType structure S. - [unitRingType of R] == clones a canonical unitRingType structure on R. - 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). - DivrPred invS == packs invS : mulr_closed S into a divrPred S, - SdivrPred invS sdivrPred S or divringPred S interface structure, - DivringPred invS corresponding to the above properties, resp., - provided S already has the supplementary ringType - closure properties. The properties above coerce - to subproperties, as explained above. - [unitRingMixin of R by <: ] == unitRingType mixin for a subType whose base - type is a unitRingType and whose predicate's - canonical key is a divringPred and whose ring - structure is compatible with the base type's. - -

- -

ComUnitRing (commutative rings with computable inverses):

- - comUnitRingType == interface type for ComUnitRing structure. - ComUnitRingMixin mulVr unitP inv0id == builds the mixin for a UnitRing (a - *non commutative* unit ring, using commutativity - to simplify the proof obligations; the carrier - type must have a comRingType structure. - WARNING: ALWAYS give an explicit type argument - to UnitRingType along with a mixin produced by - ComUnitRingMixin (see above). - [comUnitRingType of R] == a comUnitRingType structure for R created by - merging canonical comRingType and unitRingType - structures on R. - -

- -

IntegralDomain (integral, commutative, ring with partial inverses):

- - idomainType == interface type for the IntegralDomain structure. - IdomainType R mulf_eq0 == packs the integrality property into an - idomainType integral domain structure; R must - have a comUnitRingType canonical structure. - [idomainType of R for S] == R-clone of the idomainType structure S. - [idomainType of R] == clone of a canonical idomainType structure on R. - [idomainMixin of R by <: ] == mixin axiom for a idomain subType. - -

- -

Field (commutative fields):

- - fieldType == interface type for fields. - GRing.Field.mixin_of R == the field property: x != 0 -> x \is a unit, for - x : R; R must be or coerce to a unitRingType. - GRing.Field.axiom inv == the 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. - FieldUnitMixin mulVf inv0 == a *non commutative unit ring* mixin, using an - inverse function that satisfies the field axiom - and fixes 0 (arguments mulVf and inv0, resp.), - and x != 0 as the Ring.unit predicate. The - carrier type must be a canonical comRingType. - FieldIdomainMixin m == an *idomain* mixin derived from a field mixin m. - GRing.Field.IdomainType mulVf inv0 == an idomainType incorporating the two - mixins above, where FieldIdomainMixin is applied - to the trivial field mixin for FieldUnitMixin. - FieldMixin mulVf inv0 == the (trivial) field mixin for Field.IdomainType. - FieldType R m == packs the field mixin M into a fieldType. The - carrier type R must be an idomainType. -> Given proofs mulVf and inv0 as above, a non-Canonical instances - of fieldType can be created with FieldType _ (FieldMixin mulVf inv0). - For Canonical instances one should always specify the first (sort) - argument of FieldType and other instance constructors, as well as pose - Definitions for unit ring, field, and idomain mixins (in that order). - [fieldType of F for S] == F-clone of the fieldType structure S. - [fieldType of F] == clone of a canonical fieldType structure on F. - [fieldMixin of R by <: ] == mixin axiom for a field subType. - -

- -

DecidableField (fields with a decidable first order theory):

- - decFieldType == interface type for DecidableField structure. - DecFieldMixin satP == builds the mixin for a DecidableField from the - correctness of its satisfiability predicate. The - carrier type must have a unitRingType structure. - DecFieldType F m == packs the decidable field mixin m into a - decFieldType; the carrier type F must have a - fieldType structure. - [decFieldType of F for S] == F-clone of the decFieldType structure S. - [decFieldType of F] == clone of a canonical decFieldType structure on F - 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. - QEdecFieldMixin wfP okP == a decidable field Mixin built from a quantifier - eliminator p and proofs wfP : GRing.wf_QE_proj p - and okP : GRing.valid_QE_proj p that p returns - well-formed and valid formulae, i.e., p i (u, v) - is a quantifier-free formula equivalent to - 'exists 'X_i, u1 == 0 /\ ... /\ u_m == 0 /\ v1 != 0 ... /\ v_n != 0 - -

- -
ClosedField (algebraically closed fields):
- - closedFieldType == interface type for the ClosedField structure. - ClosedFieldType F m == packs the closed field mixin m into a - closedFieldType. The carrier F must have a - decFieldType structure. - [closedFieldType of F on S] == F-clone of a closedFieldType structure S. - [closedFieldType of F] == clone of a canonicalclosedFieldType structure - on F. - -

- -
Lmodule (module with left multiplication by external scalars).
- - lmodType R == interface type for an Lmodule structure with - scalars of type R; R must have a ringType - structure. - LmodMixin scalA scal1v scalxD scalDv == builds an Lmodule mixin from the - algebraic properties of the scaling operation; - the module carrier type must have a zmodType - structure, and the scalar carrier must have a - ringType structure. - LmodType R V m == packs the mixin v to build an Lmodule of type - lmodType R. The carrier type V must have a - zmodType structure. - [lmodType R of V for S] == V-clone of an lmodType R structure S. - [lmodType R of V] == clone of a canonical lmodType R structure on V. - 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). - SubmodPred scaleS == packs scaleS : scaler_closed S in a submodPred S - interface structure corresponding to the above - property, provided S's key is a zmodPred; - submod_closed coerces to all the prerequisites. - [lmodMixin of V by <: ] == mixin for a subType of an lmodType, whose - predicate's key is a submodPred. - -

- -
Lalgebra (left algebra, ring with scaling that associates on the left):
- - lalgType R == interface type for Lalgebra structures with - scalars in R; R must have ringType structure. - LalgType R V scalAl == packs scalAl : k (x y) = (k x) y into an - Lalgebra of type lalgType R. The carrier type V - must have both lmodType R and ringType canonical - structures. - 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. - [lalgType R of V for S] == V-clone the lalgType R structure S. - [lalgType R of V] == clone of a canonical lalgType R structure on V. - subalg_closed S <-> collective predicate S is closed under lalgType - operations (1, a *: u + v and u * v in S). - SubalgPred scaleS == packs scaleS : scaler_closed S in a subalgPred S - interface structure corresponding to the above - property, provided S's key is a subringPred; - subalg_closed coerces to all the prerequisites. - [lalgMixin of V by <: ] == mixin axiom for a subType of an lalgType. - -

- -
Algebra (ring with scaling that associates both left and right):
- - algType R == type for Algebra structure with scalars in R. - R should be a commutative ring. - AlgType R A scalAr == packs scalAr : k (x y) = x (k y) into an Algebra - Structure of type algType R. The carrier type A - must have an lalgType R structure. - CommAlgType R A == creates an Algebra structure for an A that has - both lalgType R and comRingType structures. - [algType R of V for S] == V-clone of an algType R structure on S. - [algType R of V] == clone of a canonical algType R structure on V. - [algMixin of V by <: ] == mixin axiom for a subType of an algType. - -

- -
UnitAlgebra (algebra with computable inverses):
- - unitAlgType R == interface type for UnitAlgebra structure with - scalars in R; R should have a unitRingType - structure. - [unitAlgType R of V] == a unitAlgType R structure for V created by - merging canonical algType and unitRingType on V. - 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). - DivalgPred scaleS == packs scaleS : scaler_closed S in a divalgPred S - interface structure corresponding to the above - property, provided S's key is a divringPred; - divalg_closed coerces to all the prerequisites. - -

- - In addition to this structure hierarchy, we also develop a separate, - parallel hierarchy for morphisms linking these structures: - -

- -
Additive (additive functions):
- - 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 -). - -
-
- := {morph f : u v / u + v}. - {additive U -> V} == the interface type for a Structure (keyed on - a function f : U -> V) that encapsulates the - additive property; both U and V must have - zmodType canonical structures. - Additive add_f == packs add_f : additive f into an additive - function structure of type {additive U -> V}. - [additive of f as g] == an f-clone of the additive structure on the - function g -- f and g must be convertible. - [additive of f] == a clone of an existing additive structure on f. - -

- -
RMorphism (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 ringType structures. - rmorphism f <-> f is a ring morphism, i.e., f is both additive - and multiplicative. - {rmorphism R -> S} == the interface type for ring morphisms, i.e., - a Structure that encapsulates the rmorphism - property for functions f : R -> S; both R and S - must have ringType structures. - RMorphism morph_f == packs morph_f : rmorphism f into a Ring morphism - structure of type {rmorphism R -> S}. - AddRMorphism mul_f == packs mul_f : multiplicative f into an rmorphism - structure of type {rmorphism R -> S}; f must - already have an {additive R -> S} structure. - [rmorphism of f as g] == an f-clone of the rmorphism structure of g. - [rmorphism of f] == a clone of an existing additive structure on f. -
-
> 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 if a field isomorphism - between R and its image. - -
-
> As rmorphism coerces to both additive and multiplicative, all - structures for f can be built from a single proof of rmorphism f. - -
-
> 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. - -
-
> The property duplication also means that it is not strictly necessary - to declare all Additive instances. - -
-
- -

- -
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 in scalable_for paragraph - 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. - Linear lin_f == packs lin_f : lmorphism_for s f into a linear - function structure of type {linear U -> V | s}. - As linear_for s f coerces to lmorphism_for s f, - Linear can be used with lin_f : linear_for s f - (indeed, that is the recommended usage). Note - that as linear f, scalar f, {linear U -> V} and - {scalar U} are simply notation for corresponding - generic "for" forms, Linear can be used for any - of these special cases, transparently. - AddLinear scal_f == packs scal_f : scalable_for s f into a - {linear U -> V | s} structure; f must already - have an additive structure; as with Linear, - AddLinear can be used with lin_f : linear f, etc - [linear of f as g] == an f-clone of the linear structure of g. - [linear of f] == a clone of an existing linear structure on f. - (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. The - (a *^nu u)%Rlin 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. - LRmorphism lrmorph_f == packs lrmorph_f : lrmorphism_for s f into a - linear morphism structure of type - {lrmorphism A -> B | s}. Like Linear, LRmorphism - can be used transparently for lrmorphism f. - AddLRmorphism scal_f == packs scal_f : scalable_for s f into a linear - morphism structure of type - {lrmorphism A -> B | s}; f must already have an - {rmorphism A -> B} structure, and AddLRmorphism - can be applied to a linear_for s f, linear f, - scalar f, etc argument, like AddLinear. - [lrmorphism of f] == creates an lrmorphism structure from existing - rmorphism and linear structures on f; this is - the preferred way of creating lrmorphism - structures. -
-
> Linear and rmorphism properties do not need to be specialized for - as we supply inheritance join instances in both directions. - -
-
- Finally we supply some helper notation for morphisms: - x^f == the image of x under some morphism. This - notation is only reserved (not defined) here; - it is bound locally in sections where some - morphism is used heavily (e.g., the container - morphism in the parametricity sections of poly - and matrix, or the Frobenius section here). - \0 == the constant null function, which has a - canonical linear structure, and simplifies on - application (see ssrfun.v). - f \+ g == the additive composition of f and g, i.e., the - function x |-> f x + g x; f \+ g is canonically - linear when f and g are, and simplifies on - application (see ssrfun.v). - f \- g == the function x |-> f x - g x, canonically - linear when f and g are, and simplifies on - application. - k \*: f == the function x |-> k *: f x, which is - canonically linear when f is and simplifies on - application (this is a shorter alternative to - *:%R k \o f). - GRing.in_alg A == the ring morphism that injects R into A, where A - has an lalgType R structure; GRing.in_alg A k - simplifies to k%:A. - a \*o f == the function x |-> a * f x, canonically linear - linear when f is and its codomain is an algType - and which simplifies on application. - a \o* f == the function x |-> f x * a, canonically linear - linear when f is and its codomain is an lalgType - and which simplifies on application. - The Lemmas about these structures are contained in both the GRing module - and in the submodule GRing.Theory, which can be imported when unqualified - access to the theory is needed (GRing.Theory also allows the unqualified - use of additive, linear, Linear, etc). The main GRing module should NOT be - imported. - Notations are defined in scope ring_scope (delimiter %R), except term - and formula notations, which are in term_scope (delimiter %T). - This library also extends the conventional suffixes described in library - ssrbool.v with the following: - 0 -- ring 0, as in addr0 : x + 0 = x. - 1 -- ring 1, as in mulr1 : x * 1 = x. - D -- ring addition, as in linearD : f (u + v) = f u + f v. - B -- ring subtraction, as in opprB : - (x - y) = y - x. - M -- ring multiplication, as in invfM : (x * y)^-1 = x^-1 * y^-1. - Mn -- ring by nat multiplication, as in raddfMn : f (x *+ n) = f x *+ n. - N -- ring opposite, as in mulNr : (- x) * y = - (x * y). - V -- ring inverse, as in mulVr : x^-1 * x = 1. - X -- ring exponentiation, as in rmorphX : f (x ^+ n) = f x ^+ n. - Z -- (left) module scaling, as in linearZ : f (a *: v) = s *: f v. - The operator suffixes D, B, M and X are also used for the corresponding - operations on nat, as in natrX : (m ^ n)%:R = m%:R ^+ n. For the binary - power operator, a trailing "n" suffix is used to indicate the operator - suffix applies to the left-hand ring argument, as in - expr1n : 1 ^+ n = 1 vs. expr1 : x ^+ 1 = x. -

-
- -
-Set Implicit Arguments.
- -
-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 "a \*o f" (at level 40).
-Reserved Notation "a \o* f" (at level 40).
-Reserved Notation "a \*: f" (at level 40).
- -
-Delimit Scope ring_scope with R.
-Delimit Scope term_scope with T.
-Local Open Scope ring_scope.
- -
-Module Import GRing.
- -
-Import Monoid.Theory.
- -
-Module Zmodule.
- -
-Record mixin_of (V : Type) : Type := Mixin {
-  zero : V;
-  opp : V → V;
-  add : V → V → V;
-  _ : associative add;
-  _ : commutative add;
-  _ : left_id zero add;
-  _ : left_inverse zero opp add
-}.
- -
-Section ClassDef.
- -
-Record class_of T := Class { base : Choice.class_of T; mixin : mixin_of T }.
- -
-Structure type := Pack {sort; _ : class_of sort}.
-Variables (T : Type) (cT : type).
-Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
-Definition clone c of phant_id class c := @Pack T c.
-Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of xT).
- -
-Definition pack m :=
-  fun bT b & phant_id (Choice.class bT) b ⇒ Pack (@Class T b m).
- -
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
- -
-End ClassDef.
- -
-Module Exports.
-Coercion base : class_of >-> Choice.class_of.
-Coercion mixin : class_of >-> mixin_of.
-Coercion sort : type >-> Sortclass.
-Coercion eqType : type >-> Equality.type.
-Canonical eqType.
-Coercion choiceType : type >-> Choice.type.
-Canonical choiceType.
-Notation zmodType := type.
-Notation ZmodType T m := (@pack T m _ _ id).
-Notation ZmodMixin := Mixin.
-Notation "[ 'zmodType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
-  (at level 0, format "[ 'zmodType' 'of' T 'for' cT ]") : form_scope.
-Notation "[ 'zmodType' 'of' T ]" := (@clone T _ _ id)
-  (at level 0, format "[ 'zmodType' 'of' T ]") : form_scope.
-End Exports.
- -
-End Zmodule.
-Import Zmodule.Exports.
- -
-Definition zero V := Zmodule.zero (Zmodule.class V).
-Definition opp V := Zmodule.opp (Zmodule.class V).
-Definition add V := Zmodule.add (Zmodule.class V).
- -
- -
-Definition natmul V x n := nosimpl iterop _ n +%R x (zero V).
- -
- -
- -
- -
-Section ZmoduleTheory.
- -
-Variable V : zmodType.
-Implicit Types x y : V.
- -
-Lemma addrA : @associative V +%R.
-Lemma addrC : @commutative V V +%R.
-Lemma add0r : @left_id V V 0 +%R.
-Lemma addNr : @left_inverse V V V 0 -%R +%R.
- -
-Lemma addr0 : @right_id V V 0 +%R.
- Lemma addrN : @right_inverse V V V 0 -%R +%R.
- Definition subrr := addrN.
- -
-Canonical add_monoid := Monoid.Law addrA add0r addr0.
-Canonical add_comoid := Monoid.ComLaw addrC.
- -
-Lemma addrCA : @left_commutative V V +%R.
-Lemma addrAC : @right_commutative V V +%R.
-Lemma addrACA : @interchange V +%R +%R.
- -
-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 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 mulNrn x n : (- x ) *+ n = x *- n.
- -
-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 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 mulrnA x m n : x *+ (m × n ) = x *+ m *+ n.
- -
-Lemma mulrnAC x m n : x *+ m *+ n = x *+ n *+ m.
- -
-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 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 : V) :
-  \sum_(i in A ) x = x *+ #|A |.
- -
-Lemma telescope_sumr n m (f : nat → V) : n ≤ m →
-  \sum_(n ≤ k < m ) (f k .+1 - f k ) = f m - f n.
- -
-Section ClosedPredicates.
- -
-Variable S : {pred V }.
- -
-Definition addr_closed := 0 \in S ∧ {in S &, ∀ u v, u + v \in S }.
-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.
- -
-End ClosedPredicates.
- -
-End ZmoduleTheory.
- -
- -
-Module Ring.
- -
-Record mixin_of (R : zmodType) : Type := Mixin {
-  one : R;
-  mul : R → R → R;
-  _ : associative mul;
-  _ : left_id one mul;
-  _ : right_id one mul;
-  _ : left_distributive mul +%R;
-  _ : right_distributive mul +%R;
-  _ : one != 0
-}.
- -
-Definition EtaMixin R one mul mulA mul1x mulx1 mul_addl mul_addr nz1 :=
-  let _ := @Mixin R one mul mulA mul1x mulx1 mul_addl mul_addr nz1 in
-  @Mixin (Zmodule.Pack (Zmodule.class R)) _ _
-     mulA mul1x mulx1 mul_addl mul_addr nz1.
- -
-Section ClassDef.
- -
-Record class_of (R : Type) : Type := Class {
-  base : Zmodule.class_of R;
-  mixin : mixin_of (Zmodule.Pack base)
-}.
- -
-Structure type := Pack {sort; _ : class_of sort}.
-Variables (T : Type) (cT : type).
-Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
-Definition clone c of phant_id class c := @Pack T c.
-Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of xT).
- -
-Definition pack b0 (m0 : mixin_of (@Zmodule.Pack T b0)) :=
-  fun bT b & phant_id (Zmodule.class bT) b ⇒
-  fun m & phant_id m0 m ⇒ Pack (@Class T b m).
- -
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition zmodType := @Zmodule.Pack cT xclass.
- -
-End ClassDef.
- -
-Module Exports.
-Coercion base : class_of >-> Zmodule.class_of.
-Coercion mixin : class_of >-> mixin_of.
-Coercion sort : type >-> Sortclass.
-Coercion eqType : type >-> Equality.type.
-Canonical eqType.
-Coercion choiceType : type >-> Choice.type.
-Canonical choiceType.
-Coercion zmodType : type >-> Zmodule.type.
-Canonical zmodType.
-Notation ringType := type.
-Notation RingType T m := (@pack T _ m _ _ id _ id).
-Notation RingMixin := Mixin.
-Notation "[ 'ringType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
-  (at level 0, format "[ 'ringType' 'of' T 'for' cT ]") : form_scope.
-Notation "[ 'ringType' 'of' T ]" := (@clone T _ _ id)
-  (at level 0, format "[ 'ringType' 'of' T ]") : form_scope.
-End Exports.
- -
-End Ring.
-Import Ring.Exports.
- -
-Definition one (R : ringType) : R := Ring.one (Ring.class R).
-Definition mul (R : ringType) : R → R → R := Ring.mul (Ring.class R).
-Definition exp R x n := nosimpl iterop _ n (@mul R) x (one R).
-Notation sign R b := (exp (- one R) (nat_of_bool b)) (only parsing).
-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. -
-
-Definition char (R : Ring.type) of phant R : nat_pred :=
-  [pred p | prime p & p %:R == 0 :> R ].
- -
- -
-
- -
- Converse ring tag. -
-
-Definition converse R : Type := R.
- -
-Section RingTheory.
- -
-Variable R : ringType.
-Implicit Types x y : R.
- -
-Lemma mulrA : @associative R *%R.
-Lemma mul1r : @left_id R R 1 *%R.
-Lemma mulr1 : @right_id R R 1 *%R.
-Lemma mulrDl : @left_distributive R R *%R +%R.
- Lemma mulrDr : @right_distributive R R *%R +%R.
- Lemma oner_neq0 : 1 != 0 :> R.
-Lemma oner_eq0 : (1 == 0 :> R ) = false.
- -
-Lemma mul0r : @left_zero R R 0 *%R.
-Lemma mulr0 : @right_zero R R 0 *%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.
- -
-Canonical mul_monoid := Monoid.Law mulrA mul1r mulr1.
-Canonical muloid := Monoid.MulLaw mul0r mulr0.
-Canonical addoid := Monoid.AddLaw 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 mulrBl x y z : (y - z ) × x = y × x - z × x.
- -
-Lemma mulrBr x y z : x × (y - z ) = x × y - x × z.
- -
-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 natrB m n : n ≤ m → (m - n )%:R = m %:R - n %: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 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 commrN x y : comm x y → comm x (- y).
- -
-Lemma commrN1 x : comm x (-1).
- -
-Lemma commrD x y z : comm x y → comm x z → comm x (y + z).
- -
-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_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 commr_sign x n : comm x ((-1) ^+ 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 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 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 mulrI0_lreg x : (∀ y, x × y = 0 → y = 0) → lreg x.
- -
-Lemma lregN x : lreg x → lreg (- x).
- -
-Lemma lreg1 : lreg (1 : R).
- -
-Lemma lregM x y : lreg x → lreg y → lreg (x × y).
- -
-Lemma lregX x n : lreg x → lreg (x ^+ n).
- -
-Lemma lreg_sign n : lreg ((-1) ^+ n : R).
- -
-Lemma prodr_const (I : finType) (A : pred I) (x : R) :
-  \prod_(i in A ) x = x ^+ #|A |.
- -
-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 prodrN (I : finType) (A : pred I) (F : I → R) :
-  \prod_(i in A ) - F i = (- 1) ^+ #|A | × \prod_(i in A ) F i.
- -
-Lemma prodrMn 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 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 exprD1n x n : (x + 1) ^+ n = \sum_(i < n .+1 ) x ^+ i *+ 'C (n , i ).
- -
-Lemma subrX1 x n : x ^+ n - 1 = (x - 1) × (\sum_(i < n ) x ^+ i ).
- -
-Lemma sqrrD1 x : (x + 1) ^+ 2 = x ^+ 2 + x *+ 2 + 1.
- -
-Lemma sqrrB1 x : (x - 1) ^+ 2 = x ^+ 2 - x *+ 2 + 1.
- -
-Lemma subr_sqr_1 x : x ^+ 2 - 1 = (x - 1) × (x + 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.
- -
-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 addrr_char2 x : x + x = 0.
- -
-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.
- -
-Canonical converse_eqType := [eqType of R ^c ].
-Canonical converse_choiceType := [choiceType of R ^c ].
-Canonical converse_zmodType := [zmodType of R ^c ].
- -
-Definition converse_ringMixin :=
-  let mul' x y := y × x in
-  let mulrA' x y z := esym (mulrA z y x) in
-  let mulrDl' x y z := mulrDr z x y in
-  let mulrDr' x y z := mulrDl y z x in
-  @Ring.Mixin converse_zmodType
-    1 mul' mulrA' mulr1 mul1r mulrDl' mulrDr' oner_neq0.
-Canonical converse_ringType := RingType R ^c converse_ringMixin.
- -
-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 smulr_closed := -1 \in S ∧ mulr_2closed.
-Definition semiring_closed := addr_closed S ∧ mulr_closed.
-Definition subring_closed := [/\ 1 \in S , subr_2closed S & mulr_2closed ].
- -
-Lemma smulr_closedM : smulr_closed → mulr_closed.
- -
-Lemma smulr_closedN : smulr_closed → oppr_closed S.
- -
-Lemma semiring_closedD : semiring_closed → addr_closed S.
- -
-Lemma semiring_closedM : semiring_closed → mulr_closed.
- -
-Lemma subring_closedB : subring_closed → zmod_closed S.
- -
-Lemma subring_closedM : subring_closed → smulr_closed.
- -
-Lemma subring_closed_semi : subring_closed → semiring_closed.
- -
-End ClosedPredicates.
- -
-End RingTheory.
- -
-Section RightRegular.
- -
-Variable R : ringType.
-Implicit Types x y : R.
-Let Rc := converse_ringType R.
- -
-Lemma mulIr_eq0 x y : rreg x → (y × x == 0) = (y == 0).
- -
-Lemma mulIr0_rreg x : (∀ y, y × x = 0 → y = 0) → rreg x.
- -
-Lemma rreg_neq0 x : rreg x → x != 0.
- -
-Lemma rregN x : rreg x → rreg (- x).
- -
-Lemma rreg1 : rreg (1 : R).
- -
-Lemma rregM x y : rreg x → rreg y → rreg (x × y).
- -
-Lemma revrX x n : (x : Rc ) ^+ n = (x : R ) ^+ n.
- -
-Lemma rregX x n : rreg x → rreg (x ^+ n).
- -
-End RightRegular.
- -
-Module Lmodule.
- -
-Structure mixin_of (R : ringType) (V : zmodType) : Type := Mixin {
-  scale : R → V → V;
-  _ : ∀ a b v, scale a (scale b v) = scale (a × b) v;
-  _ : left_id 1 scale;
-  _ : right_distributive scale +%R;
-  _ : ∀ v, {morph scale ^~ v : a b / a + b }
-}.
- -
-Section ClassDef.
- -
-Variable R : ringType.
- -
-Structure class_of V := Class {
-  base : Zmodule.class_of V;
-  mixin : mixin_of R (Zmodule.Pack base)
-}.
- -
-Structure type (phR : phant R) := Pack {sort; _ : class_of sort}.
-Variable (phR : phant R) (T : Type) (cT : type phR).
-Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
-Definition clone c of phant_id class c := @Pack phR T c.
-Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of xT).
- -
-Definition pack b0 (m0 : mixin_of R (@Zmodule.Pack T b0)) :=
-  fun bT b & phant_id (Zmodule.class bT) b ⇒
-  fun m & phant_id m0 m ⇒ Pack phR (@Class T b m).
- -
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition zmodType := @Zmodule.Pack cT xclass.
- -
-End ClassDef.
- -
-Module Import Exports.
-Coercion base : class_of >-> Zmodule.class_of.
-Coercion mixin : class_of >-> mixin_of.
-Coercion sort : type >-> Sortclass.
-Coercion eqType : type >-> Equality.type.
-Canonical eqType.
-Coercion choiceType : type >-> Choice.type.
-Canonical choiceType.
-Coercion zmodType : type >-> Zmodule.type.
-Canonical zmodType.
-Notation lmodType R := (type (Phant R)).
-Notation LmodType R T m := (@pack _ (Phant R) T _ m _ _ id _ id).
-Notation LmodMixin := Mixin.
-Notation "[ 'lmodType' R 'of' T 'for' cT ]" := (@clone _ (Phant R) T cT _ idfun)
-  (at level 0, format "[ 'lmodType' R 'of' T 'for' cT ]") : form_scope.
-Notation "[ 'lmodType' R 'of' T ]" := (@clone _ (Phant R) T _ _ id)
-  (at level 0, format "[ 'lmodType' R 'of' T ]") : form_scope.
-End Exports.
- -
-End Lmodule.
-Import Lmodule.Exports.
- -
-Definition scale (R : ringType) (V : lmodType R) :=
-  Lmodule.scale (Lmodule.class V).
- -
- -
-Section LmoduleTheory.
- -
-Variables (R : ringType) (V : lmodType R).
-Implicit Types (a b c : R) (u v : V).
- -
- -
-Lemma scalerA a b v : a *: (b *: v ) = a × b *: v.
- -
-Lemma scale1r : @left_id R V 1 *:%R.
- -
-Lemma scalerDr a : {morph *:%R a : u v / u + v }.
- -
-Lemma scalerDl v : {morph *:%R ^~ v : a b / a + b }.
- -
-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.
- -
-Module Lalgebra.
- -
-Definition axiom (R : ringType) (V : lmodType R) (mul : V → V → V) :=
-  ∀ a u v, a *: mul u v = mul (a *: u) v.
- -
-Section ClassDef.
- -
-Variable R : ringType.
- -
-Record class_of (T : Type) : Type := Class {
-  base : Ring.class_of T;
-  mixin : Lmodule.mixin_of R (Zmodule.Pack base);
-  ext : @axiom R (Lmodule.Pack _ (Lmodule.Class mixin)) (Ring.mul base)
-}.
-Definition base2 R m := Lmodule.Class (@mixin R m).
- -
-Structure type (phR : phant R) := Pack {sort; _ : class_of sort}.
-Variable (phR : phant R) (T : Type) (cT : type phR).
-Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
-Definition clone c of phant_id class c := @Pack phR T c.
-Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of xT).
- -
-Definition pack T b0 mul0 (axT : @axiom R (@Lmodule.Pack R _ T b0) mul0) :=
-  fun bT b & phant_id (Ring.class bT) (b : Ring.class_of T) ⇒
-  fun mT m & phant_id (@Lmodule.class R phR mT) (@Lmodule.Class R T b m) ⇒
-  fun ax & phant_id axT ax ⇒
-  Pack (Phant R) (@Class T b m ax).
- -
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition zmodType := @Zmodule.Pack cT xclass.
-Definition ringType := @Ring.Pack cT xclass.
-Definition lmodType := @Lmodule.Pack R phR cT xclass.
-Definition lmod_ringType := @Lmodule.Pack R phR ringType xclass.
- -
-End ClassDef.
- -
-Module Exports.
-Coercion base : class_of >-> Ring.class_of.
-Coercion base2 : class_of >-> Lmodule.class_of.
-Coercion sort : type >-> Sortclass.
-Coercion eqType : type >-> Equality.type.
-Canonical eqType.
-Coercion choiceType : type >-> Choice.type.
-Canonical choiceType.
-Coercion zmodType : type >-> Zmodule.type.
-Canonical zmodType.
-Coercion ringType : type >-> Ring.type.
-Canonical ringType.
-Coercion lmodType : type >-> Lmodule.type.
-Canonical lmodType.
-Canonical lmod_ringType.
-Notation lalgType R := (type (Phant R)).
-Notation LalgType R T a := (@pack _ (Phant R) T _ _ a _ _ id _ _ id _ id).
-Notation "[ 'lalgType' R 'of' T 'for' cT ]" := (@clone _ (Phant R) T cT _ idfun)
-  (at level 0, format "[ 'lalgType' R 'of' T 'for' cT ]")
-  : form_scope.
-Notation "[ 'lalgType' R 'of' T ]" := (@clone _ (Phant R) T _ _ id)
-  (at level 0, format "[ 'lalgType' R 'of' T ]") : form_scope.
-End Exports.
- -
-End Lalgebra.
-Import Lalgebra.Exports.
- -
-
- -
- Scalar injection (see the definition of in_alg A below). -
-
- -
-
- -
- Regular ring algebra tag. -
-
-Definition regular R : Type := R.
- -
-Section LalgebraTheory.
- -
-Variables (R : ringType) (A : lalgType R).
-Implicit Types x y : A.
- -
-Lemma scalerAl k (x y : A) : k *: (x × y ) = k *: x × y.
- -
-Lemma mulr_algl a x : a %:A × x = a *: x.
- -
-Canonical regular_eqType := [eqType of R ^o ].
-Canonical regular_choiceType := [choiceType of R ^o ].
-Canonical regular_zmodType := [zmodType of R ^o ].
-Canonical regular_ringType := [ringType of R ^o ].
- -
-Definition regular_lmodMixin :=
-  let mkMixin := @Lmodule.Mixin R regular_zmodType (@mul R) in
-  mkMixin (@mulrA R) (@mul1r R) (@mulrDr R) (fun v a b ⇒ mulrDl a b v).
- -
-Canonical regular_lmodType := LmodType R R ^o regular_lmodMixin.
-Canonical regular_lalgType := LalgType R R ^o (@mulrA regular_ringType).
- -
-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. -
-
- -
-Module Additive.
- -
-Section ClassDef.
- -
-Variables U V : zmodType.
- -
-Definition axiom (f : U → V) := {morph f : x y / x - y }.
- -
-Structure map (phUV : phant (U → V)) := Pack {apply; _ : axiom apply}.
- -
-Variables (phUV : phant (U → V)) (f g : U → V) (cF : map phUV).
-Definition class := let: Pack _ c as cF' := cF return axiom cF' in c.
-Definition clone fA of phant_id g (apply cF) & phant_id fA class :=
-  @Pack phUV f fA.
- -
-End ClassDef.
- -
-Module Exports.
-Notation additive f := (axiom f).
-Coercion apply : map >-> Funclass.
-Notation Additive fA := (Pack (Phant _) fA).
-Notation "{ 'additive' fUV }" := (map (Phant fUV))
-  (at level 0, format "{ 'additive' fUV }") : ring_scope.
-Notation "[ 'additive' 'of' f 'as' g ]" := (@clone _ _ _ f g _ _ idfun id)
-  (at level 0, format "[ 'additive' 'of' f 'as' g ]") : form_scope.
-Notation "[ 'additive' 'of' f ]" := (@clone _ _ _ f f _ _ id id)
-  (at level 0, format "[ 'additive' 'of' f ]") : form_scope.
-End Exports.
- -
-End Additive.
-Include Additive.Exports. (* Allows GRing.additive to resolve conflicts. *)
- -
-
- -
- Lifted additive operations. -
-
-Section LiftedZmod.
-Variables (U : Type) (V : zmodType).
-Definition null_fun_head (phV : phant V) of U : V := let: Phant := phV in 0.
-Definition add_fun_head t (f g : U → V) x := let: tt := t in f x + g x.
-Definition sub_fun_head t (f g : U → V) x := let: tt := t in f x - g x.
-End LiftedZmod.
- -
-
- -
- Lifted multiplication. -
-
-Section LiftedRing.
-Variables (R : ringType) (T : Type).
-Implicit Type f : T → R.
-Definition mull_fun_head t a f x := let: tt := t in a × f x.
-Definition mulr_fun_head t a f x := let: tt := t in f x × a.
-End LiftedRing.
- -
-
- -
- Lifted linear operations. -
-
-Section LiftedScale.
-Variables (R : ringType) (U : Type) (V : lmodType R) (A : lalgType R).
-Definition scale_fun_head t a (f : U → V) x := let: tt := t in a *: f x.
-Definition in_alg_head (phA : phant A) k : A := let: Phant := phA in k %:A.
-End LiftedScale.
- -
-Notation null_fun V := (null_fun_head (Phant V)) (only parsing).
-
- -
- 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. -
-
- -
- -
-Section AdditiveTheory.
- -
-Section Properties.
- -
-Variables (U V : zmodType) (k : unit) (f : {additive U → V }).
- -
-Lemma raddfB : {morph f : x y / x - y }.
- -
-Lemma raddf0 : f 0 = 0.
- -
-Lemma raddf_eq0 x : injective f → (f x == 0) = (x == 0).
- -
-Lemma raddfN : {morph f : x / - x }.
- -
-Lemma raddfD : {morph f : x y / x + y }.
- -
-Lemma raddfMn n : {morph f : x / x *+ n }.
- -
-Lemma raddfMNn 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_additive f' : cancel f f' → cancel f' f → additive f'.
- -
-Lemma bij_additive :
-  bijective f → exists2 f' : {additive V → U }, cancel f f' & cancel f' f.
- -
-Fact locked_is_additive : additive (locked_with k (f : U → V)).
- Canonical locked_additive := Additive locked_is_additive.
- -
-End Properties.
- -
-Section RingProperties.
- -
-Variables (R S : ringType) (f : {additive R → S }).
- -
-Lemma raddfMnat n x : f (n %:R × x) = n %:R × f x.
- -
-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 idfun_is_additive : additive (@idfun U).
- Canonical idfun_additive := Additive idfun_is_additive.
- -
-Fact comp_is_additive : additive (f \o h).
- Canonical comp_additive := Additive comp_is_additive.
- -
-Fact opp_is_additive : additive (-%R : U → U).
- Canonical opp_additive := Additive opp_is_additive.
- -
-Fact null_fun_is_additive : additive (\0 : U → V).
- Canonical null_fun_additive := Additive null_fun_is_additive.
- -
-Fact add_fun_is_additive : additive (f \+ g).
-Canonical add_fun_additive := Additive add_fun_is_additive.
- -
-Fact sub_fun_is_additive : additive (f \- g).
-Canonical sub_fun_additive := Additive sub_fun_is_additive.
- -
-End AddFun.
- -
-Section MulFun.
- -
-Variables (R : ringType) (U : zmodType).
-Variables (a : R) (f : {additive U → R }).
- -
-Fact mull_fun_is_additive : additive (a \*o f).
- Canonical mull_fun_additive := Additive mull_fun_is_additive.
- -
-Fact mulr_fun_is_additive : additive (a \o × f).
- Canonical mulr_fun_additive := Additive mulr_fun_is_additive.
- -
-End MulFun.
- -
-Section ScaleFun.
- -
-Variables (R : ringType) (U : zmodType) (V : lmodType R).
-Variables (a : R) (f : {additive U → V }).
- -
-Canonical scale_additive := Additive (@scalerBr R V a).
-Canonical scale_fun_additive := [additive of a \*: f as f \; *:%R a ].
- -
-End ScaleFun.
- -
-End AdditiveTheory.
- -
-Module RMorphism.
- -
-Section ClassDef.
- -
-Variables R S : ringType.
- -
-Definition mixin_of (f : R → S) :=
-  {morph f : x y / x × y }%R × (f 1 = 1) : Prop.
- -
-Record class_of f : Prop := Class {base : additive f; mixin : mixin_of f}.
- -
-Structure map (phRS : phant (R → S)) := Pack {apply; _ : class_of apply}.
-Variables (phRS : phant (R → S)) (f g : R → S) (cF : map phRS).
- -
-Definition class := let: Pack _ c as cF' := cF return class_of cF' in c.
- -
-Definition clone fM of phant_id g (apply cF) & phant_id fM class :=
-  @Pack phRS f fM.
- -
-Definition pack (fM : mixin_of f) :=
-  fun (bF : Additive.map phRS) fA & phant_id (Additive.class bF) fA ⇒
-  Pack phRS (Class fA fM).
- -
-Canonical additive := Additive.Pack phRS class.
- -
-End ClassDef.
- -
-Module Exports.
-Notation multiplicative f := (mixin_of f).
-Notation rmorphism f := (class_of f).
-Coercion base : rmorphism >-> Additive.axiom.
-Coercion mixin : rmorphism >-> multiplicative.
-Coercion apply : map >-> Funclass.
-Notation RMorphism fM := (Pack (Phant _) fM).
-Notation AddRMorphism fM := (pack fM id).
-Notation "{ 'rmorphism' fRS }" := (map (Phant fRS))
-  (at level 0, format "{ 'rmorphism' fRS }") : ring_scope.
-Notation "[ 'rmorphism' 'of' f 'as' g ]" := (@clone _ _ _ f g _ _ idfun id)
-  (at level 0, format "[ 'rmorphism' 'of' f 'as' g ]") : form_scope.
-Notation "[ 'rmorphism' 'of' f ]" := (@clone _ _ _ f f _ _ id id)
-  (at level 0, format "[ 'rmorphism' 'of' f ]") : form_scope.
-Coercion additive : map >-> Additive.map.
-Canonical additive.
-End Exports.
- -
-End RMorphism.
-Include RMorphism.Exports.
- -
-Section RmorphismTheory.
- -
-Section Properties.
- -
-Variables (R S : ringType) (k : unit) (f : {rmorphism R → S }).
- -
-Lemma rmorph0 : f 0 = 0.
-Lemma rmorphN : {morph f : x / - x }.
-Lemma rmorphD : {morph f : x y / x + y }.
-Lemma rmorphB : {morph f : x y / x - y }.
-Lemma rmorphMn n : {morph f : x / x *+ n }.
-Lemma rmorphMNn 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 rmorphMsign n : {morph f : x / (- 1) ^+ n × x }.
- -
-Lemma rmorphismP : rmorphism f.
-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 rmorphX n : {morph f : x / x ^+ n }.
- -
-Lemma rmorph_nat n : f n %:R = n %:R.
-Lemma rmorphN1 : f (- 1) = (- 1).
- -
-Lemma rmorph_sign n : f ((- 1) ^+ n) = (- 1) ^+ n.
- -
-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 → rmorphism f'.
- -
-Lemma bij_rmorphism :
-  bijective f → exists2 f' : {rmorphism S → R }, cancel f f' & cancel f' f.
- -
-Fact locked_is_multiplicative : multiplicative (locked_with k (f : R → S)).
- Canonical locked_rmorphism := AddRMorphism locked_is_multiplicative.
- -
-End Properties.
- -
-Section Projections.
- -
-Variables (R S T : ringType) (f : {rmorphism S → T }) (g : {rmorphism R → S }).
- -
-Fact idfun_is_multiplicative : multiplicative (@idfun R).
- Canonical idfun_rmorphism := AddRMorphism idfun_is_multiplicative.
- -
-Fact comp_is_multiplicative : multiplicative (f \o g).
- Canonical comp_rmorphism := AddRMorphism comp_is_multiplicative.
- -
-End Projections.
- -
-Section InAlgebra.
- -
-Variables (R : ringType) (A : lalgType R).
- -
-Fact in_alg_is_rmorphism : rmorphism (in_alg_loc A).
-Canonical in_alg_additive := Additive in_alg_is_rmorphism.
-Canonical in_alg_rmorphism := RMorphism in_alg_is_rmorphism.
- -
-Lemma in_algE a : in_alg_loc A a = a %:A.
- -
-End InAlgebra.
- -
-End RmorphismTheory.
- -
-Module Scale.
- -
-Section ScaleLaw.
- -
-Structure law (R : ringType) (V : zmodType) (s : R → V → V) := Law {
-  op : R → V → V;
-  _ : op = s;
-  _ : op (-1) =1 -%R;
-  _ : ∀ a, additive (op a)
-}.
- -
-Definition mul_law R := Law (erefl *%R) (@mulN1r R) (@mulrBr R).
-Definition scale_law R U := Law (erefl *:%R) (@scaleN1r R U) (@scalerBr R U).
- -
-Variables (R : ringType) (V : zmodType) (s : R → V → V) (s_law : law s).
- -
-Lemma opE : s_op = s.
-Lemma N1op : s_op (-1) =1 -%R.
-Fact opB a : additive (s_op a).
-Definition op_additive a := Additive (opB a).
- -
-Variables (aR : ringType) (nu : {rmorphism aR → R }).
-Fact comp_opE : nu \; s_op = nu \; s.
-Fact compN1op : (nu \; s_op) (-1) =1 -%R.
- Definition comp_law : law (nu \; s) := Law comp_opE compN1op (fun a ⇒ opB _).
- -
-End ScaleLaw.
- -
-End Scale.
- -
-Module Linear.
- -
-Section ClassDef.
- -
-Variables (R : ringType) (U : lmodType R) (V : zmodType) (s : R → V → V).
-Implicit Type phUV : phant (U → V).
- -
-Definition axiom (f : U → V) (s_law : Scale.law s) of s = s_law :=
-  ∀ a, {morph f : u v / a *: u + v >-> s a u + v }.
-Definition mixin_of (f : U → V) :=
-  ∀ a, {morph f : v / a *: v >-> s a v }.
- -
-Record class_of f : Prop := Class {base : additive f; mixin : mixin_of f}.
- -
-Lemma class_of_axiom f s_law Ds : @axiom f s_law Ds → class_of f.
- -
-Structure map (phUV : phant (U → V)) := Pack {apply; _ : class_of apply}.
- -
-Variables (phUV : phant (U → V)) (f g : U → V) (cF : map phUV).
-Definition class := let: Pack _ c as cF' := cF return class_of cF' in c.
-Definition clone fL of phant_id g (apply cF) & phant_id fL class :=
-  @Pack phUV f fL.
- -
-Definition pack (fZ : mixin_of f) :=
-  fun (bF : Additive.map phUV) fA & phant_id (Additive.class bF) fA ⇒
-  Pack phUV (Class fA fZ).
- -
-Canonical additive := Additive.Pack phUV class.
- -
-
- -
- Support for right-to-left rewriting with the generic linearZ rule. -
-
-Notation mapUV := (map (Phant (U → V))).
-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 ClassDef.
- -
-Module Exports.
-Canonical Scale.mul_law.
-Canonical Scale.scale_law.
-Canonical Scale.comp_law.
-Canonical Scale.op_additive.
-Delimit Scope linear_ring_scope with linR.
-Notation "a *: u" := (@Scale.op _ _ *:%R _ a u) : linear_ring_scope.
-Notation "a * u" := (@Scale.op _ _ *%R _ a u) : linear_ring_scope.
-Notation "a *:^ nu u" := (@Scale.op _ _ (nu \; *:%R) _ a u)
-  (at level 40, nu at level 1, format "a *:^ nu u") : linear_ring_scope.
-Notation "a *^ nu u" := (@Scale.op _ _ (nu \; *%R) _ a u)
-  (at level 40, nu at level 1, format "a *^ nu u") : linear_ring_scope.
-Notation scalable_for s f := (mixin_of s f).
-Notation scalable f := (scalable_for *:%R f).
-Notation linear_for s f := (axiom f (erefl s)).
-Notation linear f := (linear_for *:%R f).
-Notation scalar f := (linear_for *%R f).
-Notation lmorphism_for s f := (class_of s f).
-Notation lmorphism f := (lmorphism_for *:%R f).
-Coercion class_of_axiom : axiom >-> lmorphism_for.
-Coercion base : lmorphism_for >-> Additive.axiom.
-Coercion mixin : lmorphism_for >-> scalable.
-Coercion apply : map >-> Funclass.
-Notation Linear fL := (Pack (Phant _) fL).
-Notation AddLinear fZ := (pack fZ id).
-Notation "{ 'linear' fUV | s }" := (map s (Phant fUV))
-  (at level 0, format "{ 'linear' fUV | s }") : ring_scope.
-Notation "{ 'linear' fUV }" := {linear fUV | *:%R }
-  (at level 0, format "{ 'linear' fUV }") : ring_scope.
-Notation "{ 'scalar' U }" := {linear U → _ | *%R }
-  (at level 0, format "{ 'scalar' U }") : ring_scope.
-Notation "[ 'linear' 'of' f 'as' g ]" := (@clone _ _ _ _ _ f g _ _ idfun id)
-  (at level 0, format "[ 'linear' 'of' f 'as' g ]") : form_scope.
-Notation "[ 'linear' 'of' f ]" := (@clone _ _ _ _ _ f f _ _ id id)
-  (at level 0, format "[ 'linear' 'of' f ]") : form_scope.
-Coercion additive : map >-> Additive.map.
-Canonical additive.
-
- -
- Support for right-to-left rewriting with the generic linearZ rule. -
-
-Coercion map_for_map : map_for >-> map.
-Coercion unify_map_at : map_at >-> map_for.
-Canonical unify_map_at.
-Coercion unwrap : wrapped >-> map.
-Coercion wrap : map_class >-> wrapped.
-Canonical wrap.
-End Exports.
- -
-End Linear.
-Include Linear.Exports.
- -
-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 }.
- -
-Fact locked_is_scalable : scalable_for s (locked_with k (f : U → V)).
- Canonical locked_linear := AddLinear locked_is_scalable.
- -
-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 : S → V → V) (h_law : Scale.law h).
- -
-Lemma linearZ c a (h_c := Scale.op h_law 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_linear f' : cancel f f' → cancel f' f → linear f'.
- -
-Lemma bij_linear :
-  bijective f → exists2 f' : {linear V → U }, cancel f f' & cancel f' 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) (s : R → V → V).
-Variables (f : {linear U → V | s }) (h : {linear W → U }).
- -
-Lemma idfun_is_scalable : scalable (@idfun U).
-Canonical idfun_linear := AddLinear idfun_is_scalable.
- -
-Lemma opp_is_scalable : scalable (-%R : U → U).
- Canonical opp_linear := AddLinear opp_is_scalable.
- -
-Lemma comp_is_scalable : scalable_for s (f \o h).
- Canonical comp_linear := AddLinear comp_is_scalable.
- -
-Variables (s_law : Scale.law s) (g : {linear U → V | Scale.op s_law }).
-Let Ds : s =1 Scale.op s_law.
- -
-Lemma null_fun_is_scalable : scalable_for (Scale.op s_law) (\0 : U → V).
- Canonical null_fun_linear := AddLinear null_fun_is_scalable.
- -
-Lemma add_fun_is_scalable : scalable_for s (f \+ g).
- Canonical add_fun_linear := AddLinear add_fun_is_scalable.
- -
-Lemma sub_fun_is_scalable : scalable_for s (f \- g).
- Canonical sub_fun_linear := AddLinear sub_fun_is_scalable.
- -
-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).
- Canonical mulr_fun_linear := AddLinear mulr_fun_is_scalable.
- -
-End LinearLalg.
- -
-End LinearTheory.
- -
-Module LRMorphism.
- -
-Section ClassDef.
- -
-Variables (R : ringType) (A : lalgType R) (B : ringType) (s : R → B → B).
- -
-Record class_of (f : A → B) : Prop :=
-  Class {base : rmorphism f; mixin : scalable_for s f}.
-Definition base2 f (fLM : class_of f) := Linear.Class fLM (mixin fLM).
- -
-Structure map (phAB : phant (A → B)) := Pack {apply; _ : class_of apply}.
- -
-Variables (phAB : phant (A → B)) (f : A → B) (cF : map phAB).
-Definition class := let: Pack _ c as cF' := cF return class_of cF' in c.
- -
-Definition clone :=
-  fun (g : RMorphism.map phAB) fM & phant_id (RMorphism.class g) fM ⇒
-  fun (h : Linear.map s phAB) fZ &
-     phant_id (Linear.mixin (Linear.class h)) fZ ⇒
-  Pack phAB (@Class f fM fZ).
- -
-Definition pack (fZ : scalable_for s f) :=
-  fun (g : RMorphism.map phAB) fM & phant_id (RMorphism.class g) fM ⇒
-  Pack phAB (Class fM fZ).
- -
-Canonical additive := Additive.Pack phAB class.
-Canonical rmorphism := RMorphism.Pack phAB class.
-Canonical linear := Linear.Pack phAB class.
-Canonical join_rmorphism := @RMorphism.Pack _ _ phAB linear class.
-Canonical join_linear := @Linear.Pack R A B s phAB rmorphism class.
- -
-End ClassDef.
- -
-Module Exports.
-Notation lrmorphism_for s f := (class_of s f).
-Notation lrmorphism f := (lrmorphism_for *:%R f).
-Coercion base : lrmorphism_for >-> RMorphism.class_of.
-Coercion base2 : lrmorphism_for >-> lmorphism_for.
-Coercion apply : map >-> Funclass.
-Notation LRMorphism f_lrM := (Pack (Phant _) (Class f_lrM f_lrM)).
-Notation AddLRMorphism fZ := (pack fZ id).
-Notation "{ 'lrmorphism' fAB | s }" := (map s (Phant fAB))
-  (at level 0, format "{ 'lrmorphism' fAB | s }") : ring_scope.
-Notation "{ 'lrmorphism' fAB }" := {lrmorphism fAB | *:%R }
-  (at level 0, format "{ 'lrmorphism' fAB }") : ring_scope.
-Notation "[ 'lrmorphism' 'of' f ]" := (@clone _ _ _ _ _ f _ _ id _ _ id)
-  (at level 0, format "[ 'lrmorphism' 'of' f ]") : form_scope.
-Coercion additive : map >-> Additive.map.
-Canonical additive.
-Coercion rmorphism : map >-> RMorphism.map.
-Canonical rmorphism.
-Coercion linear : map >-> Linear.map.
-Canonical linear.
-Canonical join_rmorphism.
-Canonical join_linear.
-End Exports.
- -
-End LRMorphism.
-Include LRMorphism.Exports.
- -
-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 }).
- -
-Definition idfun_lrmorphism := [lrmorphism of @idfun A ].
-Definition comp_lrmorphism := [lrmorphism of g \o f ].
-Definition locked_lrmorphism := [lrmorphism of locked_with k (f : A → B)].
- -
-Lemma rmorph_alg a : f a %:A = a %:A.
- -
-Lemma lrmorphismP : lrmorphism f.
- -
-Lemma can2_lrmorphism f' : cancel f f' → cancel f' f → lrmorphism f'.
- -
-Lemma bij_lrmorphism :
-  bijective f → exists2 f' : {lrmorphism B → A }, cancel f f' & cancel f' f.
- -
-End LRMorphismTheory.
- -
-Module ComRing.
- -
-Definition RingMixin R one mul mulA mulC mul1x mul_addl :=
-  let mulx1 := Monoid.mulC_id mulC mul1x in
-  let mul_addr := Monoid.mulC_dist mulC mul_addl in
-  @Ring.EtaMixin R one mul mulA mul1x mulx1 mul_addl mul_addr.
- -
-Section ClassDef.
- -
-Record class_of R :=
-  Class {base : Ring.class_of R; mixin : commutative (Ring.mul base)}.
- -
-Structure type := Pack {sort; _ : class_of sort}.
-Variable (T : Type) (cT : type).
-Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
-Definition clone c of phant_id class c := @Pack T c.
-Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of xT).
- -
-Definition pack mul0 (m0 : @commutative T T mul0) :=
-  fun bT b & phant_id (Ring.class bT) b ⇒
-  fun m & phant_id m0 m ⇒ Pack (@Class T b m).
- -
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition zmodType := @Zmodule.Pack cT xclass.
-Definition ringType := @Ring.Pack cT xclass.
- -
-End ClassDef.
- -
-Module Exports.
-Coercion base : class_of >-> Ring.class_of.
-Coercion mixin : class_of >-> commutative.
-Coercion sort : type >-> Sortclass.
-Coercion eqType : type >-> Equality.type.
-Canonical eqType.
-Coercion choiceType : type >-> Choice.type.
-Canonical choiceType.
-Coercion zmodType : type >-> Zmodule.type.
-Canonical zmodType.
-Coercion ringType : type >-> Ring.type.
-Canonical ringType.
-Notation comRingType := type.
-Notation ComRingType T m := (@pack T _ m _ _ id _ id).
-Notation ComRingMixin := RingMixin.
-Notation "[ 'comRingType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
-  (at level 0, format "[ 'comRingType' 'of' T 'for' cT ]") : form_scope.
-Notation "[ 'comRingType' 'of' T ]" := (@clone T _ _ id)
-  (at level 0, format "[ 'comRingType' 'of' T ]") : form_scope.
-End Exports.
- -
-End ComRing.
-Import ComRing.Exports.
- -
-Section ComRingTheory.
- -
-Variable R : comRingType.
-Implicit Types x y : R.
- -
-Lemma mulrC : @commutative R R *%R.
-Canonical mul_comoid := Monoid.ComLaw 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 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 sqrrD x y : (x + y ) ^+ 2 = x ^+ 2 + x × y *+ 2 + y ^+ 2.
- -
-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_rmorphism : rmorphism (Frobenius_aut charRp).
- -
-Canonical Frobenius_aut_additive := Additive Frobenius_aut_is_rmorphism.
-Canonical Frobenius_aut_rmorphism := RMorphism Frobenius_aut_is_rmorphism.
- -
-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).
- Canonical scale_linear := AddLinear scale_is_scalable.
- -
-Lemma scale_fun_is_scalable : scalable (b \*: f).
- Canonical scale_fun_linear := AddLinear scale_fun_is_scalable.
- -
-End ScaleLinear.
- -
-End ComRingTheory.
- -
-Module Algebra.
- -
-Section Mixin.
- -
-Variables (R : ringType) (A : lalgType R).
- -
-Definition axiom := ∀ k (x y : A), k *: (x × y ) = x × (k *: y ).
- -
-Lemma comm_axiom : phant A → commutative (@mul A) → axiom.
- -
-End Mixin.
- -
-Section ClassDef.
- -
-Variable R : ringType.
- -
-Record class_of (T : Type) : Type := Class {
-  base : Lalgebra.class_of R T;
-  mixin : axiom (Lalgebra.Pack _ base)
-}.
- -
-Structure type (phR : phant R) := Pack {sort; _ : class_of sort}.
-Variable (phR : phant R) (T : Type) (cT : type phR).
-Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
-Definition clone c of phant_id class c := @Pack phR T c.
-Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of xT).
- -
-Definition pack b0 (ax0 : @axiom R b0) :=
-  fun bT b & phant_id (@Lalgebra.class R phR bT) b ⇒
-  fun ax & phant_id ax0 ax ⇒ Pack phR (@Class T b ax).
- -
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition zmodType := @Zmodule.Pack cT xclass.
-Definition ringType := @Ring.Pack cT xclass.
-Definition lmodType := @Lmodule.Pack R phR cT xclass.
-Definition lalgType := @Lalgebra.Pack R phR cT xclass.
- -
-End ClassDef.
- -
-Module Exports.
-Coercion base : class_of >-> Lalgebra.class_of.
-Coercion sort : type >-> Sortclass.
-Coercion eqType : type >-> Equality.type.
-Canonical eqType.
-Coercion choiceType : type >-> Choice.type.
-Canonical choiceType.
-Coercion zmodType : type >-> Zmodule.type.
-Canonical zmodType.
-Coercion ringType : type >-> Ring.type.
-Canonical ringType.
-Coercion lmodType : type >-> Lmodule.type.
-Canonical lmodType.
-Coercion lalgType : type >-> Lalgebra.type.
-Canonical lalgType.
-Notation algType R := (type (Phant R)).
-Notation AlgType R A ax := (@pack _ (Phant R) A _ ax _ _ id _ id).
-Notation CommAlgType R A := (AlgType R A (comm_axiom (Phant A) (@mulrC _))).
-Notation "[ 'algType' R 'of' T 'for' cT ]" := (@clone _ (Phant R) T cT _ idfun)
-  (at level 0, format "[ 'algType' R 'of' T 'for' cT ]")
-  : form_scope.
-Notation "[ 'algType' R 'of' T ]" := (@clone _ (Phant R) T _ _ id)
-  (at level 0, format "[ 'algType' R 'of' T ]") : form_scope.
-End Exports.
- -
-End Algebra.
-Import Algebra.Exports.
- -
-Section AlgebraTheory.
- -
-Variables (R : comRingType) (A : algType R).
-Implicit Types (k : R) (x y : A).
- -
-Lemma scalerAr k x y : k *: (x × y ) = x × (k *: y ).
- -
-Lemma scalerCA k x y : k *: x × y = x × (k *: y ).
- -
-Lemma mulr_algr a x : x × a %: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 |.
- -
-Canonical regular_comRingType := [comRingType of R ^o ].
-Canonical regular_algType := CommAlgType R R ^o.
- -
-Variables (U : lmodType R) (a : A) (f : {linear U → A }).
- -
-Lemma mull_fun_is_scalable : scalable (a \*o f).
- Canonical mull_fun_linear := AddLinear mull_fun_is_scalable.
- -
-End AlgebraTheory.
- -
-Module UnitRing.
- -
-Record mixin_of (R : ringType) : Type := Mixin {
-  unit : pred R;
-  inv : R → R;
-  _ : {in unit , left_inverse 1 inv *%R };
-  _ : {in unit , right_inverse 1 inv *%R };
-  _ : ∀ x y, y × x = 1 ∧ x × y = 1 → unit x;
-  _ : {in [predC unit ], inv =1 id }
-}.
- -
-Definition EtaMixin R unit inv mulVr mulrV unitP inv_out :=
-  let _ := @Mixin R unit inv mulVr mulrV unitP inv_out in
-  @Mixin (Ring.Pack (Ring.class R)) unit inv mulVr mulrV unitP inv_out.
- -
-Section ClassDef.
- -
-Record class_of (R : Type) : Type := Class {
-  base : Ring.class_of R;
-  mixin : mixin_of (Ring.Pack base)
-}.
- -
-Structure type := Pack {sort; _ : class_of sort}.
-Variables (T : Type) (cT : type).
-Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
-Definition clone c of phant_id class c := @Pack T c.
-Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of xT).
- -
-Definition pack b0 (m0 : mixin_of (@Ring.Pack T b0)) :=
-  fun bT b & phant_id (Ring.class bT) b ⇒
-  fun m & phant_id m0 m ⇒ Pack (@Class T b m).
- -
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition zmodType := @Zmodule.Pack cT xclass.
-Definition ringType := @Ring.Pack cT xclass.
- -
-End ClassDef.
- -
-Module Exports.
-Coercion base : class_of >-> Ring.class_of.
-Coercion mixin : class_of >-> mixin_of.
-Coercion sort : type >-> Sortclass.
-Coercion eqType : type >-> Equality.type.
-Canonical eqType.
-Coercion choiceType : type >-> Choice.type.
-Canonical choiceType.
-Coercion zmodType : type >-> Zmodule.type.
-Canonical zmodType.
-Coercion ringType : type >-> Ring.type.
-Canonical ringType.
-Notation unitRingType := type.
-Notation UnitRingType T m := (@pack T _ m _ _ id _ id).
-Notation UnitRingMixin := EtaMixin.
-Notation "[ 'unitRingType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
-  (at level 0, format "[ 'unitRingType' 'of' T 'for' cT ]") : form_scope.
-Notation "[ 'unitRingType' 'of' T ]" := (@clone T _ _ id)
-  (at level 0, format "[ 'unitRingType' 'of' T ]") : form_scope.
-End Exports.
- -
-End UnitRing.
-Import UnitRing.Exports.
- -
-Definition unit {R : unitRingType} :=
-  [qualify a u : R | UnitRing.unit (UnitRing.class R) u ].
-Fact unit_key R : pred_key (@unit R).
-Canonical unit_keyed R := KeyedQualifier (@unit_key R).
-Definition inv {R : unitRingType} : R → R := UnitRing.inv (UnitRing.class R).
- -
- -
-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 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.
- -
-Definition converse_unitRingMixin :=
-  @UnitRing.Mixin _ (unit : {pred R ^c }) _ mulrV mulVr rev_unitrP invr_out.
-Canonical converse_unitRingType := UnitRingType R ^c converse_unitRingMixin.
-Canonical regular_unitRingType := [unitRingType of R ^o ].
- -
-Section ClosedPredicates.
- -
-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 ClosedPredicates.
- -
-End UnitRingTheory.
- -
- -
-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.
- -
-Module ComUnitRing.
- -
-Section Mixin.
- -
-Variables (R : comRingType) (unit : pred R) (inv : R → R).
-Hypothesis mulVx : {in unit , left_inverse 1 inv *%R }.
-Hypothesis unitPl : ∀ x y, y × x = 1 → unit x.
- -
-Fact mulC_mulrV : {in unit , right_inverse 1 inv *%R }.
- -
-Fact mulC_unitP x y : y × x = 1 ∧ x × y = 1 → unit x.
- -
-Definition Mixin := UnitRingMixin mulVx mulC_mulrV mulC_unitP.
- -
-End Mixin.
- -
-Section ClassDef.
- -
-Record class_of (R : Type) : Type := Class {
-  base : ComRing.class_of R;
-  mixin : UnitRing.mixin_of (Ring.Pack base)
-}.
-Definition base2 R m := UnitRing.Class (@mixin R m).
- -
-Structure type := Pack {sort; _ : class_of sort}.
-Variables (T : Type) (cT : type).
-Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
-Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of xT).
- -
-Definition pack :=
-  fun bT b & phant_id (ComRing.class bT) (b : ComRing.class_of T) ⇒
-  fun mT m & phant_id (UnitRing.class mT) (@UnitRing.Class T b m) ⇒
-  Pack (@Class T b m).
- -
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition zmodType := @Zmodule.Pack cT xclass.
-Definition ringType := @Ring.Pack cT xclass.
-Definition comRingType := @ComRing.Pack cT xclass.
-Definition unitRingType := @UnitRing.Pack cT xclass.
-Definition com_unitRingType := @UnitRing.Pack comRingType xclass.
- -
-End ClassDef.
- -
-Module Import Exports.
-Coercion base : class_of >-> ComRing.class_of.
-Coercion mixin : class_of >-> UnitRing.mixin_of.
-Coercion base2 : class_of >-> UnitRing.class_of.
-Coercion sort : type >-> Sortclass.
-Coercion eqType : type >-> Equality.type.
-Canonical eqType.
-Coercion choiceType : type >-> Choice.type.
-Canonical choiceType.
-Coercion zmodType : type >-> Zmodule.type.
-Canonical zmodType.
-Coercion ringType : type >-> Ring.type.
-Canonical ringType.
-Coercion comRingType : type >-> ComRing.type.
-Canonical comRingType.
-Coercion unitRingType : type >-> UnitRing.type.
-Canonical unitRingType.
-Canonical com_unitRingType.
-Notation comUnitRingType := type.
-Notation ComUnitRingMixin := Mixin.
-Notation "[ 'comUnitRingType' 'of' T ]" := (@pack T _ _ id _ _ id)
-  (at level 0, format "[ 'comUnitRingType' 'of' T ]") : form_scope.
-End Exports.
- -
-End ComUnitRing.
-Import ComUnitRing.Exports.
- -
-Module UnitAlgebra.
- -
-Section ClassDef.
- -
-Variable R : ringType.
- -
-Record class_of (T : Type) : Type := Class {
-  base : Algebra.class_of R T;
-  mixin : GRing.UnitRing.mixin_of (Ring.Pack base)
-}.
-Definition base2 R m := UnitRing.Class (@mixin R m).
- -
-Structure type (phR : phant R) := Pack {sort; _ : class_of sort}.
-Variable (phR : phant R) (T : Type) (cT : type phR).
-Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
-Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of xT).
- -
-Definition pack :=
-  fun bT b & phant_id (@Algebra.class R phR bT) (b : Algebra.class_of R T) ⇒
-  fun mT m & phant_id (UnitRing.mixin (UnitRing.class mT)) m ⇒
-  Pack (Phant R) (@Class T b m).
- -
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition zmodType := @Zmodule.Pack cT xclass.
-Definition ringType := @Ring.Pack cT xclass.
-Definition unitRingType := @UnitRing.Pack cT xclass.
-Definition lmodType := @Lmodule.Pack R phR cT xclass.
-Definition lalgType := @Lalgebra.Pack R phR cT xclass.
-Definition algType := @Algebra.Pack R phR cT xclass.
-Definition lmod_unitRingType := @Lmodule.Pack R phR unitRingType xclass.
-Definition lalg_unitRingType := @Lalgebra.Pack R phR unitRingType xclass.
-Definition alg_unitRingType := @Algebra.Pack R phR unitRingType xclass.
- -
-End ClassDef.
- -
-Module Exports.
-Coercion base : class_of >-> Algebra.class_of.
-Coercion base2 : class_of >-> UnitRing.class_of.
-Coercion sort : type >-> Sortclass.
-Coercion eqType : type >-> Equality.type.
-Canonical eqType.
-Coercion choiceType : type >-> Choice.type.
-Canonical choiceType.
-Coercion zmodType : type >-> Zmodule.type.
-Canonical zmodType.
-Coercion ringType : type >-> Ring.type.
-Canonical ringType.
-Coercion unitRingType : type >-> UnitRing.type.
-Canonical unitRingType.
-Coercion lmodType : type >-> Lmodule.type.
-Canonical lmodType.
-Coercion lalgType : type >-> Lalgebra.type.
-Canonical lalgType.
-Coercion algType : type >-> Algebra.type.
-Canonical algType.
-Canonical lmod_unitRingType.
-Canonical lalg_unitRingType.
-Canonical alg_unitRingType.
-Notation unitAlgType R := (type (Phant R)).
-Notation "[ 'unitAlgType' R 'of' T ]" := (@pack _ (Phant R) T _ _ id _ _ id)
-  (at level 0, format "[ 'unitAlgType' R 'of' T ]") : form_scope.
-End Exports.
- -
-End UnitAlgebra.
-Import UnitAlgebra.Exports.
- -
-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.
- -
-Canonical regular_comUnitRingType := [comUnitRingType of R ^o ].
-Canonical regular_unitAlgType := [unitAlgType R of R ^o ].
- -
-End ComUnitRingTheory.
- -
-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.
- -
-
- -
- Interface structures for algebraically closed predicates. -
-
-Module Pred.
- -
-Structure opp V S := Opp {opp_key : pred_key S; _ : @oppr_closed V S}.
-Structure add V S := Add {add_key : pred_key S; _ : @addr_closed V S}.
-Structure mul R S := Mul {mul_key : pred_key S; _ : @mulr_closed R S}.
-Structure zmod V S := Zmod {zmod_add : add S; _ : @oppr_closed V S}.
-Structure semiring R S := Semiring {semiring_add : add S; _ : @mulr_closed R S}.
-Structure smul R S := Smul {smul_opp : opp S; _ : @mulr_closed R S}.
-Structure div R S := Div {div_mul : mul S; _ : @invr_closed R S}.
-Structure submod R V S :=
-  Submod {submod_zmod : zmod S; _ : @scaler_closed R V S}.
-Structure subring R S := Subring {subring_zmod : zmod S; _ : @mulr_closed R S}.
-Structure sdiv R S := Sdiv {sdiv_smul : smul S; _ : @invr_closed R S}.
-Structure subalg (R : ringType) (A : lalgType R) S :=
-  Subalg {subalg_ring : subring S; _ : @scaler_closed R A S}.
-Structure divring R S :=
-  Divring {divring_ring : subring S; _ : @invr_closed R S}.
-Structure divalg (R : ringType) (A : unitAlgType R) S :=
-  Divalg {divalg_ring : divring S; _ : @scaler_closed R A S}.
- -
-Section Subtyping.
- -
-Ltac done := case⇒ *; assumption.
-Fact zmod_oppr R S : @zmod R S → oppr_closed S.
-Fact semiring_mulr R S : @semiring R S → mulr_closed S.
-Fact smul_mulr R S : @smul R S → mulr_closed S.
-Fact submod_scaler R V S : @submod R V S → scaler_closed S.
-Fact subring_mulr R S : @subring R S → mulr_closed S.
-Fact sdiv_invr R S : @sdiv R S → invr_closed S.
-Fact subalg_scaler R A S : @subalg R A S → scaler_closed S.
-Fact divring_invr R S : @divring R S → invr_closed S.
-Fact divalg_scaler R A S : @divalg R A S → scaler_closed S.
- -
-Definition zmod_opp R S (addS : @zmod R S) :=
-  Opp (add_key (zmod_add addS)) (zmod_oppr addS).
-Definition semiring_mul R S (ringS : @semiring R S) :=
-  Mul (add_key (semiring_add ringS)) (semiring_mulr ringS).
-Definition smul_mul R S (mulS : @smul R S) :=
-  Mul (opp_key (smul_opp mulS)) (smul_mulr mulS).
-Definition subring_semi R S (ringS : @subring R S) :=
-  Semiring (zmod_add (subring_zmod ringS)) (subring_mulr ringS).
-Definition subring_smul R S (ringS : @subring R S) :=
-  Smul (zmod_opp (subring_zmod ringS)) (subring_mulr ringS).
-Definition sdiv_div R S (divS : @sdiv R S) :=
-  Div (smul_mul (sdiv_smul divS)) (sdiv_invr divS).
-Definition subalg_submod R A S (algS : @subalg R A S) :=
-  Submod (subring_zmod (subalg_ring algS)) (subalg_scaler algS).
-Definition divring_sdiv R S (ringS : @divring R S) :=
-  Sdiv (subring_smul (divring_ring ringS)) (divring_invr ringS).
-Definition divalg_alg R A S (algS : @divalg R A S) :=
-  Subalg (divring_ring (divalg_ring algS)) (divalg_scaler algS).
- -
-End Subtyping.
- -
-Section Extensionality.
-
- -
- This could be avoided by exploiting the Coq 8.4 eta-convertibility. -
-
- -
-Lemma opp_ext (U : zmodType) S k (kS : @keyed_pred U S k) :
-  oppr_closed kS → oppr_closed S.
- -
-Lemma add_ext (U : zmodType) S k (kS : @keyed_pred U S k) :
-  addr_closed kS → addr_closed S.
- -
-Lemma mul_ext (R : ringType) S k (kS : @keyed_pred R S k) :
-  mulr_closed kS → mulr_closed S.
- -
-Lemma scale_ext (R : ringType) (U : lmodType R) S k (kS : @keyed_pred U S k) :
-  scaler_closed kS → scaler_closed S.
- -
-Lemma inv_ext (R : unitRingType) S k (kS : @keyed_pred R S k) :
-  invr_closed kS → invr_closed S.
- -
-End Extensionality.
- -
-Module Default.
-Definition opp V S oppS := @Opp V S (DefaultPredKey S) oppS.
-Definition add V S addS := @Add V S (DefaultPredKey S) addS.
-Definition mul R S mulS := @Mul R S (DefaultPredKey S) mulS.
-Definition zmod V S addS oppS := @Zmod V S (add addS) oppS.
-Definition semiring R S addS mulS := @Semiring R S (add addS) mulS.
-Definition smul R S oppS mulS := @Smul R S (opp oppS) mulS.
-Definition div R S mulS invS := @Div R S (mul mulS) invS.
-Definition submod R V S addS oppS linS := @Submod R V S (zmod addS oppS) linS.
-Definition subring R S addS oppS mulS := @Subring R S (zmod addS oppS) mulS.
-Definition sdiv R S oppS mulS invS := @Sdiv R S (smul oppS mulS) invS.
-Definition subalg R A S addS oppS mulS linS :=
-  @Subalg R A S (subring addS oppS mulS) linS.
-Definition divring R S addS oppS mulS invS :=
-  @Divring R S (subring addS oppS mulS) invS.
-Definition divalg R A S addS oppS mulS invS linS :=
-  @Divalg R A S (divring addS oppS mulS invS) linS.
-End Default.
- -
-Module Exports.
- -
-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.
- -
-Coercion opp_key : opp >-> pred_key.
-Coercion add_key : add >-> pred_key.
-Coercion mul_key : mul >-> pred_key.
-Coercion zmod_opp : zmod >-> opp.
-Canonical zmod_opp.
-Coercion zmod_add : zmod >-> add.
-Coercion semiring_add : semiring >-> add.
-Coercion semiring_mul : semiring >-> mul.
-Canonical semiring_mul.
-Coercion smul_opp : smul >-> opp.
-Coercion smul_mul : smul >-> mul.
-Canonical smul_mul.
-Coercion div_mul : div >-> mul.
-Coercion submod_zmod : submod >-> zmod.
-Coercion subring_zmod : subring >-> zmod.
-Coercion subring_semi : subring >-> semiring.
-Canonical subring_semi.
-Coercion subring_smul : subring >-> smul.
-Canonical subring_smul.
-Coercion sdiv_smul : sdiv >-> smul.
-Coercion sdiv_div : sdiv >-> div.
-Canonical sdiv_div.
-Coercion subalg_submod : subalg >-> submod.
-Canonical subalg_submod.
-Coercion subalg_ring : subalg >-> subring.
-Coercion divring_ring : divring >-> subring.
-Coercion divring_sdiv : divring >-> sdiv.
-Canonical divring_sdiv.
-Coercion divalg_alg : divalg >-> subalg.
-Canonical divalg_alg.
-Coercion divalg_ring : divalg >-> divring.
- -
-Notation opprPred := opp.
-Notation addrPred := add.
-Notation mulrPred := mul.
-Notation zmodPred := zmod.
-Notation semiringPred := semiring.
-Notation smulrPred := smul.
-Notation divrPred := div.
-Notation submodPred := submod.
-Notation subringPred := subring.
-Notation sdivrPred := sdiv.
-Notation subalgPred := subalg.
-Notation divringPred := divring.
-Notation divalgPred := divalg.
- -
-Definition OpprPred U S k kS NkS := Opp k (@opp_ext U S k kS NkS).
-Definition AddrPred U S k kS DkS := Add k (@add_ext U S k kS DkS).
-Definition MulrPred R S k kS MkS := Mul k (@mul_ext R S k kS MkS).
-Definition ZmodPred U S k kS NkS := Zmod k (@opp_ext U S k kS NkS).
-Definition SemiringPred R S k kS MkS := Semiring k (@mul_ext R S k kS MkS).
-Definition SmulrPred R S k kS MkS := Smul k (@mul_ext R S k kS MkS).
-Definition DivrPred R S k kS VkS := Div k (@inv_ext R S k kS VkS).
-Definition SubmodPred R U S k kS ZkS := Submod k (@scale_ext R U S k kS ZkS).
-Definition SubringPred R S k kS MkS := Subring k (@mul_ext R S k kS MkS).
-Definition SdivrPred R S k kS VkS := Sdiv k (@inv_ext R S k kS VkS).
-Definition SubalgPred (R : ringType) (A : lalgType R) S k kS ZkS :=
-  Subalg k (@scale_ext R A S k kS ZkS).
-Definition DivringPred R S k kS VkS := Divring k (@inv_ext R S k kS VkS).
-Definition DivalgPred (R : ringType) (A : unitAlgType R) S k kS ZkS :=
-  Divalg k (@scale_ext R A S k kS ZkS).
- -
-End Exports.
- -
-End Pred.
-Import Pred.Exports.
- -
-Module DefaultPred.
- -
-Canonical Pred.Default.opp.
-Canonical Pred.Default.add.
-Canonical Pred.Default.mul.
-Canonical Pred.Default.zmod.
-Canonical Pred.Default.semiring.
-Canonical Pred.Default.smul.
-Canonical Pred.Default.div.
-Canonical Pred.Default.submod.
-Canonical Pred.Default.subring.
-Canonical Pred.Default.sdiv.
-Canonical Pred.Default.subalg.
-Canonical Pred.Default.divring.
-Canonical Pred.Default.divalg.
- -
-End DefaultPred.
- -
-Section ZmodulePred.
- -
-Variables (V : zmodType) (S : {pred V }).
- -
-Section Add.
- -
-Variables (addS : addrPred S) (kS : keyed_pred addS).
- -
-Lemma rpred0D : addr_closed kS.
- -
-Lemma rpred0 : 0 \in kS.
- -
-Lemma rpredD : {in kS &, ∀ u v, u + v \in kS }.
- -
-Lemma rpred_sum I r (P : pred I) F :
-  (∀ i, P i → F i \in kS ) → \sum_(i <- r | P i ) F i \in kS.
- -
-Lemma rpredMn n : {in kS , ∀ u, u *+ n \in kS }.
- -
-End Add.
- -
-Section Opp.
- -
-Variables (oppS : opprPred S) (kS : keyed_pred oppS).
- -
-Lemma rpredNr : oppr_closed kS.
- -
-Lemma rpredN : {mono -%R : u / u \in kS }.
- -
-End Opp.
- -
-Section Sub.
- -
-Variables (subS : zmodPred S) (kS : keyed_pred subS).
- -
-Lemma rpredB : {in kS &, ∀ u v, u - v \in kS }.
- -
-Lemma rpredMNn n : {in kS , ∀ u, u *- n \in kS }.
- -
-Lemma rpredDr x y : x \in kS → (y + x \in kS ) = (y \in kS ).
- -
-Lemma rpredDl x y : x \in kS → (x + y \in kS ) = (y \in kS ).
- -
-Lemma rpredBr x y : x \in kS → (y - x \in kS ) = (y \in kS ).
- -
-Lemma rpredBl x y : x \in kS → (x - y \in kS ) = (y \in kS ).
- -
-End Sub.
- -
-End ZmodulePred.
- -
-Section RingPred.
- -
-Variables (R : ringType) (S : {pred R }).
- -
-Lemma rpredMsign (oppS : opprPred S) (kS : keyed_pred oppS) n x :
-  ((-1) ^+ n × x \in kS ) = (x \in kS ).
- -
-Section Mul.
- -
-Variables (mulS : mulrPred S) (kS : keyed_pred mulS).
- -
-Lemma rpred1M : mulr_closed kS.
- -
-Lemma rpred1 : 1 \in kS.
- -
-Lemma rpredM : {in kS &, ∀ u v, u × v \in kS }.
- -
-Lemma rpred_prod I r (P : pred I) F :
-  (∀ i, P i → F i \in kS ) → \prod_(i <- r | P i ) F i \in kS.
- -
-Lemma rpredX n : {in kS , ∀ u, u ^+ n \in kS }.
- -
-End Mul.
- -
-Lemma rpred_nat (rngS : semiringPred S) (kS : keyed_pred rngS) n : n %:R \in kS.
- -
-Lemma rpredN1 (mulS : smulrPred S) (kS : keyed_pred mulS) : -1 \in kS.
- -
-Lemma rpred_sign (mulS : smulrPred S) (kS : keyed_pred mulS) n :
-  (-1) ^+ n \in kS.
- -
-End RingPred.
- -
-Section LmodPred.
- -
-Variables (R : ringType) (V : lmodType R) (S : {pred V }).
- -
-Lemma rpredZsign (oppS : opprPred S) (kS : keyed_pred oppS) n u :
-  ((-1) ^+ n *: u \in kS ) = (u \in kS ).
- -
-Lemma rpredZnat (addS : addrPred S) (kS : keyed_pred addS) n :
-  {in kS , ∀ u, n %:R *: u \in kS }.
- -
-Lemma rpredZ (linS : submodPred S) (kS : keyed_pred linS) : scaler_closed kS.
- -
-End LmodPred.
- -
-Section UnitRingPred.
- -
-Variable R : unitRingType.
- -
-Section Div.
- -
-Variables (S : {pred R }) (divS : divrPred S) (kS : keyed_pred divS).
- -
-Lemma rpredVr x : x \in kS → x ^-1 \in kS.
- -
-Lemma rpredV x : (x ^-1 \in kS ) = (x \in kS ).
- -
-Lemma rpred_div : {in kS &, ∀ x y, x / y \in kS }.
- -
-Lemma rpredXN n : {in kS , ∀ x, x ^- n \in kS }.
- -
-Lemma rpredMl x y : x \in kS → x \is a unit → (x × y \in kS ) = (y \in kS ).
- -
-Lemma rpredMr x y : x \in kS → x \is a unit → (y × x \in kS ) = (y \in kS ).
- -
-Lemma rpred_divr x y : x \in kS → x \is a unit → (y / x \in kS ) = (y \in kS ).
- -
-Lemma rpred_divl x y : x \in kS → x \is a unit → (x / y \in kS ) = (y \in kS ).
- -
-End Div.
- -
-Fact unitr_sdivr_closed : @sdivr_closed R unit.
- -
-Canonical unit_opprPred := OpprPred unitr_sdivr_closed.
-Canonical unit_mulrPred := MulrPred unitr_sdivr_closed.
-Canonical unit_divrPred := DivrPred unitr_sdivr_closed.
-Canonical unit_smulrPred := SmulrPred unitr_sdivr_closed.
-Canonical unit_sdivrPred := SdivrPred 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 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.
- -
-
- -
- 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.
- -
- -
- -
-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.
- -
-
- -
- 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.
- -
-
- -
- Extensionality of formula evaluation -
-
-Lemma eq_holds e e' f : same_env e e' → holds e f → holds e' f.
- -
-
- -
- Evaluation and substitution by a constant -
-
-Lemma holds_fsubst e f i v :
-  holds e (fsubst f (i , v %:T )%T) ↔ holds (set_nth 0 e i v) f.
- -
-
- -
- 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.
- -
-
- -
- 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.
- -
-
- -
- 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.
- -
-
- -
- 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 ).
- -
-
- -
- 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.
- -
-
- -
- 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.
- -
-
- -
- The transformation gives a ring formula. -
-
-Lemma to_rform_rformula f : rformula (to_rform f).
- -
-
- -
- Correctness of the transformation. -
-
-Lemma to_rformP e f : holds e (to_rform f) ↔ holds e f.
- -
-
- -
- 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.
- -
-
- -
- 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.
- -
-
- -
- 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).
- -
-
- -
- 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.
- -
-
- -
- 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).
- -
-
- -
- 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.
- -
-
- -
- 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).
- -
-
- -
- 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.
- -
- -
-Module IntegralDomain.
- -
-Definition axiom (R : ringType) :=
-  ∀ x y : R, x × y = 0 → (x == 0) || (y == 0).
- -
-Section ClassDef.
- -
-Record class_of (R : Type) : Type :=
-  Class {base : ComUnitRing.class_of R; mixin : axiom (Ring.Pack base)}.
- -
-Structure type := Pack {sort; _ : class_of sort}.
-Variable (T : Type) (cT : type).
-Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
-Definition clone c of phant_id class c := @Pack T c.
-Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of xT).
- -
-Definition pack b0 (m0 : axiom (@Ring.Pack T b0)) :=
-  fun bT b & phant_id (ComUnitRing.class bT) b ⇒
-  fun m & phant_id m0 m ⇒ Pack (@Class T b m).
- -
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition zmodType := @Zmodule.Pack cT xclass.
-Definition ringType := @Ring.Pack cT xclass.
-Definition comRingType := @ComRing.Pack cT xclass.
-Definition unitRingType := @UnitRing.Pack cT xclass.
-Definition comUnitRingType := @ComUnitRing.Pack cT xclass.
- -
-End ClassDef.
- -
-Module Exports.
-Coercion base : class_of >-> ComUnitRing.class_of.
-Coercion mixin : class_of >-> axiom.
-Coercion sort : type >-> Sortclass.
-Coercion eqType : type >-> Equality.type.
-Canonical eqType.
-Coercion choiceType : type >-> Choice.type.
-Canonical choiceType.
-Coercion zmodType : type >-> Zmodule.type.
-Canonical zmodType.
-Coercion ringType : type >-> Ring.type.
-Canonical ringType.
-Coercion comRingType : type >-> ComRing.type.
-Canonical comRingType.
-Coercion unitRingType : type >-> UnitRing.type.
-Canonical unitRingType.
-Coercion comUnitRingType : type >-> ComUnitRing.type.
-Canonical comUnitRingType.
-Notation idomainType := type.
-Notation IdomainType T m := (@pack T _ m _ _ id _ id).
-Notation "[ 'idomainType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
-  (at level 0, format "[ 'idomainType' 'of' T 'for' cT ]") : form_scope.
-Notation "[ 'idomainType' 'of' T ]" := (@clone T _ _ id)
-  (at level 0, format "[ 'idomainType' 'of' T ]") : form_scope.
-End Exports.
- -
-End IntegralDomain.
-Import IntegralDomain.Exports.
- -
-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).
- -
-Canonical regular_idomainType := [idomainType of R ^o ].
- -
-End IntegralDomainTheory.
- -
- -
-Module Field.
- -
-Definition mixin_of (R : unitRingType) := ∀ x : R, x != 0 → x \in unit.
- -
-Lemma IdomainMixin R : mixin_of R → IntegralDomain.axiom R.
- -
-Section Mixins.
- -
-Definition axiom (R : ringType) inv := ∀ x : R, x != 0 → inv x × x = 1.
- -
-Variables (R : comRingType) (inv : R → R).
-Hypotheses (mulVf : axiom inv) (inv0 : inv 0 = 0).
- -
-Fact intro_unit (x y : R) : y × x = 1 → x != 0.
- -
-Fact inv_out : {in predC (predC1 0), inv =1 id }.
- -
-Definition UnitMixin := ComUnitRing.Mixin mulVf intro_unit inv_out.
- -
-Definition UnitRingType := [comUnitRingType of UnitRingType R UnitMixin ].
- -
-Definition IdomainType :=
-  IdomainType UnitRingType (@IdomainMixin UnitRingType (fun ⇒ id)).
- -
-Lemma Mixin : mixin_of IdomainType.
- -
-End Mixins.
- -
-Section ClassDef.
- -
-Record class_of (F : Type) : Type := Class {
-  base : IntegralDomain.class_of F;
-  mixin : mixin_of (UnitRing.Pack base)
-}.
- -
-Structure type := Pack {sort; _ : class_of sort}.
-Variable (T : Type) (cT : type).
-Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
-Definition clone c of phant_id class c := @Pack T c.
-Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of xT).
- -
-Definition pack b0 (m0 : mixin_of (@UnitRing.Pack T b0)) :=
-  fun bT b & phant_id (IntegralDomain.class bT) b ⇒
-  fun m & phant_id m0 m ⇒ Pack (@Class T b m).
- -
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition zmodType := @Zmodule.Pack cT xclass.
-Definition ringType := @Ring.Pack cT xclass.
-Definition comRingType := @ComRing.Pack cT xclass.
-Definition unitRingType := @UnitRing.Pack cT xclass.
-Definition comUnitRingType := @ComUnitRing.Pack cT xclass.
-Definition idomainType := @IntegralDomain.Pack cT xclass.
- -
-End ClassDef.
- -
-Module Exports.
-Coercion base : class_of >-> IntegralDomain.class_of.
-Coercion mixin : class_of >-> mixin_of.
-Coercion sort : type >-> Sortclass.
-Coercion eqType : type >-> Equality.type.
-Canonical eqType.
-Coercion choiceType : type >-> Choice.type.
-Canonical choiceType.
-Coercion zmodType : type >-> Zmodule.type.
-Canonical zmodType.
-Coercion ringType : type >-> Ring.type.
-Canonical ringType.
-Coercion comRingType : type >-> ComRing.type.
-Canonical comRingType.
-Coercion unitRingType : type >-> UnitRing.type.
-Canonical unitRingType.
-Coercion comUnitRingType : type >-> ComUnitRing.type.
-Canonical comUnitRingType.
-Coercion idomainType : type >-> IntegralDomain.type.
-Canonical idomainType.
-Notation fieldType := type.
-Notation FieldType T m := (@pack T _ m _ _ id _ id).
-Notation FieldUnitMixin := UnitMixin.
-Notation FieldIdomainMixin := IdomainMixin.
-Notation FieldMixin := Mixin.
-Notation "[ 'fieldType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
-  (at level 0, format "[ 'fieldType' 'of' T 'for' cT ]") : form_scope.
-Notation "[ 'fieldType' 'of' T ]" := (@clone T _ _ id)
-  (at level 0, format "[ 'fieldType' 'of' T ]") : form_scope.
-End Exports.
- -
-End Field.
-Import Field.Exports.
- -
-Section FieldTheory.
- -
-Variable F : fieldType.
-Implicit Types x y : F.
- -
-Lemma fieldP : Field.mixin_of 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 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 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_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.
- -
-Canonical regular_fieldType := [fieldType of F ^o ].
- -
-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).
- -
-Lemma rpredZeq S (modS : submodPred S) (kS : keyed_pred modS) a v :
-  (a *: v \in kS ) = (a == 0) || (v \in kS ).
- -
-End ModuleTheory.
- -
-Lemma char_lalg (A : lalgType F) : [char A ] =i [char F ].
- -
-Section Predicates.
- -
-Context (S : {pred F }) (divS : @divrPred F S) (kS : keyed_pred divS).
- -
-Lemma fpredMl x y : x \in kS → x != 0 → (x × y \in kS ) = (y \in kS ).
- -
-Lemma fpredMr x y : x \in kS → x != 0 → (y × x \in kS ) = (y \in kS ).
- -
-Lemma fpred_divl x y : x \in kS → x != 0 → (x / y \in kS ) = (y \in kS ).
- -
-Lemma fpred_divr x y : x \in kS → x != 0 → (y / x \in kS ) = (y \in kS ).
- -
-End Predicates.
- -
-End FieldTheory.
- -
- -
-Module DecidableField.
- -
-Definition axiom (R : unitRingType) (s : seq R → pred (formula R)) :=
-  ∀ e f, reflect (holds e f) (s e f).
- -
-Record mixin_of (R : unitRingType) : Type :=
-  Mixin { sat : seq R → pred (formula R); satP : axiom sat}.
- -
-Section ClassDef.
- -
-Record class_of (F : Type) : Type :=
-  Class {base : Field.class_of F; mixin : mixin_of (UnitRing.Pack base)}.
- -
-Structure type := Pack {sort; _ : class_of sort}.
-Variable (T : Type) (cT : type).
-Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
-Definition clone c of phant_id class c := @Pack T c.
-Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of xT).
- -
-Definition pack b0 (m0 : mixin_of (@UnitRing.Pack T b0)) :=
-  fun bT b & phant_id (Field.class bT) b ⇒
-  fun m & phant_id m0 m ⇒ Pack (@Class T b m).
- -
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition zmodType := @Zmodule.Pack cT xclass.
-Definition ringType := @Ring.Pack cT xclass.
-Definition comRingType := @ComRing.Pack cT xclass.
-Definition unitRingType := @UnitRing.Pack cT xclass.
-Definition comUnitRingType := @ComUnitRing.Pack cT xclass.
-Definition idomainType := @IntegralDomain.Pack cT xclass.
-Definition fieldType := @Field.Pack cT xclass.
- -
-End ClassDef.
- -
-Module Exports.
-Coercion base : class_of >-> Field.class_of.
-Coercion mixin : class_of >-> mixin_of.
-Coercion sort : type >-> Sortclass.
-Coercion eqType : type >-> Equality.type.
-Canonical eqType.
-Coercion choiceType : type >-> Choice.type.
-Canonical choiceType.
-Coercion zmodType : type >-> Zmodule.type.
-Canonical zmodType.
-Coercion ringType : type >-> Ring.type.
-Canonical ringType.
-Coercion comRingType : type >-> ComRing.type.
-Canonical comRingType.
-Coercion unitRingType : type >-> UnitRing.type.
-Canonical unitRingType.
-Coercion comUnitRingType : type >-> ComUnitRing.type.
-Canonical comUnitRingType.
-Coercion idomainType : type >-> IntegralDomain.type.
-Canonical idomainType.
-Coercion fieldType : type >-> Field.type.
-Canonical fieldType.
-Notation decFieldType := type.
-Notation DecFieldType T m := (@pack T _ m _ _ id _ id).
-Notation DecFieldMixin := Mixin.
-Notation "[ 'decFieldType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
-  (at level 0, format "[ 'decFieldType' 'of' T 'for' cT ]") : form_scope.
-Notation "[ 'decFieldType' 'of' T ]" := (@clone T _ _ id)
-  (at level 0, format "[ 'decFieldType' 'of' T ]") : form_scope.
-End Exports.
- -
-End DecidableField.
-Import DecidableField.Exports.
- -
-Section DecidableFieldTheory.
- -
-Variable F : decFieldType.
- -
-Definition sat := DecidableField.sat (DecidableField.class F).
- -
-Lemma satP : DecidableField.axiom sat.
- -
-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.
- -
- -
-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. -
-
-Definition wf_QE_proj :=
-  ∀ i bc (bc_i := proj i bc),
-  dnf_rterm bc → qf_form bc_i && rformula bc_i.
- -
-
- -
- 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.
- -
-Definition QEdecFieldMixin := DecidableField.Mixin proj_satP.
- -
-End QE_Mixin.
- -
-Module ClosedField.
- -
-
- -
- Axiom == all non-constant monic polynomials have a root -
-
-Definition axiom (R : ringType) :=
-  ∀ n (P : nat → R), n > 0 →
-   ∃ x : R , x ^+ n = \sum_(i < n ) P i × (x ^+ i ).
- -
-Section ClassDef.
- -
-Record class_of (F : Type) : Type :=
-  Class {base : DecidableField.class_of F; _ : axiom (Ring.Pack base)}.
- -
-Structure type := Pack {sort; _ : class_of sort}.
-Variable (T : Type) (cT : type).
-Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
-Definition clone c of phant_id class c := @Pack T c.
-Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of xT).
- -
-Definition pack b0 (m0 : axiom (@Ring.Pack T b0)) :=
-  fun bT b & phant_id (DecidableField.class bT) b ⇒
-  fun m & phant_id m0 m ⇒ Pack (@Class T b m).
- -
-
- -
- There should eventually be a constructor from polynomial resolution - that builds the DecidableField mixin using QE. -
-
- -
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition zmodType := @Zmodule.Pack cT xclass.
-Definition ringType := @Ring.Pack cT xclass.
-Definition comRingType := @ComRing.Pack cT xclass.
-Definition unitRingType := @UnitRing.Pack cT xclass.
-Definition comUnitRingType := @ComUnitRing.Pack cT xclass.
-Definition idomainType := @IntegralDomain.Pack cT xclass.
-Definition fieldType := @Field.Pack cT xclass.
-Definition decFieldType := @DecidableField.Pack cT class.
- -
-End ClassDef.
- -
-Module Exports.
-Coercion base : class_of >-> DecidableField.class_of.
-Coercion sort : type >-> Sortclass.
-Coercion eqType : type >-> Equality.type.
-Canonical eqType.
-Coercion choiceType : type >-> Choice.type.
-Canonical choiceType.
-Coercion zmodType : type >-> Zmodule.type.
-Canonical zmodType.
-Coercion ringType : type >-> Ring.type.
-Canonical ringType.
-Coercion comRingType : type >-> ComRing.type.
-Canonical comRingType.
-Coercion unitRingType : type >-> UnitRing.type.
-Canonical unitRingType.
-Coercion comUnitRingType : type >-> ComUnitRing.type.
-Canonical comUnitRingType.
-Coercion idomainType : type >-> IntegralDomain.type.
-Canonical idomainType.
-Coercion fieldType : type >-> Field.type.
-Canonical fieldType.
-Coercion decFieldType : type >-> DecidableField.type.
-Canonical decFieldType.
-Notation closedFieldType := type.
-Notation ClosedFieldType T m := (@pack T _ m _ _ id _ id).
-Notation "[ 'closedFieldType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
-  (at level 0, format "[ 'closedFieldType' 'of' T 'for' cT ]") : form_scope.
-Notation "[ 'closedFieldType' 'of' T ]" := (@clone T _ _ id)
-  (at level 0, format "[ 'closedFieldType' 'of' T ]") : form_scope.
-End Exports.
- -
-End ClosedField.
-Import ClosedField.Exports.
- -
-Section ClosedFieldTheory.
- -
-Variable F : closedFieldType.
- -
-Lemma solve_monicpoly : ClosedField.axiom F.
- -
-Lemma imaginary_exists : {i : F | i ^+ 2 = -1}.
- -
-End ClosedFieldTheory.
- -
-Module SubType.
- -
-Section Zmodule.
- -
-Variables (V : zmodType) (S : {pred V }).
-Variables (subS : zmodPred S) (kS : keyed_pred subS).
-Variable U : subType (mem kS).
- -
-Let inU v Sv : U := Sub v Sv.
-Let zeroU := inU (rpred0 kS).
- -
-Let oppU (u : U) := inU (rpredNr (valP u)).
-Let addU (u1 u2 : U) := inU (rpredD (valP u1) (valP u2)).
- -
-Fact addA : associative addU.
- Fact addC : commutative addU.
- Fact add0 : left_id zeroU addU.
- Fact addN : left_inverse zeroU oppU addU.
- -
-Definition zmodMixin of phant U := ZmodMixin addA addC add0 addN.
- -
-End Zmodule.
- -
-Section Ring.
- -
-Variables (R : ringType) (S : {pred R }).
-Variables (ringS : subringPred S) (kS : keyed_pred ringS).
- -
-Definition cast_zmodType (V : zmodType) T (VeqT : V = T :> Type) :=
-  let cast mV := let: erefl in _ = T := VeqT return Zmodule.class_of T in mV in
-  Zmodule.Pack (cast (Zmodule.class V)).
- -
-Variable (T : subType (mem kS)) (V : zmodType) (VeqT: V = T :> Type).
- -
-Let inT x Sx : T := Sub x Sx.
-Let oneT := inT (rpred1 kS).
-Let mulT (u1 u2 : T) := inT (rpredM (valP u1) (valP u2)).
-Let T' := cast_zmodType VeqT.
- -
-Hypothesis valM : {morph (val : T' → R ) : x y / x - y }.
- -
-Let val0 : val (0 : T') = 0.
- Let valD : {morph (val : T' → R ): x y / x + y }.
- -
-Fact mulA : @associative T' mulT.
- Fact mul1l : left_id oneT mulT.
- Fact mul1r : right_id oneT mulT.
- Fact mulDl : @left_distributive T' T' mulT +%R.
- Fact mulDr : @right_distributive T' T' mulT +%R.
- Fact nz1 : oneT != 0 :> T'.
- -
-Definition ringMixin := RingMixin mulA mul1l mul1r mulDl mulDr nz1.
- -
-End Ring.
- -
-Section Lmodule.
- -
-Variables (R : ringType) (V : lmodType R) (S : {pred V }).
-Variables (linS : submodPred S) (kS : keyed_pred linS).
-Variables (W : subType (mem kS)) (Z : zmodType) (ZeqW : Z = W :> Type).
- -
-Let scaleW a (w : W) := (Sub _ : _ → W) (rpredZ a (valP w)).
-Let W' := cast_zmodType ZeqW.
- -
-Hypothesis valD : {morph (val : W' → V ) : x y / x + y }.
- -
-Fact scaleA a b (w : W') : scaleW a (scaleW b w) = scaleW (a × b) w.
- Fact scale1 : left_id 1 scaleW.
- Fact scaleDr : @right_distributive R W' scaleW +%R.
- Fact scaleDl w : {morph (scaleW ^~ w : R → W') : a b / a + b }.
- -
-Definition lmodMixin := LmodMixin scaleA scale1 scaleDr scaleDl.
- -
-End Lmodule.
- -
-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 } → Lalgebra.axiom mulB.
- -
-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 : comRingType) (A : algType R) (B : lalgType R) (f : B → A) :
-    phant B → injective f → {morph f : x y / x × y } → scalable f →
-  @Algebra.axiom R B.
- -
-Section UnitRing.
- -
-Definition cast_ringType (Q : ringType) T (QeqT : Q = T :> Type) :=
-  let cast rQ := let: erefl in _ = T := QeqT return Ring.class_of T in rQ in
-  Ring.Pack (cast (Ring.class Q)).
- -
-Variables (R : unitRingType) (S : {pred R }).
-Variables (ringS : divringPred S) (kS : keyed_pred ringS).
- -
-Variables (T : subType (mem kS)) (Q : ringType) (QeqT : Q = T :> Type).
- -
-Let inT x Sx : T := Sub x Sx.
-Let invT (u : T) := inT (rpredVr (valP u)).
-Let unitT := [qualify a u : T | val u \is a unit ].
-Let T' := cast_ringType QeqT.
- -
-Hypothesis val1 : val (1 : T') = 1.
-Hypothesis valM : {morph (val : T' → R ) : x y / x × y }.
- -
-Fact mulVr :
-  {in (unitT : {pred T'}), left_inverse (1 : T') invT (@mul T')}.
- -
-Fact mulrV : {in unitT , right_inverse (1 : T') invT (@mul T')}.
- -
-Fact unitP (u v : T') : v × u = 1 ∧ u × v = 1 → u \in unitT.
- -
-Fact unit_id : {in [predC unitT ], invT =1 id }.
- -
-Definition unitRingMixin := UnitRingMixin mulVr mulrV unitP unit_id.
- -
-End UnitRing.
- -
-Lemma idomainMixin (R : idomainType) (T : ringType) (f : T → R) :
-    phant T → injective f → f 0 = 0 → {morph f : u v / u × v } →
-  @IntegralDomain.axiom T.
- -
-Lemma fieldMixin (F : fieldType) (K : unitRingType) (f : K → F) :
-    phant K → injective f → f 0 = 0 → {mono f : u / u \in unit } →
-  @Field.mixin_of K.
- -
-Module Exports.
- -
-Notation "[ 'zmodMixin' 'of' U 'by' <: ]" := (zmodMixin (Phant U))
-  (at level 0, format "[ 'zmodMixin' 'of' U 'by' <: ]") : form_scope.
-Notation "[ 'ringMixin' 'of' R 'by' <: ]" :=
-  (@ringMixin _ _ _ _ _ _ (@erefl Type R%type) (rrefl _))
-  (at level 0, format "[ 'ringMixin' 'of' R 'by' <: ]") : form_scope.
-Notation "[ 'lmodMixin' 'of' U 'by' <: ]" :=
-  (@lmodMixin _ _ _ _ _ _ _ (@erefl Type U%type) (rrefl _))
-  (at level 0, format "[ 'lmodMixin' 'of' U 'by' <: ]") : form_scope.
-Notation "[ 'lalgMixin' 'of' A 'by' <: ]" :=
-  ((lalgMixin (Phant A) val_inj (rrefl _)) *%R (rrefl _))
-  (at level 0, format "[ 'lalgMixin' 'of' A 'by' <: ]") : form_scope.
-Notation "[ 'comRingMixin' 'of' R 'by' <: ]" :=
-  (comRingMixin (Phant R) val_inj (rrefl _))
-  (at level 0, format "[ 'comRingMixin' 'of' R 'by' <: ]") : form_scope.
-Notation "[ 'algMixin' 'of' A 'by' <: ]" :=
-  (algMixin (Phant A) val_inj (rrefl _) (rrefl _))
-  (at level 0, format "[ 'algMixin' 'of' A 'by' <: ]") : form_scope.
-Notation "[ 'unitRingMixin' 'of' R 'by' <: ]" :=
-  (@unitRingMixin _ _ _ _ _ _ (@erefl Type R%type) (erefl _) (rrefl _))
-  (at level 0, format "[ 'unitRingMixin' 'of' R 'by' <: ]") : form_scope.
-Notation "[ 'idomainMixin' 'of' R 'by' <: ]" :=
-  (idomainMixin (Phant R) val_inj (erefl _) (rrefl _))
-  (at level 0, format "[ 'idomainMixin' 'of' R 'by' <: ]") : form_scope.
-Notation "[ 'fieldMixin' 'of' F 'by' <: ]" :=
-  (fieldMixin (Phant F) val_inj (erefl _) (frefl _))
-  (at level 0, format "[ 'fieldMixin' 'of' F 'by' <: ]") : form_scope.
- -
-End Exports.
- -
-End SubType.
- -
-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.
-Definition opprK := @opprK.
-Definition oppr_inj := @oppr_inj.
-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 telescope_sumr := telescope_sumr.
-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 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 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 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 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 prodr_const := prodr_const.
-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 := 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 commrV := commrV.
-Definition unitrE := unitrE.
-Definition invrK := @invrK.
-Definition invr_inj := @invr_inj.
-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 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 rpredMNn := rpredMNn.
-Definition rpredDr := rpredDr.
-Definition rpredDl := rpredDl.
-Definition rpredBr := rpredBr.
-Definition rpredBl := rpredBl.
-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 rpredZsign := rpredZsign.
-Definition rpredZnat := rpredZnat.
-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 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 addf_div := addf_div.
-Definition mulf_div := mulf_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 raddf0 := raddf0.
-Definition raddf_eq0 := raddf_eq0.
-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_additive := can2_additive.
-Definition bij_additive := bij_additive.
-Definition rmorph0 := rmorph0.
-Definition rmorphN := rmorphN.
-Definition rmorphD := rmorphD.
-Definition rmorphB := rmorphB.
-Definition rmorph_sum := rmorph_sum.
-Definition rmorphMn := rmorphMn.
-Definition rmorphMNn := rmorphMNn.
-Definition rmorphismP := rmorphismP.
-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 rmorphX := rmorphX.
-Definition rmorphN1 := rmorphN1.
-Definition rmorph_sign := rmorph_sign.
-Definition rmorph_char := rmorph_char.
-Definition can2_rmorphism := can2_rmorphism.
-Definition bij_rmorphism := bij_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.
-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 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 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_linear := can2_linear.
-Definition bij_linear := bij_linear.
-Definition rmorph_alg := rmorph_alg.
-Definition lrmorphismP := lrmorphismP.
-Definition can2_lrmorphism := can2_lrmorphism.
-Definition bij_lrmorphism := bij_lrmorphism.
-Definition imaginary_exists := imaginary_exists.
- -
-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).
- -
-End GRing.
- -
-Export Zmodule.Exports Ring.Exports Lmodule.Exports Lalgebra.Exports.
-Export Additive.Exports RMorphism.Exports Linear.Exports LRMorphism.Exports.
-Export ComRing.Exports Algebra.Exports UnitRing.Exports UnitAlgebra.Exports.
-Export ComUnitRing.Exports IntegralDomain.Exports Field.Exports.
-Export DecidableField.Exports ClosedField.Exports.
-Export Pred.Exports SubType.Exports.
-Notation QEdecFieldMixin := QEdecFieldMixin.
- -
-Notation "0" := (zero _) : ring_scope.
-Notation "-%R" := (@opp _) : ring_scope.
-Notation "- x" := (opp x) : ring_scope.
-Notation "+%R" := (@add _).
-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.
-Notation "[ 'char' R ]" := (char (Phant R)) : ring_scope.
-Notation Frobenius_aut chRp := (Frobenius_aut chRp).
-Notation "*%R" := (@mul _).
-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 _ _).
-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_head tt f g) : ring_scope.
-Notation "f \- g" := (sub_fun_head tt f g) : ring_scope.
-Notation "a \*: f" := (scale_fun_head tt a f) : ring_scope.
-Notation "x \*o f" := (mull_fun_head tt x f) : ring_scope.
-Notation "x \o* f" := (mulr_fun_head tt x f) : ring_scope.
- -
-Notation "\sum_ ( i <- r | P ) F" :=
-  (\big [+%R /0%R]_(i <- r | P%B) F%R) : ring_scope.
-Notation "\sum_ ( i <- r ) F" :=
-  (\big [+%R /0%R]_(i <- r) F%R) : ring_scope.
-Notation "\sum_ ( m <= i < n | P ) F" :=
-  (\big [+%R /0%R]_(m ≤ i < n | P%B) F%R) : ring_scope.
-Notation "\sum_ ( m <= i < n ) F" :=
-  (\big [+%R /0%R]_(m ≤ i < n) F%R) : ring_scope.
-Notation "\sum_ ( i | P ) F" :=
-  (\big [+%R /0%R]_(i | P%B) F%R) : ring_scope.
-Notation "\sum_ i F" :=
-  (\big [+%R /0%R]_i F%R) : ring_scope.
-Notation "\sum_ ( i : t | P ) F" :=
-  (\big [+%R /0%R]_(i : t | P%B) F%R) (only parsing) : ring_scope.
-Notation "\sum_ ( i : t ) F" :=
-  (\big [+%R /0%R]_(i : t) F%R) (only parsing) : ring_scope.
-Notation "\sum_ ( i < n | P ) F" :=
-  (\big [+%R /0%R]_(i < n | P%B) F%R) : ring_scope.
-Notation "\sum_ ( i < n ) F" :=
-  (\big [+%R /0%R]_(i < n) F%R) : ring_scope.
-Notation "\sum_ ( i 'in' A | P ) F" :=
-  (\big [+%R /0%R]_(i in A | P%B) F%R) : ring_scope.
-Notation "\sum_ ( i 'in' A ) F" :=
-  (\big [+%R /0%R]_(i in A) F%R) : ring_scope.
- -
-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.
- -
-Canonical add_monoid.
-Canonical add_comoid.
-Canonical mul_monoid.
-Canonical mul_comoid.
-Canonical muloid.
-Canonical addoid.
- -
-Canonical locked_additive.
-Canonical locked_rmorphism.
-Canonical locked_linear.
-Canonical locked_lrmorphism.
-Canonical idfun_additive.
-Canonical idfun_rmorphism.
-Canonical idfun_linear.
-Canonical idfun_lrmorphism.
-Canonical comp_additive.
-Canonical comp_rmorphism.
-Canonical comp_linear.
-Canonical comp_lrmorphism.
-Canonical opp_additive.
-Canonical opp_linear.
-Canonical scale_additive.
-Canonical scale_linear.
-Canonical null_fun_additive.
-Canonical null_fun_linear.
-Canonical scale_fun_additive.
-Canonical scale_fun_linear.
-Canonical add_fun_additive.
-Canonical add_fun_linear.
-Canonical sub_fun_additive.
-Canonical sub_fun_linear.
-Canonical mull_fun_additive.
-Canonical mull_fun_linear.
-Canonical mulr_fun_additive.
-Canonical mulr_fun_linear.
-Canonical Frobenius_aut_additive.
-Canonical Frobenius_aut_rmorphism.
-Canonical in_alg_additive.
-Canonical in_alg_rmorphism.
- -
-Notation "R ^c" := (converse R) (at level 2, format "R ^c") : type_scope.
-Canonical converse_eqType.
-Canonical converse_choiceType.
-Canonical converse_zmodType.
-Canonical converse_ringType.
-Canonical converse_unitRingType.
- -
-Notation "R ^o" := (regular R) (at level 2, format "R ^o") : type_scope.
-Canonical regular_eqType.
-Canonical regular_choiceType.
-Canonical regular_zmodType.
-Canonical regular_ringType.
-Canonical regular_lmodType.
-Canonical regular_lalgType.
-Canonical regular_comRingType.
-Canonical regular_algType.
-Canonical regular_unitRingType.
-Canonical regular_comUnitRingType.
-Canonical regular_unitAlgType.
-Canonical regular_idomainType.
-Canonical regular_fieldType.
- -
-Canonical unit_keyed.
-Canonical unit_opprPred.
-Canonical unit_mulrPred.
-Canonical unit_smulrPred.
-Canonical unit_divrPred.
-Canonical unit_sdivrPred.
- -
- -
-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 FinFunZmod.
- -
-Variable (aT : finType) (rT : zmodType).
-Implicit Types f g : {ffun aT → rT }.
- -
-Definition ffun_zero := [ffun a : aT ⇒ (0 : rT )].
-Definition ffun_opp f := [ffun a ⇒ - f a ].
-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.
- Fact ffun_addN : left_inverse ffun_zero ffun_opp ffun_add.
- -
-Definition ffun_zmodMixin :=
-  Zmodule.Mixin ffun_addA ffun_addC ffun_add0 ffun_addN.
-Canonical ffun_zmodType := Eval hnf in ZmodType _ ffun_zmodMixin.
- -
-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 FinFunZmod.
- -
-Section FinFunRing.
- -
-
- -
- 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 : ringType) (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 ffun1_nonzero : ffun_one != 0.
- -
-Definition ffun_ringMixin :=
-  RingMixin ffun_mulA ffun_mul_1l ffun_mul_1r ffun_mul_addl ffun_mul_addr
-            ffun1_nonzero.
-Definition ffun_ringType :=
-  Eval hnf in RingType {ffun aT → R } ffun_ringMixin.
- -
-End FinFunRing.
- -
-Section FinFunComRing.
- -
-Variable (aT : finType) (R : comRingType) (a : aT).
- -
-Fact ffun_mulC : commutative (@ffun_mul aT R).
- -
-Definition ffun_comRingType :=
-  Eval hnf in ComRingType (ffun_ringType R 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 }.
- -
-Definition ffun_lmodMixin :=
-  LmodMixin ffun_scaleA ffun_scale1 ffun_scale_addr ffun_scale_addl.
-Canonical ffun_lmodType :=
-  Eval hnf in LmodType R {ffun aT → rT } ffun_lmodMixin.
- -
-End FinFunLmod.
- -
-
- -
- External direct product. -
-
-Section PairZmod.
- -
-Variables M1 M2 : zmodType.
- -
-Definition opp_pair (x : M1 × M2) := (- x .1 , - x .2 ).
-Definition add_pair (x y : M1 × M2) := (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.
- -
-Fact pair_addN : left_inverse (0, 0) opp_pair add_pair.
- -
-Definition pair_zmodMixin := ZmodMixin pair_addA pair_addC pair_add0 pair_addN.
-Canonical pair_zmodType := Eval hnf in ZmodType (M1 × M2) pair_zmodMixin.
- -
-End PairZmod.
- -
-Section PairRing.
- -
-Variables R1 R2 : ringType.
- -
-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_one_neq0 : (1, 1) != 0 :> R1 × R2.
- -
-Definition pair_ringMixin :=
-  RingMixin pair_mulA pair_mul1l pair_mul1r pair_mulDl pair_mulDr pair_one_neq0.
-Canonical pair_ringType := Eval hnf in RingType (R1 × R2) pair_ringMixin.
- -
-End PairRing.
- -
-Section PairComRing.
- -
-Variables R1 R2 : comRingType.
- -
-Fact pair_mulC : commutative (@mul_pair R1 R2).
- -
-Canonical pair_comRingType := Eval hnf in ComRingType (R1 × R2) pair_mulC.
- -
-End PairComRing.
- -
-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 }.
- -
-Definition pair_lmodMixin :=
-  LmodMixin pair_scaleA pair_scale1 pair_scaleDr pair_scaleDl.
-Canonical pair_lmodType := Eval hnf in LmodType R (V1 × V2) pair_lmodMixin.
- -
-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.
- Canonical pair_lalgType := Eval hnf in LalgType R (A1 × A2) pair_scaleAl.
- -
-End PairLalg.
- -
-Section PairAlg.
- -
-Variables (R : comRingType) (A1 A2 : algType R).
- -
-Fact pair_scaleAr a (u v : A1 × A2) : a *: (u × v ) = u × (a *: v ).
- Canonical pair_algType := Eval hnf in AlgType R (A1 × A2) 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 }.
- -
-Definition pair_unitRingMixin :=
-  UnitRingMixin pair_mulVl pair_mulVr pair_unitP pair_invr_out.
-Canonical pair_unitRingType :=
-  Eval hnf in UnitRingType (R1 × R2) pair_unitRingMixin.
- -
-End PairUnitRing.
- -
-Canonical pair_comUnitRingType (R1 R2 : comUnitRingType) :=
-  Eval hnf in [comUnitRingType of R1 × R2 ].
- -
-Canonical pair_unitAlgType (R : comUnitRingType) (A1 A2 : unitAlgType R) :=
-  Eval hnf in [unitAlgType R of A1 × A2 ].
- -
-
-