Library Coq.setoid_ring.Ncring_initial

Require Import ZArith_base.
Require Import Zpow_def.
Require Import BinInt.
Require Import BinNat.
Require Import Setoid.
Require Import BinList.
Require Import BinPos.
Require Import BinNat.
Require Import BinInt.
Require Import Setoid.
Require Export Ncring.
Require Export Ncring_polynom.

Set Implicit Arguments.

Definition NotConstant := false.

Z is a ring and a setoid

Lemma Zsth : Equivalence (@eq Z).

Instance Zops:@Ring_ops Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp (@eq Z).
Defined.

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.
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}.

Library Coq.setoid_ring.Ncring_initial

Navigation