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
|
(************************************************************************)
(* 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 i*)
Require Import BinPos.
Require Import NBinDefs.
(*Unset Boxed Definitions.*)
Delimit Scope N_scope with N.
Bind Scope N_scope with N.
Open Local Scope N_scope.
(** Operations *)
Notation N := N (only parsing).
Notation N0 := N0 (only parsing).
Notation Npos := Npos (only parsing).
Notation Nsucc := succ (only parsing).
Notation Npred := pred (only parsing).
Notation Nplus := plus (only parsing).
Notation Nminus := minus (only parsing).
Notation Nmult := times (only parsing).
Notation Ncompare := Ncompare (only parsing).
Notation Nlt := lt (only parsing).
Notation Nle := le (only parsing).
Definition Ngt (x y : N) := (Ncompare x y) = Gt.
Definition Nge (x y : N) := (Ncompare x y) <> Lt.
Notation Nmin := min (only parsing).
Notation Nmax := max (only parsing).
(* If the notations for operations above had been actual definitions, the
arguments scopes would have been N_scope due to the instruction "Bind Scope
N_scope with N". However, the operations were declared in NBinary, where
N_scope has not yet been declared. Therefore, we need to assign the
arguments scopes manually. Note that this has to be done before declaring
infix notations below. Ngt and Nge get their scope from the definition. *)
Arguments Scope succ [N_scope].
Arguments Scope pred [N_scope].
Arguments Scope plus [N_scope N_scope].
Arguments Scope minus [N_scope N_scope].
Arguments Scope times [N_scope N_scope].
Arguments Scope NBinDefs.Ncompare [N_scope N_scope].
Arguments Scope lt [N_scope N_scope].
Arguments Scope le [N_scope N_scope].
Arguments Scope min [N_scope N_scope].
Arguments Scope max [N_scope N_scope].
Infix "+" := Nplus : N_scope.
Infix "-" := Nminus : N_scope.
Infix "*" := Nmult : N_scope.
Infix "?=" := Ncompare (at level 70, no associativity) : N_scope.
Infix "<=" := Nle : N_scope.
Infix "<" := Nlt : N_scope.
Infix ">=" := Nge : N_scope.
Infix ">" := Ngt : N_scope.
(** Peano induction and recursion *)
Notation Nrect := Nrect (only parsing).
Notation Nrect_base := Nrect_base (only parsing).
Notation Nrect_step := Nrect_step (only parsing).
Definition Nind (P : N -> Prop) := Nrect P.
Definition Nrec (P : N -> Set) := Nrect P.
Theorem Nrec_base : forall P a f, Nrec P a f N0 = a.
Proof.
intros P a f; unfold Nrec; apply Nrect_base.
Qed.
Theorem Nrec_step : forall P a f n, Nrec P a f (Nsucc n) = f n (Nrec P a f n).
Proof.
intros P a f; unfold Nrec; apply Nrect_step.
Qed.
(** Properties of successor and predecessor *)
Notation Npred_succ := pred_succ (only parsing).
Notation Nsucc_0 := neq_succ_0 (only parsing).
Notation Nsucc_inj := succ_inj (only parsing).
(** Properties of addition *)
Notation Nplus_0_l := plus_0_l (only parsing).
Notation Nplus_0_r := plus_0_r (only parsing).
Notation Nplus_comm := plus_comm (only parsing).
Notation Nplus_assoc := plus_assoc (only parsing).
Notation Nplus_succ := plus_succ_l (only parsing).
Notation Nplus_reg_l := (fun n m p : N => proj1 (plus_cancel_l m p n)) (only parsing).
(** Properties of subtraction. *)
Notation Nminus_N0_Nle := minus_0_le (only parsing).
Notation Nminus_0_r := minus_0_r (only parsing).
Notation Nminus_succ_r := minus_succ_r (only parsing).
(** Properties of multiplication *)
Notation Nmult_0_l := times_0_l (only parsing).
Notation Nmult_1_l := times_1_l (only parsing).
Notation Nmult_1_r := times_1_r (only parsing).
Theorem Nmult_Sn_m : forall n m : N, (Nsucc n) * m = m + n * m.
Proof.
intros; now rewrite times_succ_l, Nplus_comm.
Qed.
Notation Nmult_comm := times_comm (only parsing).
Notation Nmult_assoc := times_assoc (only parsing).
Notation Nmult_plus_distr_r := times_plus_distr_r (only parsing).
Notation Nmult_reg_r :=
(fun (n m p : N) (H : p <> N0) => proj1 (times_cancel_r n m p H)) (only parsing).
(** Properties of comparison *)
Notation Ncompare_Eq_eq := (fun n m : N => proj1 (Ncompare_eq_correct n m)) (only parsing).
Notation Ncompare_refl := Ncompare_diag (only parsing).
Notation Nlt_irrefl := lt_irrefl (only parsing).
Lemma Ncompare_antisym : forall n m, CompOpp (n ?= m) = (m ?= n).
Proof.
destruct n; destruct m; simpl; auto.
exact (Pcompare_antisym p p0 Eq).
Qed.
Theorem Ncompare_0 : forall n : N, Ncompare n N0 <> Lt.
Proof.
destruct n; discriminate.
Qed.
(** Other properties and operations; given explicitly *)
Definition Ndiscr : forall n : N, {p : positive | n = Npos p} + {n = N0}.
Proof.
destruct n; auto.
left; exists p; auto.
Defined.
(** Operation x -> 2 * x + 1 *)
Definition Ndouble_plus_one x :=
match x with
| N0 => Npos 1
| Npos p => Npos p~1
end.
(** Operation x -> 2 * x *)
Definition Ndouble n :=
match n with
| N0 => N0
| Npos p => Npos p~0
end.
(** convenient induction principles *)
Theorem N_ind_double :
forall (a:N) (P:N -> Prop),
P N0 ->
(forall a, P a -> P (Ndouble a)) ->
(forall a, P a -> P (Ndouble_plus_one a)) -> P a.
Proof.
intros; elim a. trivial.
simple induction p. intros.
apply (H1 (Npos p0)); trivial.
intros; apply (H0 (Npos p0)); trivial.
intros; apply (H1 N0); assumption.
Qed.
Lemma N_rec_double :
forall (a:N) (P:N -> Set),
P N0 ->
(forall a, P a -> P (Ndouble a)) ->
(forall a, P a -> P (Ndouble_plus_one a)) -> P a.
Proof.
intros; elim a. trivial.
simple induction p. intros.
apply (H1 (Npos p0)); trivial.
intros; apply (H0 (Npos p0)); trivial.
intros; apply (H1 N0); assumption.
Qed.
(** Division by 2 *)
Definition Ndiv2 (n:N) :=
match n with
| N0 => N0
| Npos 1 => N0
| Npos p~0 => Npos p
| Npos p~1 => Npos p
end.
Lemma Ndouble_div2 : forall n:N, Ndiv2 (Ndouble n) = n.
Proof.
destruct n; trivial.
Qed.
Lemma Ndouble_plus_one_div2 :
forall n:N, Ndiv2 (Ndouble_plus_one n) = n.
Proof.
destruct n; trivial.
Qed.
Lemma Ndouble_inj : forall n m, Ndouble n = Ndouble m -> n = m.
Proof.
intros. rewrite <- (Ndouble_div2 n). rewrite H. apply Ndouble_div2.
Qed.
Lemma Ndouble_plus_one_inj :
forall n m, Ndouble_plus_one n = Ndouble_plus_one m -> n = m.
Proof.
intros. rewrite <- (Ndouble_plus_one_div2 n). rewrite H. apply Ndouble_plus_one_div2.
Qed.
|
