Library Stdlib.setoid_ring.Ncring_initial
From Stdlib Require Import BinInt.
From Stdlib Require Import Zpow_def.
From Stdlib Require Import BinInt.
From Stdlib Require Import BinNat.
From Stdlib Require Import Setoid.
From Stdlib Require Import BinList.
From Stdlib Require Import BinPos.
From Stdlib Require Import BinNat.
From Stdlib Require Import BinInt.
From Stdlib Require Import Setoid.
From Stdlib Require Export Ncring.
From Stdlib Require Export Ncring_polynom.
From Stdlib Require Zbool.
Set Implicit Arguments.
Definition NotConstant := false.
Z is a ring and a setoid
Lemma Zsth : Equivalence (@eq Z).
#[global]
Instance Zops:@Ring_ops Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp (@eq Z).
Defined.
#[global]
Instance Zr: (@Ring _ _ _ _ _ _ _ _ Zops).
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.
Declare Scope ZMORPHISM.
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_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.
#[deprecated(since="9.0")]
Lemma gen_Zeqb_ok : forall x y,
Z.eqb x y = true -> [x] == [y].
End ZMORPHISM.
#[global]
Instance multiplication_phi_ring{R:Type}`{Ring R} : Multiplication :=
{multiplication x y := (gen_phiZ x) * y}.
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.
Declare Scope ZMORPHISM.
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_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.
#[deprecated(since="9.0")]
Lemma gen_Zeqb_ok : forall x y,
Z.eqb x y = true -> [x] == [y].
End ZMORPHISM.
#[global]
Instance multiplication_phi_ring{R:Type}`{Ring R} : Multiplication :=
{multiplication x y := (gen_phiZ x) * y}.