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 : NB: The documentation is currently being reworked. Main guideline: it should focus on describing factories (and mixins which are a special case).

Zmodule (additive abelian groups):

zmodType == interface type for Zmodule structure. 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. List of factories (to use with HB.instance Definition _ := )

• IsZmodule.Build T addA addC add0x addNx Requires a choiceType on T and declares a Zmodule on T from the algebraic properties of its operations. NB: we have removed the notation ZmodMixin and used IsZmodule.Build
• PreZmodule.Build T injf f0 fN fD Requires a choiceType on T and declares a Zmodule on T from an injection into a Zmodule and morphism properties

Ring (non-commutative rings):

ringType == interface type for a Ring 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. <number> == <number>%:R with <number> a sequence of digits x * y == the ring product of x and y. \prod<range> e == iterated product for a ring (cf bigop.v). x ^+ n == x to the nth power with n in nat (non-negative), i.e., x * (x * .. (x * x)..) (n factors); x ^+ 1 is thus convertible to x, and x ^+ 2 to x * x. GRing.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 R] has at most one element, and is implemented as a pred_nat collective predicate (see prime.v); thus the statement p \in [char R] can be read as `R has characteristic p', while [char R] =i pred0 means `R has characteristic 0' when R is a field. Frobenius_aut chRp == the Frobenius automorphism mapping x in R to x ^+ p, where chRp : p \in [char R] is a proof that R has (non-zero) characteristic p. mulr_closed S <-> collective predicate S is closed under finite products (1 and x * y in S for x, y in S). 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. List of factories (to use with HB.instance Definition _ := )

• Zmodule_isRing.Build T mulA mul1x mulx1 mulDx mulxD nonzero1 Requires a Zmodule on T and declares a ring on T using the algebraic properties of its multiplicative operators NB: we have removed the notation RingMixin and used Zmodule_isRing.Build instead
• IsRing.Build zero opp add one mul addrA addrC add0r addNr mulrA mul1r mulr1 mulrDl mulrDr oner_neq0 Requires a choiceType on T and declares a ringType on T from the properties of the additive and multiplicative operators
  • PreRing.Build T injf f1 fM Requires a zmodType on T and declares a ringType on T from an injection into a ringType and morphism properties
  * 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.

[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. List of factories (to use with HB.instance Definition _ := )

• Ring_hasCommutativeMul.Build T mulC Requires a ringType on T and declares a comRingType on T from the commutativity of the multiplication.
• Zmodule_isComRing.Build T mulA mulC mul1x mulDl nonzero1 Requires a zmodType on T and declares a comRingType on T from the algebraic properties of the multiplication. NB: replacement for ComRingMixin that used to construct only a ring
  • PreComRing.Build T injf f1 fM Requires a ringType on T and declares a comRingType on T from an injection into a comRingType and morphism properties
  * UnitRing (Rings whose units have computable inverses): unitRingType == interface type for the UnitRing 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. List of factories (to use with HB.instance Definition _ := )

• Ring_hasMulInverse R unit inv mulVr divrr unitrP invr_out Requires a ring on R and declares a unitRing on R using 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 x itself (property invr_out) NB: replaces "UnitRingMixin mulVr mulrV unitP inv0id"
  • PreUnitRing.Build R injf fM fV Requires a ringType on R and declares a unitRingType on R from an injection into a unitRingType and morphism properties
  * 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). List of factories (to use with HB.instance Definition _ := )

• ComRing_hasMulInverse.Build T mulVp intro_unit inv_out Requires a comRingType on T and declares a comUnitRingType on T from algebraic properties of the inverse

[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. List of factories (to use with HB.instance Definition _ := )

• ComUnitRing_isIntegral.Build T idomAxiom Requires a comUnitRingType on T and declares an integral idomainType on T from the property of no nonzero zero-divisors
  * 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. List of factories (to use with HB.instance Definition _ := )

• IsField.Build R fieldP Requires a unitRingType on R and declares a fieldType on R from the field axiom (every non-zero is a unit).
• ComRing_isField.Build R mulVf invr0 Requires a comRingType on R and declares a fieldType on R from the algeraic properties of the inverse
  * 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 List of factories (to use with HB.instance Definition _ := )

• Field_isDec.Build F satP Requires a FieldType and on R and declares a decFieldType on F from the decidable satifiability theory axiom

TODO : revise name "decidable_of_QE", check explicit arguments.

• decidable_of_QE.build F wf_proj ok_proj Requires a FieldType on F and declares a decFieldType on F from the properties of a quantifier elimination projection function.

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. List of factories (to use with HB.instance Definition _ := )

• Field_isAlgClosed.Build F Requires a FieldType on F and declares a closedFieldType on F from the closure property.

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. [TODO: is this still up-to-date? ] List of factories (to use with HB.instance Definition _ := )

• Zmodule_isLmodule.Build R T scalA scal1x scalDr scalDl builds Requires a ringType on R and a Zmodule on T and declares an Lmodule on R T from the algebraic properties of the
  • PreLmodule.Build R T injf fZ Requires a ringType on R and a Zmodule on T and declares a lmodType on R T from an injection into a lmodType and morphism properties
    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. List of factories (to use with HB.instance Definition _ := )

• Lmodule_isLalgebra.Build R T scalAl Requires a ringType on R and on T, and an Lmodule on R T and declares an Lalgebra on R T from the associativity of scaling
  • PreLalgebra.Build R T injf fM fZ Requires a ringType on T and and a Lmodule on R T and declares a lalgType on R T from an injection into a lalgType and morphism properties
    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. List of factories (to use with HB.instance Definition _ := )

• Lalgebra_isAlgebra R V scalrAr Requires a ringType on R and an Lalgebra on R V, and declares an algebra on R V using an algebraic property of the scalar operation Requires a ringType on T and declares a lalgType on R T from an injection into a lalgType and morphism properties
  • Prealgebra.Build R V injf fM fZ Requires a ringType on R and declares a algType on R V from an injection into an algType and morphism properties
  * 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.
  * ComAlgebra (commutative algebra): comAlgType R == interface type for ComAlgebra structure with scalars in R; R should have a comRingType structure. [comAlgType R of V] == a comAlgType R structure for V created by merging canonical algType and comRingType on V.

List of factories (to use with HB.instance Definition _ := )

• is_ComAlgebra.Build R T Requires a comRing on T and an Lalgebra on R T, and declares a commutative algebra on R T
  * ComUnitAlgebra (commutative algebra with computable inverses): comUnitAlgType R == interface type for ComUnitAlgebra structure with scalars in R; R should have a comUnitRingType structure.

[comUnitAlgType R of V] == a comUnitAlgType R structure for V created by merging canonical comAlgType and unitRingType on V. TODO : Adding documentation for substructures 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 is 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. \- g == the function x |-> - f x, canonically linear when f is, 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. f \* g == the function x |-> f x * g x; f \* g 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.

Patch for recurring Coq parser bug: Coq seg faults when a level 200 notation is used as a pattern.

The ``field'' characteristic; the definition, and many of the theorems, has to apply to rings as well; indeed, we need the Frobenius automorphism results for a non commutative ring in the proof of Gorenstein 2.6.3.

Converse ring tag.

TODO: fix the type for the exported operation