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
|
Require Import NArith.
Require Import Ndec.
Require Export NDepRec.
Require Export NTimesOrder.
Require Export NMinus.
Require Export NMiscFunct.
Open Local Scope N_scope.
Module NBinaryDomain : NDomainEqSignature
with Definition N := N
with Definition E := (@eq N)
with Definition e := Neqb.
Definition N := N.
Definition E := (@eq N).
Definition e := Neqb.
Theorem E_equiv_e : forall x y : N, E x y <-> e x y.
Proof.
unfold E, e; intros x y; split; intro H;
[rewrite H; now rewrite Neqb_correct |
apply Neqb_complete; now inversion H].
Qed.
Definition E_equiv : equiv N E := eq_equiv N.
Add Relation N E
reflexivity proved by (proj1 E_equiv)
symmetry proved by (proj2 (proj2 E_equiv))
transitivity proved by (proj1 (proj2 E_equiv))
as E_rel.
End NBinaryDomain.
Module BinaryNat <: NBaseSig.
Module Export NDomainModule := NBinaryDomain.
Definition O := N0.
Definition S := Nsucc.
Add Morphism S with signature E ==> E as succ_wd.
Proof.
congruence.
Qed.
Theorem induction :
forall P : N -> Prop, predicate_wd E P ->
P 0 -> (forall n, P n -> P (S n)) -> forall n, P n.
Proof.
intros P predicate_wd; apply Nind.
Qed.
Definition recursion (A : Set) (a : A) (f : N -> A -> A) (n : N) :=
Nrec (fun _ => A) a f n.
Implicit Arguments recursion [A].
Theorem recursion_wd :
forall (A : Set) (EA : relation A),
forall a a' : A, EA a a' ->
forall f f' : N -> A -> A, eq_fun2 E EA EA f f' ->
forall x x' : N, x = x' ->
EA (recursion a f x) (recursion a' f' x').
Proof.
unfold fun2_wd, E, eq_fun2.
intros A EA a a' Eaa' f f' Eff'.
intro x; pattern x; apply Nind.
intros x' H; now rewrite <- H.
clear x.
intros x IH x' H; rewrite <- H.
unfold recursion, Nrec in *; do 2 rewrite Nrect_step.
now apply Eff'; [| apply IH].
Qed.
Theorem recursion_0 :
forall (A : Set) (a : A) (f : N -> A -> A), recursion a f 0 = a.
Proof.
intros A a f; unfold recursion; unfold Nrec; now rewrite Nrect_base.
Qed.
Theorem recursion_succ :
forall (A : Set) (EA : relation A) (a : A) (f : N -> A -> A),
EA a a -> fun2_wd E EA EA f ->
forall n : N, EA (recursion a f (S n)) (f n (recursion a f n)).
Proof.
unfold E, recursion, Nrec, fun2_wd; intros A EA a f EAaa f_wd n; pattern n; apply Nind.
rewrite Nrect_step; rewrite Nrect_base; now apply f_wd.
clear n; intro n; do 2 rewrite Nrect_step; intro IH. apply f_wd; [reflexivity|].
now rewrite Nrect_step.
Qed.
End BinaryNat.
Module NBinaryDepRec <: NDepRecSignature.
Module Export NDomainModule := NBinaryDomain.
Module Export NBaseMod := BinaryNat.
Definition dep_recursion := Nrec.
Theorem dep_recursion_0 :
forall (A : N -> Set) (a : A 0) (f : forall n, A n -> A (S n)),
dep_recursion A a f 0 = a.
Proof.
intros A a f; unfold dep_recursion; unfold Nrec; now rewrite Nrect_base.
Qed.
Theorem dep_recursion_succ :
forall (A : N -> Set) (a : A 0) (f : forall n, A n -> A (S n)) (n : N),
dep_recursion A a f (S n) = f n (dep_recursion A a f n).
Proof.
intros A a f n; unfold dep_recursion; unfold Nrec; now rewrite Nrect_step.
Qed.
End NBinaryDepRec.
Module NBinaryPlus <: NPlusSig.
Module Export NBaseMod := BinaryNat.
Definition plus := Nplus.
Add Morphism plus with signature E ==> E ==> E as plus_wd.
Proof.
unfold E; congruence.
Qed.
Theorem plus_0_l : forall n, 0 + n = n.
Proof.
exact Nplus_0_l.
Qed.
Theorem plus_succ_l : forall n m, (S n) + m = S (n + m).
Proof.
exact Nplus_succ.
Qed.
End NBinaryPlus.
Module NBinaryTimes <: NTimesSig.
Module Export NPlusMod := NBinaryPlus.
Definition times := Nmult.
Add Morphism times with signature E ==> E ==> E as times_wd.
Proof.
unfold E; congruence.
Qed.
Theorem times_0_r : forall n, n * 0 = 0.
Proof.
intro n; rewrite Nmult_comm; apply Nmult_0_l.
Qed.
Theorem times_succ_r : forall n m, n * (S m) = n * m + n.
Proof.
intros n m; rewrite Nmult_comm; rewrite Nmult_succn_m.
rewrite Nplus_comm; now rewrite Nmult_comm.
Qed.
End NBinaryTimes.
Module NBinaryOrder <: NOrderSig.
Module Export NBaseMod := BinaryNat.
Definition lt (m n : N) := comp_bool (Ncompare m n) Lt.
Definition le (m n : N) := let c := (Ncompare m n) in orb (comp_bool c Lt) (comp_bool c Eq).
Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd.
Proof.
unfold E; congruence.
Qed.
Add Morphism le with signature E ==> E ==> eq_bool as le_wd.
Proof.
unfold E; congruence.
Qed.
Theorem le_lt : forall n m, le n m <-> lt n m \/ n = m.
Proof.
intros n m.
assert (H : (n ?= m) = Eq <-> n = m).
(split; intro H); [now apply Ncompare_Eq_eq | rewrite H; apply Ncompare_refl].
unfold le, lt; rewrite eq_true_or. repeat rewrite comp_bool_correct. now rewrite H.
Qed.
Theorem lt_0 : forall x, ~ (lt x 0).
Proof.
unfold lt; destruct x as [|x]; simpl; now intro.
Qed.
Theorem lt_succ : forall x y, lt x (S y) <-> le x y.
Proof.
intros x y. rewrite le_lt.
assert (H1 : lt x (S y) <-> Ncompare x (S y) = Lt);
[unfold lt, comp_bool; destruct (x ?= S y); simpl; split; now intro |].
assert (H2 : lt x y <-> Ncompare x y = Lt);
[unfold lt, comp_bool; destruct (x ?= y); simpl; split; now intro |].
pose proof (Ncompare_n_succm x y) as H. tauto.
Qed.
End NBinaryOrder.
Module Export NBinaryTimesOrderProperties := NTimesOrderProperties NBinaryTimes NBinaryOrder.
(* Todo: N implements NPred.v and NMinus.v *)
(*Module Export BinaryRecEx := MiscFunctFunctor BinaryNat.*)
(* Just some fun comparing the efficiency of the generic log defined
by strong (course-of-value) recursion and the log defined by recursion
on notation *)
(* Time Eval compute in (log 100000). *) (* 98 sec *)
(*
Fixpoint binposlog (p : positive) : N :=
match p with
| xH => 0
| xO p' => Nsucc (binposlog p')
| xI p' => Nsucc (binposlog p')
end.
Definition binlog (n : N) : N :=
match n with
| 0 => 0
| Npos p => binposlog p
end.
*)
(* Eval compute in (binlog 1000000000000000000). *) (* Works very fast *)
(*
Local Variables:
tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
End:
*)
|
