1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
8
(* Evgeny Makarov, INRIA, 2007 *)
9
(************************************************************************)
11
(*i $Id: NDefOps.v 11674 2008-12-12 19:48:40Z letouzey $ i*)
13
Require Import Bool. (* To get the orb and negb function *)
14
Require Export NStrongRec.
16
Module NdefOpsPropFunct (Import NAxiomsMod : NAxiomsSig).
17
Module Export NStrongRecPropMod := NStrongRecPropFunct NAxiomsMod.
18
Open Local Scope NatScope.
20
(*****************************************************)
23
Definition def_add (x y : N) := recursion y (fun _ p => S p) x.
25
Infix Local "++" := def_add (at level 50, left associativity).
27
Add Morphism def_add with signature Neq ==> Neq ==> Neq as def_add_wd.
30
intros x x' Exx' y y' Eyy'.
31
apply recursion_wd with (Aeq := Neq).
33
unfold fun2_eq; intros _ _ _ p p' Epp'; now rewrite Epp'.
37
Theorem def_add_0_l : forall y : N, 0 ++ y == y.
39
intro y. unfold def_add. now rewrite recursion_0.
42
Theorem def_add_succ_l : forall x y : N, S x ++ y == S (x ++ y).
44
intros x y; unfold def_add.
45
rewrite (@recursion_succ N Neq); try reflexivity.
46
unfold fun2_wd. intros _ _ _ m1 m2 H2. now rewrite H2.
49
Theorem def_add_add : forall n m : N, n ++ m == n + m.
52
now rewrite def_add_0_l, add_0_l.
53
intros n H. now rewrite def_add_succ_l, add_succ_l, H.
56
(*****************************************************)
59
Definition def_mul (x y : N) := recursion 0 (fun _ p => p ++ x) y.
61
Infix Local "**" := def_mul (at level 40, left associativity).
63
Lemma def_mul_step_wd : forall x : N, fun2_wd Neq Neq Neq (fun _ p => def_add p x).
65
unfold fun2_wd. intros. now apply def_add_wd.
68
Lemma def_mul_step_equal :
69
forall x x' : N, x == x' ->
70
fun2_eq Neq Neq Neq (fun _ p => def_add p x) (fun x p => def_add p x').
72
unfold fun2_eq; intros; apply def_add_wd; assumption.
75
Add Morphism def_mul with signature Neq ==> Neq ==> Neq as def_mul_wd.
78
intros x x' Exx' y y' Eyy'.
79
apply recursion_wd with (Aeq := Neq).
80
reflexivity. apply def_mul_step_equal. assumption. assumption.
83
Theorem def_mul_0_r : forall x : N, x ** 0 == 0.
85
intro. unfold def_mul. now rewrite recursion_0.
88
Theorem def_mul_succ_r : forall x y : N, x ** S y == x ** y ++ x.
90
intros x y; unfold def_mul.
91
now rewrite (@recursion_succ N Neq); [| apply def_mul_step_wd |].
94
Theorem def_mul_mul : forall n m : N, n ** m == n * m.
97
now rewrite def_mul_0_r, mul_0_r.
98
intros m IH; now rewrite def_mul_succ_r, mul_succ_r, def_add_add, IH.
101
(*****************************************************)
104
Definition def_ltb (m : N) : N -> bool :=
107
(fun _ f => fun n => recursion false (fun n' _ => f n') n)
110
Infix Local "<<" := def_ltb (at level 70, no associativity).
112
Lemma lt_base_wd : fun_wd Neq (@eq bool) (if_zero false true).
113
unfold fun_wd; intros; now apply if_zero_wd.
117
fun2_wd Neq (fun_eq Neq (@eq bool)) (fun_eq Neq (@eq bool))
118
(fun _ f => fun n => recursion false (fun n' _ => f n') n).
120
unfold fun2_wd, fun_eq.
121
intros x x' Exx' f f' Eff' y y' Eyy'.
122
apply recursion_wd with (Aeq := @eq bool).
124
unfold fun2_eq; intros; now apply Eff'.
129
forall m m' : N, m == m' -> fun_eq Neq (@eq bool) (def_ltb m) (def_ltb m').
133
apply recursion_wd with (Aeq := fun_eq Neq (@eq bool)).
139
Add Morphism def_ltb with signature Neq ==> Neq ==> (@eq bool) as def_ltb_wd.
141
intros; now apply lt_curry_wd.
144
Theorem def_ltb_base : forall n : N, 0 << n = if_zero false true n.
146
intro n; unfold def_ltb; now rewrite recursion_0.
149
Theorem def_ltb_step :
150
forall m n : N, S m << n = recursion false (fun n' _ => m << n') n.
152
intros m n; unfold def_ltb.
156
(fun_eq Neq (@eq bool))
158
(fun _ f => fun n => recursion false (fun n' _ => f n') n)
165
(* Above, we rewrite applications of function. Is it possible to rewrite
166
functions themselves, i.e., rewrite (recursion lt_base lt_step (S n)) to
167
lt_step n (recursion lt_base lt_step n)? *)
169
Theorem def_ltb_0 : forall n : N, n << 0 = false.
172
rewrite def_ltb_base; now rewrite if_zero_0.
173
intro n; rewrite def_ltb_step. now rewrite recursion_0.
176
Theorem def_ltb_0_succ : forall n : N, 0 << S n = true.
178
intro n; rewrite def_ltb_base; now rewrite if_zero_succ.
181
Theorem succ_def_ltb_mono : forall n m : N, (S n << S m) = (n << m).
184
rewrite def_ltb_step. rewrite (@recursion_succ bool (@eq bool)); try reflexivity.
185
unfold fun2_wd; intros; now apply def_ltb_wd.
188
Theorem def_ltb_lt : forall n m : N, n << m = true <-> n < m.
192
rewrite def_ltb_0. split; intro H; [discriminate H | false_hyp H nlt_0_r].
193
intro n. rewrite def_ltb_0_succ. split; intro; [apply lt_0_succ | reflexivity].
194
intro n. rewrite def_ltb_0. split; intro H; [discriminate | false_hyp H nlt_0_r].
195
intros n m. rewrite succ_def_ltb_mono. now rewrite <- succ_lt_mono.
199
(*****************************************************)
202
Definition even (x : N) := recursion true (fun _ p => negb p) x.
204
Lemma even_step_wd : fun2_wd Neq (@eq bool) (@eq bool) (fun x p => if p then false else true).
207
intros x x' Exx' b b' Ebb'.
208
unfold eq_bool; destruct b; destruct b'; now simpl.
211
Add Morphism even with signature Neq ==> (@eq bool) as even_wd.
214
apply recursion_wd with (A := bool) (Aeq := (@eq bool)).
216
unfold fun2_eq. intros _ _ _ b b' Ebb'. unfold eq_bool; destruct b; destruct b'; now simpl.
220
Theorem even_0 : even 0 = true.
223
now rewrite recursion_0.
226
Theorem even_succ : forall x : N, even (S x) = negb (even x).
229
intro x; rewrite (recursion_succ (@eq bool)); try reflexivity.
231
intros _ _ _ b b' Ebb'. destruct b; destruct b'; now simpl.
234
(*****************************************************)
237
Definition half_aux (x : N) : N * N :=
238
recursion (0, 0) (fun _ p => let (x1, x2) := p in ((S x2, x1))) x.
240
Definition half (x : N) := snd (half_aux x).
242
Definition E2 := prod_rel Neq Neq.
244
Add Relation (prod N N) E2
245
reflexivity proved by (prod_rel_refl N N Neq Neq E_equiv E_equiv)
246
symmetry proved by (prod_rel_sym N N Neq Neq E_equiv E_equiv)
247
transitivity proved by (prod_rel_trans N N Neq Neq E_equiv E_equiv)
250
Lemma half_step_wd: fun2_wd Neq E2 E2 (fun _ p => let (x1, x2) := p in ((S x2, x1))).
252
unfold fun2_wd, E2, prod_rel.
253
intros _ _ _ p1 p2 [H1 H2].
254
destruct p1; destruct p2; simpl in *.
255
now split; [rewrite H2 |].
258
Add Morphism half with signature Neq ==> Neq as half_wd.
261
assert (H: forall x y, x == y -> E2 (half_aux x) (half_aux y)).
262
intros x y Exy; unfold half_aux; apply recursion_wd with (Aeq := E2); unfold E2.
264
unfold prod_rel; simpl; now split.
265
unfold fun2_eq, prod_rel; simpl.
266
intros _ _ _ p1 p2; destruct p1; destruct p2; simpl.
267
intros [H1 H2]; split; [rewrite H2 | assumption]. reflexivity. assumption.
268
unfold E2, prod_rel in H. intros x y Exy; apply H in Exy.
272
(*****************************************************)
273
(** Logarithm for the base 2 *)
275
Definition log (x : N) : N :=
279
else if (e x 1) then 0
283
Add Morphism log with signature Neq ==> Neq as log_wd.
285
intros x x' Exx'. unfold log.
286
apply strong_rec_wd with (Aeq := Neq); try (reflexivity || assumption).
287
unfold fun2_eq. intros y y' Eyy' g g' Egg'.
288
assert (H : e y 0 = e y' 0); [now apply e_wd|].
289
rewrite <- H; clear H.
290
assert (H : e y 1 = e y' 1); [now apply e_wd|].
291
rewrite <- H; clear H.
292
assert (H : S (g (half y)) == S (g' (half y')));
293
[apply succ_wd; apply Egg'; now apply half_wd|].
294
now destruct (e y 0); destruct (e y 1).
297
End NdefOpsPropFunct.
added
removed
theories/Numbers/Natural/Abstract/NDefOps.v
