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.
Z is a ring and a setoid
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).
Two generic morphisms from Z to (abrbitrary) rings, second one is more convenient for proofs but they are ext. equal
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.
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.
N is a semi-ring and a setoid
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.
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.