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