1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
|
Require Import NPlus.
Require Export ZAxioms.
Module NatPairsDomain (Import NPlusModule : NPlusSignature) <: ZDomainSignature.
(* with Definition Z :=
(NPM.NatModule.DomainModule.N * NPM.NatModule.DomainModule.N)%type
with Definition E :=
fun p1 p2 =>
NPM.NatModule.DomainModule.E (NPM.plus (fst p1) (snd p2)) (NPM.plus (fst p2) (snd p1))
with Definition e :=
fun p1 p2 =>
NPM.NatModule.DomainModule.e (NPM.plus (fst p1) (snd p2)) (NPM.plus (fst p2) (snd p1)).*)
Module Export NPlusPropertiesModule := NPlusProperties NatModule NPlusModule.
Open Local Scope NatScope.
Definition Z : Set := (N * N)%type.
Definition E (p1 p2 : Z) := ((fst p1) + (snd p2) == (fst p2) + (snd p1)).
Definition e (p1 p2 : Z) := e ((fst p1) + (snd p2)) ((fst p2) + (snd p1)).
Delimit Scope IntScope with Int.
Bind Scope IntScope with Z.
Notation "x == y" := (E x y) (at level 70) : IntScope.
Notation "x # y" := (~ E x y) (at level 70) : IntScope.
Theorem E_equiv_e : forall x y : Z, E x y <-> e x y.
Proof.
intros x y; unfold E, e; apply E_equiv_e.
Qed.
Theorem ZE_refl : reflexive Z E.
Proof.
unfold reflexive, E; reflexivity.
Qed.
Theorem ZE_symm : symmetric Z E.
Proof.
unfold symmetric, E; now symmetry.
Qed.
Theorem ZE_trans : transitive Z E.
Proof.
unfold transitive, E. intros x y z H1 H2.
apply plus_cancel_l with (p := fst y + snd y).
rewrite (plus_shuffle2 (fst y) (snd y) (fst x) (snd z)).
rewrite (plus_shuffle2 (fst y) (snd y) (fst z) (snd x)).
rewrite plus_comm. rewrite (plus_comm (snd y) (fst x)).
rewrite (plus_comm (snd y) (fst z)). now apply plus_wd.
Qed.
Theorem E_equiv : equiv Z E.
Proof.
unfold equiv; split; [apply ZE_refl | split; [apply ZE_trans | apply ZE_symm]].
Qed.
Add Relation Z E
reflexivity proved by (proj1 E_equiv)
symmetry proved by (proj2 (proj2 E_equiv))
transitivity proved by (proj1 (proj2 E_equiv))
as E_rel.
Add Morphism (@pair N N)
with signature NDomainModule.E ==> NDomainModule.E ==> E
as pair_wd.
Proof.
intros x1 x2 H1 y1 y2 H2; unfold E; simpl; rewrite H1; now rewrite H2.
Qed.
End NatPairsDomain.
Module NatPairsInt (Import NPlusModule : NPlusSignature) <: IntSignature.
Module Export ZDomainModule := NatPairsDomain NPlusModule.
Module Export ZDomainModuleProperties := ZDomainProperties ZDomainModule.
Open Local Scope IntScope.
Definition O : Z := (0, 0)%Nat.
Definition S (n : Z) := (NatModule.S (fst n), snd n).
Definition P (n : Z) := (fst n, NatModule.S (snd n)).
(* Unfortunately, we do not have P (S n) = n but only P (S 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. We do not do this because this is more complex
and because we do not have the predecessor function on N at this point. *)
Notation "0" := O : IntScope.
Add Morphism S with signature E ==> E as S_wd.
Proof.
unfold S, E; intros n m H; simpl.
do 2 rewrite plus_S_l; now rewrite H.
Qed.
Add Morphism P with signature E ==> E as P_wd.
Proof.
unfold P, E; intros n m H; simpl.
do 2 rewrite plus_S_r; now rewrite H.
Qed.
Theorem S_inj : forall x y : Z, S x == S y -> x == y.
Proof.
unfold S, E; simpl; intros x y H.
do 2 rewrite plus_S_l in H. now apply S_inj in H.
Qed.
Theorem S_P : forall x : Z, S (P x) == x.
Proof.
intro x; unfold S, P, E; simpl.
rewrite plus_S_l; now rewrite plus_S_r.
Qed.
Section Induction.
Open Scope NatScope. (* automatically closes at the end of the section *)
Variable Q : Z -> Prop.
Hypothesis Q_wd : pred_wd E Q.
Add Morphism Q with signature E ==> iff as Q_morph.
Proof.
exact Q_wd.
Qed.
Theorem induction :
Q 0 -> (forall x, Q x -> Q (S x)) -> (forall x, Q x -> Q (P x)) -> forall x, Q x.
Proof.
intros Q0 QS QP x; unfold O, S, P, pred_wd, E in *.
destruct x as [n m].
cut (forall p : N, Q (p, 0)); [intro H1 |].
cut (forall p : N, Q (0, p)); [intro H2 |].
destruct (plus_dichotomy n m) as [[p H] | [p H]].
rewrite (Q_wd (n, m) (0, p)); simpl. rewrite plus_0_l; now rewrite plus_comm. apply H2.
rewrite (Q_wd (n, m) (p, 0)); simpl. now rewrite plus_0_r. apply H1.
induct p. assumption. intros p IH.
replace 0 with (fst (0, p)); [| reflexivity].
replace p with (snd (0, p)); [| reflexivity]. now apply QP.
induct p. assumption. intros p IH.
replace 0 with (snd (p, 0)); [| reflexivity].
replace p with (fst (p, 0)); [| reflexivity]. now apply QS.
Qed.
End Induction.
End NatPairsInt.
|
