Library Stdlib.Numbers.Integer.NatPairs.ZNatPairs


Require Import NSub ZAxioms.
Require Export Ring.

Declare Scope pair_scope.
Local Open Scope pair_scope.

Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope.
Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope.

Module ZPairsAxiomsMod (Import N : NAxiomsMiniSig) <: ZAxiomsMiniSig.
 Module Import NProp.
   Include NSubProp N.
 End NProp.

Declare Scope NScope.
Delimit Scope NScope with N.
Bind Scope NScope with N.t.
Infix "==" := N.eq (at level 70) : NScope.
Notation "x ~= y" := (~ N.eq x y) (at level 70) : NScope.
Notation "0" := N.zero : NScope.
Notation "1" := N.one : NScope.
Notation "2" := N.two : NScope.
Infix "+" := N.add : NScope.
Infix "-" := N.sub : NScope.
Infix "*" := N.mul : NScope.
Infix "<" := N.lt : NScope.
Infix "<=" := N.le : NScope.
Local Open Scope NScope.

The definitions of functions (add, mul, etc.) will be unfolded by the properties functor. Since we don't want add_comm to refer to unfolded definitions of equality: fun p1 p2 => (fst p1 + snd p2) = (fst p2 + snd p1), we will provide an extra layer of definitions.

Module Z.

Definition t := (N.t * N.t)%type.
Definition zero : t := (0, 0).
Definition one : t := (1,0).
Definition two : t := (2,0).
Definition eq (p q : t) := (p#1 + q#2 == q#1 + p#2).
Definition succ (n : t) : t := (N.succ n#1, n#2).
Definition pred (n : t) : t := (n#1, N.succ n#2).
Definition opp (n : t) : t := (n#2, n#1).
Definition add (n m : t) : t := (n#1 + m#1, n#2 + m#2).
Definition sub (n m : t) : t := (n#1 + m#2, n#2 + m#1).
Definition mul (n m : t) : t :=
  (n#1 * m#1 + n#2 * m#2, n#1 * m#2 + n#2 * m#1).
Definition lt (n m : t) := n#1 + m#2 < m#1 + n#2.
Definition le (n m : t) := n#1 + m#2 <= m#1 + n#2.
Definition min (n m : t) : t := (min (n#1 + m#2) (m#1 + n#2), n#2 + m#2).
Definition max (n m : t) : t := (max (n#1 + m#2) (m#1 + n#2), n#2 + m#2).

NB : We do not have Z.pred (Z.succ n) = n but only Z.pred (Z.succ n) == n. It could be possible to consider as canonical only pairs where one of the elements is 0, and make all operations convert canonical values into other canonical values. In that case, we could get rid of setoids and arrive at integers as signed natural numbers.
NB : Unfortunately, the elements of the pair keep increasing during many operations, even during subtraction.

End Z.

Declare Scope ZScope.
Delimit Scope ZScope with Z.
Bind Scope ZScope with Z.t.
Infix "==" := Z.eq (at level 70) : ZScope.
Notation "x ~= y" := (~ Z.eq x y) (at level 70) : ZScope.
Notation "0" := Z.zero : ZScope.
Notation "1" := Z.one : ZScope.
Notation "2" := Z.two : ZScope.
Infix "+" := Z.add : ZScope.
Infix "-" := Z.sub : ZScope.
Infix "*" := Z.mul : ZScope.
Notation "- x" := (Z.opp x) : ZScope.
Infix "<" := Z.lt : ZScope.
Infix "<=" := Z.le : ZScope.
Local Open Scope ZScope.

Lemma sub_add_opp : forall n m, Z.sub n m = Z.add n (Z.opp m).

#[global]
Instance eq_equiv : Equivalence Z.eq.

#[global]
Instance pair_wd : Proper (N.eq==>N.eq==>Z.eq) (@pair N.t N.t).

#[global]
Instance succ_wd : Proper (Z.eq ==> Z.eq) Z.succ.

#[global]
Instance pred_wd : Proper (Z.eq ==> Z.eq) Z.pred.

#[global]
Instance add_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) Z.add.

#[global]
Instance opp_wd : Proper (Z.eq ==> Z.eq) Z.opp.

#[global]
Instance sub_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) Z.sub.

Lemma mul_comm : forall n m, n*m == m*n.

#[global]
Instance mul_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) Z.mul.

Section Induction.
Variable A : Z.t -> Prop.
Hypothesis A_wd : Proper (Z.eq==>iff) A.

Theorem bi_induction :
  A 0 -> (forall n, A n <-> A (Z.succ n)) -> forall n, A n.
Open Scope NScope.
    Close Scope NScope.

End Induction.


Theorem pred_succ : forall n, Z.pred (Z.succ n) == n.

Theorem succ_pred : forall n, Z.succ (Z.pred n) == n.

Theorem one_succ : 1 == Z.succ 0.

Theorem two_succ : 2 == Z.succ 1.

Theorem opp_0 : - 0 == 0.

Theorem opp_succ : forall n, - (Z.succ n) == Z.pred (- n).

Theorem add_0_l : forall n, 0 + n == n.

Theorem add_succ_l : forall n m, (Z.succ n) + m == Z.succ (n + m).

Theorem sub_0_r : forall n, n - 0 == n.

Theorem sub_succ_r : forall n m, n - (Z.succ m) == Z.pred (n - m).

Theorem mul_0_l : forall n, 0 * n == 0.

Theorem mul_succ_l : forall n m, (Z.succ n) * m == n * m + m.

Order

Lemma lt_eq_cases : forall n m, n<=m <-> n<m \/ n==m.

Theorem lt_irrefl : forall n, ~ (n < n).

Theorem lt_succ_r : forall n m, n < (Z.succ m) <-> n <= m.

Theorem min_l : forall n m, n <= m -> Z.min n m == n.

Theorem min_r : forall n m, m <= n -> Z.min n m == m.

Theorem max_l : forall n m, m <= n -> Z.max n m == n.

Theorem max_r : forall n m, n <= m -> Z.max n m == m.

Theorem lt_nge : forall n m, n < m <-> ~(m<=n).

#[global]
Instance lt_wd : Proper (Z.eq ==> Z.eq ==> iff) Z.lt.

Definition t := Z.t.
Definition eq := Z.eq.
Definition zero := Z.zero.
Definition one := Z.one.
Definition two := Z.two.
Definition succ := Z.succ.
Definition pred := Z.pred.
Definition add := Z.add.
Definition sub := Z.sub.
Definition mul := Z.mul.
Definition opp := Z.opp.
Definition lt := Z.lt.
Definition le := Z.le.
Definition min := Z.min.
Definition max := Z.max.

End ZPairsAxiomsMod.