Library Coq.setoid_ring.InitialRing

Require Import Zbool.
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 Zeq_bool 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,
   Zeq_bool 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 Zeq_bool 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.