Library Stdlib.micromega.ZCoeff

From Stdlib Require Import OrderedRing.
From Stdlib Require Import RingMicromega.
From Stdlib Require Import BinInt.
From Stdlib Require Import InitialRing.
From Stdlib Require Import Setoid.
From Stdlib Require Import ZArithRing.

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 (@Equivalence_Reflexive _ _ (SORsetoid sor))
  symmetry proved by (@Equivalence_Symmetric _ _ (SORsetoid sor))
  transitivity proved by (@Equivalence_Transitive _ _ (SORsetoid sor))
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
             Z.eqb 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, Z.eqb x y = false -> [x] ~= [y].

End InitialMorphism.