Library Coq.setoid_ring.Ncring_initial
Z is a ring and a setoid
Two generic morphisms from Z to (arbitrary) rings, second one is more convenient for proofs but they are ext. equal
Section ZMORPHISM.
Context {
R:
Type}`{
Ring R}.
Ltac rrefl :=
reflexivity.
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) :
ZMORPHISM.
Open Scope ZMORPHISM.
Definition get_signZ z :=
match z with
|
Zneg p =>
Some (
Zpos p)
|
_ =>
None
end.
Ltac norm :=
gen_rewrite.
Ltac add_push :=
Ncring.gen_add_push.
Ltac rsimpl :=
simpl.
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.
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 (
Z.pos_sub x y)
== 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_opp :
forall x,
[- x] == - [x].
Lemma gen_phiZ_mul :
forall x y,
[x * y] == [x] * [y].
Lemma gen_phiZ_ext :
forall x y :
Z,
x = y -> [x] == [y].
Global Instance gen_phiZ_morph :
(@
Ring_morphism (
Z:
Type)
R _ _ _ _ _ _ _ Zops Zr _ _ _ _ _ _ _ _ _ gen_phiZ) .
Defined.
End ZMORPHISM.
Instance multiplication_phi_ring{
R:
Type}`{
Ring R} :
Multiplication :=
{
multiplication x y :=
(gen_phiZ x) * y}.