From ed05182cece6bb3706e09b2ce14af4a41a2e8141 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 20 Apr 2018 10:54:22 +0200 Subject: generate the documentation for 1.7 --- docs/htmldoc/mathcomp.algebra.ssralg.html | 6323 +++++++++++++++++++++++++++++ 1 file changed, 6323 insertions(+) create mode 100644 docs/htmldoc/mathcomp.algebra.ssralg.html (limited to 'docs/htmldoc/mathcomp.algebra.ssralg.html') diff --git a/docs/htmldoc/mathcomp.algebra.ssralg.html b/docs/htmldoc/mathcomp.algebra.ssralg.html new file mode 100644 index 0000000..8466ee9 --- /dev/null +++ b/docs/htmldoc/mathcomp.algebra.ssralg.html @@ -0,0 +1,6323 @@ + + + + + +mathcomp.algebra.ssralg + + + + +
+ + + +
+ +

Library mathcomp.algebra.ssralg

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

+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+ +
+ 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, 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.axiom inv == the field axiom (x != 0 -> inv x * x = 1). + FieldUnitMixin mulVx unitP inv0id == builds a *non commutative unit ring* + mixin, using the field axiom to simplify proof + obligations. The carrier type must have a + comRingType canonical structure. + FieldMixin mulVx == builds the field mixin from the field axiom. The + carrier type must have a comRingType structure. + FieldIdomainMixin m == builds an *idomain* mixin from a field mixin m. + FieldType R m == packs the field mixin M into a fieldType. The + carrier type R must be an idomainType. + [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; _ : Type}.
+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 T.
+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) bPack (@Class T b m) T.
+ +
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+ +
+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 yx - y).
+ Lemma addrI : @right_injective V V V +%R.
+ Lemma addIr : @left_injective V V V +%R.
+ Lemma subrI : right_injective (fun x yx - y).
+ Lemma subIr : left_injective (fun x yx - 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 xx *+ n) : x y / x + y}.
+ +
+Lemma mulrnDr x m n : x *+ (m + n) = x *+ m + x *+ n.
+ +
+Lemma mulrnBl n : {morph (fun xx *+ 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 : predPredType 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) 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 R)
+}.
+ +
+Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+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 T.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
+ +
+Definition pack b0 (m0 : mixin_of (@Zmodule.Pack T b0 T)) :=
+  fun bT b & phant_id (Zmodule.class bT) b
+  fun m & phant_id m0 mPack (@Class T b m) T.
+ +
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition zmodType := @Zmodule.Pack cT xclass xT.
+ +
+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 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 xx ^+ 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.
+ +
+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 : predPredType 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 V)
+}.
+ +
+Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}.
+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 T.
+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 T)) :=
+  fun bT b & phant_id (Zmodule.class bT) b
+  fun m & phant_id m0 mPack phR (@Class T b m) T.
+ +
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition zmodType := @Zmodule.Pack cT xclass xT.
+ +
+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 : predPredType 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 T);
+  ext : @axiom R (Lmodule.Pack _ (Lmodule.Class mixin) T) (Ring.mul base)
+}.
+Definition base2 R m := Lmodule.Class (@mixin R m).
+ +
+Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}.
+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 T.
+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 T) 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) T.
+ +
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition zmodType := @Zmodule.Pack cT xclass xT.
+Definition ringType := @Ring.Pack cT xclass xT.
+Definition lmodType := @Lmodule.Pack R phR cT xclass xT.
+Definition lmod_ringType := @Lmodule.Pack R phR ringType xclass xT.
+ +
+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 bmulrDl 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 : predPredType 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 aopB _).
+ +
+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; _ : Type}.
+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 T.
+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 mPack (@Class T b m) T.
+ +
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition zmodType := @Zmodule.Pack cT xclass xT.
+Definition ringType := @Ring.Pack cT xclass xT.
+ +
+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 xx ^+ 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 T)
+}.
+ +
+Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}.
+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 T.
+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 axPack phR (@Class T b ax) T.
+ +
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition zmodType := @Zmodule.Pack cT xclass xT.
+Definition ringType := @Ring.Pack cT xclass xT.
+Definition lmodType := @Lmodule.Pack R phR cT xclass xT.
+Definition lalgType := @Lalgebra.Pack R phR cT xclass xT.
+ +
+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) 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 R)
+}.
+ +
+Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+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 T.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
+ +
+Definition pack b0 (m0 : mixin_of (@Ring.Pack T b0 T)) :=
+  fun bT b & phant_id (Ring.class bT) b
+  fun m & phant_id m0 mPack (@Class T b m) T.
+ +
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition zmodType := @Zmodule.Pack cT xclass xT.
+Definition ringType := @Ring.Pack cT xclass xT.
+ +
+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 yx / y)}.
+ +
+Lemma divIr : {in unit, left_injective (fun x yx / 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_class) : 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 : predPredType 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 R)
+}.
+Definition base2 R m := UnitRing.Class (@mixin R m).
+ +
+Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+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) T.
+ +
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition zmodType := @Zmodule.Pack cT xclass xT.
+Definition ringType := @Ring.Pack cT xclass xT.
+Definition comRingType := @ComRing.Pack cT xclass xT.
+Definition unitRingType := @UnitRing.Pack cT xclass xT.
+Definition com_unitRingType := @UnitRing.Pack comRingType xclass xT.
+ +
+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 T)
+}.
+Definition base2 R m := UnitRing.Class (@mixin R m).
+ +
+Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}.
+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) T.
+ +
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition zmodType := @Zmodule.Pack cT xclass xT.
+Definition ringType := @Ring.Pack cT xclass xT.
+Definition unitRingType := @UnitRing.Pack cT xclass xT.
+Definition lmodType := @Lmodule.Pack R phR cT xclass xT.
+Definition lalgType := @Lalgebra.Pack R phR cT xclass xT.
+Definition algType := @Algebra.Pack R phR cT xclass xT.
+Definition lmod_unitRingType := @Lmodule.Pack R phR unitRingType xclass xT.
+Definition lalg_unitRingType := @Lalgebra.Pack R phR unitRingType xclass xT.
+Definition alg_unitRingType := @Algebra.Pack R phR unitRingType xclass xT.
+ +
+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 yx / 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 : predPredType 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 : predPredType 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 : predPredType 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 : predPredType 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 : predPredType 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_iif i == s.1 then s.2 else t
+  | _%:T | _%:Rt
+  | t1 + t2tsubst t1 s + tsubst t2 s
+  | - t1- tsubst t1 s
+  | t1 *+ ntsubst t1 s *+ n
+  | t1 × t2tsubst t1 s × tsubst t2 s
+  | t1^-1(tsubst t1 s)^-1
+  | t1 ^+ ntsubst t1 s ^+ n
+  end%T.
+ +
+Fixpoint fsubst (f : formula R) (s : nat × term R) :=
+  match f with
+  | Bool _f
+  | t1 == t2tsubst t1 s == tsubst t2 s
+  | Unit t1Unit (tsubst t1 s)
+  | f1 f2fsubst f1 s fsubst f2 s
+  | f1 f2fsubst f1 s fsubst f2 s
+  | f1 ==> f2fsubst 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)%Te`_i
+  | (x%:T)%Tx
+  | (n%:R)%Tn%:R
+  | (t1 + t2)%Teval e t1 + eval e t2
+  | (- t1)%T- eval e t1
+  | (t1 *+ n)%Teval e t1 *+ n
+  | (t1 × t2)%Teval e t1 × eval e t2
+  | t1^-1%T(eval e t1)^-1
+  | (t1 ^+ n)%Teval 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 bb
+  | (t1 == t2)%Teval e t1 = eval e t2
+  | Unit t1eval e t1 \in unit
+  | (f1 f2)%Tholds e f1 holds e f2
+  | (f1 f2)%Tholds e f1 holds e f2
+  | (f1 ==> f2)%Tholds 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
+  | _^-1false
+  | t1 + t2 | t1 × t2rterm 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 == t2rterm t1 && rterm t2
+  | Unit t1false
+  | f1 f2 | f1 f2 | f1 ==> f2rformula 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_ii.+1
+  | t1 + t2 | t1 × t2maxn (ub_var t1) (ub_var t2)
+  | - t1 | t1 *+ _ | t1 ^+ _ | t1^-1ub_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 bf
+  | t1 == t2eq0_rform (t1 - t2)
+  | Unit t1eq0_rform (t1 × t1^-1 - 1)
+  | f1 f2to_rform f1 to_rform f2
+  | f1 f2to_rform f1 to_rform f2
+  | f1 ==> f2to_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 ==> f2qf_form f1 && qf_form f2
+  | ¬ f1qf_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 bb
+  | t1 == t2 ⇒ (eval e t1 == eval e t2)%bool
+  | Unit t1eval e t1 \in unit
+  | f1 f2loop f1 && loop f2
+  | f1 f2loop 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 bif 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 R)}.
+ +
+Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+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 T.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
+ +
+Definition pack b0 (m0 : axiom (@Ring.Pack T b0 T)) :=
+  fun bT b & phant_id (ComUnitRing.class bT) b
+  fun m & phant_id m0 mPack (@Class T b m) T.
+ +
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition zmodType := @Zmodule.Pack cT xclass xT.
+Definition ringType := @Ring.Pack cT xclass xT.
+Definition comRingType := @ComRing.Pack cT xclass xT.
+Definition unitRingType := @UnitRing.Pack cT xclass xT.
+Definition comUnitRingType := @ComUnitRing.Pack cT xclass xT.
+ +
+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 iP 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 iP 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 yx / y).
+ +
+Lemma divIf y : y != 0 injective (fun xx / 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 (F : unitRingType) := x : F, x != 0 x \in unit.
+ +
+Lemma IdomainMixin R : mixin_of R IntegralDomain.axiom R.
+ +
+Section Mixins.
+ +
+Variables (R : comRingType) (inv : R R).
+ +
+Definition axiom := x, x != 0 inv x × x = 1.
+Hypothesis mulVx : axiom.
+Hypothesis 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 mulVx intro_unit inv_out.
+ +
+Lemma Mixin : mixin_of (UnitRing.Pack (UnitRing.Class UnitMixin) R).
+ +
+End Mixins.
+ +
+Section ClassDef.
+ +
+Record class_of (F : Type) : Type := Class {
+  base : IntegralDomain.class_of F;
+  mixin : mixin_of (UnitRing.Pack base F)
+}.
+ +
+Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+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 T.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
+ +
+Definition pack b0 (m0 : mixin_of (@UnitRing.Pack T b0 T)) :=
+  fun bT b & phant_id (IntegralDomain.class bT) b
+  fun m & phant_id m0 mPack (@Class T b m) T.
+ +
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition zmodType := @Zmodule.Pack cT xclass xT.
+Definition ringType := @Ring.Pack cT xclass xT.
+Definition comRingType := @ComRing.Pack cT xclass xT.
+Definition unitRingType := @UnitRing.Pack cT xclass xT.
+Definition comUnitRingType := @ComUnitRing.Pack cT xclass xT.
+Definition idomainType := @IntegralDomain.Pack cT xclass xT.
+ +
+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 yx / 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_class) (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 F)}.
+ +
+Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+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 T.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
+ +
+Definition pack b0 (m0 : mixin_of (@UnitRing.Pack T b0 T)) :=
+  fun bT b & phant_id (Field.class bT) b
+  fun m & phant_id m0 mPack (@Class T b m) T.
+ +
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition zmodType := @Zmodule.Pack cT xclass xT.
+Definition ringType := @Ring.Pack cT xclass xT.
+Definition comRingType := @ComRing.Pack cT xclass xT.
+Definition unitRingType := @UnitRing.Pack cT xclass xT.
+Definition comUnitRingType := @ComUnitRing.Pack cT xclass xT.
+Definition idomainType := @IntegralDomain.Pack cT xclass xT.
+Definition fieldType := @Field.Pack cT xclass xT.
+ +
+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 F)}.
+ +
+Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+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 T.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
+ +
+Definition pack b0 (m0 : axiom (@Ring.Pack T b0 T)) :=
+  fun bT b & phant_id (DecidableField.class bT) b
+  fun m & phant_id m0 mPack (@Class T b m) T.
+ +
+
+ +
+ There should eventually be a constructor from polynomial resolution + that builds the DecidableField mixin using QE. +
+
+ +
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition zmodType := @Zmodule.Pack cT xclass xT.
+Definition ringType := @Ring.Pack cT xclass xT.
+Definition comRingType := @ComRing.Pack cT xclass xT.
+Definition unitRingType := @UnitRing.Pack cT xclass xT.
+Definition comUnitRingType := @ComUnitRing.Pack cT xclass xT.
+Definition idomainType := @IntegralDomain.Pack cT xclass xT.
+Definition fieldType := @Field.Pack cT xclass xT.
+Definition decFieldType := @DecidableField.Pack cT class xT.
+ +
+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 : predPredType 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 : predPredType 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)) T.
+ +
+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 : predPredType 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)) T.
+ +
+Variables (R : unitRingType) (S : predPredType 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 : predPredType 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 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].
+ +
+
+
+ + + +
+ + + \ No newline at end of file -- cgit v1.2.3