Library Coq.Numbers.Integer.NatPairs.ZNatPairs
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.
NB : We do not have Zpred (Zsucc n) = n but only Zpred (Zsucc 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.
Delimit Scope ZScope with Z.
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.succ Z.zero) :
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).
Instance eq_equiv :
Equivalence Z.eq.
Instance pair_wd :
Proper (
N.eq==>N.eq==>Z.eq) (@
pair N.t N.t).
Instance succ_wd :
Proper (
Z.eq ==> Z.eq)
Z.succ.
Instance pred_wd :
Proper (
Z.eq ==> Z.eq)
Z.pred.
Instance add_wd :
Proper (
Z.eq ==> Z.eq ==> Z.eq)
Z.add.
Instance opp_wd :
Proper (
Z.eq ==> Z.eq)
Z.opp.
Instance sub_wd :
Proper (
Z.eq ==> Z.eq ==> Z.eq)
Z.sub.
Lemma mul_comm :
forall n m,
n*m == m*n.
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.
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 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