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
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
|
(************************************************************************)
(* 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: NDefOps.v 11039 2008-06-02 23:26:13Z letouzey $ i*)
Require Import Bool. (* To get the orb and negb function *)
Require Export NStrongRec.
Module NdefOpsPropFunct (Import NAxiomsMod : NAxiomsSig).
Module Export NStrongRecPropMod := NStrongRecPropFunct NAxiomsMod.
Open Local Scope NatScope.
(*****************************************************)
(** Addition *)
Definition def_add (x y : N) := recursion y (fun _ p => S p) x.
Infix Local "++" := def_add (at level 50, left associativity).
Add Morphism def_add with signature Neq ==> Neq ==> Neq as def_add_wd.
Proof.
unfold def_add.
intros x x' Exx' y y' Eyy'.
apply recursion_wd with (Aeq := Neq).
assumption.
unfold fun2_eq; intros _ _ _ p p' Epp'; now rewrite Epp'.
assumption.
Qed.
Theorem def_add_0_l : forall y : N, 0 ++ y == y.
Proof.
intro y. unfold def_add. now rewrite recursion_0.
Qed.
Theorem def_add_succ_l : forall x y : N, S x ++ y == S (x ++ y).
Proof.
intros x y; unfold def_add.
rewrite (@recursion_succ N Neq); try reflexivity.
unfold fun2_wd. intros _ _ _ m1 m2 H2. now rewrite H2.
Qed.
Theorem def_add_add : forall n m : N, n ++ m == n + m.
Proof.
intros n m; induct n.
now rewrite def_add_0_l, add_0_l.
intros n H. now rewrite def_add_succ_l, add_succ_l, H.
Qed.
(*****************************************************)
(** Multiplication *)
Definition def_mul (x y : N) := recursion 0 (fun _ p => p ++ x) y.
Infix Local "**" := def_mul (at level 40, left associativity).
Lemma def_mul_step_wd : forall x : N, fun2_wd Neq Neq Neq (fun _ p => def_add p x).
Proof.
unfold fun2_wd. intros. now apply def_add_wd.
Qed.
Lemma def_mul_step_equal :
forall x x' : N, x == x' ->
fun2_eq Neq Neq Neq (fun _ p => def_add p x) (fun x p => def_add p x').
Proof.
unfold fun2_eq; intros; apply def_add_wd; assumption.
Qed.
Add Morphism def_mul with signature Neq ==> Neq ==> Neq as def_mul_wd.
Proof.
unfold def_mul.
intros x x' Exx' y y' Eyy'.
apply recursion_wd with (Aeq := Neq).
reflexivity. apply def_mul_step_equal. assumption. assumption.
Qed.
Theorem def_mul_0_r : forall x : N, x ** 0 == 0.
Proof.
intro. unfold def_mul. now rewrite recursion_0.
Qed.
Theorem def_mul_succ_r : forall x y : N, x ** S y == x ** y ++ x.
Proof.
intros x y; unfold def_mul.
now rewrite (@recursion_succ N Neq); [| apply def_mul_step_wd |].
Qed.
Theorem def_mul_mul : forall n m : N, n ** m == n * m.
Proof.
intros n m; induct m.
now rewrite def_mul_0_r, mul_0_r.
intros m IH; now rewrite def_mul_succ_r, mul_succ_r, def_add_add, IH.
Qed.
(*****************************************************)
(** Order *)
Definition def_ltb (m : N) : N -> bool :=
recursion
(if_zero false true)
(fun _ f => fun n => recursion false (fun n' _ => f n') n)
m.
Infix Local "<<" := def_ltb (at level 70, no associativity).
Lemma lt_base_wd : fun_wd Neq (@eq bool) (if_zero false true).
unfold fun_wd; intros; now apply if_zero_wd.
Qed.
Lemma lt_step_wd :
fun2_wd Neq (fun_eq Neq (@eq bool)) (fun_eq Neq (@eq bool))
(fun _ f => fun n => recursion false (fun n' _ => f n') n).
Proof.
unfold fun2_wd, fun_eq.
intros x x' Exx' f f' Eff' y y' Eyy'.
apply recursion_wd with (Aeq := @eq bool).
reflexivity.
unfold fun2_eq; intros; now apply Eff'.
assumption.
Qed.
Lemma lt_curry_wd :
forall m m' : N, m == m' -> fun_eq Neq (@eq bool) (def_ltb m) (def_ltb m').
Proof.
unfold def_ltb.
intros m m' Emm'.
apply recursion_wd with (Aeq := fun_eq Neq (@eq bool)).
apply lt_base_wd.
apply lt_step_wd.
assumption.
Qed.
Add Morphism def_ltb with signature Neq ==> Neq ==> (@eq bool) as def_ltb_wd.
Proof.
intros; now apply lt_curry_wd.
Qed.
Theorem def_ltb_base : forall n : N, 0 << n = if_zero false true n.
Proof.
intro n; unfold def_ltb; now rewrite recursion_0.
Qed.
Theorem def_ltb_step :
forall m n : N, S m << n = recursion false (fun n' _ => m << n') n.
Proof.
intros m n; unfold def_ltb.
pose proof
(@recursion_succ
(N -> bool)
(fun_eq Neq (@eq bool))
(if_zero false true)
(fun _ f => fun n => recursion false (fun n' _ => f n') n)
lt_base_wd
lt_step_wd
m n n) as H.
now rewrite H.
Qed.
(* Above, we rewrite applications of function. Is it possible to rewrite
functions themselves, i.e., rewrite (recursion lt_base lt_step (S n)) to
lt_step n (recursion lt_base lt_step n)? *)
Theorem def_ltb_0 : forall n : N, n << 0 = false.
Proof.
cases n.
rewrite def_ltb_base; now rewrite if_zero_0.
intro n; rewrite def_ltb_step. now rewrite recursion_0.
Qed.
Theorem def_ltb_0_succ : forall n : N, 0 << S n = true.
Proof.
intro n; rewrite def_ltb_base; now rewrite if_zero_succ.
Qed.
Theorem succ_def_ltb_mono : forall n m : N, (S n << S m) = (n << m).
Proof.
intros n m.
rewrite def_ltb_step. rewrite (@recursion_succ bool (@eq bool)); try reflexivity.
unfold fun2_wd; intros; now apply def_ltb_wd.
Qed.
Theorem def_ltb_lt : forall n m : N, n << m = true <-> n < m.
Proof.
double_induct n m.
cases m.
rewrite def_ltb_0. split; intro H; [discriminate H | false_hyp H nlt_0_r].
intro n. rewrite def_ltb_0_succ. split; intro; [apply lt_0_succ | reflexivity].
intro n. rewrite def_ltb_0. split; intro H; [discriminate | false_hyp H nlt_0_r].
intros n m. rewrite succ_def_ltb_mono. now rewrite <- succ_lt_mono.
Qed.
(*
(*****************************************************)
(** Even *)
Definition even (x : N) := recursion true (fun _ p => negb p) x.
Lemma even_step_wd : fun2_wd Neq (@eq bool) (@eq bool) (fun x p => if p then false else true).
Proof.
unfold fun2_wd.
intros x x' Exx' b b' Ebb'.
unfold eq_bool; destruct b; destruct b'; now simpl.
Qed.
Add Morphism even with signature Neq ==> (@eq bool) as even_wd.
Proof.
unfold even; intros.
apply recursion_wd with (A := bool) (Aeq := (@eq bool)).
now unfold eq_bool.
unfold fun2_eq. intros _ _ _ b b' Ebb'. unfold eq_bool; destruct b; destruct b'; now simpl.
assumption.
Qed.
Theorem even_0 : even 0 = true.
Proof.
unfold even.
now rewrite recursion_0.
Qed.
Theorem even_succ : forall x : N, even (S x) = negb (even x).
Proof.
unfold even.
intro x; rewrite (recursion_succ (@eq bool)); try reflexivity.
unfold fun2_wd.
intros _ _ _ b b' Ebb'. destruct b; destruct b'; now simpl.
Qed.
(*****************************************************)
(** Division by 2 *)
Definition half_aux (x : N) : N * N :=
recursion (0, 0) (fun _ p => let (x1, x2) := p in ((S x2, x1))) x.
Definition half (x : N) := snd (half_aux x).
Definition E2 := prod_rel Neq Neq.
Add Relation (prod N N) E2
reflexivity proved by (prod_rel_refl N N Neq Neq E_equiv E_equiv)
symmetry proved by (prod_rel_symm N N Neq Neq E_equiv E_equiv)
transitivity proved by (prod_rel_trans N N Neq Neq E_equiv E_equiv)
as E2_rel.
Lemma half_step_wd: fun2_wd Neq E2 E2 (fun _ p => let (x1, x2) := p in ((S x2, x1))).
Proof.
unfold fun2_wd, E2, prod_rel.
intros _ _ _ p1 p2 [H1 H2].
destruct p1; destruct p2; simpl in *.
now split; [rewrite H2 |].
Qed.
Add Morphism half with signature Neq ==> Neq as half_wd.
Proof.
unfold half.
assert (H: forall x y, x == y -> E2 (half_aux x) (half_aux y)).
intros x y Exy; unfold half_aux; apply recursion_wd with (Aeq := E2); unfold E2.
unfold E2.
unfold prod_rel; simpl; now split.
unfold fun2_eq, prod_rel; simpl.
intros _ _ _ p1 p2; destruct p1; destruct p2; simpl.
intros [H1 H2]; split; [rewrite H2 | assumption]. reflexivity. assumption.
unfold E2, prod_rel in H. intros x y Exy; apply H in Exy.
exact (proj2 Exy).
Qed.
(*****************************************************)
(** Logarithm for the base 2 *)
Definition log (x : N) : N :=
strong_rec 0
(fun x g =>
if (e x 0) then 0
else if (e x 1) then 0
else S (g (half x)))
x.
Add Morphism log with signature Neq ==> Neq as log_wd.
Proof.
intros x x' Exx'. unfold log.
apply strong_rec_wd with (Aeq := Neq); try (reflexivity || assumption).
unfold fun2_eq. intros y y' Eyy' g g' Egg'.
assert (H : e y 0 = e y' 0); [now apply e_wd|].
rewrite <- H; clear H.
assert (H : e y 1 = e y' 1); [now apply e_wd|].
rewrite <- H; clear H.
assert (H : S (g (half y)) == S (g' (half y')));
[apply succ_wd; apply Egg'; now apply half_wd|].
now destruct (e y 0); destruct (e y 1).
Qed.
*)
End NdefOpsPropFunct.
|
