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
224
225
226
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
(*i $Id$ i*)
Require Export NMulOrder.
Module NSubPropFunct (Import N : NAxiomsSig).
Include NMulOrderPropFunct N.
Local Open Scope NumScope.
Theorem sub_0_l : forall n, 0 - n == 0.
Proof.
induct n.
apply sub_0_r.
intros n IH; rewrite sub_succ_r; rewrite IH. now apply pred_0.
Qed.
Theorem sub_succ : forall n m, S n - S m == n - m.
Proof.
intro n; induct m.
rewrite sub_succ_r. do 2 rewrite sub_0_r. now rewrite pred_succ.
intros m IH. rewrite sub_succ_r. rewrite IH. now rewrite sub_succ_r.
Qed.
Theorem sub_diag : forall n, n - n == 0.
Proof.
induct n. apply sub_0_r. intros n IH; rewrite sub_succ; now rewrite IH.
Qed.
Theorem sub_gt : forall n m, n > m -> n - m ~= 0.
Proof.
intros n m H; elim H using lt_ind_rel; clear n m H.
solve_relation_wd.
intro; rewrite sub_0_r; apply neq_succ_0.
intros; now rewrite sub_succ.
Qed.
Theorem add_sub_assoc : forall n m p, p <= m -> n + (m - p) == (n + m) - p.
Proof.
intros n m p; induct p.
intro; now do 2 rewrite sub_0_r.
intros p IH H. do 2 rewrite sub_succ_r.
rewrite <- IH by (apply lt_le_incl; now apply -> le_succ_l).
rewrite add_pred_r by (apply sub_gt; now apply -> le_succ_l).
reflexivity.
Qed.
Theorem sub_succ_l : forall n m, n <= m -> S m - n == S (m - n).
Proof.
intros n m H. rewrite <- (add_1_l m). rewrite <- (add_1_l (m - n)).
symmetry; now apply add_sub_assoc.
Qed.
Theorem add_sub : forall n m, (n + m) - m == n.
Proof.
intros n m. rewrite <- add_sub_assoc by (apply le_refl).
rewrite sub_diag; now rewrite add_0_r.
Qed.
Theorem sub_add : forall n m, n <= m -> (m - n) + n == m.
Proof.
intros n m H. rewrite add_comm. rewrite add_sub_assoc by assumption.
rewrite add_comm. apply add_sub.
Qed.
Theorem add_sub_eq_l : forall n m p, m + p == n -> n - m == p.
Proof.
intros n m p H. symmetry.
assert (H1 : m + p - m == n - m) by now rewrite H.
rewrite add_comm in H1. now rewrite add_sub in H1.
Qed.
Theorem add_sub_eq_r : forall n m p, m + p == n -> n - p == m.
Proof.
intros n m p H; rewrite add_comm in H; now apply add_sub_eq_l.
Qed.
(* This could be proved by adding m to both sides. Then the proof would
use add_sub_assoc and sub_0_le, which is proven below. *)
Theorem add_sub_eq_nz : forall n m p, p ~= 0 -> n - m == p -> m + p == n.
Proof.
intros n m p H; double_induct n m.
intros m H1; rewrite sub_0_l in H1. symmetry in H1; false_hyp H1 H.
intro n; rewrite sub_0_r; now rewrite add_0_l.
intros n m IH H1. rewrite sub_succ in H1. apply IH in H1.
rewrite add_succ_l; now rewrite H1.
Qed.
Theorem sub_add_distr : forall n m p, n - (m + p) == (n - m) - p.
Proof.
intros n m; induct p.
rewrite add_0_r; now rewrite sub_0_r.
intros p IH. rewrite add_succ_r; do 2 rewrite sub_succ_r. now rewrite IH.
Qed.
Theorem add_sub_swap : forall n m p, p <= n -> n + m - p == n - p + m.
Proof.
intros n m p H.
rewrite (add_comm n m).
rewrite <- add_sub_assoc by assumption.
now rewrite (add_comm m (n - p)).
Qed.
(** Sub and order *)
Theorem le_sub_l : forall n m, n - m <= n.
Proof.
intro n; induct m.
rewrite sub_0_r; now apply eq_le_incl.
intros m IH. rewrite sub_succ_r.
apply le_trans with (n - m); [apply le_pred_l | assumption].
Qed.
Theorem sub_0_le : forall n m, n - m == 0 <-> n <= m.
Proof.
double_induct n m.
intro m; split; intro; [apply le_0_l | apply sub_0_l].
intro m; rewrite sub_0_r; split; intro H;
[false_hyp H neq_succ_0 | false_hyp H nle_succ_0].
intros n m H. rewrite <- succ_le_mono. now rewrite sub_succ.
Qed.
(** Sub and mul *)
Theorem mul_pred_r : forall n m, n * (P m) == n * m - n.
Proof.
intros n m; cases m.
now rewrite pred_0, mul_0_r, sub_0_l.
intro m; rewrite pred_succ, mul_succ_r, <- add_sub_assoc.
now rewrite sub_diag, add_0_r.
now apply eq_le_incl.
Qed.
Theorem mul_sub_distr_r : forall n m p, (n - m) * p == n * p - m * p.
Proof.
intros n m p; induct n.
now rewrite sub_0_l, mul_0_l, sub_0_l.
intros n IH. destruct (le_gt_cases m n) as [H | H].
rewrite sub_succ_l by assumption. do 2 rewrite mul_succ_l.
rewrite (add_comm ((n - m) * p) p), (add_comm (n * p) p).
rewrite <- (add_sub_assoc p (n * p) (m * p)) by now apply mul_le_mono_r.
now apply <- add_cancel_l.
assert (H1 : S n <= m); [now apply <- le_succ_l |].
setoid_replace (S n - m) with 0 by now apply <- sub_0_le.
setoid_replace ((S n * p) - m * p) with 0 by (apply <- sub_0_le; now apply mul_le_mono_r).
apply mul_0_l.
Qed.
Theorem mul_sub_distr_l : forall n m p, p * (n - m) == p * n - p * m.
Proof.
intros n m p; rewrite (mul_comm p (n - m)), (mul_comm p n), (mul_comm p m).
apply mul_sub_distr_r.
Qed.
(** Alternative definitions of [<=] and [<] based on [+] *)
Definition le_alt n m := exists p, p + n == m.
Definition lt_alt n m := exists p, S p + n == m.
Lemma le_equiv : forall n m, le_alt n m <-> n <= m.
Proof.
split.
intros (p,H). rewrite <- H, add_comm. apply le_add_r.
intro H. exists (m-n). now apply sub_add.
Qed.
Lemma lt_equiv : forall n m, lt_alt n m <-> n < m.
Proof.
split.
intros (p,H). rewrite <- H, add_succ_l, lt_succ_r, add_comm. apply le_add_r.
intro H. exists (m-S n). rewrite add_succ_l, <- add_succ_r.
apply sub_add. now rewrite le_succ_l.
Qed.
Instance le_alt_wd : Proper (eq==>eq==>iff) le_alt.
Proof.
intros x x' Hx y y' Hy; unfold le_alt.
setoid_rewrite Hx. setoid_rewrite Hy. auto with *.
Qed.
Instance lt_alt_wd : Proper (eq==>eq==>iff) lt_alt.
Proof.
intros x x' Hx y y' Hy; unfold lt_alt.
setoid_rewrite Hx. setoid_rewrite Hy. auto with *.
Qed.
(** With these alternative definition, the dichotomy:
[forall n m, n <= m \/ m <= n]
becomes:
[forall n m, (exists p, p + n == m) \/ (exists p, p + m == n)]
We will need this in the proof of induction principle for integers
constructed as pairs of natural numbers. This formula can be proved
from know properties of [<=]. However, it can also be done directly. *)
Theorem le_alt_dichotomy : forall n m, le_alt n m \/ le_alt m n.
Proof.
intros n m; induct n.
left; exists m; apply add_0_r.
intros n IH.
destruct IH as [[p H] | [p H]].
destruct (zero_or_succ p) as [H1 | [p' H1]]; rewrite H1 in H.
rewrite add_0_l in H. right; exists (S 0); rewrite H, add_succ_l;
now rewrite add_0_l.
left; exists p'; rewrite add_succ_r; now rewrite add_succ_l in H.
right; exists (S p). rewrite add_succ_l; now rewrite H.
Qed.
Theorem add_dichotomy :
forall n m, (exists p, p + n == m) \/ (exists p, p + m == n).
Proof le_alt_dichotomy.
End NSubPropFunct.
|
