← Back to branch summary

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

« back to all changes in this revision

Viewing changes to theories/Lists/MonoList.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/Lists/MonoList.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: MonoList.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
10
 
 
11
(** THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED ***)
 
12
 
 
13
Require Import Le.
 
14
 
 
15
Parameter List_Dom : Set.
 
16
Definition A := List_Dom.
 
17
 
 
18
Inductive list : Set :=
 
19
  | nil : list
 
20
  | cons : A -> list -> list.
 
21
 
 
22
Fixpoint app (l m:list) {struct l} : list :=
 
23
  match l return list with
 
24
  | nil => m
 
25
  | cons a l1 => cons a (app l1 m)
 
26
  end.
 
27
 
 
28
 
 
29
Lemma app_nil_end : forall l:list, l = app l nil.
 
30
Proof. 
 
31
        intro l; elim l; simpl in |- *; auto.
 
32
        simple induction 1; auto.
 
33
Qed.
 
34
Hint Resolve app_nil_end: list v62.
 
35
 
 
36
Lemma app_ass : forall l m n:list, app (app l m) n = app l (app m n).
 
37
Proof. 
 
38
        intros l m n; elim l; simpl in |- *; auto with list.
 
39
        simple induction 1; auto with list.
 
40
Qed.
 
41
Hint Resolve app_ass: list v62.
 
42
 
 
43
Lemma ass_app : forall l m n:list, app l (app m n) = app (app l m) n.
 
44
Proof. 
 
45
        auto with list.
 
46
Qed.
 
47
Hint Resolve ass_app: list v62.
 
48
 
 
49
Definition tail (l:list) : list :=
 
50
  match l return list with
 
51
  | cons _ m => m
 
52
  | _ => nil
 
53
  end.
 
54
                   
 
55
 
 
56
Lemma nil_cons : forall (a:A) (m:list), nil <> cons a m.
 
57
  intros; discriminate.
 
58
Qed.
 
59
 
 
60
(****************************************)
 
61
(* Length of lists                      *)
 
62
(****************************************)
 
63
 
 
64
Fixpoint length (l:list) : nat :=
 
65
  match l return nat with
 
66
  | cons _ m => S (length m)
 
67
  | _ => 0
 
68
  end.
 
69
 
 
70
(******************************)
 
71
(* Length order of lists      *)
 
72
(******************************)
 
73
 
 
74
Section length_order.
 
75
Definition lel (l m:list) := length l <= length m.
 
76
 
 
77
Hint Unfold lel: list.
 
78
 
 
79
Variables a b : A.
 
80
Variables l m n : list.
 
81
 
 
82
Lemma lel_refl : lel l l.
 
83
Proof. 
 
84
        unfold lel in |- *; auto with list.
 
85
Qed.
 
86
 
 
87
Lemma lel_trans : lel l m -> lel m n -> lel l n.
 
88
Proof. 
 
89
        unfold lel in |- *; intros.
 
90
        apply le_trans with (length m); auto with list.
 
91
Qed.
 
92
 
 
93
Lemma lel_cons_cons : lel l m -> lel (cons a l) (cons b m).
 
94
Proof. 
 
95
        unfold lel in |- *; simpl in |- *; auto with list arith.
 
96
Qed.
 
97
 
 
98
Lemma lel_cons : lel l m -> lel l (cons b m).
 
99
Proof. 
 
100
        unfold lel in |- *; simpl in |- *; auto with list arith.
 
101
Qed.
 
102
 
 
103
Lemma lel_tail : lel (cons a l) (cons b m) -> lel l m.
 
104
Proof. 
 
105
        unfold lel in |- *; simpl in |- *; auto with list arith.
 
106
Qed.
 
107
 
 
108
Lemma lel_nil : forall l':list, lel l' nil -> nil = l'.
 
109
Proof. 
 
110
        intro l'; elim l'; auto with list arith.
 
111
        intros a' y H H0.
 
112
        (*  <list>nil=(cons a' y)
 
113
            ============================
 
114
              H0 : (lel (cons a' y) nil)
 
115
              H : (lel y nil)->(<list>nil=y)
 
116
              y : list
 
117
              a' : A
 
118
              l' : list *)
 
119
        absurd (S (length y) <= 0); auto with list arith.
 
120
Qed.
 
121
End length_order.
 
122
 
 
123
Hint Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons: list
 
124
  v62.
 
125
 
 
126
Fixpoint In (a:A) (l:list) {struct l} : Prop :=
 
127
  match l with
 
128
  | nil => False
 
129
  | cons b m => b = a \/ In a m
 
130
  end.
 
131
 
 
132
Lemma in_eq : forall (a:A) (l:list), In a (cons a l).
 
133
Proof. 
 
134
        simpl in |- *; auto with list.
 
135
Qed.
 
136
Hint Resolve in_eq: list v62.
 
137
 
 
138
Lemma in_cons : forall (a b:A) (l:list), In b l -> In b (cons a l).
 
139
Proof. 
 
140
        simpl in |- *; auto with list.
 
141
Qed.
 
142
Hint Resolve in_cons: list v62.
 
143
 
 
144
Lemma in_app_or : forall (l m:list) (a:A), In a (app l m) -> In a l \/ In a m.
 
145
Proof. 
 
146
        intros l m a.
 
147
        elim l; simpl in |- *; auto with list.
 
148
        intros a0 y H H0.
 
149
        (*  ((<A>a0=a)\/(In a y))\/(In a m)
 
150
            ============================
 
151
              H0 : (<A>a0=a)\/(In a (app y m))
 
152
              H : (In a (app y m))->((In a y)\/(In a m))
 
153
              y : list
 
154
              a0 : A
 
155
              a : A
 
156
              m : list
 
157
              l : list *)
 
158
        elim H0; auto with list.
 
159
        intro H1.
 
160
        (*  ((<A>a0=a)\/(In a y))\/(In a m)
 
161
            ============================
 
162
              H1 : (In a (app y m)) *)
 
163
        elim (H H1); auto with list.
 
164
Qed.
 
165
Hint Immediate in_app_or: list v62.
 
166
 
 
167
Lemma in_or_app : forall (l m:list) (a:A), In a l \/ In a m -> In a (app l m).
 
168
Proof. 
 
169
        intros l m a.
 
170
        elim l; simpl in |- *; intro H.
 
171
        (* 1 (In a m)
 
172
            ============================
 
173
              H : False\/(In a m)
 
174
              a : A
 
175
              m : list
 
176
              l : list *)
 
177
        elim H; auto with list; intro H0.
 
178
        (*  (In a m)
 
179
            ============================
 
180
              H0 : False *)
 
181
        elim H0. (* subProof completed *)
 
182
        intros y H0 H1.
 
183
        (*  2 (<A>H=a)\/(In a (app y m))
 
184
            ============================
 
185
              H1 : ((<A>H=a)\/(In a y))\/(In a m)
 
186
              H0 : ((In a y)\/(In a m))->(In a (app y m))
 
187
              y : list *)
 
188
        elim H1; auto 4 with list.
 
189
        intro H2.
 
190
        (*  (<A>H=a)\/(In a (app y m))
 
191
            ============================
 
192
              H2 : (<A>H=a)\/(In a y) *)
 
193
        elim H2; auto with list.
 
194
Qed.
 
195
Hint Resolve in_or_app: list v62.
 
196
 
 
197
Definition incl (l m:list) := forall a:A, In a l -> In a m.
 
198
 
 
199
Hint Unfold incl: list v62.
 
200
 
 
201
Lemma incl_refl : forall l:list, incl l l.
 
202
Proof. 
 
203
        auto with list.
 
204
Qed.
 
205
Hint Resolve incl_refl: list v62.
 
206
 
 
207
Lemma incl_tl : forall (a:A) (l m:list), incl l m -> incl l (cons a m).
 
208
Proof. 
 
209
        auto with list.
 
210
Qed.
 
211
Hint Immediate incl_tl: list v62.
 
212
 
 
213
Lemma incl_tran : forall l m n:list, incl l m -> incl m n -> incl l n.
 
214
Proof. 
 
215
        auto with list.
 
216
Qed.
 
217
 
 
218
Lemma incl_appl : forall l m n:list, incl l n -> incl l (app n m).
 
219
Proof. 
 
220
        auto with list.
 
221
Qed.
 
222
Hint Immediate incl_appl: list v62.
 
223
 
 
224
Lemma incl_appr : forall l m n:list, incl l n -> incl l (app m n).
 
225
Proof. 
 
226
        auto with list.
 
227
Qed.
 
228
Hint Immediate incl_appr: list v62.
 
229
 
 
230
Lemma incl_cons :
 
231
 forall (a:A) (l m:list), In a m -> incl l m -> incl (cons a l) m.
 
232
Proof. 
 
233
        unfold incl in |- *; simpl in |- *; intros a l m H H0 a0 H1.
 
234
        (*  (In a0 m)
 
235
            ============================
 
236
              H1 : (<A>a=a0)\/(In a0 l)
 
237
              a0 : A
 
238
              H0 : (a:A)(In a l)->(In a m)
 
239
              H : (In a m)
 
240
              m : list
 
241
              l : list
 
242
              a : A *)
 
243
        elim H1.
 
244
        (*  1 (<A>a=a0)->(In a0 m) *)
 
245
        elim H1; auto with list; intro H2.
 
246
        (*  (<A>a=a0)->(In a0 m)
 
247
            ============================
 
248
              H2 : <A>a=a0 *)
 
249
        elim H2; auto with list. (* solves subgoal *)
 
250
        (*  2 (In a0 l)->(In a0 m) *)
 
251
        auto with list.
 
252
Qed.
 
253
Hint Resolve incl_cons: list v62.
 
254
 
 
255
Lemma incl_app : forall l m n:list, incl l n -> incl m n -> incl (app l m) n.
 
256
Proof. 
 
257
        unfold incl in |- *; simpl in |- *; intros l m n H H0 a H1.
 
258
        (*  (In a n)
 
259
            ============================
 
260
              H1 : (In a (app l m))
 
261
              a : A
 
262
              H0 : (a:A)(In a m)->(In a n)
 
263
              H : (a:A)(In a l)->(In a n)
 
264
              n : list
 
265
              m : list
 
266
              l : list *)
 
267
        elim (in_app_or l m a); auto with list.
 
268
Qed.
 
269
Hint Resolve incl_app: list v62.
 
 
b'\\ No newline at end of file'