Library Coq.micromega.ZCoeff

Require Import OrderedRing.
Require Import RingMicromega.
Require Import ZArith.
Require Import InitialRing.
Require Import Setoid.

Import OrderedRingSyntax.

Set Implicit Arguments.

Section InitialMorphism.

Variable R : Type.
Variables rO rI : R.
Variables rplus rtimes rminus: R -> R -> R.
Variable ropp : R -> R.
Variables req rle rlt : R -> R -> Prop.

Variable sor : SOR rO rI rplus rtimes rminus ropp req rle rlt.

Notation "0" := rO.
Notation "1" := rI.
Notation "x + y" := (rplus x y).
Notation "x * y " := (rtimes x y).
Notation "x - y " := (rminus x y).
Notation "- x" := (ropp x).
Notation "x == y" := (req x y).
Notation "x ~= y" := (~ req x y).
Notation "x <= y" := (rle x y).
Notation "x < y" := (rlt x y).

Lemma req_refl : forall x, req x x.

Lemma req_sym : forall x y, req x y -> req y x.

Lemma req_trans : forall x y z, req x y -> req y z -> req x z.

Add Relation R req
  reflexivity proved by sor.(SORsetoid).(@Equivalence_Reflexive _ _)
  symmetry proved by sor.(SORsetoid).(@Equivalence_Symmetric _ _)
  transitivity proved by sor.(SORsetoid).(@Equivalence_Transitive _ _)
as sor_setoid.

Add Morphism rplus with signature req ==> req ==> req as rplus_morph.
Add Morphism rtimes with signature req ==> req ==> req as rtimes_morph.
Add Morphism ropp with signature req ==> req as ropp_morph.
Add Morphism rle with signature req ==> req ==> iff as rle_morph.
Add Morphism rlt with signature req ==> req ==> iff as rlt_morph.
Add Morphism rminus with signature req ==> req ==> req as rminus_morph.

Ltac le_less := rewrite (Rle_lt_eq sor); left; try assumption.
Ltac le_equal := rewrite (Rle_lt_eq sor); right; try reflexivity; try assumption.

Definition gen_order_phi_Z : Z -> R := gen_phiZ 0 1 rplus rtimes ropp.

Notation phi_pos := (gen_phiPOS 1 rplus rtimes).
Notation phi_pos1 := (gen_phiPOS1 1 rplus rtimes).

Notation "[ x ]" := (gen_order_phi_Z x).

Lemma ring_ops_wd : ring_eq_ext rplus rtimes ropp req.

Lemma Zring_morph :
  ring_morph 0 1 rplus rtimes rminus ropp req
             0%Z 1%Z Z.add Z.mul Z.sub Z.opp
             Zeq_bool gen_order_phi_Z.

Lemma phi_pos1_pos : forall x : positive, 0 < phi_pos1 x.

Lemma phi_pos1_succ : forall x : positive, phi_pos1 (Pos.succ x) == 1 + phi_pos1 x.

Lemma clt_pos_morph : forall x y : positive, (x < y)%positive -> phi_pos1 x < phi_pos1 y.

Lemma clt_morph : forall x y : Z, (x < y)%Z -> [x] < [y].

Lemma Zcleb_morph : forall x y : Z, Z.leb x y = true -> [x] <= [y].

Lemma Zcneqb_morph : forall x y : Z, Zeq_bool x y = false -> [x] ~= [y].

End InitialMorphism.