# Library Coq.setoid_ring.InitialRing

Require Import ZArith_base.
Require Import Zpow_def.
Require Import BinInt.
Require Import BinNat.
Require Import Setoid.
Require Import Ring_theory.
Require Import Ring_polynom.
Require Import ZOdiv_def.
Import List.
Import RingSyntax.
Definition NotConstant := false.
Z is a ring and a setoid
Lemma Zsth : Setoid_Theory Z (@eq Z).
Lemma Zeqe : ring_eq_ext Zplus Zmult Zopp (@eq Z).
Lemma Zth : ring_theory Z0 (Zpos xH) Zplus Zmult Zminus Zopp (@eq Z).
Two generic morphisms from Z to (abrbitrary) rings,
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 Setoid R req Rsth as R_setoid3.
Ltac rrefl := gen_reflexivity Rsth.
Variable Reqe : ring_eq_ext radd rmul ropp req.
Add Morphism radd : radd_ext3.
Add Morphism rmul : rmul_ext3.
Add Morphism ropp : 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 Zopp Zeq_bool get_signZ.
Section ALMOST_RING.
Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req.
Add Morphism rsub : 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 (Psucc 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 : 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_add_pos_neg : forall x y,
gen_phiZ1
match (x ?= y)%positive Eq with
| Eq => Z0
| Lt => Zneg (y - x)
| Gt => Zpos (x - y)
end
== gen_phiPOS1 x + -gen_phiPOS1 y.
Lemma match_compOpp : forall x (B:Type) (be bl bg:B),
match CompOpp x with Eq => be | Lt => bl | Gt => bg end
= match x with Eq => be | Lt => bg | Gt => bl end.
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)
Zplus Zmult Zminus Zopp Zeq_bool gen_phiZ.
End ZMORPHISM.
N is a semi-ring and a setoid
Lemma Nsth : Setoid_Theory N (@eq N).
Lemma Nseqe : sring_eq_ext Nplus Nmult (@eq N).
Lemma Nth : semi_ring_theory N0 (Npos xH) Nplus Nmult (@eq N).
Definition Nsub := SRsub Nplus.
Definition Nopp := (@SRopp N).
Lemma Neqe : ring_eq_ext Nplus Nmult Nopp (@eq N).
Lemma Nath :
almost_ring_theory N0 (Npos xH) Nplus Nmult Nsub Nopp (@eq N).
Definition Neq_bool (x y:N) :=
match Ncompare x y with
| Eq => true
| _ => false
end.
Lemma Neq_bool_ok : forall x y, Neq_bool x y = true -> x = y.
Lemma Neq_bool_complete : forall x y, Neq_bool 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 Setoid R req 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 : radd_ext4.
Add Morphism rmul : rmul_ext4.
Add Morphism ropp : ropp_ext4.
Add Morphism rsub : rsub_ext5.
Ltac norm := gen_srewrite 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
N0 (Npos xH) Nplus Nmult Nsub Nopp Neq_bool 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 Neq_bool 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 Setoid R req Rsth as R_setoid5.
Ltac rrefl := gen_reflexivity Rsth.
Variable Reqe : ring_eq_ext radd rmul ropp req.
Add Morphism radd : radd_ext5.
Add Morphism rmul : rmul_ext5.
Add Morphism ropp : ropp_ext5.
Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req.
Add Morphism rsub : 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 Setoid R req Rsth as R_set1.
Ltac rrefl := gen_reflexivity Rsth.
Add Morphism radd : radd_ext.
Add Morphism rmul : rmul_ext.
Add Morphism ropp : ropp_ext.
Add Morphism rsub : 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 Zplus Zmult zphi ZOdiv_eucl.
Variable nphi : N -> R.
Lemma Ntriv_div_th : div_theory req Nplus Nmult nphi Ndiv_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 Zplus Zmult ?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 Nplus Nmult ?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 =>
match 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
match 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
match d_spec with
| @mkhypo (div_theory _ _ _ _ ?cdiv) ?dd_spec =>
let gen_lemma2_2 := constr:(gen_lemma2_1 cdiv dd_spec) in
match 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 4 "ring: bad sign specification"
end
| _ => fail 3 "ring: bad coefficiant division specification"
end
| _ => fail 2 "ring: bad power specification"
end
| _ => fail 1 "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
| P_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.