Library ssralg

Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq choice fintype.
Require Import finfun bigops prime binomial.

  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

      zmodType        == type for Zmodule structure                        
      ZmodMixin       == builds the mixin containing the definition        
                         of a Zmodule                                      
      ZmodType R M    == packs the mixin M to build a Zmodule of type      
                         zmodType. (The underlying type R should have a    
                         choiceType canonical structure)                   
      0               == the additive identity element of a Zmodule        
      x + y           == the addition operation of a Zmodule               
      - x             == the opposite operation of a Zmodule               
      x - y           == the substraction operation of a Zmodule           
                      := x + - y                                           
      x +* n , x -* n == the generic multiplication by a nat               
      \sum_<range> e  == iterated sum for a Zmodule (cf bigops.v)          
      e`_i            == nth 0 e i, when e : seq M and M is a zmodType     
      ... and a many classical Lemmas on these Zmodule laws                


 

Ring

      ringType      == type for ring structure                             
      RingMixin     == builds the mixin containing the definitions of a    
                       ring (the underlying type should have a zmodType    
                       structure)                                          
      RingType R M  == packs the ring mixin M to build a ring on type R    
      RevRingType T == repacks T to build the ring where the               
                       multiplicative law is reversed ( x *' y = y * x )   
      1             == the multiplicative identity element of a Ring       
      n%:R          == the ring image of a nat n (e.g., 1%:R := 1%R)       
      x * y         == the multiplication operation of a ring              
    \prod_<range> e == iterated product for a ring (cf bigops.v)           
      x ^+ y        == the exponentiation operation of a ring              
     GRing.comm x y <=> x and y commute, i.e., x * y = y * x               
      [char R]      == the characteristic of R, i.e., the set of prime     
                       numbers p such that p%:R = 0 in R. The set [char p] 
                       has a most one element, and is represented 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 : R to x ^+ p, 
                       where chRp : p \in [char R] is a proof that R has   
                       indeed (non-zero) characteristic p.                 


 

Commutative Ring

      comRingType      == type for commutative ring structure              
    ComRingType R mulC == packs mulC to build a commutative ring.          
                          (The underlying type R should have a ring        
                          canonical structure)                             
      ComRingMixin     == builds the mixin containing the definitions of a 
                          *non commutative* ring, using the commutativity  
                          to decrease the number of axioms.                


 

Unit Ring

      unitRingType   == type for unit ring structure                       
      UnitRingMixin  == builds the mixin containing the definitions        
                        of a unit ring. (The underlying type should        
                        have a ring canonical structure)                   
    UnitRingType R M == packs the unit ring mixin M to build a unit ring.  
                        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 and   
                        will not be used by type inference.                
      GRing.unit x   == x is a unit (i.e., has an inverse)                 
      x^-1           == the inversion operation element of a unit ring     
                        (returns x if is x is not an unit)                 
      x / y          := x * y^-1                                           
      x ^- n         := (x ^+ n)^-1                                        


 

Commutative Unit Ring

      comUnitRingType   == type for unit ring structure                    
      ComUnitRingMixin  == builds the mixin containing the definitions     
                           of a *non commutative unit ring*, but using     
                           the commutative property. The underlying type   
                           should have a commutative ring canonical        
                           structure. WARNING: ALWAYS give an explicit     
                           type argument to UnitRingType along with a      
                           mixin produced by ComUnitRingMixin (see above). 


 

Integral Domain (integral, commutative, unit ring)

      idomainType       == type for integral domain structure              
      IdomainType R M   == packs the idomain mixin M to build a integral   
                           domain. (The underlying type R should have a    
                           commutative unit ring canonical structure)      


 

Field

      fieldType         == type for field structure                        
      FieldUnitMixin    == builds a *non commutative unit ring* mixin,     
                           using some field properties. (The underlying    
                           type should have a *commutative ring* canonical 
                           structure)                                      
      FieldMixin        == builds the field mixin. (The underlying type    
                           should have a *commutative ring* canonical      
                           structure)                                      
      FieldIdomainMixin == builds an *idomain* mixin, using a field mixin  
      FieldType R M     == packs the field mixin M to build a field        
                           (The underlying type R should have a            
                           integral domain canonical structure)            


 

Decidable Field

      decFieldType      == type for decidable field structure              
      DecFieldMixin     == builds the mixin containing the definitions of  
                           a decidable Field. (The underlying type should  
                           have a unit ring canonical structure)           
      DecFieldType R M  == packs the decidable field mixin M to build a    
                           decidable field. (The underlying type R should  
                           have a field canonical structure)               
      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      
                           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_eval e f   == the value (in bool) of a quantifier-free f.     
      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.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    


 

Closed Field

      closedFieldType   == type for closed field structure                 
    ClosedFieldType R M == packs the closed field mixin M to build a       
                           closed field. (The underlying type R should     
                           have a decidable field canonical structure.)    


 

Morphism

     GRing.morphism f <=> f is a ring morphism: f commutes with 0, +, -,   
                          *, 1, and with ^-1 and / in integral domains.    
                   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).      
Lmodule

      lmodType R      == type for Lmodule structure over the ring R        
      LmodMixin R     == builds the mixin containing the definition        
                         of a Lmodule over the ring R                      
      LmodType R T M  == packs the mixin M to build a Lmodule of type      
                         lmodType R. (The underlying type T should have a  
                         zmodType canonical structure)                     
      a *: x          == the external operation of a Lmodule               


 

 The Lemmas about theses structures are all contained in GRing.Theory.     
 Notations are defined in scope ring_scope (delimiter %R), except term and 
 formula notations, which are in term_scope (delimiter %T).                


 

 NB: The module GRing should not be imported, only the main module and     
     GRing.Theory should be.

Import Prenex Implicits.

Abstract algebra framework for ssreflect.                          
 We define a number of structures that ``package'' common algebraic 
 properties of operations. These extend the combinatorial classes   
 with notation and theory for classical algebraic structures.

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 "[ '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").

Delimit Scope ring_scope with R.
Delimit Scope term_scope with T.
Local Open Scope ring_scope.

Module GRing.

Import Monoid.Theory.

Module Zmodule.

Record mixin_of (M : Type) : Type := Mixin {
  zero : M;
  opp : M -> M;
  add : M -> M -> M;
  _ : associative add;
  _ : commutative add;
  _ : left_id zero add;
  _ : left_inverse zero opp add
}.

Record class_of (M : Type) : Type :=
  Class { base :> Choice.class_of M; ext :> mixin_of M }.

Structure type : Type := Pack {sort :> Type; _ : class_of sort; _ : Type}.
Definition class cT := let: Pack _ c _ := cT return class_of cT in c.
Definition clone T cT c of phant_id (class cT) c := @Pack T c T.

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

Coercion eqType cT := Equality.Pack (class cT) cT.
Coercion choiceType cT := Choice.Pack (class cT) cT.

End Zmodule.

Canonical Structure Zmodule.eqType.
Canonical Structure Zmodule.choiceType.

Definition zero M := Zmodule.zero (Zmodule.class M).
Definition opp M := Zmodule.opp (Zmodule.class M).
Definition add M := Zmodule.add (Zmodule.class M).

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 M x n := nosimpl iterop _ n +%R x (zero M).

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 M : Zmodule.type.
Implicit Types x y : M.

Lemma addrA : @associative M +%R.

Lemma addrC : @commutative M M +%R.

Lemma add0r : @left_id M M 0 +%R.

Lemma addNr : @left_inverse M M M 0 -%R +%R.

Lemma addr0 : @right_id M M 0 +%R.
Lemma addrN : @right_inverse M M M 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 M M +%R.

Lemma addrAC : @right_commutative M M +%R.

Lemma addKr : @left_loop M M -%R +%R.
Lemma addNKr : @rev_left_loop M M -%R +%R.
Lemma addrK : @right_loop M M -%R +%R.
Lemma addrNK : @rev_right_loop M M -%R +%R.
Definition subrK := addrNK.
Lemma addrI : @right_injective M M M +%R.
Lemma addIr : @left_injective M M M +%R.
Lemma opprK : @involutive M -%R.
Lemma oppr0 : -0 = 0 :> M.
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 : M}.

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 mulr0n : forall x, x *+ 0 = 0.

Lemma mulr1n : forall x, x *+ 1 = 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 :> M.

Lemma oppr_muln : forall x n, - (x *+ n) = x *- n :> M.

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 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 -> M),
  (\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 -> M),
  \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 -> M) 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 : M),
  \sum_(i \in A) x = x *+ #|A|.

End ZmoduleTheory.

Module Ring.

Record mixin_of (R : Zmodule.type) : 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.

Record class_of (R : Type) : Type := Class {
  base :> Zmodule.class_of R;
  ext :> mixin_of (Zmodule.Pack base R)
}.

Structure type : Type := Pack {sort :> Type; _ : class_of sort; _ : Type}.
Definition class cT := let: Pack _ c _ := cT return class_of cT in c.
Definition clone T cT c of phant_id (class cT) c := @Pack T c T.

Definition pack T 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.

Coercion eqType cT := Equality.Pack (class cT) cT.
Coercion choiceType cT := Choice.Pack (class cT) cT.
Coercion zmodType cT := Zmodule.Pack (class cT) cT.

End Ring.

Canonical Structure Ring.eqType.
Canonical Structure Ring.choiceType.
Canonical Structure Ring.zmodType.

Definition one (R : Ring.type) : R := Ring.one (Ring.class R).
Definition mul (R : Ring.type) : R -> R -> R := Ring.mul (Ring.class R).
Definition exp R x n := nosimpl iterop _ n (@mul R) x (one R).

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

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.

Section RingTheory.

Variable R : Ring.type.
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_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_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 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.

Definition commDef x y := x * y = y * x.
Notation comm := commDef.

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 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 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 subr_expn_1 : forall x n, x ^+ n - 1 = (x - 1) * (\sum_(i < n) x ^+ i).

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

Section Frobenius.

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

Definition RevRingMixin :=
  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 R 1 mul' mulrA' mulr1 mul1r mulr_addl' mulr_addr' nonzero1r.

Definition RevRingType := Ring.Pack (Ring.Class RevRingMixin) R.

End RingTheory.

Notation comm := (@commDef _).

Notation rev :=
  (let R := _ in fun (x : Ring.sort R) => x : Ring.sort (RevRingType R)).

Definition morphism (aR rR : Ring.type) (f : aR -> rR) :=
  [/\ {morph f : x y / x - y}, {morph f : x y / x * y} & f 1 = 1].

Section RingMorphTheory.

Variables aR' aR rR : Ring.type.
Variables (f : aR -> rR) (g : aR' -> aR).
Hypotheses (fM : morphism f) (gM : morphism g).

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

Lemma ringM_0 : f 0 = 0.

Lemma ringM_1 : f 1 = 1.

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

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

Definition ringM_sum := big_morph f ringM_add ringM_0.

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

Definition ringM_prod := big_morph f ringM_mul ringM_1.

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

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

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

Lemma ringM_sign : forall k, f ((- 1) ^+ k) = (- 1) ^+ k.

Lemma ringM_char : forall p, p \in [char aR] -> p \in [char rR].

Lemma comp_ringM : morphism (f \o g).

Lemma ringM_isom :
  bijective f -> exists f', [/\ cancel f f', cancel f' f & morphism f'].

End RingMorphTheory.

Module ComRing.

Record class_of (R : Type) : Type :=
  Class {base :> Ring.class_of R; _ : commutative (Ring.mul base)}.

Structure type : Type := Pack {sort :> Type; _ : class_of sort; _ : Type}.
Definition class cT := let: Pack _ c _ := cT return class_of cT in c.
Definition clone T cT c of phant_id (class cT) c := @Pack T c T.

Definition pack T 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 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.

Coercion eqType cT := Equality.Pack (class cT) cT.
Coercion choiceType cT := Choice.Pack (class cT) cT.
Coercion zmodType cT := Zmodule.Pack (class cT) cT.
Coercion ringType cT := Ring.Pack (class cT) cT.

End ComRing.

Canonical Structure ComRing.eqType.
Canonical Structure ComRing.choiceType.
Canonical Structure ComRing.zmodType.
Canonical Structure ComRing.ringType.

Section ComRingTheory.

Variable R : ComRing.type.
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 ringM_comm : forall (rR : Ring.type) (f : R -> rR),
  morphism f -> forall x y, comm (f x) (f y).

Lemma Frobenius_aut_RM : forall p (charRp : p \in [char R]),
  morphism (Frobenius_aut charRp).

End ComRingTheory.

Module UnitRing.

Record mixin_of (R : Ring.type) : 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.

Record class_of (R : Type) : Type := Class {
  base :> Ring.class_of R;
  mixin :> mixin_of (Ring.Pack base R)
}.

Structure type : Type := Pack {sort :> Type; _ : class_of sort; _ : Type}.
Definition class cT := let: Pack _ c _ := cT return class_of cT in c.
Definition clone T cT c of phant_id (class cT) c := @Pack T c T.

Definition pack T 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.

Coercion eqType cT := Equality.Pack (class cT) cT.
Coercion choiceType cT := Choice.Pack (class cT) cT.
Coercion zmodType cT := Zmodule.Pack (class cT) cT.
Coercion ringType cT := Ring.Pack (class cT) cT.

End UnitRing.

Canonical Structure UnitRing.eqType.
Canonical Structure UnitRing.zmodType.
Canonical Structure UnitRing.ringType.

Definition unitDef (R : UnitRing.type) : pred R :=
  UnitRing.unit (UnitRing.class R).
Notation unit := (@unitDef _).
Definition inv (R : UnitRing.type) : R -> R := UnitRing.inv (UnitRing.class R).

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

Section UnitRingTheory.

Variable R : UnitRing.type.
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 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).

End UnitRingTheory.

Section UnitRingMorphism.

Variables (aR rR : UnitRing.type) (f : aR -> rR).
Hypothesis fM : morphism f.

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

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

Lemma ringM_div : forall x y, unit y -> f (x / y) = f x / f y.

End UnitRingMorphism.

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 : UnitRing.type.

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

Boolean test selecting formulas in the theory of rings

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.

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 constructable set, 
 i.e. formulas without quantifiers.

The quantifier elimination check.

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

Record class_of (R : Type) : Type := Class {
  base1 :> ComRing.class_of R;
  ext :> UnitRing.mixin_of (Ring.Pack base1 R)
}.

Coercion base2 R m := UnitRing.Class (@ext R m).

Structure type : Type := Pack {sort :> Type; _ : class_of sort; _ : Type}.
Definition class cT := let: Pack _ c _ := cT return class_of cT in c.

Section Mixin.

Variables (R : ComRing.type) (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 := UnitRing.EtaMixin mulVx mulC_mulrV mulC_unitP.

End Mixin.

Definition pack T :=
  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.

Coercion eqType cT := Equality.Pack (class cT) cT.
Coercion choiceType cT := Choice.Pack (class cT) cT.
Coercion zmodType cT := Zmodule.Pack (class cT) cT.
Coercion ringType cT := Ring.Pack (class cT) cT.
Coercion comRingType cT := ComRing.Pack (class cT) cT.
Coercion unitRingType cT := UnitRing.Pack (class cT) cT.
Definition com_unitRingType cT :=
  @UnitRing.Pack (comRingType cT) (class cT) cT.

End ComUnitRing.

Canonical Structure ComUnitRing.eqType.
Canonical Structure ComUnitRing.choiceType.
Canonical Structure ComUnitRing.zmodType.
Canonical Structure ComUnitRing.ringType.
Canonical Structure ComUnitRing.unitRingType.
Canonical Structure ComUnitRing.comRingType.

Section ComUnitRingTheory.

Variable R : ComUnitRing.type.
Implicit Types x y : R.

Lemma unitr_mul : forall x y, unit (x * y) = unit x && unit y.

End ComUnitRingTheory.

Module IntegralDomain.

Definition axiom (R : Ring.type) :=
  forall x y : R, x * y = 0 -> (x == 0) || (y == 0).

Record class_of (R : Type) : Type :=
  Class {base :> ComUnitRing.class_of R; ext : axiom (Ring.Pack base R)}.

Structure type : Type := Pack {sort :> Type; _ : class_of sort; _ : Type}.
Definition class cT := let: Pack _ c _ := cT return class_of cT in c.
Definition clone T cT c of phant_id (class cT) c := @Pack T c T.

Definition pack T 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.

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

End IntegralDomain.

Canonical Structure IntegralDomain.eqType.
Canonical Structure IntegralDomain.choiceType.
Canonical Structure IntegralDomain.zmodType.
Canonical Structure IntegralDomain.ringType.
Canonical Structure IntegralDomain.unitRingType.
Canonical Structure IntegralDomain.comRingType.
Canonical Structure IntegralDomain.comUnitRingType.

Section IntegralDomainTheory.

Variable R : IntegralDomain.type.
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).

End IntegralDomainTheory.

Module Field.

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

Record class_of (F : Type) : Type := Class {
  base :> IntegralDomain.class_of F;
  ext: mixin_of (UnitRing.Pack base F)
}.

Structure type : Type := Pack {sort :> Type; _ : class_of sort; _ : Type}.
Definition class cT := let: Pack _ c _ := cT return class_of cT in c.
Definition clone T cT c of phant_id (class cT) c := @Pack T c T.

Definition pack T 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.

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

Section Mixins.

Variables (R : ComRing.type) (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.

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

End Field.

Canonical Structure Field.eqType.
Canonical Structure Field.choiceType.
Canonical Structure Field.zmodType.
Canonical Structure Field.ringType.
Canonical Structure Field.unitRingType.
Canonical Structure Field.comRingType.
Canonical Structure Field.comUnitRingType.
Canonical Structure Field.idomainType.

Section FieldTheory.

Variable F : Field.type.
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).

Section FieldMorphismInj.

Variables (R : Ring.type) (f : F -> R).
Hypothesis fRM : morphism f.

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

Lemma fieldM_inj : injective f.

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

End FieldMorphismInj.

Section FieldMorphismInv.

Variables (R : UnitRing.type) (f : F -> R).
Hypothesis fRM : morphism f.

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

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

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

End FieldMorphismInv.

End FieldTheory.

Module DecidableField.

Definition axiom (R : UnitRing.type) (s : seq R -> pred (formula R)) :=
  forall e f, reflect (holds e f) (s e f).

Record mixin_of (R : UnitRing.type) : Type :=
  Mixin { sat : seq R -> pred (formula R); satP : axiom sat}.

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

Structure type : Type := Pack {sort :> Type; _ : class_of sort; _ : Type}.
Definition class cT := let: Pack _ c _ := cT return class_of cT in c.
Definition clone T cT c of phant_id (class cT) c := @Pack T c T.

Definition pack T 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.

Ultimately, there should be a QE Mixin constructor

Structure of field with quantifier elimination

Module QE.

Section Axioms.

Variable R : UnitRing.type.
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 : UnitRing.type) : Type := Mixin {
  proj : nat -> (seq (term R) * seq (term R)) -> formula R;
  wf_proj : wf_proj_axiom proj;
  holds_proj : holds_proj_axiom proj
}.

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

Structure type : Type := Pack {sort :> Type; _ : class_of sort; _ : Type}.
Definition class cT := let: Pack _ c _ := cT return class_of cT in c.
Definition clone T cT c of phant_id (class cT) c := @Pack T c T.

Definition pack T 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.

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

End QE.

Canonical Structure QE.eqType.
Canonical Structure QE.choiceType.
Canonical Structure QE.zmodType.
Canonical Structure QE.ringType.
Canonical Structure QE.unitRingType.
Canonical Structure QE.comRingType.
Canonical Structure QE.comUnitRingType.
Canonical Structure QE.idomainType.
Canonical Structure QE.fieldType.

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.

Let elim_aux f n := foldr Or False (map (proj n) (qf_to_dnf f false)).

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.

Canonical Structure QEDecidableField :=
  DecidableField.Pack (DecidableField.Class QEDecidableFieldMixin) F.

End QE_theory.

Module ClosedField.

Axiom == all non-constant monic polynomials have a root

Definition axiom (R : Ring.type) :=
  forall n (P : nat -> R), n > 0 ->
   exists x : R, x ^+ n = \sum_(i < n) P i * (x ^+ i).

Record class_of (F : Type) : Type :=
  Class {base :> DecidableField.class_of F; _ : axiom (Ring.Pack base F)}.

Structure type : Type := Pack {sort :> Type; _ : class_of sort; _ : Type}.
Definition class cT := let: Pack _ c _ := cT return class_of cT in c.
Definition clone T cT c of phant_id (class cT) c := @Pack T c T.

Definition pack T 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.

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

End ClosedField.

Canonical Structure ClosedField.eqType.
Canonical Structure ClosedField.choiceType.
Canonical Structure ClosedField.zmodType.
Canonical Structure ClosedField.ringType.
Canonical Structure ClosedField.unitRingType.
Canonical Structure ClosedField.comRingType.
Canonical Structure ClosedField.comUnitRingType.
Canonical Structure ClosedField.idomainType.
Canonical Structure ClosedField.fieldType.
Canonical Structure ClosedField.decFieldType.

Section ClosedFieldTheory.

Variable F : ClosedField.type.

Lemma solve_monicpoly : ClosedField.axiom F.

End ClosedFieldTheory.

Module Lmodule.

Section Lmodule.

Variable R : Ring.type.
Implicit Type phR : phant R.

Structure mixin_of (M : Zmodule.type) : Type := Mixin {
  scale : R -> M -> M;
  _ : forall a b m, scale a (scale b m) = scale (a * b) m;
  _ : left_id 1 scale;
  _ : forall a, {morph scale a : m n / m + n};
  _ : forall m, {morph scale^~ m : a b / a + b}
}.

Structure class_of M := Class {
  base :> Zmodule.class_of M;
  ext :> mixin_of (Zmodule.Pack base M)
}.

Structure type phR := Pack {sort :> Type; _ : class_of sort; _ : Type}.
Definition class phR (cT : type phR) :=
  let: Pack _ c _ := cT return class_of cT in c.
Definition clone phR T cT c of phant_id (@class phR cT) c := @Pack phR T c T.
Definition pack phR T 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 phR (@Class T b m) T.

Coercion eqType phR cT := Equality.Pack (@class phR cT) cT.
Coercion choiceType phR cT := Choice.Pack (@class phR cT) cT.
Coercion zmodType phR cT := Zmodule.Pack (@class phR cT) cT.

End Lmodule.

End Lmodule.

Canonical Structure Lmodule.eqType.
Canonical Structure Lmodule.choiceType.
Canonical Structure Lmodule.zmodType.

Definition scale R (M : @Lmodule.type R (Phant R)) : R -> M -> M :=
  Lmodule.scale (Lmodule.class M).

Local Notation "*:%R" := (@scale _ _) : ring_scope.
Local Notation "a *: m" := (scale a m) (at level 40) : ring_scope.

Section LmoduleTheory.

Variable (R : Ring.type) (M : Lmodule.type (Phant R)).
Implicit Type a b c : R.
Implicit Type m : M.

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

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

Lemma scaler_addr : forall a, {morph (scale a : M -> M) : x y / x + y}.

Lemma scaler_addl : forall m, {morph (@scale _ _)^~ m : a b / a + b}.

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

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

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

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

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

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

Lemma scaler_subr : forall a m1 m2, a *: (m1 - m2) = a *: m1 - a *: m2.

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

Lemma scaler_suml : forall m I r (P : pred I) F,
(\sum_(i <- r | P i) F i) *: m = \sum_(i <- r | P i) F i *: m.

Lemma scaler_sumr : forall a I r (P : pred I) (F : I -> M),
   a *: (\sum_(i <- r | P i) F i) = \sum_(i <- r | P i) a *: F i.

End LmoduleTheory.

Module NCalgebra.

Section NCalgebra.

Variable R : Ring.type.
Implicit Type phR : phant R.

Notation scale T L := (@scale R (@Lmodule.pack _ (Phant R) T _ L _ _ id _ id)).
Definition axiom (T: Ring.type) (L: Lmodule.mixin_of R T) :=
  forall k x y, scale T L k (x * y) = scale T L k x * y.

Record class_of (T : Type) : Type := Class {
  base1 :> Ring.class_of T;
  mixin :> Lmodule.mixin_of R (Zmodule.Pack base1 T);
  ext : @axiom (Ring.Pack base1 T) mixin
}.

Coercion base2 R m := Lmodule.Class (@mixin R m).

Structure type phR := Pack {sort :> Type; _ : class_of sort; _ : Type}.
Definition class phR (cT : type phR) :=
  let: Pack _ c _ := cT return class_of cT in c.
Definition clone phR T cT c of phant_id (@class phR cT) c := @Pack phR T c T.
Definition pack phR T b0 m0 (axT: @axiom (@Ring.Pack T b0 T) m0) :=
  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.

Coercion eqType phR cT := Equality.Pack (@class phR cT) cT.
Coercion choiceType phR cT := Choice.Pack (@class phR cT) cT.
Coercion zmodType phR cT := Zmodule.Pack (@class phR cT) cT.
Coercion ringType phR cT := Ring.Pack (@class phR cT) cT.
Coercion lmoduleType phR cT := Lmodule.Pack phR (@class phR cT) cT.

Definition lmod_ringType phR cT :=
  @Lmodule.Pack R phR (Ring.sort (@ringType phR cT)) (base2 (class cT)) (Ring.sort (ringType cT)).

End NCalgebra.

End NCalgebra.

Canonical Structure NCalgebra.eqType.
Canonical Structure NCalgebra.choiceType.
Canonical Structure NCalgebra.zmodType.
Canonical Structure NCalgebra.ringType.
Canonical Structure NCalgebra.lmoduleType.

Section NCalgebraTheory.

Variable R : Ring.type.
Variable A : NCalgebra.type (Phant R).
Implicit Types k: R.
Implicit Types x y: A.

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

Lemma morph_sunit: morphism (fun k => k *: (1: A)).

End NCalgebraTheory.

Module Algebra.

Section Algebra.

Variable R : Ring.type.
Implicit Type phR : phant R.

Definition axiom T1 T2 (scalop: T1->T2->T2) (mulop: T2->T2->T2) :=
               forall k x y, (scalop k (mulop x y)) = (mulop x (scalop k y)) .

Record class_of (T : Type) : Type :=
  Class {base :> NCalgebra.class_of R T;
         _ : axiom (Lmodule.scale (NCalgebra.mixin base)) (Ring.mul (NCalgebra.base1 base))}.

Coercion base2 b   c A := Lmodule.Class (@NCalgebra.mixin b c A).

Structure type phR :Type := Pack {sort :> Type; _ : class_of sort; _ : Type}.
Definition class phR (cT : type phR) :=
  let: Pack _ c _ := cT return class_of cT in c.
Definition clone phR T cT c of phant_id (@class phR cT) c := @Pack phR T c T.

Definition pack phR T scale0 mul0 (axT : @axiom R T scale0 mul0) :=
  fun bT b & phant_id (@NCalgebra.class R phR bT) b =>
  fun ax & phant_id axT ax => Pack phR (@Class T b ax) T.

Coercion eqType phR cT := Equality.Pack (@class phR cT) cT.
Coercion choiceType phR cT := Choice.Pack (@class phR cT) cT.
Coercion zmodType phR cT := Zmodule.Pack (@class phR cT) cT.
Coercion ringType phR cT := Ring.Pack (@class phR cT) cT.
Coercion lmoduleType phR cT := Lmodule.Pack phR (@class phR cT) cT.
Coercion ncalgebraType phR cT := NCalgebra.Pack phR (@class phR cT) cT.

End Algebra.

End Algebra.

Canonical Structure Algebra.eqType.
Canonical Structure Algebra.choiceType.
Canonical Structure Algebra.zmodType.
Canonical Structure Algebra.ringType.
Canonical Structure Algebra.lmoduleType.
Canonical Structure Algebra.ncalgebraType.

Section AlgebraTheory.

Variable R : Ring.type.
Variable A : Algebra.type (Phant R).
Implicit Types k: R.
Implicit Types x y: A.

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

End AlgebraTheory.

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 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 mulrS := mulrS.
Definition mulr1n := mulr1n.
Definition mulrSr := mulrSr.
Definition mulrb := mulrb.
Definition mul0rn := mul0rn.
Definition oppr_muln := oppr_muln.
Definition mulrn_addl := mulrn_addl.
Definition mulrn_addr := mulrn_addr.
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_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_mul := natr_mul.
Definition natr_exp := natr_exp.
Definition expr0 := expr0.
Definition exprS := exprS.
Definition expr1 := expr1.
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 signr_odd := signr_odd.
Definition signr_eq0 := signr_eq0.
Definition signr_addb := signr_addb.
Definition exprN := exprN.
Definition exprn_addl_comm := exprn_addl_comm.
Definition exprn_subl_comm := exprn_subl_comm.
Definition subr_expn_comm := subr_expn_comm.
Definition subr_expn_1 := subr_expn_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 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 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 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 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 ringM_sub := ringM_sub.
Definition ringM_0 := ringM_0.
Definition ringM_1 := ringM_1.
Definition ringM_opp := ringM_opp.
Definition ringM_add := ringM_add.
Definition ringM_sum := ringM_sum.
Definition ringM_mul := ringM_mul.
Definition ringM_prod := ringM_prod.
Definition ringM_natmul := ringM_natmul.
Definition ringM_nat := ringM_nat.
Definition ringM_exp := ringM_exp.
Definition ringM_sign := ringM_sign.
Definition ringM_char := ringM_char.
Definition comp_ringM := comp_ringM.
Definition ringM_isom := ringM_isom.
Definition ringM_comm := ringM_comm.
Definition ringM_unit := ringM_unit.
Definition Frobenius_aut_RM := Frobenius_aut_RM.
Definition fieldM_eq0 := fieldM_eq0.
Definition fieldM_inj := fieldM_inj.
Definition ringM_inv := ringM_inv.
Definition fieldM_char := fieldM_char.
Definition ringM_div := ringM_div.
Definition fieldM_unit := fieldM_unit.
Definition fieldM_inv := fieldM_inv.
Definition fieldM_div := fieldM_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_suml := scaler_suml.
Definition scaler_sumr := scaler_sumr.
Definition scaler_mull := scaler_mull.
Definition morph_sunit := morph_sunit.

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

End Theory.

End GRing.

Canonical Structure GRing.Zmodule.eqType.
Canonical Structure GRing.Zmodule.choiceType.
Canonical Structure GRing.Ring.eqType.
Canonical Structure GRing.Ring.choiceType.
Canonical Structure GRing.Ring.zmodType.
Canonical Structure GRing.UnitRing.eqType.
Canonical Structure GRing.UnitRing.choiceType.
Canonical Structure GRing.UnitRing.zmodType.
Canonical Structure GRing.UnitRing.ringType.
Canonical Structure GRing.ComRing.eqType.
Canonical Structure GRing.ComRing.choiceType.
Canonical Structure GRing.ComRing.zmodType.
Canonical Structure GRing.ComRing.ringType.
Canonical Structure GRing.ComUnitRing.eqType.
Canonical Structure GRing.ComUnitRing.choiceType.
Canonical Structure GRing.ComUnitRing.zmodType.
Canonical Structure GRing.ComUnitRing.ringType.
Canonical Structure GRing.ComUnitRing.unitRingType.
Canonical Structure GRing.ComUnitRing.comRingType.
Canonical Structure GRing.ComUnitRing.com_unitRingType.
Canonical Structure GRing.IntegralDomain.eqType.
Canonical Structure GRing.IntegralDomain.choiceType.
Canonical Structure GRing.IntegralDomain.zmodType.
Canonical Structure GRing.IntegralDomain.ringType.
Canonical Structure GRing.IntegralDomain.unitRingType.
Canonical Structure GRing.IntegralDomain.comRingType.
Canonical Structure GRing.IntegralDomain.comUnitRingType.
Canonical Structure GRing.Field.eqType.
Canonical Structure GRing.Field.choiceType.
Canonical Structure GRing.Field.zmodType.
Canonical Structure GRing.Field.ringType.
Canonical Structure GRing.Field.unitRingType.
Canonical Structure GRing.Field.comRingType.
Canonical Structure GRing.Field.comUnitRingType.
Canonical Structure GRing.Field.idomainType.
Canonical Structure GRing.DecidableField.eqType.
Canonical Structure GRing.DecidableField.choiceType.
Canonical Structure GRing.DecidableField.zmodType.
Canonical Structure GRing.DecidableField.ringType.
Canonical Structure GRing.DecidableField.unitRingType.
Canonical Structure GRing.DecidableField.comRingType.
Canonical Structure GRing.DecidableField.comUnitRingType.
Canonical Structure GRing.DecidableField.idomainType.
Canonical Structure GRing.DecidableField.fieldType.
Canonical Structure GRing.ClosedField.eqType.
Canonical Structure GRing.ClosedField.choiceType.
Canonical Structure GRing.ClosedField.zmodType.
Canonical Structure GRing.ClosedField.ringType.
Canonical Structure GRing.ClosedField.unitRingType.
Canonical Structure GRing.ClosedField.comRingType.
Canonical Structure GRing.ClosedField.comUnitRingType.
Canonical Structure GRing.ClosedField.idomainType.
Canonical Structure GRing.ClosedField.fieldType.
Canonical Structure GRing.ClosedField.decFieldType.

Canonical Structure GRing.add_monoid.
Canonical Structure GRing.add_comoid.
Canonical Structure GRing.mul_monoid.
Canonical Structure GRing.mul_comoid.
Canonical Structure GRing.muloid.
Canonical Structure GRing.addoid.

Canonical Structure GRing.Lmodule.eqType.
Canonical Structure GRing.Lmodule.choiceType.
Canonical Structure GRing.Lmodule.zmodType.

Canonical Structure GRing.NCalgebra.eqType.
Canonical Structure GRing.NCalgebra.choiceType.
Canonical Structure GRing.NCalgebra.zmodType.
Canonical Structure GRing.NCalgebra.ringType.
Canonical Structure GRing.NCalgebra.lmoduleType.

Notation "0" := (GRing.zero _) : ring_scope.
Notation "-%R" := (@GRing.opp _) : ring_scope.
Notation "- x" := (GRing.opp x) : ring_scope.
Notation "+%R" := (@GRing.add _).
Notation "x + y" := (GRing.add x y) : ring_scope.
Notation "x - y" := (GRing.add x (- y)) : ring_scope.
Notation "x *+ n" := (GRing.natmul x n) : ring_scope.
Notation "x *- n" := (GRing.natmul (- x) n) : ring_scope.
Notation "s `_ i" := (seq.nth 0%R s%R i) : ring_scope.

Notation "1" := (GRing.one _) : ring_scope.
Notation "- 1" := (- (1))%R : ring_scope.

Notation "n %:R" := (GRing.natmul 1 n) : ring_scope.
Notation "[ 'char' R ]" := (GRing.char (Phant R)) : ring_scope.
Notation Frobenius_aut chRp := (GRing.Frobenius_aut chRp).
Notation "*%R" := (@GRing.mul _).
Notation "x * y" := (GRing.mul x y) : ring_scope.
Notation "x ^+ n" := (GRing.exp x n) : ring_scope.
Notation "x ^-1" := (GRing.inv x) : ring_scope.
Notation "x ^- n" := (x ^+ n)^-1%R : ring_scope.
Notation "x / y" := (GRing.mul x y^-1) : ring_scope.

Implicit Arguments GRing.unitDef [].

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

Notation "*:%R" := (@GRing.scale _ _) : ring_scope.
Notation "a *: m" := (GRing.scale a m) (at level 40) : 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.

Notation zmodType := GRing.Zmodule.type.
Notation ZmodType T m := (@GRing.Zmodule.pack T m _ _ id).
Notation ZmodMixin := GRing.Zmodule.Mixin.
Notation "[ 'zmodType' 'of' T 'for' cT ]" := (@GRing.Zmodule.clone T cT _ idfun)
  (at level 0, format "[ 'zmodType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'zmodType' 'of' T ]" := (@GRing.Zmodule.clone T _ _ id)
  (at level 0, format "[ 'zmodType' 'of' T ]") : form_scope.

Notation ringType := GRing.Ring.type.
Notation RingType T m := (@GRing.Ring.pack T _ m _ _ id _ id).
Notation RingMixin := GRing.Ring.Mixin.
Notation RevRingType := GRing.RevRingType.
Notation "[ 'ringType' 'of' T 'for' cT ]" := (@GRing.Ring.clone T cT _ idfun)
  (at level 0, format "[ 'ringType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'ringType' 'of' T ]" := (@GRing.Ring.clone T _ _ id)
  (at level 0, format "[ 'ringType' 'of' T ]") : form_scope.

Notation comRingType := GRing.ComRing.type.
Notation ComRingType T m := (@GRing.ComRing.pack T _ m _ _ id _ id).
Notation ComRingMixin := GRing.ComRing.RingMixin.
Notation "[ 'comRingType' 'of' T 'for' cT ]" :=
    (@GRing.ComRing.clone T cT _ idfun)
  (at level 0, format "[ 'comRingType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'comRingType' 'of' T ]" := (@GRing.ComRing.clone T _ _ id)
  (at level 0, format "[ 'comRingType' 'of' T ]") : form_scope.

Notation unitRingType := GRing.UnitRing.type.
Notation UnitRingType T m := (@GRing.UnitRing.pack T _ m _ _ id _ id).
Notation UnitRingMixin := GRing.UnitRing.EtaMixin.
Notation "[ 'unitRingType' 'of' T 'for' cT ]" :=
    (@GRing.UnitRing.clone T cT _ idfun)
  (at level 0, format "[ 'unitRingType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'unitRingType' 'of' T ]" := (@GRing.UnitRing.clone T _ _ id)
  (at level 0, format "[ 'unitRingType' 'of' T ]") : form_scope.

Notation comUnitRingType := GRing.ComUnitRing.type.
Notation ComUnitRingMixin := GRing.ComUnitRing.Mixin.
Notation "[ 'comUnitRingType' 'of' T ]" :=
    (@GRing.ComUnitRing.pack T _ _ id _ _ id)
  (at level 0, format "[ 'comUnitRingType' 'of' T ]") : form_scope.

Notation idomainType := GRing.IntegralDomain.type.
Notation IdomainType T m := (@GRing.IntegralDomain.pack T _ m _ _ id _ id).
Notation "[ 'idomainType' 'of' T 'for' cT ]" :=
    (@GRing.IntegralDomain.clone T cT _ idfun)
  (at level 0, format "[ 'idomainType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'idomainType' 'of' T ]" := (@GRing.IntegralDomain.clone T _ _ id)
  (at level 0, format "[ 'idomainType' 'of' T ]") : form_scope.

Notation fieldType := GRing.Field.type.
Notation FieldType T m := (@GRing.Field.pack T _ m _ _ id _ id).
Notation FieldUnitMixin := GRing.Field.UnitMixin.
Notation FieldIdomainMixin := GRing.Field.IdomainMixin.
Notation FieldMixin := GRing.Field.Mixin.
Notation "[ 'fieldType' 'of' T 'for' cT ]" := (@GRing.Field.clone T cT _ idfun)
  (at level 0, format "[ 'fieldType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'fieldType' 'of' T ]" := (@GRing.Field.clone T _ _ id)
  (at level 0, format "[ 'fieldType' 'of' T ]") : form_scope.

Notation decFieldType := GRing.DecidableField.type.
Notation DecFieldType T m := (@GRing.DecidableField.pack T _ m _ _ id _ id).
Notation DecFieldMixin := GRing.DecidableField.Mixin.
Notation "[ 'decFieldType' 'of' T 'for' cT ]" :=
    (@GRing.DecidableField.clone T cT _ idfun)
  (at level 0, format "[ 'decFieldType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'decFieldType' 'of' T ]" := (@GRing.DecidableField.clone T _ _ id)
  (at level 0, format "[ 'decFieldType' 'of' T ]") : form_scope.

Notation closedFieldType := GRing.ClosedField.type.
Notation ClosedFieldType T m := (GRing.ClosedField.pack T _ m _ _ id _ id).
Notation "[ 'closedFieldType' 'of' T 'for' cT ]" :=
    (@GRing.ClosedField.clone T cT _ idfun)
  (at level 0,
   format "[ 'closedFieldType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'closedFieldType' 'of' T ]" := (@GRing.ClosedField.clone T _ _ id)
  (at level 0, format "[ 'closedFieldType' 'of' T ]") : form_scope.

Notation lmodType R := (GRing.Lmodule.type (Phant R)).
Notation LmodType R T m :=
   (@GRing.Lmodule.pack _ (Phant R) T _ m _ _ id _ id).
Notation LmodMixin := GRing.Lmodule.Mixin.
Notation "[ 'lmodType' [ R ] 'of' T 'for' cT ]" :=
  (@GRing.Lmodule.clone _ (Phant R) T cT _ idfun)
  (at level 0, format "[ 'lmodType' [ R ] 'of' T 'for' cT ]")
  : form_scope.
Notation "[ 'lmodType' [ R ] 'of' T ]" :=
  (@GRing.Lmodule.clone _ (Phant R) T _ _ id)
  (at level 0, format "[ 'lmodType' [ R ] 'of' T ]") : form_scope.

Notation ncalgebraType R := (GRing.NCalgebra.type (Phant R)).
Notation NCalgebraType R T m a :=
   (@GRing.NCalgebra.pack _ (Phant R) T _ m a _ _ id _ _ id _ id).
Notation "[ 'ncalgebraType' [ R ] 'of' T 'for' cT ]" :=
  (@GRing.NCalgebra.clone _ (Phant R) T cT _ idfun)
  (at level 0, format "[ 'ncalgebraType' [ R ] 'of' T 'for' cT ]")
  : form_scope.
Notation "[ 'ncalgebraType' [ R ] 'of' T ]" :=
  (@GRing.NCalgebra.clone _ (Phant R) T _ _ id)
  (at level 0, format "[ 'ncalgebraType' [ R ] 'of' T ]") : form_scope.