Library Stdlib.setoid_ring.InitialRing

Require Import BinInt.
Require Import BinNat.
Require Import Setoid.
Require Import Ring_theory.
Require Import Ring_polynom.
Import List.

Set Implicit Arguments.

Import RingSyntax.

Definition NotConstant := false.

Lemma Zsth : Setoid_Theory Z (@eq Z).

Lemma Zeqe : ring_eq_ext Z.add Z.mul Z.opp (@eq Z).

Lemma Zth : ring_theory Z0 (Zpos xH) Z.add Z.mul Z.sub Z.opp (@eq Z).

Section ZMORPHISM.
 Variable R : Type.
 Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R).
 Variable req : R -> R -> Prop.
  Notation "0" := rO. Notation "1" := rI.
  Notation "x + y" := (radd x y). Notation "x * y " := (rmul x y).
  Notation "x - y " := (rsub x y). Notation "- x" := (ropp x).
  Notation "x == y" := (req x y).
  Variable Rsth : Setoid_Theory R req.
     Add Parametric Relation : R req
       reflexivity proved by (@Equivalence_Reflexive _ _ Rsth)
       symmetry proved by (@Equivalence_Symmetric _ _ Rsth)
       transitivity proved by (@Equivalence_Transitive _ _ Rsth)
      as R_setoid3.
     Ltac rrefl := gen_reflexivity Rsth.
 Variable Reqe : ring_eq_ext radd rmul ropp req.
   Add Morphism radd with signature (req ==> req ==> req) as radd_ext3.
   Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext3.
   Add Morphism ropp with signature (req ==> req) as ropp_ext3.

 Fixpoint gen_phiPOS1 (p:positive) : R :=
  match p with
  | xH => 1
  | xO p => (1 + 1) * (gen_phiPOS1 p)
  | xI p => 1 + ((1 + 1) * (gen_phiPOS1 p))
  end.

 Fixpoint gen_phiPOS (p:positive) : R :=
  match p with
  | xH => 1
  | xO xH => (1 + 1)
  | xO p => (1 + 1) * (gen_phiPOS p)
  | xI xH => 1 + (1 +1)
  | xI p => 1 + ((1 + 1) * (gen_phiPOS p))
  end.

 Definition gen_phiZ1 z :=
  match z with
  | Zpos p => gen_phiPOS1 p
  | Z0 => 0
  | Zneg p => -(gen_phiPOS1 p)
  end.

 Definition gen_phiZ z :=
  match z with
  | Zpos p => gen_phiPOS p
  | Z0 => 0
  | Zneg p => -(gen_phiPOS p)
  end.
 Notation "[ x ]" := (gen_phiZ x).

 Definition get_signZ z :=
  match z with
  | Zneg p => Some (Zpos p)
  | _ => None
  end.

 Lemma get_signZ_th : sign_theory Z.opp Z.eqb get_signZ.

 Section ALMOST_RING.
 Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req.
   Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext3.
   Ltac norm := gen_srewrite Rsth Reqe ARth.
   Ltac add_push := gen_add_push radd Rsth Reqe ARth.

 Lemma same_gen : forall x, gen_phiPOS1 x == gen_phiPOS x.

 Lemma ARgen_phiPOS_Psucc : forall x,
   gen_phiPOS1 (Pos.succ x) == 1 + (gen_phiPOS1 x).

 Lemma ARgen_phiPOS_add : forall x y,
   gen_phiPOS1 (x + y) == (gen_phiPOS1 x) + (gen_phiPOS1 y).

 Lemma ARgen_phiPOS_mult :
   forall x y, gen_phiPOS1 (x * y) == gen_phiPOS1 x * gen_phiPOS1 y.

 End ALMOST_RING.

 Variable Rth : ring_theory 0 1 radd rmul rsub ropp req.
 Let ARth := Rth_ARth Rsth Reqe Rth.
   Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext4.
   Ltac norm := gen_srewrite Rsth Reqe ARth.
   Ltac add_push := gen_add_push radd Rsth Reqe ARth.

 Lemma same_genZ : forall x, [x] == gen_phiZ1 x.

 Lemma gen_Zeqb_ok : forall x y,
   Z.eqb x y = true -> [x] == [y].

 Lemma gen_phiZ1_pos_sub : forall x y,
 gen_phiZ1 (Z.pos_sub x y) == gen_phiPOS1 x + -gen_phiPOS1 y.

 Lemma gen_phiZ_add : forall x y, [x + y] == [x] + [y].

 Lemma gen_phiZ_mul : forall x y, [x * y] == [x] * [y].

 Lemma gen_phiZ_ext : forall x y : Z, x = y -> [x] == [y].

 Lemma gen_phiZ_morph :
  ring_morph 0 1 radd rmul rsub ropp req Z0 (Zpos xH)
   Z.add Z.mul Z.sub Z.opp Z.eqb gen_phiZ.

End ZMORPHISM.

Lemma Nsth : Setoid_Theory N (@eq N).

Lemma Nseqe : sring_eq_ext N.add N.mul (@eq N).

Lemma Nth : semi_ring_theory 0%N 1%N N.add N.mul (@eq N).

Definition Nsub := SRsub N.add.
Definition Nopp := (@SRopp N).

Lemma Neqe : ring_eq_ext N.add N.mul Nopp (@eq N).

Lemma Nath :
 almost_ring_theory 0%N 1%N N.add N.mul Nsub Nopp (@eq N).

Lemma Neqb_ok : forall x y, N.eqb x y = true -> x = y.

Section NMORPHISM.
 Variable R : Type.
 Variable (rO rI : R) (radd rmul: R->R->R).
 Variable req : R -> R -> Prop.
  Notation "0" := rO. Notation "1" := rI.
  Notation "x + y" := (radd x y). Notation "x * y " := (rmul x y).
 Variable Rsth : Setoid_Theory R req.
     Add Parametric Relation : R req
       reflexivity proved by (@Equivalence_Reflexive _ _ Rsth)
       symmetry proved by (@Equivalence_Symmetric _ _ Rsth)
       transitivity proved by (@Equivalence_Transitive _ _ Rsth)
       as R_setoid4.
     Ltac rrefl := gen_reflexivity Rsth.
 Variable SReqe : sring_eq_ext radd rmul req.
 Variable SRth : semi_ring_theory 0 1 radd rmul req.
 Let ARth := SRth_ARth Rsth SRth.
 Let Reqe := SReqe_Reqe SReqe.
 Let ropp := (@SRopp R).
 Let rsub := (@SRsub R radd).
  Notation "x - y " := (rsub x y). Notation "- x" := (ropp x).
  Notation "x == y" := (req x y).
   Add Morphism radd with signature (req ==> req ==> req) as radd_ext4.
   Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext4.
   Ltac norm := gen_srewrite_sr Rsth Reqe ARth.

 Definition gen_phiN1 x :=
  match x with
  | N0 => 0
  | Npos x => gen_phiPOS1 1 radd rmul x
  end.

 Definition gen_phiN x :=
  match x with
  | N0 => 0
  | Npos x => gen_phiPOS 1 radd rmul x
  end.
 Notation "[ x ]" := (gen_phiN x).

 Lemma same_genN : forall x, [x] == gen_phiN1 x.

 Lemma gen_phiN_add : forall x y, [x + y] == [x] + [y].

 Lemma gen_phiN_mult : forall x y, [x * y] == [x] * [y].

 Lemma gen_phiN_sub : forall x y, [Nsub x y] == [x] - [y].

 Lemma gen_phiN_morph : ring_morph 0 1 radd rmul rsub ropp req
                           0%N 1%N N.add N.mul Nsub Nopp N.eqb gen_phiN.

End NMORPHISM.

Definition Nword := list N.
Definition NwO : Nword := nil.
Definition NwI : Nword := 1%N :: nil.

Definition Nwcons n (w : Nword) : Nword :=
  match w, n with
  | nil, 0%N => nil
  | _, _ => n :: w
  end.

Fixpoint Nwadd (w1 w2 : Nword) {struct w1} : Nword :=
  match w1, w2 with
  | n1::w1', n2:: w2' => (n1+n2)%N :: Nwadd w1' w2'
  | nil, _ => w2
  | _, nil => w1
  end.

Definition Nwopp (w:Nword) : Nword := Nwcons 0%N w.

Definition Nwsub w1 w2 := Nwadd w1 (Nwopp w2).

Fixpoint Nwscal (n : N) (w : Nword) {struct w} : Nword :=
  match w with
  | m :: w' => (n*m)%N :: Nwscal n w'
  | nil => nil
  end.

Fixpoint Nwmul (w1 w2 : Nword) {struct w1} : Nword :=
  match w1 with
  | 0%N::w1' => Nwopp (Nwmul w1' w2)
  | n1::w1' => Nwsub (Nwscal n1 w2) (Nwmul w1' w2)
  | nil => nil
  end.
Fixpoint Nw_is0 (w : Nword) : bool :=
  match w with
  | nil => true
  | 0%N :: w' => Nw_is0 w'
  | _ => false
  end.

Fixpoint Nweq_bool (w1 w2 : Nword) {struct w1} : bool :=
  match w1, w2 with
  | n1::w1', n2::w2' =>
     if N.eqb n1 n2 then Nweq_bool w1' w2' else false
  | nil, _ => Nw_is0 w2
  | _, nil => Nw_is0 w1
  end.

Section NWORDMORPHISM.
 Variable R : Type.
 Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R).
 Variable req : R -> R -> Prop.
  Notation "0" := rO. Notation "1" := rI.
  Notation "x + y" := (radd x y). Notation "x * y " := (rmul x y).
  Notation "x - y " := (rsub x y). Notation "- x" := (ropp x).
  Notation "x == y" := (req x y).
  Variable Rsth : Setoid_Theory R req.
     Add Parametric Relation : R req
       reflexivity proved by (@Equivalence_Reflexive _ _ Rsth)
       symmetry proved by (@Equivalence_Symmetric _ _ Rsth)
       transitivity proved by (@Equivalence_Transitive _ _ Rsth)
      as R_setoid5.
     Ltac rrefl := gen_reflexivity Rsth.
 Variable Reqe : ring_eq_ext radd rmul ropp req.
   Add Morphism radd with signature (req ==> req ==> req) as radd_ext5.
   Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext5.
   Add Morphism ropp with signature (req ==> req) as ropp_ext5.

 Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req.
   Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext7.
   Ltac norm := gen_srewrite Rsth Reqe ARth.
   Ltac add_push := gen_add_push radd Rsth Reqe ARth.

 Fixpoint gen_phiNword (w : Nword) : R :=
  match w with
  | nil => 0
  | n :: nil => gen_phiN rO rI radd rmul n
  | N0 :: w' => - gen_phiNword w'
  | n::w' => gen_phiN rO rI radd rmul n - gen_phiNword w'
  end.

 Lemma gen_phiNword0_ok : forall w, Nw_is0 w = true -> gen_phiNword w == 0.

  Lemma gen_phiNword_cons : forall w n,
    gen_phiNword (n::w) == gen_phiN rO rI radd rmul n - gen_phiNword w.

  Lemma gen_phiNword_Nwcons : forall w n,
    gen_phiNword (Nwcons n w) == gen_phiN rO rI radd rmul n - gen_phiNword w.

 Lemma gen_phiNword_ok : forall w1 w2,
   Nweq_bool w1 w2 = true -> gen_phiNword w1 == gen_phiNword w2.

Lemma Nwadd_ok : forall x y,
   gen_phiNword (Nwadd x y) == gen_phiNword x + gen_phiNword y.

Lemma Nwopp_ok : forall x, gen_phiNword (Nwopp x) == - gen_phiNword x.

Lemma Nwscal_ok : forall n x,
  gen_phiNword (Nwscal n x) == gen_phiN rO rI radd rmul n * gen_phiNword x.

Lemma Nwmul_ok : forall x y,
   gen_phiNword (Nwmul x y) == gen_phiNword x * gen_phiNword y.

 Lemma gen_phiNword_morph :
  ring_morph 0 1 radd rmul rsub ropp req
   NwO NwI Nwadd Nwmul Nwsub Nwopp Nweq_bool gen_phiNword.

End NWORDMORPHISM.

Section GEN_DIV.

  Variables (R : Type) (rO : R) (rI : R) (radd : R -> R -> R)
              (rmul : R -> R -> R) (rsub : R -> R -> R) (ropp : R -> R)
              (req : R -> R -> Prop) (C : Type) (cO : C) (cI : C)
              (cadd : C -> C -> C) (cmul : C -> C -> C) (csub : C -> C -> C)
              (copp : C -> C) (ceqb : C -> C -> bool) (phi : C -> R).
 Variable Rsth : Setoid_Theory R req.
 Variable Reqe : ring_eq_ext radd rmul ropp req.
 Variable ARth : almost_ring_theory rO rI radd rmul rsub ropp req.
 Variable morph : ring_morph rO rI radd rmul rsub ropp req cO cI cadd cmul csub copp ceqb phi.

  Add Parametric Relation : R req
    reflexivity proved by (@Equivalence_Reflexive _ _ Rsth)
    symmetry proved by (@Equivalence_Symmetric _ _ Rsth)
    transitivity proved by (@Equivalence_Transitive _ _ Rsth)
   as R_set1.
 Ltac rrefl := gen_reflexivity Rsth.
  Add Morphism radd with signature (req ==> req ==> req) as radd_ext.
  Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext.
  Add Morphism ropp with signature (req ==> req) as ropp_ext.
  Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext.
 Ltac rsimpl := gen_srewrite Rsth Reqe ARth.

 Definition triv_div x y :=
   if ceqb x y then (cI, cO)
   else (cO, x).

 Ltac Esimpl :=repeat (progress (
   match goal with
   | |- context [phi cO] => rewrite (morph0 morph)
   | |- context [phi cI] => rewrite (morph1 morph)
   | |- context [phi (cadd ?x ?y)] => rewrite ((morph_add morph) x y)
   | |- context [phi (cmul ?x ?y)] => rewrite ((morph_mul morph) x y)
   | |- context [phi (csub ?x ?y)] => rewrite ((morph_sub morph) x y)
   | |- context [phi (copp ?x)] => rewrite ((morph_opp morph) x)
   end)).

 Lemma triv_div_th : Ring_theory.div_theory req cadd cmul phi triv_div.

 Variable zphi : Z -> R.

 Lemma Ztriv_div_th : div_theory req Z.add Z.mul zphi Z.quotrem.

 Variable nphi : N -> R.

 Lemma Ntriv_div_th : div_theory req N.add N.mul nphi N.div_eucl.

End GEN_DIV.

 Ltac inv_gen_phi_pos rI add mul t :=
   let rec inv_cst t :=
   match t with
     rI => constr:(1%positive)
   | (add rI rI) => constr:(2%positive)
   | (add rI (add rI rI)) => constr:(3%positive)
   | (mul (add rI rI) ?p) =>
       match inv_cst p with
         NotConstant => constr:(NotConstant)
       | 1%positive => constr:(NotConstant)
       | ?p => constr:(xO p)
       end
   | (add rI (mul (add rI rI) ?p)) =>
       match inv_cst p with
         NotConstant => constr:(NotConstant)
       | 1%positive => constr:(NotConstant)
       | ?p => constr:(xI p)
       end
   | _ => constr:(NotConstant)
   end in
   inv_cst t.

 Ltac inv_gen_phiNword rO rI add mul opp t :=
   match t with
     rO => constr:(NwO)
   | _ =>
     match inv_gen_phi_pos rI add mul t with
       NotConstant => constr:(NotConstant)
     | ?p => constr:(Npos p::nil)
     end
   end.

 Ltac inv_gen_phiN rO rI add mul t :=
   match t with
     rO => constr:(0%N)
   | _ =>
     match inv_gen_phi_pos rI add mul t with
       NotConstant => constr:(NotConstant)
     | ?p => constr:(Npos p)
     end
   end.

 Ltac inv_gen_phiZ rO rI add mul opp t :=
   match t with
     rO => constr:(0%Z)
   | (opp ?p) =>
     match inv_gen_phi_pos rI add mul p with
       NotConstant => constr:(NotConstant)
     | ?p => constr:(Zneg p)
     end
   | _ =>
     match inv_gen_phi_pos rI add mul t with
       NotConstant => constr:(NotConstant)
     | ?p => constr:(Zpos p)
     end
   end.

Ltac inv_gen_phi rO rI cO cI t :=
  match t with
  | rO => cO
  | rI => cI
  end.

 Ltac inv_morph_nothing t := constr:(NotConstant).

Ltac coerce_to_almost_ring set ext rspec :=
  match type of rspec with
  | ring_theory _ _ _ _ _ _ _ => constr:(Rth_ARth set ext rspec)
  | semi_ring_theory _ _ _ _ _ => constr:(SRth_ARth set rspec)
  | almost_ring_theory _ _ _ _ _ _ _ => rspec
  | _ => fail 1 "not a valid ring theory"
  end.

Ltac coerce_to_ring_ext ext :=
  match type of ext with
  | ring_eq_ext _ _ _ _ => ext
  | sring_eq_ext _ _ _ => constr:(SReqe_Reqe ext)
  | _ => fail 1 "not a valid ring_eq_ext theory"
  end.

Ltac abstract_ring_morphism set ext rspec :=
  match type of rspec with
  | ring_theory _ _ _ _ _ _ _ => constr:(gen_phiZ_morph set ext rspec)
  | semi_ring_theory _ _ _ _ _ => constr:(gen_phiN_morph set ext rspec)
  | almost_ring_theory _ _ _ _ _ _ _ =>
      constr:(gen_phiNword_morph set ext rspec)
  | _ => fail 1 "bad ring structure"
  end.

Record hypo : Type := mkhypo {
   hypo_type : Type;
   hypo_proof : hypo_type
 }.

Ltac gen_ring_pow set arth pspec :=
 match pspec with
 | None =>
   match type of arth with
   | @almost_ring_theory ?R ?rO ?rI ?radd ?rmul ?rsub ?ropp ?req =>
     constr:(mkhypo (@pow_N_th R rI rmul req set))
   | _ => fail 1 "gen_ring_pow"
   end
 | Some ?t => constr:(t)
 end.

Ltac gen_ring_sign morph sspec :=
  match sspec with
  | None =>
    match type of morph with
    | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
               Z ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceqb ?phi =>
       constr:(@mkhypo (sign_theory copp ceqb get_signZ) get_signZ_th)
    | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
               ?C ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceqb ?phi =>
        constr:(mkhypo (@get_sign_None_th C copp ceqb))
    | _ => fail 2 "ring anomaly : default_sign_spec"
    end
 | Some ?t => constr:(t)
 end.

Ltac default_div_spec set reqe arth morph :=
 match type of morph with
 | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
               Z ?c0 ?c1 Z.add Z.mul ?csub ?copp ?ceq_b ?phi =>
      constr:(mkhypo (Ztriv_div_th set phi))
 | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
               N ?c0 ?c1 N.add N.mul ?csub ?copp ?ceq_b ?phi =>
      constr:(mkhypo (Ntriv_div_th set phi))
 | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
               ?C ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceq_b ?phi =>
      constr:(mkhypo (triv_div_th set reqe arth morph))
 | _ => fail 1 "ring anomaly : default_sign_spec"
 end.

Ltac gen_ring_div set reqe arth morph dspec :=
 match dspec with
 | None => default_div_spec set reqe arth morph
 | Some ?t => constr:(t)
 end.

Ltac ring_elements set ext rspec pspec sspec dspec rk :=
  let arth := coerce_to_almost_ring set ext rspec in
  let ext_r := coerce_to_ring_ext ext in
  let morph :=
    match rk with
    | Abstract => abstract_ring_morphism set ext rspec
    | @Computational ?reqb_ok =>
        match type of arth with
        | almost_ring_theory ?rO ?rI ?add ?mul ?sub ?opp _ =>
            constr:(IDmorph rO rI add mul sub opp set _ reqb_ok)
        | _ => fail 2 "ring anomaly"
        end
    | @Morphism ?m =>
       match type of m with
       | ring_morph _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ => m
       | @semi_morph _ _ _ _ _ _ _ _ _ _ _ _ _ =>
           constr:(SRmorph_Rmorph set m)
       | _ => fail 2 "ring anomaly"
       end
    | _ => fail 1 "ill-formed ring kind"
    end in
  let p_spec := gen_ring_pow set arth pspec in
  let s_spec := gen_ring_sign morph sspec in
  let d_spec := gen_ring_div set ext_r arth morph dspec in
  fun f => f arth ext_r morph p_spec s_spec d_spec.


 Ltac ring_lemmas set ext rspec pspec sspec dspec rk :=
  let gen_lemma2 :=
    match pspec with
    | None => constr:(ring_rw_correct)
    | Some _ => constr:(ring_rw_pow_correct)
    end in
  ring_elements set ext rspec pspec sspec dspec rk
    ltac:(fun arth ext_r morph p_spec s_spec d_spec =>
       lazymatch type of morph with
       | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
               ?C ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceq_b ?phi =>
          let gen_lemma2_0 :=
              constr:(gen_lemma2 R r0 rI radd rmul rsub ropp req set ext_r arth
                                C c0 c1 cadd cmul csub copp ceq_b phi morph) in
          lazymatch p_spec with
          | @mkhypo (power_theory _ _ _ ?Cp_phi ?rpow) ?pp_spec =>
             let gen_lemma2_1 := constr:(gen_lemma2_0 _ Cp_phi rpow pp_spec) in
             lazymatch d_spec with
             | @mkhypo (div_theory _ _ _ _ ?cdiv) ?dd_spec =>
                let gen_lemma2_2 := constr:(gen_lemma2_1 cdiv dd_spec) in
                lazymatch s_spec with
                | @mkhypo (sign_theory _ _ ?get_sign) ?ss_spec =>
                  let lemma2 := constr:(gen_lemma2_2 get_sign ss_spec) in
                  let lemma1 :=
                    constr:(ring_correct set ext_r arth morph pp_spec dd_spec) in
                  fun f => f arth ext_r morph lemma1 lemma2
                | _ => fail "ring: bad sign specification"
                end
             | _ => fail "ring: bad coefficient division specification"
             end
          | _ => fail "ring: bad power specification"
          end
       | _ => fail "ring internal error: ring_lemmas, please report"
       end).

Ltac isnatcst t :=
  match t with
    O => constr:(true)
  | S ?p => isnatcst p
  | _ => constr:(false)
  end.

Ltac isPcst t :=
  match t with
  | xI ?p => isPcst p
  | xO ?p => isPcst p
  | xH => constr:(true)
  
  | Pos.of_succ_nat ?n => isnatcst n
  | _ => constr:(false)
  end.

Ltac isNcst t :=
  match t with
    N0 => constr:(true)
  | Npos ?p => isPcst p
  | _ => constr:(false)
  end.

Ltac isZcst t :=
  match t with
    Z0 => constr:(true)
  | Zpos ?p => isPcst p
  | Zneg ?p => isPcst p
  
  | Z.of_nat ?n => isnatcst n
  
  | Z.of_N ?n => isNcst n
  
  | _ => constr:(false)
  end.

Register PExpr as plugins.ring.pexpr.
Register PEc as plugins.ring.const.
Register PEX as plugins.ring.var.
Register PEadd as plugins.ring.add.
Register PEsub as plugins.ring.sub.
Register PEmul as plugins.ring.mul.
Register PEopp as plugins.ring.opp.
Register PEpow as plugins.ring.pow.
Register PEeval as plugins.ring.eval.

Register almost_ring_theory as plugins.ring.almost_ring_theory.
Register semi_ring_theory as plugins.ring.semi_ring_theory.
Register ring_theory as plugins.ring.ring_theory.

Register Eqsth as plugins.ring.Eqsth.
Register Eq_ext as plugins.ring.Eq_ext.
Register Eq_s_ext as plugins.ring.Eq_s_ext.

Register Abstract as plugins.ring.Abstract.
Register Computational as plugins.ring.Computational.
Register Morphism as plugins.ring.Morphism.

Register IDphi as plugins.ring.IDphi.
Register gen_phiZ as plugins.ring.gen_phiZ.

Register Pphi_dev as plugins.ring.Pphi_dev.
Register Pphi_pow as plugins.ring.Pphi_pow.

Register mk_reqe as plugins.ring.mk_reqe.
Register mk_seqe as plugins.ring.mk_seqe.

Register mkhypo as plugins.ring.mkhypo.
Register hypo as plugins.ring.hypo.