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
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
|
Require Import NumPrelude.
Require Import ZDomain.
Require Import ZAxioms.
Module Type PlusSignature.
Declare Module Export IntModule : IntSignature.
Open Local Scope ZScope.
Parameter Inline plus : Z -> Z -> Z.
Parameter Inline minus : Z -> Z -> Z.
Parameter Inline uminus : Z -> Z.
Notation "x + y" := (plus x y) : ZScope.
Notation "x - y" := (minus x y) : ZScope.
Notation "- x" := (uminus x) : ZScope.
Add Morphism plus with signature E ==> E ==> E as plus_wd.
Add Morphism minus with signature E ==> E ==> E as minus_wd.
Add Morphism uminus with signature E ==> E as uminus_wd.
Axiom plus_0 : forall n, 0 + n == n.
Axiom plus_S : forall n m, (S n) + m == S (n + m).
Axiom minus_0 : forall n, n - 0 == n.
Axiom minus_S : forall n m, n - (S m) == P (n - m).
Axiom uminus_0 : - 0 == 0.
Axiom uminus_S : forall n, - (S n) == P (- n).
End PlusSignature.
Module PlusProperties (Export PlusModule : PlusSignature).
Module Export IntPropertiesModule := IntProperties IntModule.
Open Local Scope ZScope.
Theorem plus_P : forall n m, P n + m == P (n + m).
Proof.
intros n m. rewrite_S_P n at 2. rewrite plus_S. now rewrite P_S.
Qed.
Theorem minus_P : forall n m, n - (P m) == S (n - m).
Proof.
intros n m. rewrite_S_P m at 2. rewrite minus_S. now rewrite S_P.
Qed.
Theorem uminus_P : forall n, - (P n) == S (- n).
Proof.
intro n. rewrite_S_P n at 2. rewrite uminus_S. now rewrite S_P.
Qed.
Theorem plus_n_0 : forall n, n + 0 == n.
Proof.
induct n.
now rewrite plus_0.
intros n IH. rewrite plus_S. now rewrite IH.
intros n IH. rewrite plus_P. now rewrite IH.
Qed.
Theorem plus_n_Sm : forall n m, n + S m == S (n + m).
Proof.
intros n m; induct n.
now do 2 rewrite plus_0.
intros n IH. do 2 rewrite plus_S. now rewrite IH.
intros n IH. do 2 rewrite plus_P. rewrite IH. rewrite P_S; now rewrite S_P.
Qed.
Theorem plus_n_Pm : forall n m, n + P m == P (n + m).
Proof.
intros n m; rewrite_S_P m at 2. rewrite plus_n_Sm; now rewrite P_S.
Qed.
Theorem plus_opp_minus : forall n m, n + (- m) == n - m.
Proof.
induct m.
rewrite uminus_0; rewrite minus_0; now rewrite plus_n_0.
intros m IH. rewrite uminus_S; rewrite minus_S. rewrite plus_n_Pm; now rewrite IH.
intros m IH. rewrite uminus_P; rewrite minus_P. rewrite plus_n_Sm; now rewrite IH.
Qed.
Theorem minus_0_n : forall n, 0 - n == - n.
Proof.
intro n; rewrite <- plus_opp_minus; now rewrite plus_0.
Qed.
Theorem minus_Sn_m : forall n m, S n - m == S (n - m).
Proof.
intros n m; do 2 rewrite <- plus_opp_minus; now rewrite plus_S.
Qed.
Theorem minus_Pn_m : forall n m, P n - m == P (n - m).
Proof.
intros n m. rewrite_S_P n at 2; rewrite minus_Sn_m; now rewrite P_S.
Qed.
Theorem plus_assoc : forall n m p, n + (m + p) == (n + m) + p.
Proof.
intros n m p; induct n.
now do 2 rewrite plus_0.
intros n IH. do 3 rewrite plus_S. now rewrite IH.
intros n IH. do 3 rewrite plus_P. now rewrite IH.
Qed.
Theorem plus_comm : forall n m, n + m == m + n.
Proof.
intros n m; induct n.
rewrite plus_0; now rewrite plus_n_0.
intros n IH; rewrite plus_S; rewrite plus_n_Sm; now rewrite IH.
intros n IH; rewrite plus_P; rewrite plus_n_Pm; now rewrite IH.
Qed.
Theorem minus_diag : forall n, n - n == 0.
Proof.
induct n.
now rewrite minus_0.
intros n IH. rewrite minus_S; rewrite minus_Sn_m; rewrite P_S; now rewrite IH.
intros n IH. rewrite minus_P; rewrite minus_Pn_m; rewrite S_P; now rewrite IH.
Qed.
Theorem plus_opp_r : forall n, n + (- n) == 0.
Proof.
intro n; rewrite plus_opp_minus; now rewrite minus_diag.
Qed.
Theorem plus_opp_l : forall n, - n + n == 0.
Proof.
intro n; rewrite plus_comm; apply plus_opp_r.
Qed.
Theorem minus_swap : forall n m, - m + n == n - m.
Proof.
intros n m; rewrite <- plus_opp_minus; now rewrite plus_comm.
Qed.
Theorem plus_minus_inverse : forall n m, n + (m - n) == m.
Proof.
intros n m; rewrite <- minus_swap. rewrite plus_assoc;
rewrite plus_opp_r; now rewrite plus_0.
Qed.
Theorem plus_minus_distr : forall n m p, n + (m - p) == (n + m) - p.
Proof.
intros n m p; do 2 rewrite <- plus_opp_minus; now rewrite plus_assoc.
Qed.
Theorem double_opp : forall n, - (- n) == n.
Proof.
induct n.
now do 2 rewrite uminus_0.
intros n IH. rewrite uminus_S; rewrite uminus_P; now rewrite IH.
intros n IH. rewrite uminus_P; rewrite uminus_S; now rewrite IH.
Qed.
Theorem opp_plus_distr : forall n m, - (n + m) == - n + (- m).
Proof.
intros n m; induct n.
rewrite uminus_0; now do 2 rewrite plus_0.
intros n IH. rewrite plus_S; do 2 rewrite uminus_S. rewrite IH. now rewrite plus_P.
intros n IH. rewrite plus_P; do 2 rewrite uminus_P. rewrite IH. now rewrite plus_S.
Qed.
Theorem opp_minus_distr : forall n m, - (n - m) == - n + m.
Proof.
intros n m; rewrite <- plus_opp_minus; rewrite opp_plus_distr.
now rewrite double_opp.
Qed.
Theorem opp_inj : forall n m, - n == - m -> n == m.
Proof.
intros n m H. apply uminus_wd in H. now do 2 rewrite double_opp in H.
Qed.
Theorem minus_plus_distr : forall n m p, n - (m + p) == (n - m) - p.
Proof.
intros n m p; rewrite <- plus_opp_minus. rewrite opp_plus_distr. rewrite plus_assoc.
now do 2 rewrite plus_opp_minus.
Qed.
Theorem minus_minus_distr : forall n m p, n - (m - p) == (n - m) + p.
Proof.
intros n m p; rewrite <- plus_opp_minus. rewrite opp_minus_distr. rewrite plus_assoc.
now rewrite plus_opp_minus.
Qed.
Theorem plus_minus_swap : forall n m p, n + m - p == n - p + m.
Proof.
intros n m p. rewrite <- plus_minus_distr.
rewrite <- (plus_opp_minus n p). rewrite <- plus_assoc. now rewrite minus_swap.
Qed.
Theorem plus_cancel_l : forall n m p, n + m == n + p -> m == p.
Proof.
intros n m p H.
assert (H1 : - n + n + m == -n + n + p).
do 2 rewrite <- plus_assoc; now rewrite H.
rewrite plus_opp_l in H1; now do 2 rewrite plus_0 in H1.
Qed.
Theorem plus_cancel_r : forall n m p, n + m == p + m -> n == p.
Proof.
intros n m p H.
rewrite plus_comm in H. set (k := m + n) in H. rewrite plus_comm in H.
unfold k in H; clear k. now apply plus_cancel_l with m.
Qed.
Theorem plus_minus_l : forall n m p, m + p == n -> p == n - m.
Proof.
intros n m p H.
assert (H1 : - m + m + p == - m + n).
rewrite <- plus_assoc; now rewrite H.
rewrite plus_opp_l in H1. rewrite plus_0 in H1. now rewrite minus_swap in H1.
Qed.
Theorem plus_minus_r : forall n m p, m + p == n -> m == n - p.
Proof.
intros n m p H; rewrite plus_comm in H; now apply plus_minus_l in H.
Qed.
Lemma minus_eq : forall n m, n - m == 0 -> n == m.
Proof.
intros n m H. rewrite <- (plus_minus_inverse m n). rewrite H. apply plus_n_0.
Qed.
End PlusProperties.
|
