← Back to branch summary

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

« back to all changes in this revision

Viewing changes to theories/Arith/Plus.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/Arith/Plus.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: Plus.v 9750 2007-04-06 00:58:14Z letouzey $ i*)
 
10
 
 
11
(** Properties of addition. [add] is defined in [Init/Peano.v] as:
 
12
<<
 
13
Fixpoint plus (n m:nat) {struct n} : nat :=
 
14
  match n with
 
15
  | O => m
 
16
  | S p => S (p + m)
 
17
  end
 
18
where "n + m" := (plus n m) : nat_scope.
 
19
>>
 
20
 *)
 
21
 
 
22
Require Import Le.
 
23
Require Import Lt.
 
24
 
 
25
Open Local Scope nat_scope.
 
26
 
 
27
Implicit Types m n p q : nat.
 
28
 
 
29
(** * Zero is neutral *)
 
30
 
 
31
Lemma plus_0_l : forall n, 0 + n = n.
 
32
Proof.
 
33
  reflexivity.
 
34
Qed.
 
35
 
 
36
Lemma plus_0_r : forall n, n + 0 = n.
 
37
Proof.
 
38
  intro; symmetry  in |- *; apply plus_n_O.
 
39
Qed.
 
40
 
 
41
(** * Commutativity *)
 
42
 
 
43
Lemma plus_comm : forall n m, n + m = m + n.
 
44
Proof.
 
45
  intros n m; elim n; simpl in |- *; auto with arith.
 
46
  intros y H; elim (plus_n_Sm m y); auto with arith.
 
47
Qed.
 
48
Hint Immediate plus_comm: arith v62.
 
49
 
 
50
(** * Associativity *)
 
51
 
 
52
Lemma plus_Snm_nSm : forall n m, S n + m = n + S m.
 
53
Proof.
 
54
  intros.
 
55
  simpl in |- *.
 
56
  rewrite (plus_comm n m).
 
57
  rewrite (plus_comm n (S m)).
 
58
  trivial with arith.
 
59
Qed.
 
60
 
 
61
Lemma plus_assoc : forall n m p, n + (m + p) = n + m + p.
 
62
Proof.
 
63
  intros n m p; elim n; simpl in |- *; auto with arith.
 
64
Qed.
 
65
Hint Resolve plus_assoc: arith v62.
 
66
 
 
67
Lemma plus_permute : forall n m p, n + (m + p) = m + (n + p).
 
68
Proof. 
 
69
  intros; rewrite (plus_assoc m n p); rewrite (plus_comm m n); auto with arith.
 
70
Qed.
 
71
 
 
72
Lemma plus_assoc_reverse : forall n m p, n + m + p = n + (m + p).
 
73
Proof.
 
74
  auto with arith.
 
75
Qed.
 
76
Hint Resolve plus_assoc_reverse: arith v62.
 
77
 
 
78
(** * Simplification *)
 
79
 
 
80
Lemma plus_reg_l : forall n m p, p + n = p + m -> n = m.
 
81
Proof.
 
82
  intros m p n; induction n; simpl in |- *; auto with arith.
 
83
Qed.
 
84
 
 
85
Lemma plus_le_reg_l : forall n m p, p + n <= p + m -> n <= m.
 
86
Proof.
 
87
  induction p; simpl in |- *; auto with arith.
 
88
Qed.
 
89
 
 
90
Lemma plus_lt_reg_l : forall n m p, p + n < p + m -> n < m.
 
91
Proof.
 
92
  induction p; simpl in |- *; auto with arith.
 
93
Qed.
 
94
 
 
95
(** * Compatibility with order *)
 
96
 
 
97
Lemma plus_le_compat_l : forall n m p, n <= m -> p + n <= p + m.
 
98
Proof.
 
99
  induction p; simpl in |- *; auto with arith.
 
100
Qed.
 
101
Hint Resolve plus_le_compat_l: arith v62.
 
102
 
 
103
Lemma plus_le_compat_r : forall n m p, n <= m -> n + p <= m + p.
 
104
Proof.
 
105
  induction 1; simpl in |- *; auto with arith.
 
106
Qed.
 
107
Hint Resolve plus_le_compat_r: arith v62.
 
108
 
 
109
Lemma le_plus_l : forall n m, n <= n + m.
 
110
Proof.
 
111
  induction n; simpl in |- *; auto with arith.
 
112
Qed.
 
113
Hint Resolve le_plus_l: arith v62.
 
114
 
 
115
Lemma le_plus_r : forall n m, m <= n + m.
 
116
Proof.
 
117
  intros n m; elim n; simpl in |- *; auto with arith.
 
118
Qed.
 
119
Hint Resolve le_plus_r: arith v62.
 
120
 
 
121
Theorem le_plus_trans : forall n m p, n <= m -> n <= m + p.
 
122
Proof.
 
123
  intros; apply le_trans with (m := m); auto with arith.
 
124
Qed.
 
125
Hint Resolve le_plus_trans: arith v62.
 
126
 
 
127
Theorem lt_plus_trans : forall n m p, n < m -> n < m + p.
 
128
Proof.
 
129
  intros; apply lt_le_trans with (m := m); auto with arith.
 
130
Qed.
 
131
Hint Immediate lt_plus_trans: arith v62.
 
132
 
 
133
Lemma plus_lt_compat_l : forall n m p, n < m -> p + n < p + m.
 
134
Proof.
 
135
  induction p; simpl in |- *; auto with arith.
 
136
Qed.
 
137
Hint Resolve plus_lt_compat_l: arith v62.
 
138
 
 
139
Lemma plus_lt_compat_r : forall n m p, n < m -> n + p < m + p.
 
140
Proof.
 
141
  intros n m p H; rewrite (plus_comm n p); rewrite (plus_comm m p).
 
142
  elim p; auto with arith.
 
143
Qed.
 
144
Hint Resolve plus_lt_compat_r: arith v62.
 
145
 
 
146
Lemma plus_le_compat : forall n m p q, n <= m -> p <= q -> n + p <= m + q.
 
147
Proof.
 
148
  intros n m p q H H0.
 
149
  elim H; simpl in |- *; auto with arith.
 
150
Qed.
 
151
 
 
152
Lemma plus_le_lt_compat : forall n m p q, n <= m -> p < q -> n + p < m + q.
 
153
Proof.
 
154
  unfold lt in |- *. intros. change (S n + p <= m + q) in |- *. rewrite plus_Snm_nSm.
 
155
  apply plus_le_compat; assumption.
 
156
Qed.
 
157
 
 
158
Lemma plus_lt_le_compat : forall n m p q, n < m -> p <= q -> n + p < m + q.
 
159
Proof.
 
160
  unfold lt in |- *. intros. change (S n + p <= m + q) in |- *. apply plus_le_compat; assumption.
 
161
Qed.
 
162
 
 
163
Lemma plus_lt_compat : forall n m p q, n < m -> p < q -> n + p < m + q.
 
164
Proof.
 
165
  intros. apply plus_lt_le_compat. assumption.
 
166
  apply lt_le_weak. assumption.
 
167
Qed.
 
168
 
 
169
(** * Inversion lemmas *)
 
170
 
 
171
Lemma plus_is_O : forall n m, n + m = 0 -> n = 0 /\ m = 0.
 
172
Proof.
 
173
  intro m; destruct m as [| n]; auto.
 
174
  intros. discriminate H.
 
175
Qed.
 
176
 
 
177
Definition plus_is_one :
 
178
  forall m n, m + n = 1 -> {m = 0 /\ n = 1} + {m = 1 /\ n = 0}.
 
179
Proof.
 
180
  intro m; destruct m as [| n]; auto.
 
181
  destruct n; auto.
 
182
  intros. 
 
183
  simpl in H. discriminate H.
 
184
Defined.
 
185
 
 
186
(** * Derived properties *)
 
187
 
 
188
Lemma plus_permute_2_in_4 : forall n m p q, n + m + (p + q) = n + p + (m + q).
 
189
Proof.
 
190
  intros m n p q. 
 
191
  rewrite <- (plus_assoc m n (p + q)). rewrite (plus_assoc n p q).
 
192
  rewrite (plus_comm n p). rewrite <- (plus_assoc p n q). apply plus_assoc.
 
193
Qed.
 
194
 
 
195
(** * Tail-recursive plus *)
 
196
 
 
197
(** [tail_plus] is an alternative definition for [plus] which is 
 
198
    tail-recursive, whereas [plus] is not. This can be useful
 
199
    when extracting programs. *)
 
200
 
 
201
Fixpoint tail_plus n m {struct n} : nat :=
 
202
  match n with
 
203
    | O => m
 
204
    | S n => tail_plus n (S m)
 
205
  end.
 
206
 
 
207
Lemma plus_tail_plus : forall n m, n + m = tail_plus n m.
 
208
induction n as [| n IHn]; simpl in |- *; auto.
 
209
intro m; rewrite <- IHn; simpl in |- *; auto.
 
210
Qed.
 
211
 
 
212
(** * Discrimination *)
 
213
 
 
214
Lemma succ_plus_discr : forall n m, n <> S (plus m n).
 
215
Proof.
 
216
  intros n m; induction n as [|n IHn].
 
217
  discriminate.
 
218
  intro H; apply IHn; apply eq_add_S; rewrite H; rewrite <- plus_n_Sm; 
 
219
    reflexivity.
 
220
Qed.
 
221
 
 
222
Lemma n_SSn : forall n, n <> S (S n).
 
223
Proof.
 
224
  intro n; exact (succ_plus_discr n 1).
 
225
Qed.
 
226
 
 
227
Lemma n_SSSn : forall n, n <> S (S (S n)).
 
228
Proof.
 
229
  intro n; exact (succ_plus_discr n 2).
 
230
Qed.
 
231
 
 
232
Lemma n_SSSSn : forall n, n <> S (S (S (S n))).
 
233
Proof.
 
234
  intro n; exact (succ_plus_discr n 3).
 
235
Qed.