ZNatPairs.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)
(*                      Evgeny Makarov, INRIA, 2007                     *)
(************************************************************************)

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).forall n m : Z.t, n - m = n + - m
Proof.forall n m : Z.t, n - m = n + - m reflexivity. Qed.

Instance eq_equiv : Equivalence Z.eq.Equivalence Z.eq
Proof.Equivalence Z.eq
split.Reflexive Z.eq
Symmetric Z.eq
Transitive Z.eq
unfold Reflexive, Z.eq.forall x : Z.t, (x#1 + x#2 == x#1 + x#2)%N
Symmetric Z.eq
Transitive Z.eq reflexivity.Symmetric Z.eq
Transitive Z.eq
unfold Symmetric, Z.eq; now symmetry.Transitive Z.eq
unfold Transitive, Z.eq.forall x y z : Z.t,
(x#1 + y#2 == y#1 + x#2)%N ->
(y#1 + z#2 == z#1 + y#2)%N ->
(x#1 + z#2 == z#1 + x#2)%N intros (n1,n2) (m1,m2) (p1,p2) H1 H2; simpl in *.n1, n2, m1, m2, p1, p2:t
H1:(n1 + m2 == m1 + n2)%N
H2:(m1 + p2 == p1 + m2)%N
(n1 + p2 == p1 + n2)%N
apply (add_cancel_r _ _ (m1+m2)%N).n1, n2, m1, m2, p1, p2:t
H1:(n1 + m2 == m1 + n2)%N
H2:(m1 + p2 == p1 + m2)%N
(n1 + p2 + (m1 + m2) == p1 + n2 + (m1 + m2))%N
rewrite add_shuffle2, H1, add_shuffle1, H2.n1, n2, m1, m2, p1, p2:t
H1:(n1 + m2 == m1 + n2)%N
H2:(m1 + p2 == p1 + m2)%N
(p1 + m2 + (n2 + m1) == p1 + n2 + (m1 + m2))%N
now rewrite add_shuffle1, (add_comm m1).
Qed.

Instance pair_wd : Proper (N.eq==>N.eq==>Z.eq) (@pair N.t N.t).Proper (eq ==> eq ==> Z.eq) pair
Proof.Proper (eq ==> eq ==> Z.eq) pair
intros n1 n2 H1 m1 m2 H2; unfold Z.eq; simpl; now rewrite H1, H2.
Qed.

Instance succ_wd : Proper (Z.eq ==> Z.eq) Z.succ.Proper (Z.eq ==> Z.eq) Z.succ
Proof.Proper (Z.eq ==> Z.eq) Z.succ
unfold Z.succ, Z.eq; intros n m H; simpl.n, m:Z.t
H:(n#1 + m#2 == m#1 + n#2)%N
(succ n#1 + m#2 == succ m#1 + n#2)%N
do 2 rewrite add_succ_l; now rewrite H.
Qed.

Instance pred_wd : Proper (Z.eq ==> Z.eq) Z.pred.Proper (Z.eq ==> Z.eq) Z.pred
Proof.Proper (Z.eq ==> Z.eq) Z.pred
unfold Z.pred, Z.eq; intros n m H; simpl.n, m:Z.t
H:(n#1 + m#2 == m#1 + n#2)%N
(n#1 + succ m#2 == m#1 + succ n#2)%N
do 2 rewrite add_succ_r; now rewrite H.
Qed.

Instance add_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) Z.add.Proper (Z.eq ==> Z.eq ==> Z.eq) Z.add
Proof.Proper (Z.eq ==> Z.eq ==> Z.eq) Z.add
unfold Z.eq, Z.add; intros n1 m1 H1 n2 m2 H2; simpl.n1, m1:Z.t
H1:(n1#1 + m1#2 == m1#1 + n1#2)%N
n2, m2:Z.t
H2:(n2#1 + m2#2 == m2#1 + n2#2)%N
(n1#1 + n2#1 + (m1#2 + m2#2) ==
 m1#1 + m2#1 + (n1#2 + n2#2))%N
now rewrite add_shuffle1, H1, H2, add_shuffle1.
Qed.

Instance opp_wd : Proper (Z.eq ==> Z.eq) Z.opp.Proper (Z.eq ==> Z.eq) Z.opp
Proof.Proper (Z.eq ==> Z.eq) Z.opp
unfold Z.eq, Z.opp; intros (n1,n2) (m1,m2) H; simpl in *.n1, n2, m1, m2:t
H:(n1 + m2 == m1 + n2)%N
(n2 + m1 == m2 + n1)%N
now rewrite (add_comm n2), (add_comm m2).
Qed.

Instance sub_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) Z.sub.Proper (Z.eq ==> Z.eq ==> Z.eq) Z.sub
Proof.Proper (Z.eq ==> Z.eq ==> Z.eq) Z.sub
intros n1 m1 H1 n2 m2 H2.n1, m1:Z.t
H1:n1 == m1
n2, m2:Z.t
H2:n2 == m2
n1 - n2 == m1 - m2 rewrite 2 sub_add_opp.n1, m1:Z.t
H1:n1 == m1
n2, m2:Z.t
H2:n2 == m2
n1 + - n2 == m1 + - m2 now do 2 f_equiv.
Qed.

Lemma mul_comm : forall n m, n*m == m*n.forall n m : Z.t, n * m == m * n
Proof.forall n m : Z.t, n * m == m * n
intros (n1,n2) (m1,m2); compute.n1, n2, m1, m2:t
(n1 * m1 + n2 * m2 + (m1 * n2 + m2 * n1) ==
 m1 * n1 + m2 * n2 + (n1 * m2 + n2 * m1))%N
rewrite (add_comm (m1*n2)%N).n1, n2, m1, m2:t
(n1 * m1 + n2 * m2 + (m2 * n1 + m1 * n2) ==
 m1 * n1 + m2 * n2 + (n1 * m2 + n2 * m1))%N
do 2 f_equiv; apply mul_comm.
Qed.

Instance mul_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) Z.mul.Proper (Z.eq ==> Z.eq ==> Z.eq) Z.mul
Proof.Proper (Z.eq ==> Z.eq ==> Z.eq) Z.mul
assert (forall n, Proper (Z.eq ==> Z.eq) (Z.mul n)).forall n : Z.t, Proper (Z.eq ==> Z.eq) (Z.mul n)
H:forall n : Z.t, Proper (Z.eq ==> Z.eq) (Z.mul n)
Proper (Z.eq ==> Z.eq ==> Z.eq) Z.mul
 unfold Z.mul, Z.eq.forall n : Z.t,
Proper
  ((fun p q : Z.t => (p#1 + q#2 == q#1 + p#2)%N) ==>
   (fun p q : Z.t => (p#1 + q#2 == q#1 + p#2)%N))
  (fun m : Z.t =>
   ((n#1 * m#1 + n#2 * m#2)%N,
   (n#1 * m#2 + n#2 * m#1)%N))
H:forall n : Z.t, Proper (Z.eq ==> Z.eq) (Z.mul n)
Proper (Z.eq ==> Z.eq ==> Z.eq) Z.mul intros (n1,n2) (p1,p2) (q1,q2) H; simpl in *.n1, n2, p1, p2, q1, q2:t
H:(p1 + q2 == q1 + p2)%N
(n1 * p1 + n2 * p2 + (n1 * q2 + n2 * q1) ==
 n1 * q1 + n2 * q2 + (n1 * p2 + n2 * p1))%N
H:forall n : Z.t, Proper (Z.eq ==> Z.eq) (Z.mul n)
Proper (Z.eq ==> Z.eq ==> Z.eq) Z.mul
 rewrite add_shuffle1, (add_comm (n1*p1)%N).n1, n2, p1, p2, q1, q2:t
H:(p1 + q2 == q1 + p2)%N
(n1 * q2 + n1 * p1 + (n2 * p2 + n2 * q1) ==
 n1 * q1 + n2 * q2 + (n1 * p2 + n2 * p1))%N
H:forall n : Z.t, Proper (Z.eq ==> Z.eq) (Z.mul n)
Proper (Z.eq ==> Z.eq ==> Z.eq) Z.mul
 symmetry.n1, n2, p1, p2, q1, q2:t
H:(p1 + q2 == q1 + p2)%N
(n1 * q1 + n2 * q2 + (n1 * p2 + n2 * p1) ==
 n1 * q2 + n1 * p1 + (n2 * p2 + n2 * q1))%N
H:forall n : Z.t, Proper (Z.eq ==> Z.eq) (Z.mul n)
Proper (Z.eq ==> Z.eq ==> Z.eq) Z.mul rewrite add_shuffle1.n1, n2, p1, p2, q1, q2:t
H:(p1 + q2 == q1 + p2)%N
(n1 * q1 + n1 * p2 + (n2 * q2 + n2 * p1) ==
 n1 * q2 + n1 * p1 + (n2 * p2 + n2 * q1))%N
H:forall n : Z.t, Proper (Z.eq ==> Z.eq) (Z.mul n)
Proper (Z.eq ==> Z.eq ==> Z.eq) Z.mul
 rewrite <- ! mul_add_distr_l.n1, n2, p1, p2, q1, q2:t
H:(p1 + q2 == q1 + p2)%N
(n1 * (q1 + p2) + n2 * (q2 + p1) ==
 n1 * (q2 + p1) + n2 * (p2 + q1))%N
H:forall n : Z.t, Proper (Z.eq ==> Z.eq) (Z.mul n)
Proper (Z.eq ==> Z.eq ==> Z.eq) Z.mul
 rewrite (add_comm p2), (add_comm q2), H.n1, n2, p1, p2, q1, q2:t
H:(p1 + q2 == q1 + p2)%N
(n1 * (q1 + p2) + n2 * (q1 + p2) ==
 n1 * (q1 + p2) + n2 * (q1 + p2))%N
H:forall n : Z.t, Proper (Z.eq ==> Z.eq) (Z.mul n)
Proper (Z.eq ==> Z.eq ==> Z.eq) Z.mul
 reflexivity.H:forall n : Z.t, Proper (Z.eq ==> Z.eq) (Z.mul n)
Proper (Z.eq ==> Z.eq ==> Z.eq) Z.mul
intros n n' Hn m m' Hm.H:forall n0 : Z.t, Proper (Z.eq ==> Z.eq) (Z.mul n0)
n, n':Z.t
Hn:n == n'
m, m':Z.t
Hm:m == m'
n * m == n' * m'
rewrite Hm, (mul_comm n), (mul_comm n'), Hn.H:forall n0 : Z.t, Proper (Z.eq ==> Z.eq) (Z.mul n0)
n, n':Z.t
Hn:n == n'
m, m':Z.t
Hm:m == m'
m' * n' == m' * n'
reflexivity.
Qed.

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.A:Z.t -> Prop
A_wd:Proper (Z.eq ==> iff) A
A 0 ->
(forall n : Z.t, A n <-> A (Z.succ n)) ->
forall n : Z.t, A n
Proof.A:Z.t -> Prop
A_wd:Proper (Z.eq ==> iff) A
A 0 ->
(forall n : Z.t, A n <-> A (Z.succ n)) ->
forall n : Z.t, A n
Open Scope NScope.A:Z.t -> Prop
A_wd:Proper (Z.eq ==> iff) A
A 0 ->
(forall n : Z.t, A n <-> A (Z.succ n)) ->
forall n : Z.t, A n
intros A0 AS n; unfold Z.zero, Z.succ, Z.eq in *.A:Z.t -> Prop
A_wd:Proper
  ((fun p q : Z.t => p#1 + q#2 == q#1 + p#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n:Z.t
A n
destruct n as [n m].A:Z.t -> Prop
A_wd:Proper
  ((fun p q : Z.t => p#1 + q#2 == q#1 + p#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m:t
A (n, m)
cut (forall p, A (p, 0)); [intro H1 |].A:Z.t -> Prop
A_wd:Proper
  ((fun p q : Z.t => p#1 + q#2 == q#1 + p#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m:t
H1:forall p : t, A (p, 0)
A (n, m)
A:Z.t -> Prop
A_wd:Proper
  ((fun p q : Z.t => p#1 + q#2 == q#1 + p#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m:t
forall p : t, A (p, 0)
cut (forall p, A (0, p)); [intro H2 |].A:Z.t -> Prop
A_wd:Proper
  ((fun p q : Z.t => p#1 + q#2 == q#1 + p#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m:t
H1:forall p : t, A (p, 0)
H2:forall p : t, A (0, p)
A (n, m)
A:Z.t -> Prop
A_wd:Proper
  ((fun p q : Z.t => p#1 + q#2 == q#1 + p#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m:t
H1:forall p : t, A (p, 0)
forall p : t, A (0, p)
A:Z.t -> Prop
A_wd:Proper
  ((fun p q : Z.t => p#1 + q#2 == q#1 + p#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m:t
forall p : t, A (p, 0)
destruct (add_dichotomy n m) as [[p H] | [p H]].A:Z.t -> Prop
A_wd:Proper
  ((fun p0 q : Z.t => p0#1 + q#2 == q#1 + p0#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m:t
H1:forall p0 : t, A (p0, 0)
H2:forall p0 : t, A (0, p0)
p:t
H:p + n == m
A (n, m)
A:Z.t -> Prop
A_wd:Proper
  ((fun p0 q : Z.t => p0#1 + q#2 == q#1 + p0#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m:t
H1:forall p0 : t, A (p0, 0)
H2:forall p0 : t, A (0, p0)
p:t
H:p + m == n
A (n, m)
A:Z.t -> Prop
A_wd:Proper
  ((fun p q : Z.t => p#1 + q#2 == q#1 + p#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m:t
H1:forall p : t, A (p, 0)
forall p : t, A (0, p)
A:Z.t -> Prop
A_wd:Proper
  ((fun p q : Z.t => p#1 + q#2 == q#1 + p#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m:t
forall p : t, A (p, 0)
rewrite (A_wd (n, m) (0, p)) by (rewrite add_0_l; now rewrite add_comm).A:Z.t -> Prop
A_wd:Proper
  ((fun p0 q : Z.t => p0#1 + q#2 == q#1 + p0#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m:t
H1:forall p0 : t, A (p0, 0)
H2:forall p0 : t, A (0, p0)
p:t
H:p + n == m
A (0, p)
A:Z.t -> Prop
A_wd:Proper
  ((fun p0 q : Z.t => p0#1 + q#2 == q#1 + p0#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m:t
H1:forall p0 : t, A (p0, 0)
H2:forall p0 : t, A (0, p0)
p:t
H:p + m == n
A (n, m)
A:Z.t -> Prop
A_wd:Proper
  ((fun p q : Z.t => p#1 + q#2 == q#1 + p#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m:t
H1:forall p : t, A (p, 0)
forall p : t, A (0, p)
A:Z.t -> Prop
A_wd:Proper
  ((fun p q : Z.t => p#1 + q#2 == q#1 + p#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m:t
forall p : t, A (p, 0)
apply H2.A:Z.t -> Prop
A_wd:Proper
  ((fun p0 q : Z.t => p0#1 + q#2 == q#1 + p0#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m:t
H1:forall p0 : t, A (p0, 0)
H2:forall p0 : t, A (0, p0)
p:t
H:p + m == n
A (n, m)
A:Z.t -> Prop
A_wd:Proper
  ((fun p q : Z.t => p#1 + q#2 == q#1 + p#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m:t
H1:forall p : t, A (p, 0)
forall p : t, A (0, p)
A:Z.t -> Prop
A_wd:Proper
  ((fun p q : Z.t => p#1 + q#2 == q#1 + p#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m:t
forall p : t, A (p, 0)
rewrite (A_wd (n, m) (p, 0)) by now rewrite add_0_r.A:Z.t -> Prop
A_wd:Proper
  ((fun p0 q : Z.t => p0#1 + q#2 == q#1 + p0#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m:t
H1:forall p0 : t, A (p0, 0)
H2:forall p0 : t, A (0, p0)
p:t
H:p + m == n
A (p, 0)
A:Z.t -> Prop
A_wd:Proper
  ((fun p q : Z.t => p#1 + q#2 == q#1 + p#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m:t
H1:forall p : t, A (p, 0)
forall p : t, A (0, p)
A:Z.t -> Prop
A_wd:Proper
  ((fun p q : Z.t => p#1 + q#2 == q#1 + p#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m:t
forall p : t, A (p, 0) apply H1.A:Z.t -> Prop
A_wd:Proper
  ((fun p q : Z.t => p#1 + q#2 == q#1 + p#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m:t
H1:forall p : t, A (p, 0)
forall p : t, A (0, p)
A:Z.t -> Prop
A_wd:Proper
  ((fun p q : Z.t => p#1 + q#2 == q#1 + p#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m:t
forall p : t, A (p, 0)
induct p.A:Z.t -> Prop
A_wd:Proper
  ((fun p q : Z.t => p#1 + q#2 == q#1 + p#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m:t
H1:forall p : t, A (p, 0)
A (0, 0)
A:Z.t -> Prop
A_wd:Proper
  ((fun p q : Z.t => p#1 + q#2 == q#1 + p#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m:t
H1:forall p : t, A (p, 0)
forall n0 : t, A (0, n0) -> A (0, succ n0)
A:Z.t -> Prop
A_wd:Proper
  ((fun p q : Z.t => p#1 + q#2 == q#1 + p#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m:t
forall p : t, A (p, 0) assumption.A:Z.t -> Prop
A_wd:Proper
  ((fun p q : Z.t => p#1 + q#2 == q#1 + p#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m:t
H1:forall p : t, A (p, 0)
forall n0 : t, A (0, n0) -> A (0, succ n0)
A:Z.t -> Prop
A_wd:Proper
  ((fun p q : Z.t => p#1 + q#2 == q#1 + p#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m:t
forall p : t, A (p, 0) intros p IH.A:Z.t -> Prop
A_wd:Proper
  ((fun p0 q : Z.t => p0#1 + q#2 == q#1 + p0#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m:t
H1:forall p0 : t, A (p0, 0)
p:t
IH:A (0, p)
A (0, succ p)
A:Z.t -> Prop
A_wd:Proper
  ((fun p q : Z.t => p#1 + q#2 == q#1 + p#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m:t
forall p : t, A (p, 0)
apply (A_wd (0, p) (1, N.succ p)) in IH; [| now rewrite add_0_l, add_1_l].A:Z.t -> Prop
A_wd:Proper
  ((fun p0 q : Z.t => p0#1 + q#2 == q#1 + p0#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m:t
H1:forall p0 : t, A (p0, 0)
p:t
IH:A (1, succ p)
A (0, succ p)
A:Z.t -> Prop
A_wd:Proper
  ((fun p q : Z.t => p#1 + q#2 == q#1 + p#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m:t
forall p : t, A (p, 0)
rewrite one_succ in IH.A:Z.t -> Prop
A_wd:Proper
  ((fun p0 q : Z.t => p0#1 + q#2 == q#1 + p0#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m:t
H1:forall p0 : t, A (p0, 0)
p:t
IH:A (succ 0, succ p)
A (0, succ p)
A:Z.t -> Prop
A_wd:Proper
  ((fun p q : Z.t => p#1 + q#2 == q#1 + p#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m:t
forall p : t, A (p, 0) now apply AS.A:Z.t -> Prop
A_wd:Proper
  ((fun p q : Z.t => p#1 + q#2 == q#1 + p#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m:t
forall p : t, A (p, 0)
induct p.A:Z.t -> Prop
A_wd:Proper
  ((fun p q : Z.t => p#1 + q#2 == q#1 + p#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m:t
A (0, 0)
A:Z.t -> Prop
A_wd:Proper
  ((fun p q : Z.t => p#1 + q#2 == q#1 + p#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m:t
forall n0 : t, A (n0, 0) -> A (succ n0, 0) assumption.A:Z.t -> Prop
A_wd:Proper
  ((fun p q : Z.t => p#1 + q#2 == q#1 + p#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m:t
forall n0 : t, A (n0, 0) -> A (succ n0, 0) intros p IH.A:Z.t -> Prop
A_wd:Proper
  ((fun p0 q : Z.t => p0#1 + q#2 == q#1 + p0#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m, p:t
IH:A (p, 0)
A (succ p, 0)
replace 0 with (snd (p, 0)); [| reflexivity].A:Z.t -> Prop
A_wd:Proper
  ((fun p0 q : Z.t => p0#1 + q#2 == q#1 + p0#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m, p:t
IH:A (p, 0)
A (succ p, (p, 0)#2)
replace (N.succ p) with (N.succ (fst (p, 0))); [| reflexivity].A:Z.t -> Prop
A_wd:Proper
  ((fun p0 q : Z.t => p0#1 + q#2 == q#1 + p0#2) ==>
   iff) A
A0:A (0, 0)
AS:forall n0 : Z.t, A n0 <-> A (succ n0#1, n0#2)
n, m, p:t
IH:A (p, 0)
A (succ (p, 0)#1, (p, 0)#2) now apply -> AS.
Close Scope NScope.
Qed.

End Induction.

(* Time to prove theorems in the language of Z *)

Theorem pred_succ : forall n, Z.pred (Z.succ n) == n.forall n : Z.t, Z.pred (Z.succ n) == n
Proof.forall n : Z.t, Z.pred (Z.succ n) == n
unfold Z.pred, Z.succ, Z.eq; intro n; simpl; now nzsimpl.
Qed.

Theorem succ_pred : forall n, Z.succ (Z.pred n) == n.forall n : Z.t, Z.succ (Z.pred n) == n
Proof.forall n : Z.t, Z.succ (Z.pred n) == n
intro n; unfold Z.succ, Z.pred, Z.eq; simpl; now nzsimpl.
Qed.

Theorem one_succ : 1 == Z.succ 0.1 == Z.succ 0
Proof.1 == Z.succ 0
unfold Z.eq; simpl.(1 + 0 == succ 0 + 0)%N now nzsimpl'.
Qed.

Theorem two_succ : 2 == Z.succ 1.2 == Z.succ 1
Proof.2 == Z.succ 1
unfold Z.eq; simpl.(2 + 0 == succ 1 + 0)%N now nzsimpl'.
Qed.

Theorem opp_0 : - 0 == 0.- 0 == 0
Proof.- 0 == 0
unfold Z.opp, Z.eq; simpl.(0 + 0 == 0 + 0)%N now nzsimpl.
Qed.

Theorem opp_succ : forall n, - (Z.succ n) == Z.pred (- n).forall n : Z.t, - Z.succ n == Z.pred (- n)
Proof.forall n : Z.t, - Z.succ n == Z.pred (- n)
reflexivity.
Qed.

Theorem add_0_l : forall n, 0 + n == n.forall n : Z.t, 0 + n == n
Proof.forall n : Z.t, 0 + n == n
intro n; unfold Z.add, Z.eq; simpl.n:Z.t
(0 + n#1 + n#2 == n#1 + (0 + n#2))%N now nzsimpl.
Qed.

Theorem add_succ_l : forall n m, (Z.succ n) + m == Z.succ (n + m).forall n m : Z.t, Z.succ n + m == Z.succ (n + m)
Proof.forall n m : Z.t, Z.succ n + m == Z.succ (n + m)
intros n m; unfold Z.add, Z.eq; simpl.n, m:Z.t
(succ n#1 + m#1 + (n#2 + m#2) ==
 succ (n#1 + m#1) + (n#2 + m#2))%N now nzsimpl.
Qed.

Theorem sub_0_r : forall n, n - 0 == n.forall n : Z.t, n - 0 == n
Proof.forall n : Z.t, n - 0 == n
intro n; unfold Z.sub, Z.eq; simpl.n:Z.t
(n#1 + 0 + n#2 == n#1 + (n#2 + 0))%N now nzsimpl.
Qed.

Theorem sub_succ_r : forall n m, n - (Z.succ m) == Z.pred (n - m).forall n m : Z.t, n - Z.succ m == Z.pred (n - m)
Proof.forall n m : Z.t, n - Z.succ m == Z.pred (n - m)
intros n m; unfold Z.sub, Z.eq; simpl.n, m:Z.t
(n#1 + m#2 + succ (n#2 + m#1) ==
 n#1 + m#2 + (n#2 + succ m#1))%N symmetry; now rewrite add_succ_r.
Qed.

Theorem mul_0_l : forall n, 0 * n == 0.forall n : Z.t, 0 * n == 0
Proof.forall n : Z.t, 0 * n == 0
intros (n1,n2); unfold Z.mul, Z.eq; simpl; now nzsimpl.
Qed.

Theorem mul_succ_l : forall n m, (Z.succ n) * m == n * m + m.forall n m : Z.t, Z.succ n * m == n * m + m
Proof.forall n m : Z.t, Z.succ n * m == n * m + m
intros (n1,n2) (m1,m2); unfold Z.mul, Z.succ, Z.eq; simpl; nzsimpl.n1, n2, m1, m2:t
(n1 * m1 + m1 + n2 * m2 + (n1 * m2 + n2 * m1 + m2) ==
 n1 * m1 + n2 * m2 + m1 + (n1 * m2 + m2 + n2 * m1))%N
rewrite <- (add_assoc _ m1), (add_comm m1), (add_assoc _ _ m1).n1, n2, m1, m2:t
(n1 * m1 + n2 * m2 + m1 + (n1 * m2 + n2 * m1 + m2) ==
 n1 * m1 + n2 * m2 + m1 + (n1 * m2 + m2 + n2 * m1))%N
now rewrite <- (add_assoc _ m2), (add_comm m2), (add_assoc _ (n2*m1)%N m2).
Qed.

Order

Lemma lt_eq_cases : forall n m, n<=m <-> n<m \/ n==m.forall n m : Z.t, n <= m <-> n < m \/ n == m
Proof.forall n m : Z.t, n <= m <-> n < m \/ n == m
intros; apply N.lt_eq_cases.
Qed.

Theorem lt_irrefl : forall n, ~ (n < n).forall n : Z.t, ~ n < n
Proof.forall n : Z.t, ~ n < n
intros; apply N.lt_irrefl.
Qed.

Theorem lt_succ_r : forall n m, n < (Z.succ m) <-> n <= m.forall n m : Z.t, n < Z.succ m <-> n <= m
Proof.forall n m : Z.t, n < Z.succ m <-> n <= m
intros n m; unfold Z.lt, Z.le, Z.eq; simpl; nzsimpl.n, m:Z.t
(n#1 + m#2 < succ (m#1 + n#2))%N <->
(n#1 + m#2 <= m#1 + n#2)%N apply lt_succ_r.
Qed.

Theorem min_l : forall n m, n <= m -> Z.min n m == n.forall n m : Z.t, n <= m -> Z.min n m == n
Proof.forall n m : Z.t, n <= m -> Z.min n m == n
unfold Z.min, Z.le, Z.eq; simpl; intros (n1,n2) (m1,m2) H; simpl in *.n1, n2, m1, m2:t
H:(n1 + m2 <= m1 + n2)%N
(min (n1 + m2) (m1 + n2) + n2 == n1 + (n2 + m2))%N
rewrite min_l by assumption.n1, n2, m1, m2:t
H:(n1 + m2 <= m1 + n2)%N
(n1 + m2 + n2 == n1 + (n2 + m2))%N
now rewrite <- add_assoc, (add_comm m2).
Qed.

Theorem min_r : forall n m, m <= n -> Z.min n m == m.forall n m : Z.t, m <= n -> Z.min n m == m
Proof.forall n m : Z.t, m <= n -> Z.min n m == m
unfold Z.min, Z.le, Z.eq; simpl; intros (n1,n2) (m1,m2) H; simpl in *.n1, n2, m1, m2:t
H:(m1 + n2 <= n1 + m2)%N
(min (n1 + m2) (m1 + n2) + m2 == m1 + (n2 + m2))%N
rewrite min_r by assumption.n1, n2, m1, m2:t
H:(m1 + n2 <= n1 + m2)%N
(m1 + n2 + m2 == m1 + (n2 + m2))%N
now rewrite add_assoc.
Qed.

Theorem max_l : forall n m, m <= n -> Z.max n m == n.forall n m : Z.t, m <= n -> Z.max n m == n
Proof.forall n m : Z.t, m <= n -> Z.max n m == n
unfold Z.max, Z.le, Z.eq; simpl; intros (n1,n2) (m1,m2) H; simpl in *.n1, n2, m1, m2:t
H:(m1 + n2 <= n1 + m2)%N
(max (n1 + m2) (m1 + n2) + n2 == n1 + (n2 + m2))%N
rewrite max_l by assumption.n1, n2, m1, m2:t
H:(m1 + n2 <= n1 + m2)%N
(n1 + m2 + n2 == n1 + (n2 + m2))%N
now rewrite <- add_assoc, (add_comm m2).
Qed.

Theorem max_r : forall n m, n <= m -> Z.max n m == m.forall n m : Z.t, n <= m -> Z.max n m == m
Proof.forall n m : Z.t, n <= m -> Z.max n m == m
unfold Z.max, Z.le, Z.eq; simpl; intros n m H.n, m:Z.t
H:(n#1 + m#2 <= m#1 + n#2)%N
(max (n#1 + m#2) (m#1 + n#2) + m#2 ==
 m#1 + (n#2 + m#2))%N
rewrite max_r by assumption.n, m:Z.t
H:(n#1 + m#2 <= m#1 + n#2)%N
(m#1 + n#2 + m#2 == m#1 + (n#2 + m#2))%N
now rewrite add_assoc.
Qed.

Theorem lt_nge : forall n m, n < m <-> ~(m<=n).forall n m : Z.t, n < m <-> ~ m <= n
Proof.forall n m : Z.t, n < m <-> ~ m <= n
intros.n, m:Z.t
n < m <-> ~ m <= n apply lt_nge.
Qed.

Instance lt_wd : Proper (Z.eq ==> Z.eq ==> iff) Z.lt.Proper (Z.eq ==> Z.eq ==> iff) Z.lt
Proof.Proper (Z.eq ==> Z.eq ==> iff) Z.lt
assert (forall n, Proper (Z.eq==>iff) (Z.lt n)).forall n : Z.t, Proper (Z.eq ==> iff) (Z.lt n)
H:forall n : Z.t, Proper (Z.eq ==> iff) (Z.lt n)
Proper (Z.eq ==> Z.eq ==> iff) Z.lt
 intros (n1,n2).n1, n2:t
Proper (Z.eq ==> iff) (Z.lt (n1, n2))
H:forall n : Z.t, Proper (Z.eq ==> iff) (Z.lt n)
Proper (Z.eq ==> Z.eq ==> iff) Z.lt apply proper_sym_impl_iff; auto with *.n1, n2:t
Proper (Z.eq ==> Basics.impl) (Z.lt (n1, n2))
H:forall n : Z.t, Proper (Z.eq ==> iff) (Z.lt n)
Proper (Z.eq ==> Z.eq ==> iff) Z.lt
 unfold Z.lt, Z.eq; intros (r1,r2) (s1,s2) Eq H; simpl in *.n1, n2, r1, r2, s1, s2:t
Eq:(r1 + s2 == s1 + r2)%N
H:(n1 + r2 < r1 + n2)%N
(n1 + s2 < s1 + n2)%N
H:forall n : Z.t, Proper (Z.eq ==> iff) (Z.lt n)
Proper (Z.eq ==> Z.eq ==> iff) Z.lt
 apply le_lt_add_lt with (r1+r2)%N (r1+r2)%N; [apply le_refl; auto with *|].n1, n2, r1, r2, s1, s2:t
Eq:(r1 + s2 == s1 + r2)%N
H:(n1 + r2 < r1 + n2)%N
(n1 + s2 + (r1 + r2) < s1 + n2 + (r1 + r2))%N
H:forall n : Z.t, Proper (Z.eq ==> iff) (Z.lt n)
Proper (Z.eq ==> Z.eq ==> iff) Z.lt
 rewrite add_shuffle2, (add_comm s2), Eq.n1, n2, r1, r2, s1, s2:t
Eq:(r1 + s2 == s1 + r2)%N
H:(n1 + r2 < r1 + n2)%N
(n1 + r2 + (s1 + r2) < s1 + n2 + (r1 + r2))%N
H:forall n : Z.t, Proper (Z.eq ==> iff) (Z.lt n)
Proper (Z.eq ==> Z.eq ==> iff) Z.lt
 rewrite (add_comm s1 n2), (add_shuffle1 n2), (add_comm n2 r1).n1, n2, r1, r2, s1, s2:t
Eq:(r1 + s2 == s1 + r2)%N
H:(n1 + r2 < r1 + n2)%N
(n1 + r2 + (s1 + r2) < r1 + n2 + (s1 + r2))%N
H:forall n : Z.t, Proper (Z.eq ==> iff) (Z.lt n)
Proper (Z.eq ==> Z.eq ==> iff) Z.lt
 now rewrite <- add_lt_mono_r.H:forall n : Z.t, Proper (Z.eq ==> iff) (Z.lt n)
Proper (Z.eq ==> Z.eq ==> iff) Z.lt
intros n n' Hn m m' Hm.H:forall n0 : Z.t, Proper (Z.eq ==> iff) (Z.lt n0)
n, n':Z.t
Hn:n == n'
m, m':Z.t
Hm:m == m'
n < m <-> n' < m'
rewrite Hm.H:forall n0 : Z.t, Proper (Z.eq ==> iff) (Z.lt n0)
n, n':Z.t
Hn:n == n'
m, m':Z.t
Hm:m == m'
n < m' <-> n' < m' rewrite 2 lt_nge, 2 lt_eq_cases, Hn; auto with *.
Qed.

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.

(* For example, let's build integers out of pairs of Peano natural numbers
and get their properties *)

(* The following lines increase the compilation time at least twice *)
(*
Require PeanoNat.

Module Export ZPairsPeanoAxiomsMod := ZPairsAxiomsMod PeanoNat.Nat.
Module Export ZPairsPropMod := ZPropFunct ZPairsPeanoAxiomsMod.

Eval compute in (3, 5) * (4, 6).
*)