← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to theories/Init/Peano.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
theories/Init/Peano.v
 
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
 
 
9
(*i $Id: Peano.v 11735 2009-01-02 17:22:31Z herbelin $ i*)
 
10
 
 
11
(** The type [nat] of Peano natural numbers (built from [O] and [S])
 
12
    is defined in [Datatypes.v] *)
 
13
 
 
14
(** This module defines the following operations on natural numbers :
 
15
    - predecessor [pred]
 
16
    - addition [plus]
 
17
    - multiplication [mult]
 
18
    - less or equal order [le]
 
19
    - less [lt]
 
20
    - greater or equal [ge]
 
21
    - greater [gt]
 
22
 
 
23
   It states various lemmas and theorems about natural numbers,
 
24
   including Peano's axioms of arithmetic (in Coq, these are provable).
 
25
   Case analysis on [nat] and induction on [nat * nat] are provided too
 
26
 *)
 
27
 
 
28
Require Import Notations.
 
29
Require Import Datatypes.
 
30
Require Import Logic.
 
31
Unset Boxed Definitions.
 
32
 
 
33
Open Scope nat_scope.
 
34
 
 
35
Definition eq_S := f_equal S.
 
36
 
 
37
Hint Resolve (f_equal S): v62.
 
38
Hint Resolve (f_equal (A:=nat)): core.
 
39
 
 
40
(** The predecessor function *)
 
41
 
 
42
Definition pred (n:nat) : nat := match n with
 
43
                                 | O => n
 
44
                                 | S u => u
 
45
                                 end.
 
46
Hint Resolve (f_equal pred): v62.
 
47
 
 
48
Theorem pred_Sn : forall n:nat, n = pred (S n).
 
49
Proof.
 
50
  simpl; reflexivity.
 
51
Qed.
 
52
 
 
53
(** Injectivity of successor *)
 
54
 
 
55
Theorem eq_add_S : forall n m:nat, S n = S m -> n = m.
 
56
Proof.
 
57
  intros n m Sn_eq_Sm.
 
58
  replace (n=m) with (pred (S n) = pred (S m)) by auto using pred_Sn.
 
59
  rewrite Sn_eq_Sm; trivial.
 
60
Qed.
 
61
 
 
62
Hint Immediate eq_add_S: core.
 
63
 
 
64
Theorem not_eq_S : forall n m:nat, n <> m -> S n <> S m.
 
65
Proof.
 
66
  red in |- *; auto.
 
67
Qed.
 
68
Hint Resolve not_eq_S: core.
 
69
 
 
70
Definition IsSucc (n:nat) : Prop :=
 
71
  match n with
 
72
  | O => False
 
73
  | S p => True
 
74
  end.
 
75
 
 
76
(** Zero is not the successor of a number *)
 
77
 
 
78
Theorem O_S : forall n:nat, 0 <> S n.
 
79
Proof.
 
80
  unfold not; intros n H.
 
81
  inversion H.
 
82
Qed.
 
83
Hint Resolve O_S: core.
 
84
 
 
85
Theorem n_Sn : forall n:nat, n <> S n.
 
86
Proof.
 
87
  induction n; auto.
 
88
Qed.
 
89
Hint Resolve n_Sn: core.
 
90
 
 
91
(** Addition *)
 
92
 
 
93
Fixpoint plus (n m:nat) {struct n} : nat :=
 
94
  match n with
 
95
  | O => m
 
96
  | S p => S (p + m)
 
97
  end
 
98
 
 
99
where "n + m" := (plus n m) : nat_scope.
 
100
 
 
101
Hint Resolve (f_equal2 plus): v62.
 
102
Hint Resolve (f_equal2 (A1:=nat) (A2:=nat)): core.
 
103
 
 
104
Lemma plus_n_O : forall n:nat, n = n + 0.
 
105
Proof.
 
106
  induction n; simpl in |- *; auto.
 
107
Qed.
 
108
Hint Resolve plus_n_O: core.
 
109
 
 
110
Lemma plus_O_n : forall n:nat, 0 + n = n.
 
111
Proof.
 
112
  auto.
 
113
Qed.
 
114
 
 
115
Lemma plus_n_Sm : forall n m:nat, S (n + m) = n + S m.
 
116
Proof.
 
117
  intros n m; induction n; simpl in |- *; auto.
 
118
Qed.
 
119
Hint Resolve plus_n_Sm: core.
 
120
 
 
121
Lemma plus_Sn_m : forall n m:nat, S n + m = S (n + m).
 
122
Proof.
 
123
  auto.
 
124
Qed.
 
125
 
 
126
(** Standard associated names *)
 
127
 
 
128
Notation plus_0_r_reverse := plus_n_O (only parsing).
 
129
Notation plus_succ_r_reverse := plus_n_Sm (only parsing).
 
130
 
 
131
(** Multiplication *)
 
132
 
 
133
Fixpoint mult (n m:nat) {struct n} : nat :=
 
134
  match n with
 
135
  | O => 0
 
136
  | S p => m + p * m
 
137
  end
 
138
 
 
139
where "n * m" := (mult n m) : nat_scope.
 
140
 
 
141
Hint Resolve (f_equal2 mult): core.
 
142
 
 
143
Lemma mult_n_O : forall n:nat, 0 = n * 0.
 
144
Proof.
 
145
  induction n; simpl in |- *; auto.
 
146
Qed.
 
147
Hint Resolve mult_n_O: core.
 
148
 
 
149
Lemma mult_n_Sm : forall n m:nat, n * m + n = n * S m.
 
150
Proof.
 
151
  intros; induction n as [| p H]; simpl in |- *; auto.
 
152
  destruct H; rewrite <- plus_n_Sm; apply (f_equal S).
 
153
  pattern m at 1 3 in |- *; elim m; simpl in |- *; auto.
 
154
Qed.
 
155
Hint Resolve mult_n_Sm: core.
 
156
 
 
157
(** Standard associated names *)
 
158
 
 
159
Notation mult_0_r_reverse := mult_n_O (only parsing).
 
160
Notation mult_succ_r_reverse := mult_n_Sm (only parsing).
 
161
 
 
162
(** Truncated subtraction: [m-n] is [0] if [n>=m] *)
 
163
 
 
164
Fixpoint minus (n m:nat) {struct n} : nat :=
 
165
  match n, m with
 
166
  | O, _ => n
 
167
  | S k, O => n
 
168
  | S k, S l => k - l
 
169
  end
 
170
 
 
171
where "n - m" := (minus n m) : nat_scope.
 
172
 
 
173
(** Definition of the usual orders, the basic properties of [le] and [lt]
 
174
    can be found in files Le and Lt *)
 
175
 
 
176
Inductive le (n:nat) : nat -> Prop :=
 
177
  | le_n : n <= n
 
178
  | le_S : forall m:nat, n <= m -> n <= S m
 
179
 
 
180
where "n <= m" := (le n m) : nat_scope.
 
181
 
 
182
Hint Constructors le: core.
 
183
(*i equivalent to : "Hints Resolve le_n le_S : core." i*)
 
184
 
 
185
Definition lt (n m:nat) := S n <= m.
 
186
Hint Unfold lt: core.
 
187
 
 
188
Infix "<" := lt : nat_scope.
 
189
 
 
190
Definition ge (n m:nat) := m <= n.
 
191
Hint Unfold ge: core.
 
192
 
 
193
Infix ">=" := ge : nat_scope.
 
194
 
 
195
Definition gt (n m:nat) := m < n.
 
196
Hint Unfold gt: core.
 
197
 
 
198
Infix ">" := gt : nat_scope.
 
199
 
 
200
Notation "x <= y <= z" := (x <= y /\ y <= z) : nat_scope.
 
201
Notation "x <= y < z" := (x <= y /\ y < z) : nat_scope.
 
202
Notation "x < y < z" := (x < y /\ y < z) : nat_scope.
 
203
Notation "x < y <= z" := (x < y /\ y <= z) : nat_scope.
 
204
 
 
205
(** Case analysis *)
 
206
 
 
207
Theorem nat_case :
 
208
 forall (n:nat) (P:nat -> Prop), P 0 -> (forall m:nat, P (S m)) -> P n.
 
209
Proof.
 
210
  induction n; auto.
 
211
Qed.
 
212
 
 
213
(** Principle of double induction *)
 
214
 
 
215
Theorem nat_double_ind :
 
216
 forall R:nat -> nat -> Prop,
 
217
   (forall n:nat, R 0 n) ->
 
218
   (forall n:nat, R (S n) 0) ->
 
219
   (forall n m:nat, R n m -> R (S n) (S m)) -> forall n m:nat, R n m.
 
220
Proof.
 
221
  induction n; auto.
 
222
  destruct m as [| n0]; auto.
 
223
Qed.