Library ssralg

   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.

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.comm x y <-> x and y commute, i.e., x * y = y * x. [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.

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 obligagtions. [comRingType of R for S] == R-clone of the comRingType structure S. [comRingType of R] == clone of a canonical comRingType structure on R.

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. GRing.unit x <=> 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.

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.

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.

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, and the construct Pick p_f t_f e_f can be used to emulate the pick function defined in fintype.v. 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.

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.

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 a *: 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.

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.

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. In addition to this strcture 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 maps scaling on U to scaling on V, a *: _ to a*: _. U and V must both have lmodType R structures, for the same ringType R. linear f <-> f of type U -> V is linear, i.e., f maps linear combinations in U to 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}. lmorphism f <-> f is both additive and scalable. This is in fact equivalent to linear f, although somewhat less convenient to prove. {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. Linear lin_f == packs lin_f : lmorphism f into a linear function structure of type {linear U -> V}. As linear f coerces to lmorphism f, Linear can also be used with lin_f : linear f (indeed, that is the recommended usage). AddLinear scal_f == packs scal_f : scalable f into a {linear U -> V} structure; f must already have an additive structure; lin_f : linear f may be used instead of scal_f. [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. -> Similarly to Ring morphisms, additive properties are specialized for linear functions.

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 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 scal_f == packs scal_f : scalable f into a linear morphism structure of type {lrmorphism U -> V}; f must already have a Ring morphism structure, and lin_f : linear f may be used instead of scal_f. [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. M -- ring multiplication, as in invMf : (x * y)^-1 = x^-1 * y^-1, Mn -- ring by nat multiplication, as in addfMn : 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.


Reserved Notation "+%R" (at level 0).
Reserved Notation "-%R" (at level 0).
Reserved Notation "*%R" (at level 0).
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 }.
Local Coercion base : class_of >-> Choice.class_of.

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
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.

Definition pack m :=
  fun bT b & phant_id (Choice.class bT) b => Pack (@Class T b m) T.

Definition eqType := Equality.Pack class cT.
Definition choiceType := Choice.Pack class cT.

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 Structure eqType.
Coercion choiceType : type >-> Choice.type.
Canonical Structure 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).

Local Notation "0" := (zero _) : ring_scope.
Local Notation "-%R" := (@opp _) : ring_scope.
Local Notation "- x" := (opp x) : ring_scope.
Local Notation "+%R" := (@add _) : ring_scope.
Local Notation "x + y" := (add x y) : ring_scope.
Local Notation "x - y" := (x + - y) : ring_scope.

Definition natmul V x n := nosimpl iterop _ n +%R x (zero V).

Local Notation "x *+ n" := (natmul x n) : ring_scope.
Local Notation "x *- n" := (- (x *+ n)) : ring_scope.

Local Notation "\sum_ ( i <- r | P ) F" := (\big[+%R/0]_(i <- r | P) F).
Local Notation "\sum_ ( m <= i < n ) F" := (\big[+%R/0]_(m <= i < n) F).
Local Notation "\sum_ ( i < n ) F" := (\big[+%R/0]_(i < n) F).
Local Notation "\sum_ ( i \in A ) F" := (\big[+%R/0]_(i \in A) F).

Local Notation "s `_ i" := (nth 0 s i) : ring_scope.

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 Structure add_monoid := Monoid.Law addrA add0r addr0.
Canonical Structure add_comoid := Monoid.ComLaw addrC.

Lemma addrCA : @left_commutative V V +%R.

Lemma addrAC : @right_commutative V V +%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 addrI : @right_injective V V V +%R.
Lemma addIr : @left_injective V V V +%R.
Lemma opprK : @involutive V -%R.
Lemma oppr0 : -0 = 0 :> V.
Lemma oppr_eq0 : forall x, (- x == 0) = (x == 0).

Lemma subr0 : forall x, x - 0 = x.

Lemma sub0r : forall x, 0 - x = - x.

Lemma oppr_add : {morph -%R: x y / x + y : V}.

Lemma oppr_sub : forall x y, - (x - y) = y - x.

Lemma subr_eq : forall x y z, (x - z == y) = (x == y + z).

Lemma subr_eq0 : forall x y, (x - y == 0) = (x == y).

Lemma addr_eq0 : forall x y, (x + y == 0) = (x == - y).

Lemma eqr_opp : forall x y, (- x == - y) = (x == y).

Lemma eqr_oppC : forall x y, (- x == y) = (x == - y).

Lemma mulr0n : forall x, x *+ 0 = 0.

Lemma mulr1n : forall x, x *+ 1 = x.

Lemma mulr2n : forall x, x *+ 2 = x + x.

Lemma mulrS : forall x n, x *+ n.+1 = x + x *+ n.

Lemma mulrSr : forall x n, x *+ n.+1 = x *+ n + x.

Lemma mulrb : forall x (b : bool), x *+ b = (if b then x else 0).

Lemma mul0rn : forall n, 0 *+ n = 0 :> V.

Lemma mulNrn : forall x n, (- x) *+ n = x *- n.

Lemma mulrn_addl : forall n, {morph (fun x => x *+ n) : x y / x + y}.

Lemma mulrn_addr : forall x m n, x *+ (m + n) = x *+ m + x *+ n.

Lemma mulrn_subl : forall n, {morph (fun x => x *+ n) : x y / x - y}.

Lemma mulrn_subr : forall x m n, n <= m -> x *+ (m - n) = x *+ m - x *+ n.

Lemma mulrnA : forall x m n, x *+ (m * n) = x *+ m *+ n.

Lemma mulrnAC : forall x m n, x *+ m *+ n = x *+ n *+ m.

Lemma sumr_opp : forall I r P (F : I -> V),
  (\sum_(i <- r | P i) - F i = - (\sum_(i <- r | P i) F i)).

Lemma sumr_sub : forall 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 sumr_muln : forall I r P (F : I -> V) n,
  \sum_(i <- r | P i) F i *+ n = (\sum_(i <- r | P i) F i) *+ n.

Lemma sumr_muln_r : forall 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 : forall (I : finType) (A : pred I) (x : V),
  \sum_(i \in A) x = x *+ #|A|.

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)
}.
Local Coercion base : class_of >-> Zmodule.class_of.

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
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.

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 m => Pack (@Class T b m) T.

Definition eqType := Equality.Pack class cT.
Definition choiceType := Choice.Pack class cT.
Definition zmodType := Zmodule.Pack class cT.

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 Structure eqType.
Coercion choiceType : type >-> Choice.type.
Canonical Structure choiceType.
Coercion zmodType : type >-> Zmodule.type.
Canonical Structure 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).
Definition comm R x y := @mul R x y = mul y x.

Local Notation "1" := (one _) : ring_scope.
Local Notation "- 1" := (- (1)) : ring_scope.
Local Notation "n %:R" := (1 *+ n) : ring_scope.
Local Notation "*%R" := (@mul _).
Local Notation "x * y" := (mul x y) : ring_scope.
Local Notation "x ^+ n" := (exp x n) : ring_scope.

Local Notation "\prod_ ( i <- r | P ) F" := (\big[*%R/1]_(i <- r | P) F).
Local Notation "\prod_ ( i \in A ) F" := (\big[*%R/1]_(i \in A) F).


 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)].

Local Notation "[ 'char' R ]" := (char (Phant R)) : ring_scope.

 Converse ring tag. 
Definition converse R : Type := R.
Local Notation "R ^c" := (converse R) (at level 2, format "R ^c") : type_scope.

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 mulr_addl : @left_distributive R R *%R +%R.
Lemma mulr_addr : @right_distributive R R *%R +%R.
Lemma nonzero1r : 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 : forall x y, x * (- y) = - (x * y).
Lemma mulNr : forall x y, (- x) * y = - (x * y).
Lemma mulrNN : forall x y, (- x) * (- y) = x * y.
Lemma mulN1r : forall x, -1 * x = - x.
Lemma mulrN1 : forall x, x * -1 = - x.

Canonical Structure mul_monoid := Monoid.Law mulrA mul1r mulr1.
Canonical Structure muloid := Monoid.MulLaw mul0r mulr0.
Canonical Structure addoid := Monoid.AddLaw mulr_addl mulr_addr.

Lemma mulr_suml : forall 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 : forall I r P (F : I -> R) x,
  \sum_(i <- r | P i) x * F i = x * (\sum_(i <- r | P i) F i).

Lemma mulr_subl : forall x y z, (y - z) * x = y * x - z * x.

Lemma mulr_subr : forall x y z, x * (y - z) = x * y - x * z.

Lemma mulrnAl : forall x y n, (x *+ n) * y = (x * y) *+ n.

Lemma mulrnAr : forall x y n, x * (y *+ n) = (x * y) *+ n.

Lemma mulr_natl : forall x n, n%:R * x = x *+ n.

Lemma mulr_natr : forall x n, x * n%:R = x *+ n.

Lemma natr_add : forall m n, (m + n)%:R = m%:R + n%:R :> R.

Lemma natr_sub : forall m n, n <= m -> (m - n)%:R = m%:R - n%:R :> R.

Definition natr_sum := big_morph (natmul 1) natr_add (mulr0n 1).

Lemma natr_mul : forall m n, (m * n)%:R = m%:R * n%:R :> R.

Lemma expr0 : forall x, x ^+ 0 = 1.

Lemma expr1 : forall x, x ^+ 1 = x.

Lemma expr2 : forall x, x ^+ 2 = x * x.

Lemma exprS : forall x n, x ^+ n.+1 = x * x ^+ n.

Lemma exp1rn : forall n, 1 ^+ n = 1 :> R.

Lemma exprn_addr : forall x m n, x ^+ (m + n) = x ^+ m * x ^+ n.

Lemma exprSr : forall x n, x ^+ n.+1 = x ^+ n * x.

Lemma commr_sym : forall x y, comm x y -> comm y x.

Lemma commr_refl : forall x, comm x x.

Lemma commr0 : forall x, comm x 0.

Lemma commr1 : forall x, comm x 1.

Lemma commr_opp : forall x y, comm x y -> comm x (- y).

Lemma commrN1 : forall x, comm x (-1).

Lemma commr_add : forall x y z,
  comm x y -> comm x z -> comm x (y + z).

Lemma commr_muln : forall x y n, comm x y -> comm x (y *+ n).

Lemma commr_mul : forall x y z,
  comm x y -> comm x z -> comm x (y * z).

Lemma commr_nat : forall x n, comm x n%:R.

Lemma commr_exp : forall x y n, comm x y -> comm x (y ^+ n).

Lemma commr_exp_mull : forall x y n,
  comm x y -> (x * y) ^+ n = x ^+ n * y ^+ n.

Lemma commr_sign : forall x n, comm x ((-1) ^+ n).

Lemma exprn_mulnl : forall x m n, (x *+ m) ^+ n = x ^+ n *+ (m ^ n) :> R.

Lemma exprn_mulr : forall x m n, x ^+ (m * n) = x ^+ m ^+ n.

Lemma exprn_mod : forall n x i, x ^+ n = 1 -> x ^+ (i %% n) = x ^+ i.

Lemma exprn_dvd : forall n x i, x ^+ n = 1 -> n %| i -> x ^+ i = 1.

Lemma natr_exp : forall n k, (n ^ k)%:R = n%:R ^+ k :> R.

Lemma signr_odd : forall n, (-1) ^+ (odd n) = (-1) ^+ n :> R.

Lemma signr_eq0 : forall n, ((-1) ^+ n == 0 :> R) = false.

Lemma signr_addb : forall b1 b2,
  (-1) ^+ (b1 (+) b2) = (-1) ^+ b1 * (-1) ^+ b2 :> R.

Lemma exprN : forall x n, (- x) ^+ n = (-1) ^+ n * x ^+ n :> R.

Lemma sqrrN : forall x, (- x) ^+ 2 = x ^+ 2.

Lemma prodr_const : forall (I : finType) (A : pred I) (x : R),
  \prod_(i \in A) x = x ^+ #|A|.

Lemma prodr_exp_r : forall x I r P (F : I -> nat),
  \prod_(i <- r | P i) x ^+ F i = x ^+ (\sum_(i <- r | P i) F i).

Lemma prodr_opp : forall (I : finType) (A : pred I) (F : I -> R),
  \prod_(i \in A) - F i = (- 1) ^+ #|A| * \prod_(i \in A) F i.

Lemma exprn_addl_comm : forall x y n, comm x y ->
  (x + y) ^+ n = \sum_(i < n.+1) (x ^+ (n - i) * y ^+ i) *+ 'C(n, i).

Lemma exprn_subl_comm : forall x y n, comm x y ->
  (x - y) ^+ n =
      \sum_(i < n.+1) ((-1) ^+ i * x ^+ (n - i) * y ^+ i) *+ 'C(n, i).

Lemma subr_expn_comm : forall x y n, comm x y ->
  x ^+ n - y ^+ n = (x - y) * (\sum_(i < n) x ^+ (n.-1 - i) * y ^+ i).

Lemma exprn_add1 : forall x n,
  (x + 1) ^+ n = \sum_(i < n.+1) x ^+ i *+ 'C(n, i).

Lemma subr_expn_1 : forall x n, x ^+ n - 1 = (x - 1) * (\sum_(i < n) x ^+ i).

Lemma sqrr_add1 : forall x, (x + 1) ^+ 2 = x ^+ 2 + x *+ 2 + 1.

Lemma sqrr_sub1 : forall x, (x - 1) ^+ 2 = x ^+ 2 - x *+ 2 + 1.

Lemma subr_sqr_1 : forall x, x ^+ 2 - 1 = (x - 1) * (x + 1).

Definition Frobenius_aut p of p \in [char R] := fun x => x ^+ p.

Section FrobeniusAutomorphism.

Variable p : nat.
Hypothesis charFp : p \in [char R].

Lemma charf0 : p%:R = 0 :> R.

Lemma charf_prime : prime p.

Hint Resolve charf_prime.

Lemma dvdn_charf : forall n, (p %| n)%N = (n%:R == 0 :> R).

Lemma charf_eq : [char R] =i (p : nat_pred).

Lemma bin_lt_charf_0 : forall k, 0 < k < p -> 'C(p, k)%:R = 0 :> R.

Local Notation "x ^f" := (Frobenius_aut charFp x).

Lemma Frobenius_autE : forall x, x^f = x ^+ p.

Local Notation fE := Frobenius_autE.

Lemma Frobenius_aut_0 : 0^f = 0.

Lemma Frobenius_aut_1 : 1^f = 1.

Lemma Frobenius_aut_add_comm : forall x y, comm x y -> (x + y)^f = x^f + y^f.

Lemma Frobenius_aut_muln : forall x n, (x *+ n)^f = x^f *+ n.

Lemma Frobenius_aut_nat : forall n, (n%:R)^f = n%:R.

Lemma Frobenius_aut_mul_comm : forall x y, comm x y -> (x * y)^f = x^f * y^f.

Lemma Frobenius_aut_exp : forall x n, (x ^+ n)^f = x^f ^+ n.

Lemma Frobenius_aut_opp : forall x, (- x)^f = - x^f.

Lemma Frobenius_aut_sub_comm : forall x y, comm x y -> (x - y)^f = x^f - y^f.

End FrobeniusAutomorphism.

Canonical Structure converse_eqType := [eqType of R^c].
Canonical Structure converse_choiceType := [choiceType of R^c].
Canonical Structure 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 mulr_addl' x y z := mulr_addr z x y in
  let mulr_addr' x y z := mulr_addl y z x in
  @Ring.Mixin converse_zmodType
    1 mul' mulrA' mulr1 mul1r mulr_addl' mulr_addr' nonzero1r.
Canonical Structure converse_ringType := RingType R^c converse_ringMixin.

End RingTheory.

Module Lmodule.

Structure mixin_of (R : ringType) (V : zmodType) : Type := Mixin {
  scale : R -> V -> V;
  _ : forall a b v, scale a (scale b v) = scale (a * b) v;
  _ : left_id 1 scale;
  _ : right_distributive scale +%R;
  _ : forall 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)
}.
Local Coercion base : class_of >-> Zmodule.class_of.

Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
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.

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 m => Pack phR (@Class T b m) T.

Definition eqType := Equality.Pack class cT.
Definition choiceType := Choice.Pack class cT.
Definition zmodType := Zmodule.Pack class cT.

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 Structure eqType.
Coercion choiceType : type >-> Choice.type.
Canonical Structure choiceType.
Coercion zmodType : type >-> Zmodule.type.
Canonical Structure 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).

Local Notation "*:%R" := (@scale _ _).
Local Notation "a *: v" := (scale a v) : ring_scope.

Section LmoduleTheory.

Variables (R : ringType) (V : lmodType R).
Implicit Type a b c : R.
Implicit Type u v : V.

Local Notation "*:%R" := (@scale R V).

Lemma scalerA : forall a b v, a *: (b *: v) = a * b *: v.

Lemma scale1r : @left_id R V 1 *:%R.

Lemma scaler_addr : forall a, {morph *:%R a : u v / u + v}.

Lemma scaler_addl : forall v, {morph *:%R^~ v : a b / a + b}.

Lemma scale0r : forall v, 0 *: v = 0.

Lemma scaler0 : forall a, a *: 0 = 0 :> V.

Lemma scaleNr : forall a v, - a *: v = - (a *: v).

Lemma scaleN1r : forall v, (- 1) *: v = - v.

Lemma scalerN : forall a v, a *: (- v) = - (a *: v).

Lemma scaler_subl : forall a b v, (a - b) *: v = a *: v - b *: v.

Lemma scaler_subr : forall a u v, a *: (u - v) = a *: u - a *: v.

Lemma scaler_nat : forall n v, n%:R *: v = v *+ n.

Lemma scaler_mulrnl : forall a v n, a *: v *+ n = (a *+ n) *: v.

Lemma scaler_mulrnr : forall a v n, a *: v *+ n = a *: (v *+ n).

Lemma scaler_suml : forall 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 : forall 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.

End LmoduleTheory.

Module Lalgebra.

Definition axiom (R : ringType) (V : lmodType R) (mul : V -> V -> V) :=
  forall 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).
Local Coercion base : class_of >-> Ring.class_of.
Local Coercion base2 : class_of >-> Lmodule.class_of.

Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
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.

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 class cT.
Definition choiceType := Choice.Pack class cT.
Definition zmodType := Zmodule.Pack class cT.
Definition ringType := Ring.Pack class cT.
Definition lmodType := Lmodule.Pack phR class cT.
Definition lmod_ringType := @Lmodule.Pack R phR ringType class cT.

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 Structure eqType.
Coercion choiceType : type >-> Choice.type.
Canonical Structure choiceType.
Coercion zmodType : type >-> Zmodule.type.
Canonical Structure zmodType.
Coercion ringType : type >-> Ring.type.
Canonical Structure ringType.
Coercion lmodType : type >-> Lmodule.type.
Canonical Structure lmodType.
Canonical Structure 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). 
Local Notation "k %:A" := (k *: 1) : ring_scope.

 Regular ring algebra tag. 
Definition regular R : Type := R.
Local Notation "R ^o" := (regular R) (at level 2, format "R ^o") : type_scope.

Section LalgebraTheory.

Variables (R : ringType) (A : lalgType R).
Implicit Types x y : A.

Lemma scaler_mull : forall k (x y : A), k *: (x * y) = k *: x * y.

Canonical Structure regular_eqType := [eqType of R^o].
Canonical Structure regular_choiceType := [choiceType of R^o].
Canonical Structure regular_zmodType := [zmodType of R^o].
Canonical Structure regular_ringType := [ringType of R^o].

Definition regular_lmodMixin :=
  let mkMixin := @Lmodule.Mixin R regular_zmodType (@mul R) in
  mkMixin (@mulrA R) (@mul1r R) (@mulr_addr R) (fun v a b => mulr_addl a b v).

Canonical Structure regular_lmodType := LmodType R R^o regular_lmodMixin.
Canonical Structure regular_lalgType :=
  LalgType R R^o (@mulrA regular_ringType).

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}.
Local Coercion apply : map >-> Funclass.

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.
 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 precendence when GRing.Theory is not imported.        
Local Notation in_alg_loc A := (in_alg_head (Phant A)) (only parsing).

Local Notation "\0" := (null_fun _) : ring_scope.
Local Notation "f \+ g" := (add_fun_head tt f g) : ring_scope.
Local Notation "f \- g" := (sub_fun_head tt f g) : ring_scope.
Local Notation "a \*: f" := (scale_fun_head tt a f) : ring_scope.
Local Notation "x \*o f" := (mull_fun_head tt x f) : ring_scope.
Local Notation "x \o* f" := (mulr_fun_head tt x f) : ring_scope.

Section AdditiveTheory.

Section Properties.

Variables (U V : zmodType) (f : {additive U -> V}).

Lemma raddf_sub : {morph f : x y / x - y}.

Lemma raddf0 : f 0 = 0.

Lemma raddfN : {morph f : x / - x}.

Lemma raddfD : {morph f : x y / x + y}.

Lemma raddfMn : forall n, {morph f : x / x *+ n}.

Lemma raddfMNn : forall n, {morph f : x / x *- n}.

Lemma raddf_sum : forall 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 : forall 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.

End Properties.

Section AddFun.

Variables (U V W : zmodType) (f g : {additive V -> W}) (h : {additive U -> V}).

Lemma idfun_is_additive : additive (idfun : U -> U).
Canonical Structure idfun_additive := Additive idfun_is_additive.

Lemma comp_is_additive : additive (f \o h).
Canonical Structure comp_additive := Additive comp_is_additive.

Lemma opp_is_additive : additive (-%R : U -> U).
Canonical Structure opp_additive := Additive opp_is_additive.

Lemma null_fun_is_additive : additive (\0 : U -> V).
Canonical Structure null_fun_additive := Additive null_fun_is_additive.

Lemma add_fun_is_additive : additive (f \+ g).
Canonical Structure add_fun_additive := Additive add_fun_is_additive.

Lemma sub_fun_is_additive : additive (f \- g).
Canonical Structure sub_fun_additive := Additive sub_fun_is_additive.

End AddFun.

Section MulFun.

Variables (R : ringType) (U : zmodType).
Variables (a : R) (f : {additive U -> R}).

Lemma mull_fun_is_additive : additive (a \*o f).
Canonical Structure mull_fun_additive := Additive mull_fun_is_additive.

Lemma mulr_fun_is_additive : additive (a \o* f).
Canonical Structure 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}).

Lemma scale_fun_is_additive : additive (a \*: f).
Canonical Structure scale_fun_additive := Additive scale_fun_is_additive.

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}.
Local Coercion base : class_of >-> additive.

Structure map (phRS : phant (R -> S)) := Pack {apply; _ : class_of apply}.
Local Coercion apply : map >-> Funclass.
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 Structure 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 Structure additive.
End Exports.

End RMorphism.
Include RMorphism.Exports.

Section RmorphismTheory.

Section Properties.

Variables (R S : ringType) (f : {rmorphism R -> S}).

Lemma rmorph0 : f 0 = 0.

Lemma rmorphN : {morph f : x / - x}.

Lemma rmorphD : {morph f : x y / x + y}.

Lemma rmorph_sub : {morph f: x y / x - y}.

Lemma rmorphMn : forall n, {morph f : x / x *+ n}.

Lemma rmorphMNn : forall n, {morph f : x / x *- n}.

Lemma rmorph_sum : forall I r (P : pred I) E,
  f (\sum_(i <- r | P i) E i) = \sum_(i <- r | P i) f (E i).

Lemma rmorphismP : rmorphism f.

Lemma rmorphismMP : multiplicative f.

Lemma rmorph1 : f 1 = 1.

Lemma rmorphM : {morph f: x y / x * y}.

Lemma rmorph_prod: forall I r (P : pred I) E,
  f (\prod_(i <- r | P i) E i) = \prod_(i <- r | P i) f (E i).

Lemma rmorphX : forall n, {morph f: x / x ^+ n}.

Lemma rmorph_nat : forall n, f n%:R = n%:R.

Lemma rmorph_sign : forall n, f ((- 1) ^+ n) = (- 1) ^+ n.

Lemma rmorph_char : forall p, p \in [char R] -> p \in [char S].

Lemma can2_rmorphism : forall 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.

End Properties.

Section Projections.

Variables (R S T : ringType) (f : {rmorphism S -> T}) (g : {rmorphism R -> S}).

Lemma idfun_is_multiplicative : multiplicative (idfun : R -> R).
Canonical Structure idfun_rmorphism := AddRMorphism idfun_is_multiplicative.

Definition comp_is_multiplicative : multiplicative (f \o g).
Canonical Structure comp_rmorphism := AddRMorphism comp_is_multiplicative.

End Projections.

Section InAlgebra.

Variables (R : ringType) (A : lalgType R).

Lemma in_alg_is_rmorphism : rmorphism (in_alg_loc A).
Canonical Structure in_alg_additive := Additive in_alg_is_rmorphism.
Canonical Structure in_alg_rmorphism := RMorphism in_alg_is_rmorphism.

End InAlgebra.

End RmorphismTheory.

Module Linear.

Section ClassDef.

Variables (R : ringType) (U V : lmodType R).
Implicit Type phUV : phant (U -> V).

Definition axiom (f : U -> V) := forall a, {morph f : u v / a *: u + v}.

Definition mixin_of (f : U -> V) := forall a, {morph f : v / a *: v}.

Record class_of f : Prop := Class {base : additive f; mixin : mixin_of f}.
Local Coercion base : class_of >-> additive.

Lemma class_of_axiom : forall f, axiom f -> class_of f.

Structure map (phUV : phant (U -> V)) := Pack {apply; _ : class_of apply}.
Local Coercion apply : map >-> Funclass.

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 Structure additive := Additive.Pack phUV class.

End ClassDef.

Module Exports.
Notation scalable f := (mixin_of f).
Notation linear f := (axiom f).
Notation lmorphism f := (class_of f).
Coercion class_of_axiom : linear >-> lmorphism.
Coercion base : lmorphism >-> Additive.axiom.
Coercion mixin : lmorphism >-> scalable.
Coercion apply : map >-> Funclass.
Notation Linear fL := (Pack (Phant _) fL).
Notation AddLinear fZ := (pack fZ id).
Notation "{ 'linear' fUV }" := (map (Phant fUV))
  (at level 0, format "{ 'linear' fUV }") : 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 Structure additive.
End Exports.

End Linear.
Include Linear.Exports.

Section LinearTheory.

Variable R : ringType.

Section Properties.

Variables (U V : lmodType R) (f : {linear U -> V}).

Lemma linear0 : f 0 = 0.

Lemma linearN : {morph f : x / - x}.

Lemma linearD : {morph f : x y / x + y}.

Lemma linear_sub : {morph f: x y / x - y}.

Lemma linearMn : forall n, {morph f : x / x *+ n}.

Lemma linearMNn : forall n, {morph f : x / x *- n}.

Lemma linear_sum : forall I r (P : pred I) E,
  f (\sum_(i <- r | P i) E i) = \sum_(i <- r | P i) f (E i).

Lemma linearZ : scalable f.

Lemma linearP : linear f.

Lemma can2_linear : forall 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 Properties.

Section LinearLmod.

Variables U V W : lmodType R.
Variables (f g : {linear U -> V}) (h : {linear W -> U}).

Lemma idfun_is_scalable : scalable (idfun : U -> U).

Canonical Structure idfun_linear := AddLinear idfun_is_scalable.

Lemma comp_is_scalable : scalable (f \o h).
Canonical Structure comp_linear := AddLinear comp_is_scalable.

Lemma opp_is_scalable : scalable (-%R : U -> U).
Canonical Structure opp_linear := AddLinear opp_is_scalable.

Lemma scale_is_additive : forall a, additive ( *:%R a : V -> V).
Canonical Structure scale_additive a := Additive (scale_is_additive a).

Lemma null_fun_is_scalable : scalable (\0 : U -> U).
Canonical Structure null_fun_linear := AddLinear null_fun_is_scalable.

Lemma add_fun_is_scalable : scalable (f \+ g).
Canonical Structure add_fun_linear := AddLinear add_fun_is_scalable.

Lemma sub_fun_is_scalable : scalable (f \- g).
Canonical Structure 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}).

Lemma mulr_fun_is_scalable : scalable (a \o* f).
Canonical Structure mulr_fun_linear := AddLinear mulr_fun_is_scalable.

End LinearLalg.

End LinearTheory.

Module LRMorphism.

Section ClassDef.

Variables (R : ringType) (A B : lalgType R).

Record class_of (f : A -> B) : Prop :=
  Class {base : rmorphism f; mixin : scalable f}.
Local Coercion base : class_of >-> rmorphism.
Definition base2 f (fLM : class_of f) := Linear.Class fLM (mixin fLM).
Local Coercion base2 : class_of >-> lmorphism.

Structure map (phAB : phant (A -> B)) := Pack {apply; _ : class_of apply}.
Local Coercion apply : map >-> Funclass.

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 phAB) fZ & phant_id (Linear.mixin (Linear.class h)) fZ =>
  Pack phAB (@Class f fM fZ).

Definition pack (fZ : scalable f) :=
  fun (g : RMorphism.map phAB) fM & phant_id (RMorphism.class g) fM =>
  Pack phAB (Class fM fZ).

Canonical Structure additive := Additive.Pack phAB class.
Canonical Structure rmorphism := RMorphism.Pack phAB class.
Canonical Structure linear := Linear.Pack phAB class.
Canonical Structure join_rmorphism := @RMorphism.Pack _ _ phAB linear class.
Canonical Structure join_linear := @Linear.Pack R _ _ phAB rmorphism class.

End ClassDef.

Module Exports.
Notation lrmorphism f := (class_of f).
Coercion base : lrmorphism >-> RMorphism.class_of.
Coercion base2 : lrmorphism >-> Linear.class_of.
Coercion apply : map >-> Funclass.
Notation LRMorphism fZ := (pack fZ id).
Notation "{ 'lrmorphism' fAB }" := (map (Phant fAB))
  (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 Structure additive.
Coercion rmorphism : map >-> RMorphism.map.
Canonical Structure rmorphism.
Coercion linear : map >-> Linear.map.
Canonical Structure linear.
Canonical Structure join_rmorphism.
Canonical Structure join_linear.
End Exports.

End LRMorphism.
Include LRMorphism.Exports.

Section LRMorphismTheory.

Variables (R : ringType) (A B C : lalgType R) (f : {lrmorphism B -> C}).

Definition idfun_lrmorphism := [lrmorphism of (idfun : A -> A)].

Definition comp_lrmorphism (g : {lrmorphism A -> B}) := [lrmorphism of f \o g].

Lemma can2_lrmorphism : forall f', cancel f f' -> cancel f' f -> lrmorphism f'.

Lemma bij_lrmorphism :
  bijective f -> exists2 f' : {lrmorphism C -> B}, 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; _ : commutative (Ring.mul base)}.
Local Coercion base : class_of >-> Ring.class_of.

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
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.

Definition pack mul0 (m0 : @commutative T T mul0) :=
  fun bT b & phant_id (Ring.class bT) b =>
  fun m & phant_id m0 m => Pack (@Class T b m) T.

Definition eqType := Equality.Pack class cT.
Definition choiceType := Choice.Pack class cT.
Definition zmodType := Zmodule.Pack class cT.
Definition ringType := Ring.Pack class cT.

End ClassDef.

Module Exports.
Coercion base : class_of >-> Ring.class_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical Structure eqType.
Coercion choiceType : type >-> Choice.type.
Canonical Structure choiceType.
Coercion zmodType : type >-> Zmodule.type.
Canonical Structure zmodType.
Coercion ringType : type >-> Ring.type.
Canonical Structure 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 Structure mul_comoid := Monoid.ComLaw mulrC.
Lemma mulrCA : @left_commutative R R *%R.

Lemma mulrAC : @right_commutative R R *%R.

Lemma exprn_mull : forall n, {morph (fun x => x ^+ n) : x y / x * y}.

Lemma prodr_exp : forall 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 exprn_addl : forall x y n,
  (x + y) ^+ n = \sum_(i < n.+1) (x ^+ (n - i) * y ^+ i) *+ 'C(n, i).

Lemma exprn_subl : forall x y n,
  (x - y) ^+ n =
     \sum_(i < n.+1) ((-1) ^+ i * x ^+ (n - i) * y ^+ i) *+ 'C(n, i).

Lemma subr_expn : forall x y n,
  x ^+ n - y ^+ n = (x - y) * (\sum_(i < n) x ^+ (n.-1 - i) * y ^+ i).

Lemma sqrr_add : forall x y, (x + y) ^+ 2 = x ^+ 2 + x * y *+ 2 + y ^+ 2.

Lemma sqrr_sub : forall x y, (x - y) ^+ 2 = x ^+ 2 - x * y *+ 2 + y ^+ 2.

Lemma subr_sqr : forall x y, x ^+ 2 - y ^+ 2 = (x - y) * (x + y).

Lemma subr_sqr_add_sub : forall 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 Structure Frobenius_aut_additive :=
  Additive Frobenius_aut_is_rmorphism.
Canonical Structure Frobenius_aut_rmorphism :=
  RMorphism Frobenius_aut_is_rmorphism.

End FrobeniusAutomorphism.

Lemma rmorph_comm : forall (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 Structure scale_linear := AddLinear scale_is_scalable.

Lemma scale_fun_is_scalable : scalable (b \*: f).
Canonical Structure scale_fun_linear := AddLinear scale_fun_is_scalable.

End ScaleLinear.

End ComRingTheory.

Module Algebra.

Section Mixin.

Variables (R : ringType) (A : lalgType R).

Definition axiom := forall 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)
}.
Local Coercion base : class_of >-> Lalgebra.class_of.

Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
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.

Definition pack b0 (ax0 : @axiom R b0) :=
  fun bT b & phant_id (@Lalgebra.class R phR bT) b =>
  fun ax & phant_id ax0 ax => Pack phR (@Class T b ax) T.

Definition eqType := Equality.Pack class cT.
Definition choiceType := Choice.Pack class cT.
Definition zmodType := Zmodule.Pack class cT.
Definition ringType := Ring.Pack class cT.
Definition lmodType := Lmodule.Pack phR class cT.
Definition lalgType := Lalgebra.Pack phR class cT.

End ClassDef.

Module Exports.
Coercion base : class_of >-> Lalgebra.class_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical Structure eqType.
Coercion choiceType : type >-> Choice.type.
Canonical Structure choiceType.
Coercion zmodType : type >-> Zmodule.type.
Canonical Structure zmodType.
Coercion ringType : type >-> Ring.type.
Canonical Structure ringType.
Coercion lmodType : type >-> Lmodule.type.
Canonical Structure lmodType.
Coercion lalgType : type >-> Lalgebra.type.
Canonical Structure 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.
Implicit Types x y : A.

Lemma scaler_mulr : forall k x y, k *: (x * y) = x * (k *: y).

Lemma scaler_swap : forall k x y, k *: x * y = x * (k *: y).

Lemma scaler_exp : forall k x n, (k *: x) ^+ n = k ^+ n *: x ^+ n.

Lemma scaler_prodl : forall (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 : forall (I : finType) (S : pred I) (F : I -> R) x,
  \prod_(i \in S) (F i *: x) = \prod_(i \in S) F i *: x ^+ #|S|.

Lemma scaler_prod : forall 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).

Canonical Structure regular_comRingType := [comRingType of R^o].
Canonical Structure 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 Structure 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};
  _ : forall 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)
}.
Local Coercion base : class_of >-> Ring.class_of.

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
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.

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 m => Pack (@Class T b m) T.

Definition eqType := Equality.Pack class cT.
Definition choiceType := Choice.Pack class cT.
Definition zmodType := Zmodule.Pack class cT.
Definition ringType := Ring.Pack class cT.

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 Structure eqType.
Coercion choiceType : type >-> Choice.type.
Canonical Structure choiceType.
Coercion zmodType : type >-> Zmodule.type.
Canonical Structure zmodType.
Coercion ringType : type >-> Ring.type.
Canonical Structure 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) : pred R := UnitRing.unit (UnitRing.class R).
Definition inv (R : unitRingType) : R -> R := UnitRing.inv (UnitRing.class R).

Local Notation "x ^-1" := (inv x).
Local Notation "x / y" := (x * y^-1).
Local Notation "x ^- n" := ((x ^+ n)^-1).

Section UnitRingTheory.

Variable R : unitRingType.
Implicit Types x y : R.

Lemma divrr : forall x, unit x -> x / x = 1.
Definition mulrV := divrr.

Lemma mulVr : forall x, unit x -> x^-1 * x = 1.

Lemma invr_out : forall x, ~~ unit x -> x^-1 = x.

Lemma unitrP : forall x, reflect (exists y, y * x = 1 /\ x * y = 1) (unit x).

Lemma mulKr : forall x, unit x -> cancel (mul x) (mul x^-1).

Lemma mulVKr : forall x, unit x -> cancel (mul x^-1) (mul x).

Lemma mulrK : forall x, unit x -> cancel ( *%R^~ x) ( *%R^~ x^-1).

Lemma mulrVK : forall x, unit x -> cancel ( *%R^~ x^-1) ( *%R^~ x).
Definition divrK := mulrVK.

Lemma mulrI : forall x, unit x -> injective (mul x).

Lemma mulIr : forall x, unit x -> injective ( *%R^~ x).

Lemma commr_inv : forall x, comm x x^-1.

Lemma unitrE : forall x, unit x = (x / x == 1).

Lemma invrK : involutive (@inv R).

Lemma invr_inj : injective (@inv R).

Lemma unitr_inv : forall x, unit x^-1 = unit x.

Lemma unitr1 : unit (1 : R).

Lemma invr1 : 1^-1 = 1 :> R.

Lemma div1r : forall x, 1 / x = x^-1.

Lemma divr1 : forall x, x / 1 = x.

Lemma natr_div : forall m d,
  d %| m -> unit (d%:R : R) -> (m %/ d)%:R = m%:R / d%:R :> R.

Lemma unitr0 : unit (0 : R) = false.

Lemma invr0 : 0^-1 = 0 :> R.

Lemma unitr_opp : forall x, unit (- x) = unit x.

Lemma invrN : forall x, (- x)^-1 = - x^-1.

Lemma unitr_mull : forall x y, unit y -> unit (x * y) = unit x.

Lemma unitr_mulr : forall x y, unit x -> unit (x * y) = unit y.

Lemma invr_mul : forall x y, unit x -> unit y -> (x * y)^-1 = y^-1 * x^-1.

Lemma commr_unit_mul : forall x y, comm x y -> unit (x * y) = unit x && unit y.

Lemma unitr_exp : forall x n, unit x -> unit (x ^+ n).

Lemma unitr_pexp : forall x n, n > 0 -> unit (x ^+ n) = unit x.

Lemma expr_inv : forall x n, x^-1 ^+ n = x ^- n.

Lemma invr_neq0 : forall x, x != 0 -> x^-1 != 0.

Lemma invr_eq0 : forall x, (x^-1 == 0) = (x == 0).

Lemma rev_unitrP : forall x y : R^c, y * x = 1 /\ x * y = 1 -> unit x.

Definition converse_unitRingMixin :=
  @UnitRing.Mixin _ (unit : pred R^c) _ mulrV mulVr rev_unitrP invr_out.
Canonical Structure converse_unitRingType :=
  UnitRingType R^c converse_unitRingMixin.
Canonical Structure regular_unitRingType := [unitRingType of R^o].

End UnitRingTheory.

Section UnitRingMorphism.

Variables (R S : unitRingType) (f : {rmorphism R -> S}).

Lemma rmorph_unit : forall x, unit x -> unit (f x).

Lemma rmorphV : forall x, unit x -> f x^-1 = (f x)^-1.

Lemma rmorph_div : forall x y, unit y -> 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 : forall x y, y * x = 1 -> unit x.

Lemma mulC_mulrV : {in unit, right_inverse 1 inv *%R}.

Lemma mulC_unitP : forall 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)
}.
Local Coercion base : class_of >-> ComRing.class_of.
Definition base2 R m := UnitRing.Class (@mixin R m).
Local Coercion base2 : class_of >-> UnitRing.class_of.

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Variables (T : Type) (cT : type).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.

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 class cT.
Definition choiceType := Choice.Pack class cT.
Definition zmodType := Zmodule.Pack class cT.
Definition ringType := Ring.Pack class cT.
Definition comRingType := ComRing.Pack class cT.
Definition unitRingType := UnitRing.Pack class cT.
Definition com_unitRingType := @UnitRing.Pack comRingType class cT.

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 Structure eqType.
Coercion choiceType : type >-> Choice.type.
Canonical Structure choiceType.
Coercion zmodType : type >-> Zmodule.type.
Canonical Structure zmodType.
Coercion ringType : type >-> Ring.type.
Canonical Structure ringType.
Coercion comRingType : type >-> ComRing.type.
Canonical Structure comRingType.
Coercion unitRingType : type >-> UnitRing.type.
Canonical Structure unitRingType.
Canonical Structure 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).
Local Coercion base : class_of >-> Algebra.class_of.
Local Coercion base2 : class_of >-> UnitRing.class_of.

Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Variable (phR : phant R) (T : Type) (cT : type phR).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.

Definition pack :=
  fun bT b & phant_id (@Algebra.class R phR bT) (b : Algebra.class_of R T) =>
  fun mT m & phant_id (UnitRing.class mT) (@UnitRing.Class T b m) =>
  Pack (Phant R) (@Class T b m) T.

Definition eqType := Equality.Pack class cT.
Definition choiceType := Choice.Pack class cT.
Definition zmodType := Zmodule.Pack class cT.
Definition ringType := Ring.Pack class cT.
Definition unitRingType := UnitRing.Pack class cT.
Definition lmodType := Lmodule.Pack phR class cT.
Definition lalgType := Lalgebra.Pack phR class cT.
Definition algType := Algebra.Pack phR class cT.
Definition lmod_unitRingType := @Lmodule.Pack R phR unitRingType class cT.
Definition lalg_unitRingType := @Lalgebra.Pack R phR unitRingType class cT.
Definition alg_unitRingType := @Algebra.Pack R phR unitRingType class cT.

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 Structure eqType.
Coercion choiceType : type >-> Choice.type.
Canonical Structure choiceType.
Coercion zmodType : type >-> Zmodule.type.
Canonical Structure zmodType.
Coercion ringType : type >-> Ring.type.
Canonical Structure ringType.
Coercion unitRingType : type >-> UnitRing.type.
Canonical Structure unitRingType.
Coercion lmodType : type >-> Lmodule.type.
Canonical Structure lmodType.
Coercion lalgType : type >-> Lalgebra.type.
Canonical Structure lalgType.
Coercion algType : type >-> Algebra.type.
Canonical Structure algType.
Canonical Structure lmod_unitRingType.
Canonical Structure lalg_unitRingType.
Canonical Structure 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 unitr_mul : forall x y, unit (x * y) = unit x && unit y.

Canonical Structure regular_comUnitRingType := [comUnitRingType of R^o].
Canonical Structure regular_unitAlgType := [unitAlgType R of R^o].

End ComUnitRingTheory.

Section UnitAlgebraTheory.

Variable (R : comUnitRingType) (A : unitAlgType R).
Implicit Types k : R.
Implicit Types x y : A.

Lemma scaler_injl : forall k, unit k -> @injective _ A ( *:%R k).

Lemma scaler_unit : forall k x, unit k -> unit x = unit (k *: x).

Lemma scaler_inv: forall k x, unit k -> unit x -> (k *: x)^-1 = k^-1 *: x^-1.

End UnitAlgebraTheory.

 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.


Implicit Arguments Bool [R].

Notation True := (Bool true).
Notation False := (Bool false).

Local Notation "''X_' i" := (Var _ i) : term_scope.
Local Notation "n %:R" := (NatConst _ n) : term_scope.
Local Notation "x %:T" := (Const x) : term_scope.
Local Notation "0" := 0%:R%T : term_scope.
Local Notation "1" := 1%:R%T : term_scope.
Local Infix "+" := Add : term_scope.
Local Notation "- t" := (Opp t) : term_scope.
Local Notation "t - u" := (Add t (- u)) : term_scope.
Local Infix "*" := Mul : term_scope.
Local Infix "*+" := NatMul : term_scope.
Local Notation "t ^-1" := (Inv t) : term_scope.
Local Notation "t / u" := (Mul t u^-1) : term_scope.
Local Infix "^+" := Exp : term_scope.
Local Infix "==" := Equal : term_scope.
Local Infix "/\" := And : term_scope.
Local Infix "\/" := Or : term_scope.
Local Infix "==>" := Implies : term_scope.
Local Notation "~ f" := (Not f) : term_scope.
Local Notation "x != y" := (Not (x == y)) : term_scope.
Local Notation "''exists' ''X_' i , f" := (Exists i f) : term_scope.
Local Notation "''forall' ''X_' i , f" := (Forall i f) : term_scope.

Section Substitution.

Variable R : Type.

Fixpoint tsubst (t : term R) (s : nat * term R) :=
  match t with
  | 'X_i => if i == s.1 then s.2 else t
  | _%:T | _%:R => t
  | t1 + t2 => tsubst t1 s + tsubst t2 s
  | - t1 => - tsubst t1 s
  | t1 *+ n => tsubst t1 s *+ n
  | t1 * t2 => tsubst t1 s * tsubst t2 s
  | t1^-1 => (tsubst t1 s)^-1
  | t1 ^+ n => tsubst t1 s ^+ n
  end%T.

Fixpoint fsubst (f : formula R) (s : nat * term R) :=
  match f with
  | Bool _ => f
  | t1 == t2 => tsubst t1 s == tsubst t2 s
  | Unit t1 => Unit (tsubst t1 s)
  | f1 /\ f2 => fsubst f1 s /\ fsubst f2 s
  | f1 \/ f2 => fsubst f1 s \/ fsubst f2 s
  | f1 ==> f2 => fsubst f1 s ==> fsubst f2 s
  | ~ f1 => ~ fsubst f1 s
  | ('exists 'X_i, f1) => 'exists 'X_i, if i == s.1 then f1 else fsubst f1 s
  | ('forall 'X_i, f1) => 'forall 'X_i, if i == s.1 then f1 else fsubst f1 s
  end%T.

End Substitution.

Section EvalTerm.

Variable R : unitRingType.

 Evaluation of a reified term into R a ring with units 
Fixpoint eval (e : seq R) (t : term R) {struct t} : R :=
  match t with
  | ('X_i)%T => e`_i
  | (x%:T)%T => x
  | (n%:R)%T => n%:R
  | (t1 + t2)%T => eval e t1 + eval e t2
  | (- t1)%T => - eval e t1
  | (t1 *+ n)%T => eval e t1 *+ n
  | (t1 * t2)%T => eval e t1 * eval e t2
  | t1^-1%T => (eval e t1)^-1
  | (t1 ^+ n)%T => eval e t1 ^+ n
  end.

Definition same_env (e e' : seq R) := nth 0 e =1 nth 0 e'.

Lemma eq_eval : forall e e' t, same_env e e' -> eval e t = eval e' t.

Lemma eval_tsubst : forall e t s,
  eval e (tsubst t s) = eval (set_nth 0 e s.1 (eval e s.2)) t.

 Evaluation of a reified formula 
Fixpoint holds (e : seq R) (f : formula R) {struct f} : Prop :=
  match f with
  | Bool b => b
  | (t1 == t2)%T => eval e t1 = eval e t2
  | Unit t1 => unit (eval e t1)
  | (f1 /\ f2)%T => holds e f1 /\ holds e f2
  | (f1 \/ f2)%T => holds e f1 \/ holds e f2
  | (f1 ==> f2)%T => holds e f1 -> holds e f2
  | (~ f1)%T => ~ holds e f1
  | ('exists 'X_i, f1)%T => exists x, holds (set_nth 0 e i x) f1
  | ('forall 'X_i, f1)%T => forall x, holds (set_nth 0 e i x) f1
  end.

Lemma same_env_sym : forall e e', same_env e e' -> same_env e' e.

 Extensionality of formula evaluation 
Lemma eq_holds : forall e e' f, same_env e e' -> holds e f -> holds e' f.

 Evaluation and substitution by a constant 
Lemma holds_fsubst : forall e f i v,
  holds e (fsubst f (i, v%:T)%T) <-> holds (set_nth 0 e i v) f.

 Boolean test selecting terms in the language of rings 
Fixpoint rterm (t : term R) :=
  match t with
  | _^-1 => false
  | t1 + t2 | t1 * t2 => rterm t1 && rterm t2
  | - t1 | t1 *+ _ | t1 ^+ _ => rterm t1
  | _ => true
  end%T.

 Boolean test selecting formulas in the theory of rings 
Fixpoint rformula (f : formula R) :=
  match f with
  | Bool _ => true
  | t1 == t2 => rterm t1 && rterm t2
  | Unit t1 => false
  | f1 /\ f2 | f1 \/ f2 | f1 ==> f2 => rformula f1 && rformula f2
  | ~ f1 | ('exists 'X__, f1) | ('forall 'X__, f1) => rformula f1
  end%T.

 Upper bound of the names used in a term 
Fixpoint ub_var (t : term R) :=
  match t with
  | 'X_i => i.+1
  | t1 + t2 | t1 * t2 => maxn (ub_var t1) (ub_var t2)
  | - t1 | t1 *+ _ | t1 ^+ _ | t1^-1 => ub_var t1
  | _ => 0%N
  end%T.

 Replaces inverses in the term t by fresh variables, accumulating the 
 substitution. 
Fixpoint to_rterm (t : term R) (r : seq (term R)) (n : nat) {struct t} :=
  match t with
  | t1^-1 =>
    let: (t1', r1) := to_rterm t1 r n in
      ('X_(n + size r1), rcons r1 t1')
  | t1 + t2 =>
    let: (t1', r1) := to_rterm t1 r n in
    let: (t2', r2) := to_rterm t2 r1 n in
      (t1' + t2', r2)
  | - t1 =>
   let: (t1', r1) := to_rterm t1 r n in
     (- t1', r1)
  | t1 *+ m =>
   let: (t1', r1) := to_rterm t1 r n in
     (t1' *+ m, r1)
  | t1 * t2 =>
    let: (t1', r1) := to_rterm t1 r n in
    let: (t2', r2) := to_rterm t2 r1 n in
      (Mul t1' t2', r2)
  | t1 ^+ m =>
       let: (t1', r1) := to_rterm t1 r n in
     (t1' ^+ m, r1)
  | _ => (t, r)
  end%T.

Lemma to_rterm_id : forall 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
     'forall 'X_i, (f \/ 'X_i == t /\ ~ ('exists 'X_i, f)) ==> loop r' i.+1
  end%T
  in loop r1 m.

 Transformation of a formula in the theory of rings with units into an 
 equivalent formula in the sub-theory of rings.                        
Fixpoint to_rform f :=
  match f with
  | Bool b => f
  | t1 == t2 => eq0_rform (t1 - t2)
  | Unit t1 => eq0_rform (t1 * t1^-1 - 1)
  | f1 /\ f2 => to_rform f1 /\ to_rform f2
  | f1 \/ f2 => to_rform f1 \/ to_rform f2
  | f1 ==> f2 => to_rform f1 ==> to_rform f2
  | ~ f1 => ~ to_rform f1
  | ('exists 'X_i, f1) => 'exists 'X_i, to_rform f1
  | ('forall 'X_i, f1) => 'forall 'X_i, to_rform f1
  end%T.

 The transformation gives a ring formula. 
Lemma to_rform_rformula : forall f, rformula (to_rform f).

 Correctness of the transformation. 
Lemma to_rformP : forall e f, holds e (to_rform f) <-> holds e f.

 Boolean test selecting formulas which describe a constructible set, 
 i.e. formulas without quantifiers.                                  

 The quantifier elimination check. 
Fixpoint qf_form (f : formula R) :=
  match f with
  | Bool _ | _ == _ | Unit _ => true
  | f1 /\ f2 | f1 \/ f2 | f1 ==> f2 => qf_form f1 && qf_form f2
  | ~ f1 => qf_form f1
  | _ => false
  end%T.

 Boolean holds predicate for quantifier free formulas 
Definition qf_eval e := fix loop (f : formula R) : bool :=
  match f with
  | Bool b => b
  | t1 == t2 => (eval e t1 == eval e t2)%bool
  | Unit t1 => unit (eval e t1)
  | f1 /\ f2 => loop f1 && loop f2
  | f1 \/ f2 => loop f1 || loop f2
  | f1 ==> f2 => (loop f1 ==> loop f2)%bool
  | ~ f1 => ~~ loop f1
  |_ => false
  end%T.

 qf_eval is equivalent to holds 
Lemma qf_evalP : forall e f, qf_form f -> reflect (holds e f) (qf_eval e f).

Implicit Type bc : seq (term R) * seq (term R).

 Quantifier-free formula are normalized into DNF. A DNF is 
 represented by the type seq (seq (term R) * seq (term R)), where we 
 separate positive and negative literals 

 DNF preserving conjunction 
Definition and_dnf bcs1 bcs2 :=
  \big[cat/nil]_(bc1 <- bcs1)
     map (fun bc2 => (bc1.1 ++ bc2.1, bc1.2 ++ bc2.2)) bcs2.

 Computes a DNF from a qf ring formula 
Fixpoint qf_to_dnf (f : formula R) (neg : bool) {struct f} :=
  match f with
  | Bool b => if b (+) neg then [:: ([::], [::])] else [::]
  | t1 == t2 => [:: if neg then ([::], [:: t1 - t2]) else ([:: t1 - t2], [::])]
  | f1 /\ f2 => (if neg then cat else and_dnf) [rec f1, neg] [rec f2, neg]
  | f1 \/ f2 => (if neg then and_dnf else cat) [rec f1, neg] [rec f2, neg]
  | f1 ==> f2 => (if neg then and_dnf else cat) [rec f1, ~~ neg] [rec f2, neg]
  | ~ f1 => [rec f1, ~~ neg]
  | _ => if neg then [:: ([::], [::])] else [::]
  end%T where "[ 'rec' f , neg ]" := (qf_to_dnf f neg).

 Conversely, transforms a DNF into a formula 
Definition dnf_to_form :=
  let pos_lit t := And (t == 0) in let neg_lit t := And (t != 0) in
  let cls bc := Or (foldr pos_lit True bc.1 /\ foldr neg_lit True bc.2) in
  foldr cls False.

 Catenation of dnf is the Or of formulas 
Lemma cat_dnfP : forall 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 : forall 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 : forall e,
  let qev f b := qf_eval e (dnf_to_form (qf_to_dnf f b)) in
  forall f, qf_form f && rformula f -> qev f false = qf_eval e f.

Lemma dnf_to_form_qf : forall bcs, qf_form (dnf_to_form bcs).

Definition dnf_rterm cl := all rterm cl.1 && all rterm cl.2.

Lemma qf_to_dnf_rterm : forall f b, rformula f -> all dnf_rterm (qf_to_dnf f b).

Lemma dnf_to_rform : forall bcs, rformula (dnf_to_form bcs) = all dnf_rterm bcs.

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 :
   (forall i, qf_form (pred_f i)) ->
   (forall i, qf_form (then_f i)) ->
    qf_form else_f ->
  qf_form Pick.

Lemma eval_Pick : forall 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 Type I : seq nat.
Implicit Type e : seq R.

Lemma foldExistsP : forall I e,
  (exists2 e', {in [predC I], same_env e e'} & holds e' f)
    <-> holds e (foldr Exists f I).

Lemma foldForallP : forall I e,
  (forall 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) :=
  forall x y : R, x * y = 0 -> (x == 0) || (y == 0).

Section ClassDef.

Record class_of (R : Type) : Type :=
  Class {base : ComUnitRing.class_of R; _: axiom (Ring.Pack base R)}.
Local Coercion base : class_of >-> ComUnitRing.class_of.

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
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.

Definition pack b0 (m0 : axiom (@Ring.Pack T b0 T)) :=
  fun bT b & phant_id (ComUnitRing.class bT) b =>
  fun m & phant_id m0 m => Pack (@Class T b m) T.

Definition eqType := Equality.Pack class cT.
Definition choiceType := Choice.Pack class cT.
Definition zmodType := Zmodule.Pack class cT.
Definition ringType := Ring.Pack class cT.
Definition comRingType := ComRing.Pack class cT.
Definition unitRingType := UnitRing.Pack class cT.
Definition comUnitRingType := ComUnitRing.Pack class cT.

End ClassDef.

Module Exports.
Coercion base : class_of >-> ComUnitRing.class_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical Structure eqType.
Coercion choiceType : type >-> Choice.type.
Canonical Structure choiceType.
Coercion zmodType : type >-> Zmodule.type.
Canonical Structure zmodType.
Coercion ringType : type >-> Ring.type.
Canonical Structure ringType.
Coercion comRingType : type >-> ComRing.type.
Canonical Structure comRingType.
Coercion unitRingType : type >-> UnitRing.type.
Canonical Structure unitRingType.
Coercion comUnitRingType : type >-> ComUnitRing.type.
Canonical Structure 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 : forall x y, (x * y == 0) = (x == 0) || (y == 0).

Lemma mulf_neq0 : forall x y, x != 0 -> y != 0 -> x * y != 0.

Lemma expf_eq0 : forall x n, (x ^+ n == 0) = (n > 0) && (x == 0).

Lemma expf_neq0 : forall x m, x != 0 -> x ^+ m != 0.

Lemma mulfI : forall x, x != 0 -> injective ( *%R x).

Lemma mulIf : forall x, x != 0 -> injective ( *%R^~ x).

Lemma sqrf_eq1 : forall x, (x ^+ 2 == 1) = (x == 1) || (x == -1).

Lemma expfS_eq1 : forall x n,
  (x ^+ n.+1 == 1) = (x == 1) || (\sum_(i < n.+1) x ^+ i == 0).

Canonical Structure regular_idomainType := [idomainType of R^o].

End IntegralDomainTheory.

Module Field.

Definition mixin_of (F : unitRingType) := forall x : F, x != 0 -> unit x.

Lemma IdomainMixin : forall R, mixin_of R -> IntegralDomain.axiom R.

Section Mixins.

Variables (R : comRingType) (inv : R -> R).

Definition axiom := forall x, x != 0 -> inv x * x = 1.
Hypothesis mulVx : axiom.
Hypothesis inv0 : inv 0 = 0.

Lemma intro_unit : forall x y : R, y * x = 1 -> x != 0.

Lemma 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_of (UnitRing.Pack base F)
}.
Local Coercion base : class_of >-> IntegralDomain.class_of.

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
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.

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 m => Pack (@Class T b m) T.

Definition eqType := Equality.Pack class cT.
Definition choiceType := Choice.Pack class cT.
Definition zmodType := Zmodule.Pack class cT.
Definition ringType := Ring.Pack class cT.
Definition comRingType := ComRing.Pack class cT.
Definition unitRingType := UnitRing.Pack class cT.
Definition comUnitRingType := ComUnitRing.Pack class cT.
Definition idomainType := IntegralDomain.Pack class cT.

End ClassDef.

Module Exports.
Coercion base : class_of >-> IntegralDomain.class_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical Structure eqType.
Coercion choiceType : type >-> Choice.type.
Canonical Structure choiceType.
Coercion zmodType : type >-> Zmodule.type.
Canonical Structure zmodType.
Coercion ringType : type >-> Ring.type.
Canonical Structure ringType.
Coercion comRingType : type >-> ComRing.type.
Canonical Structure comRingType.
Coercion unitRingType : type >-> UnitRing.type.
Canonical Structure unitRingType.
Coercion comUnitRingType : type >-> ComUnitRing.type.
Canonical Structure comUnitRingType.
Coercion idomainType : type >-> IntegralDomain.type.
Canonical Structure 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 unitfE : forall x, unit x = (x != 0).

Lemma mulVf : forall x, x != 0 -> x^-1 * x = 1.
Lemma divff : forall x, x != 0 -> x / x = 1.
Definition mulfV := divff.
Lemma mulKf : forall x, x != 0 -> cancel ( *%R x) ( *%R x^-1).
Lemma mulVKf : forall x, x != 0 -> cancel ( *%R x^-1) ( *%R x).
Lemma mulfK : forall x, x != 0 -> cancel ( *%R^~ x) ( *%R^~ x^-1).
Lemma mulfVK : forall x, x != 0 -> cancel ( *%R^~ x^-1) ( *%R^~ x).
Definition divfK := mulfVK.

Lemma invf_mul : {morph (fun x => x^-1) : x y / x * y}.

Lemma prodf_inv : forall 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 natf0_char : forall n,
  n > 0 -> n%:R == 0 :> F -> exists p, p \in [char F].

Lemma charf'_nat : forall n, [char F]^'.-nat n = (n%:R != 0 :> F).

Lemma charf0P : [char F] =i pred0 <-> (forall n, (n%:R == 0 :> F) = (n == 0)%N).

Lemma char0_natf_div :
  [char F] =i pred0 -> forall m d, d %| m -> (m %/ d)%:R = m%:R / d%:R :> F.

Section FieldMorphismInj.

Variables (R : ringType) (f : {rmorphism F -> R}).

Lemma fmorph_eq0 : forall x, (f x == 0) = (x == 0).

Lemma fmorph_inj : injective f.

Lemma fmorph_char : [char R] =i [char F].

End FieldMorphismInj.

Section FieldMorphismInv.

Variables (R : unitRingType) (f : {rmorphism F -> R}).

Lemma fmorph_unit : forall x, unit (f x) = (x != 0).

Lemma fmorphV : {morph f: x / x^-1}.

Lemma fmorph_div : {morph f : x y / x / y}.

End FieldMorphismInv.

Canonical Structure regular_fieldType := [fieldType of F^o].

Section ModuleTheory.

Variable V : lmodType F.
Implicit Type a : F.
Implicit Type v : V.

Lemma scalerK : forall a, a != 0 -> cancel ( *:%R a : V -> V) ( *:%R a^-1).

Lemma scalerKV : forall a, a != 0 -> cancel ( *:%R a^-1 : V -> V) ( *:%R a).

Lemma scalerI : forall a, a != 0 -> injective ( *:%R a : V -> V).

Lemma scaler_eq0 : forall a v, (a *: v == 0) = (a == 0) || (v == 0).

End ModuleTheory.

End FieldTheory.

Implicit Arguments fmorph_inj [F R x1 x2].

Module DecidableField.

Definition axiom (R : unitRingType) (s : seq R -> pred (formula R)) :=
  forall 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)}.
Local Coercion base : class_of >-> Field.class_of.

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
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.

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 m => Pack (@Class T b m) T.

Definition eqType := Equality.Pack class cT.
Definition choiceType := Choice.Pack class cT.
Definition zmodType := Zmodule.Pack class cT.
Definition ringType := Ring.Pack class cT.
Definition comRingType := ComRing.Pack class cT.
Definition unitRingType := UnitRing.Pack class cT.
Definition comUnitRingType := ComUnitRing.Pack class cT.
Definition idomainType := IntegralDomain.Pack class cT.
Definition fieldType := Field.Pack class cT.

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 Structure eqType.
Coercion choiceType : type >-> Choice.type.
Canonical Structure choiceType.
Coercion zmodType : type >-> Zmodule.type.
Canonical Structure zmodType.
Coercion ringType : type >-> Ring.type.
Canonical Structure ringType.
Coercion comRingType : type >-> ComRing.type.
Canonical Structure comRingType.
Coercion unitRingType : type >-> UnitRing.type.
Canonical Structure unitRingType.
Coercion comUnitRingType : type >-> ComUnitRing.type.
Canonical Structure comUnitRingType.
Coercion idomainType : type >-> IntegralDomain.type.
Canonical Structure idomainType.
Coercion fieldType : type >-> Field.type.
Canonical Structure 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.

Lemma sol_subproof : forall n f,
  reflect (exists 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 : forall n f, size (sol n f) = n.

Lemma solP : forall n f,
  reflect (exists2 s, size s = n & holds s f) (sat (sol n f) f).

Lemma eq_sat : forall f1 f2,
  (forall e, holds e f1 <-> holds e f2) -> sat^~ f1 =1 sat^~ f2.

Lemma eq_sol : forall f1 f2,
  (forall e, holds e f1 <-> holds e f2) -> sol^~ f1 =1 sol^~ f2.

End DecidableFieldTheory.

Implicit Arguments satP [F e f].
Implicit Arguments solP [F n f].

 Structure of field with quantifier elimination 
Module QE.

Section Axioms.

Variable R : unitRingType.
Variable proj : nat -> seq (term R) * seq (term R) -> formula R.
 proj is the elimination of a single existential quantifier 

Definition wf_proj_axiom :=
  forall i bc (bc_i := proj i bc),
    dnf_rterm bc -> qf_form bc_i && rformula bc_i : Prop.

 The elimination operator p preserves  validity 
Definition holds_proj_axiom :=
  forall i bc (ex_i_bc := ('exists 'X_i, dnf_to_form [:: bc])%T) e,
  dnf_rterm bc -> reflect (holds e ex_i_bc) (qf_eval e (proj i bc)).

End Axioms.

Record mixin_of (R : unitRingType) : Type := Mixin {
  proj : nat -> (seq (term R) * seq (term R)) -> formula R;
  wf_proj : wf_proj_axiom proj;
  holds_proj : holds_proj_axiom proj
}.

Section ClassDef.

Record class_of (F : Type) : Type :=
  Class {base : Field.class_of F; mixin : mixin_of (UnitRing.Pack base F)}.
Local Coercion base : class_of >-> Field.class_of.

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
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.

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 m => Pack (@Class T b m) T.

Definition eqType := Equality.Pack class cT.
Definition choiceType := Choice.Pack class cT.
Definition zmodType := Zmodule.Pack class cT.
Definition ringType := Ring.Pack class cT.
Definition comRingType := ComRing.Pack class cT.
Definition unitRingType := UnitRing.Pack class cT.
Definition comUnitRingType := ComUnitRing.Pack class cT.
Definition idomainType := IntegralDomain.Pack class cT.
Definition fieldType := Field.Pack class cT.

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 Structure eqType.
Coercion choiceType : type >-> Choice.type.
Canonical Structure choiceType.
Coercion zmodType : type >-> Zmodule.type.
Canonical Structure zmodType.
Coercion ringType : type >-> Ring.type.
Canonical Structure ringType.
Coercion comRingType : type >-> ComRing.type.
Canonical Structure comRingType.
Coercion unitRingType : type >-> UnitRing.type.
Canonical Structure unitRingType.
Coercion comUnitRingType : type >-> ComUnitRing.type.
Canonical Structure comUnitRingType.
Coercion idomainType : type >-> IntegralDomain.type.
Canonical Structure idomainType.
Coercion fieldType : type >-> Field.type.
Canonical Structure fieldType.
End Exports.

End QE.
Import QE.Exports.

Section QE_theory.

Variable F : QE.type.

Definition proj := QE.proj (QE.class F).

Lemma wf_proj : QE.wf_proj_axiom proj.

Lemma holds_proj : QE.holds_proj_axiom proj.

Implicit Type f : formula F.


Fixpoint quantifier_elim (f : formula F) : formula 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
  | ('exists 'X_n, f) => elim_aux (quantifier_elim f) n
  | ('forall 'X_n, f) => ~ elim_aux (~ quantifier_elim f) n
  | _ => f
  end%T.

Lemma quantifier_elim_wf : forall f (qf := quantifier_elim f),
  rformula f -> qf_form qf && rformula qf.

Lemma quantifier_elim_rformP : forall 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 QEDecidableFieldMixin := DecidableField.Mixin proj_satP.

 To be exported 
 Axiom == all non-constant monic polynomials have a root 
Definition axiom (R : ringType) :=
  forall n (P : nat -> R), n > 0 ->
   exists 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)}.
Local Coercion base : class_of >-> DecidableField.class_of.

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
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.

Definition pack b0 (m0 : axiom (@Ring.Pack T b0 T)) :=
  fun bT b & phant_id (DecidableField.class bT) b =>
  fun m & phant_id m0 m => Pack (@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 class cT.
Definition choiceType := Choice.Pack class cT.
Definition zmodType := Zmodule.Pack class cT.
Definition ringType := Ring.Pack class cT.
Definition comRingType := ComRing.Pack class cT.
Definition unitRingType := UnitRing.Pack class cT.
Definition comUnitRingType := ComUnitRing.Pack class cT.
Definition idomainType := IntegralDomain.Pack class cT.
Definition fieldType := Field.Pack class cT.
Definition decFieldType := DecidableField.Pack class cT.

End ClassDef.

Module Exports.
Coercion base : class_of >-> DecidableField.class_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical Structure eqType.
Coercion choiceType : type >-> Choice.type.
Canonical Structure choiceType.
Coercion zmodType : type >-> Zmodule.type.
Canonical Structure zmodType.
Coercion ringType : type >-> Ring.type.
Canonical Structure ringType.
Coercion comRingType : type >-> ComRing.type.
Canonical Structure comRingType.
Coercion unitRingType : type >-> UnitRing.type.
Canonical Structure unitRingType.
Coercion comUnitRingType : type >-> ComUnitRing.type.
Canonical Structure comUnitRingType.
Coercion idomainType : type >-> IntegralDomain.type.
Canonical Structure idomainType.
Coercion fieldType : type >-> Field.type.
Canonical Structure fieldType.
Coercion decFieldType : type >-> DecidableField.type.
Canonical Structure 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.

End ClosedFieldTheory.

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 addKr := addKr.
Definition addNKr := addNKr.
Definition addrK := addrK.
Definition addrNK := addrNK.
Definition subrK := subrK.
Definition addrI := addrI.
Definition addIr := addIr.
Definition opprK := opprK.
Definition oppr0 := oppr0.
Definition oppr_eq0 := oppr_eq0.
Definition oppr_add := oppr_add.
Definition oppr_sub := oppr_sub.
Definition subr0 := subr0.
Definition sub0r := sub0r.
Definition subr_eq := subr_eq.
Definition subr_eq0 := subr_eq0.
Definition addr_eq0 := addr_eq0.
Definition eqr_opp := eqr_opp.
Definition eqr_oppC := eqr_oppC.
Definition sumr_opp := sumr_opp.
Definition sumr_sub := sumr_sub.
Definition sumr_muln := sumr_muln.
Definition sumr_muln_r := sumr_muln_r.
Definition sumr_const := sumr_const.
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 mulrn_addl := mulrn_addl.
Definition mulrn_addr := mulrn_addr.
Definition mulrn_subl := mulrn_subl.
Definition mulrn_subr := mulrn_subr.
Definition mulrnA := mulrnA.
Definition mulrnAC := mulrnAC.
Definition mulrA := mulrA.
Definition mul1r := mul1r.
Definition mulr1 := mulr1.
Definition mulr_addl := mulr_addl.
Definition mulr_addr := mulr_addr.
Definition nonzero1r := nonzero1r.
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 mulr_subl := mulr_subl.
Definition mulr_subr := mulr_subr.
Definition mulrnAl := mulrnAl.
Definition mulrnAr := mulrnAr.
Definition mulr_natl := mulr_natl.
Definition mulr_natr := mulr_natr.
Definition natr_add := natr_add.
Definition natr_sub := natr_sub.
Definition natr_sum := natr_sum.
Definition natr_mul := natr_mul.
Definition natr_exp := natr_exp.
Definition expr0 := expr0.
Definition exprS := exprS.
Definition expr1 := expr1.
Definition expr2 := expr2.
Definition exp1rn := exp1rn.
Definition exprn_addr := exprn_addr.
Definition exprSr := exprSr.
Definition commr_sym := commr_sym.
Definition commr_refl := commr_refl.
Definition commr0 := commr0.
Definition commr1 := commr1.
Definition commr_opp := commr_opp.
Definition commrN1 := commrN1.
Definition commr_add := commr_add.
Definition commr_muln := commr_muln.
Definition commr_mul := commr_mul.
Definition commr_nat := commr_nat.
Definition commr_exp := commr_exp.
Definition commr_exp_mull := commr_exp_mull.
Definition commr_sign := commr_sign.
Definition exprn_mulnl := exprn_mulnl.
Definition exprn_mulr := exprn_mulr.
Definition exprn_mod := exprn_mod.
Definition exprn_dvd := exprn_dvd.
Definition signr_odd := signr_odd.
Definition signr_eq0 := signr_eq0.
Definition signr_addb := signr_addb.
Definition exprN := exprN.
Definition sqrrN := sqrrN.
Definition exprn_addl_comm := exprn_addl_comm.
Definition exprn_subl_comm := exprn_subl_comm.
Definition subr_expn_comm := subr_expn_comm.
Definition exprn_add1 := exprn_add1.
Definition subr_expn_1 := subr_expn_1.
Definition sqrr_add1 := sqrr_add1.
Definition sqrr_sub1 := sqrr_sub1.
Definition subr_sqr_1 := subr_sqr_1.
Definition charf0 := charf0.
Definition charf_prime := charf_prime.
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_aut_0 := Frobenius_aut_0.
Definition Frobenius_aut_1 := Frobenius_aut_1.
Definition Frobenius_aut_add_comm := Frobenius_aut_add_comm.
Definition Frobenius_aut_muln := Frobenius_aut_muln.
Definition Frobenius_aut_nat := Frobenius_aut_nat.
Definition Frobenius_aut_mul_comm := Frobenius_aut_mul_comm.
Definition Frobenius_aut_exp := Frobenius_aut_exp.
Definition Frobenius_aut_opp := Frobenius_aut_opp.
Definition Frobenius_aut_sub_comm := Frobenius_aut_sub_comm.
Definition prodr_const := prodr_const.
Definition mulrC := mulrC.
Definition mulrCA := mulrCA.
Definition mulrAC := mulrAC.
Definition exprn_mull := exprn_mull.
Definition prodr_exp := prodr_exp.
Definition prodr_exp_r := prodr_exp_r.
Definition prodr_opp := prodr_opp.
Definition exprn_addl := exprn_addl.
Definition exprn_subl := exprn_subl.
Definition subr_expn := subr_expn.
Definition sqrr_add := sqrr_add.
Definition sqrr_sub := sqrr_sub.
Definition subr_sqr := subr_sqr.
Definition subr_sqr_add_sub := subr_sqr_add_sub.
Definition mulrV := mulrV.
Definition divrr := divrr.
Definition mulVr := mulVr.
Definition invr_out := invr_out.
Definition unitrP := unitrP.
Definition mulKr := mulKr.
Definition mulVKr := mulVKr.
Definition mulrK := mulrK.
Definition mulrVK := mulrVK.
Definition divrK := divrK.
Definition mulrI := mulrI.
Definition mulIr := mulIr.
Definition commr_inv := commr_inv.
Definition unitrE := unitrE.
Definition invrK := invrK.
Definition invr_inj := invr_inj.
Definition unitr_inv := unitr_inv.
Definition unitr1 := unitr1.
Definition invr1 := invr1.
Definition divr1 := divr1.
Definition div1r := div1r.
Definition natr_div := natr_div.
Definition unitr0 := unitr0.
Definition invr0 := invr0.
Definition unitr_opp := unitr_opp.
Definition invrN := invrN.
Definition unitr_mull := unitr_mull.
Definition unitr_mulr := unitr_mulr.
Definition invr_mul := invr_mul.
Definition invr_eq0 := invr_eq0.
Definition invr_neq0 := invr_neq0.
Definition commr_unit_mul := commr_unit_mul.
Definition unitr_exp := unitr_exp.
Definition unitr_pexp := unitr_pexp.
Definition expr_inv := expr_inv.
Definition eq_eval := eq_eval.
Definition eval_tsubst := eval_tsubst.
Definition eq_holds := eq_holds.
Definition holds_fsubst := holds_fsubst.
Definition unitr_mul := unitr_mul.
Definition mulf_eq0 := mulf_eq0.
Definition mulf_neq0 := mulf_neq0.
Definition expf_eq0 := expf_eq0.
Definition expf_neq0 := expf_neq0.
Definition mulfI := mulfI.
Definition mulIf := mulIf.
Definition sqrf_eq1 := sqrf_eq1.
Definition expfS_eq1 := expfS_eq1.
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 invf_mul := invf_mul.
Definition prodf_inv := prodf_inv.
Definition natf0_char := natf0_char.
Definition charf'_nat := charf'_nat.
Definition charf0P := charf0P.
Definition char0_natf_div := char0_natf_div.
Definition satP := @satP.
Definition eq_sat := eq_sat.
Definition solP := @solP.
Definition eq_sol := eq_sol.
Definition size_sol := size_sol.
Definition solve_monicpoly := solve_monicpoly.
Definition raddf0 := raddf0.
Definition raddfN := raddfN.
Definition raddfD := raddfD.
Definition raddf_sub := raddf_sub.
Definition raddf_sum := raddf_sum.
Definition raddfMn := raddfMn.
Definition raddfMNn := raddfMNn.
Definition can2_additive := can2_additive.
Definition bij_additive := bij_additive.
Definition rmorph0 := rmorph0.
Definition rmorphN := rmorphN.
Definition rmorphD := rmorphD.
Definition rmorph_sub := rmorph_sub.
Definition rmorph_sum := rmorph_sum.
Definition rmorphMn := rmorphMn.
Definition rmorphMNn := rmorphMNn.
Definition rmorphismP := rmorphismP.
Definition rmorphismMP := rmorphismMP.
Definition rmorph1 := rmorph1.
Definition rmorphM := rmorphM.
Definition rmorph_nat := rmorph_nat.
Definition rmorph_prod := rmorph_prod.
Definition rmorphX := rmorphX.
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.
Implicit Arguments fmorph_inj [F R x1 x2].
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 scaler_addr := scaler_addr.
Definition scaler_addl := scaler_addl.
Definition scaler0 := scaler0.
Definition scale0r := scale0r.
Definition scaleNr := scaleNr.
Definition scaleN1r := scaleN1r.
Definition scalerN := scalerN.
Definition scaler_subl := scaler_subl.
Definition scaler_subr := scaler_subr.
Definition scaler_nat := scaler_nat.
Definition scaler_mulrnl := scaler_mulrnl.
Definition scaler_mulrnr := scaler_mulrnr.
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 scaler_mull := scaler_mull.
Definition scaler_mulr := scaler_mulr.
Definition scaler_swap := scaler_swap.
Definition scaler_exp := scaler_exp.
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 scaler_inv := scaler_inv.
Definition linearP := linearP.
Definition linear0 := linear0.
Definition linearN := linearN.
Definition linearD := linearD.
Definition linear_sub := linear_sub.
Definition linear_sum := linear_sum.
Definition linearMn := linearMn.
Definition linearMNn := linearMNn.
Definition linearZ := linearZ.
Definition can2_linear := can2_linear.
Definition bij_linear := bij_linear.
Definition can2_lrmorphism := can2_lrmorphism.
Definition bij_lrmorphism := bij_lrmorphism.

Implicit Arguments satP [F e f].
Implicit Arguments solP [F n f].

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 QE.Exports ClosedField.Exports.
Canonical Structure QEDecidableField.

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 "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_ ( <- r | P ) F" :=
  (\big[+%R/0%R]_(<- r | P%B) F%R) : 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_ ( <- r | P ) F" :=
  (\big[*%R/1%R]_(<- r | P%B) 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 Structure add_monoid.
Canonical Structure add_comoid.
Canonical Structure mul_monoid.
Canonical Structure mul_comoid.
Canonical Structure muloid.
Canonical Structure addoid.

Canonical Structure idfun_additive.
Canonical Structure idfun_rmorphism.
Canonical Structure idfun_linear.
Canonical Structure idfun_lrmorphism.
Canonical Structure comp_additive.
Canonical Structure comp_rmorphism.
Canonical Structure comp_linear.
Canonical Structure comp_lrmorphism.
Canonical Structure opp_additive.
Canonical Structure opp_linear.
Canonical Structure scale_additive.
Canonical Structure scale_linear.
Canonical Structure null_fun_additive.
Canonical Structure null_fun_linear.
Canonical Structure scale_fun_additive.
Canonical Structure scale_fun_linear.
Canonical Structure add_fun_additive.
Canonical Structure add_fun_linear.
Canonical Structure sub_fun_additive.
Canonical Structure sub_fun_linear.
Canonical Structure mull_fun_additive.
Canonical Structure mull_fun_linear.
Canonical Structure mulr_fun_additive.
Canonical Structure mulr_fun_linear.
Canonical Structure Frobenius_aut_additive.
Canonical Structure Frobenius_aut_rmorphism.
Canonical Structure in_alg_additive.
Canonical Structure in_alg_rmorphism.

Notation "R ^c" := (converse R) (at level 2, format "R ^c") : type_scope.
Canonical Structure converse_eqType.
Canonical Structure converse_choiceType.
Canonical Structure converse_zmodType.
Canonical Structure converse_ringType.
Canonical Structure converse_unitRingType.

Notation "R ^o" := (regular R) (at level 2, format "R ^o") : type_scope.
Canonical Structure regular_eqType.
Canonical Structure regular_choiceType.
Canonical Structure regular_zmodType.
Canonical Structure regular_ringType.
Canonical Structure regular_lmodType.
Canonical Structure regular_lalgType.
Canonical Structure regular_comRingType.
Canonical Structure regular_algType.
Canonical Structure regular_unitRingType.
Canonical Structure regular_comUnitRingType.
Canonical Structure regular_unitAlgType.
Canonical Structure regular_idomainType.
Canonical Structure regular_fieldType.


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].

Lemma ffun_addA : associative ffun_add.
Lemma ffun_addC : commutative ffun_add.
Lemma ffun_add0 : left_id ffun_zero ffun_add.
Lemma ffun_addN : left_inverse ffun_zero ffun_opp ffun_add.

Definition ffun_zmodMixin :=
  Zmodule.Mixin ffun_addA ffun_addC ffun_add0 ffun_addN.
Canonical Structure ffun_zmodType :=
  Eval hnf in ZmodType _ ffun_zmodMixin.

Lemma sum_ffunE:
  forall I (r : seq I) (P : pred I) (F : I -> {ffun aT -> rT}),
  \big[+%R/0]_(i <- r | P i) F i =
     [ffun x => \big[+%R/0]_(i <- r | P i) (F i x)].

Lemma ffunMn : forall f n x, (f *+ n) x = f x *+ n.

End FinFunZmod.

 As rings require 1 != 0 we cannot lift a ring structure over finfuns.      
 We would need evidence that the domain is non-empty.                       
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].

Lemma ffun_scaleA : forall k1 k2 f,
  ffun_scale k1 (ffun_scale k2 f) = ffun_scale (k1 * k2) f.
Lemma ffun_scale1 : left_id 1 ffun_scale.
Lemma ffun_scale_addr : forall k, {morph (ffun_scale k) : x y / x + y}.
Lemma ffun_scale_addl : forall u, {morph (ffun_scale)^~ u : k1 k2 / k1 + k2}.

Definition ffun_lmodMixin :=
  LmodMixin ffun_scaleA ffun_scale1 ffun_scale_addr ffun_scale_addl.
Canonical Structure ffun_lmodType :=
  Eval hnf in LmodType R {ffun aT -> rT} ffun_lmodMixin.

End FinFunLmod.