1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (*#***********************************************************************)
21 (* v * The Coq Proof Assistant / The Coq Development Team *)
23 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
25 (* \VV/ **************************************************************)
27 (* // * This file is distributed under the terms of the *)
29 (* * GNU Lesser General Public License Version 2.1 *)
31 (*#***********************************************************************)
33 (*i $Id: List.v,v 1.9.2.1 2004/07/16 19:31:05 herbelin Exp $ i*)
35 include "Arith/Le.ma".
42 cic:/Coq/Lists/List/Lists/A.var
46 Set Implicit Arguments.
49 inline procedural "cic:/Coq/Lists/List/list.ind".
52 Infix "::" := cons (at level 60, right associativity) : list_scope.
56 Open Scope list_scope.
59 (*#************************)
61 (*#* Discrimination *)
63 (*#************************)
65 inline procedural "cic:/Coq/Lists/List/nil_cons.con" as lemma.
67 (*#************************)
71 (*#************************)
73 inline procedural "cic:/Coq/Lists/List/app.con" as definition.
76 Infix "++" := app (right associativity, at level 60) : list_scope.
79 inline procedural "cic:/Coq/Lists/List/app_nil_end.con" as lemma.
82 Hint Resolve app_nil_end.
86 Ltac now_show c := change c in |- *.
89 inline procedural "cic:/Coq/Lists/List/app_ass.con" as lemma.
95 inline procedural "cic:/Coq/Lists/List/ass_app.con" as lemma.
101 inline procedural "cic:/Coq/Lists/List/app_comm_cons.con" as lemma.
103 inline procedural "cic:/Coq/Lists/List/app_eq_nil.con" as lemma.
105 inline procedural "cic:/Coq/Lists/List/app_cons_not_nil.con" as lemma.
107 inline procedural "cic:/Coq/Lists/List/app_eq_unit.con" as lemma.
109 inline procedural "cic:/Coq/Lists/List/app_inj_tail.con" as lemma.
111 (*#************************)
113 (*#* Head and tail *)
115 (*#************************)
117 inline procedural "cic:/Coq/Lists/List/head.con" as definition.
119 inline procedural "cic:/Coq/Lists/List/tail.con" as definition.
121 (*#***************************************)
123 (*#* Length of lists *)
125 (*#***************************************)
127 inline procedural "cic:/Coq/Lists/List/length.con" as definition.
129 (*#*****************************)
131 (*#* Length order of lists *)
133 (*#*****************************)
139 inline procedural "cic:/Coq/Lists/List/lel.con" as definition.
142 cic:/Coq/Lists/List/Lists/length_order/a.var
146 cic:/Coq/Lists/List/Lists/length_order/b.var
150 cic:/Coq/Lists/List/Lists/length_order/l.var
154 cic:/Coq/Lists/List/Lists/length_order/m.var
158 cic:/Coq/Lists/List/Lists/length_order/n.var
161 inline procedural "cic:/Coq/Lists/List/lel_refl.con" as lemma.
163 inline procedural "cic:/Coq/Lists/List/lel_trans.con" as lemma.
165 inline procedural "cic:/Coq/Lists/List/lel_cons_cons.con" as lemma.
167 inline procedural "cic:/Coq/Lists/List/lel_cons.con" as lemma.
169 inline procedural "cic:/Coq/Lists/List/lel_tail.con" as lemma.
171 inline procedural "cic:/Coq/Lists/List/lel_nil.con" as lemma.
178 Hint Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons.
181 (*#********************************)
183 (*#* The [In] predicate *)
185 (*#********************************)
187 inline procedural "cic:/Coq/Lists/List/In.con" as definition.
189 inline procedural "cic:/Coq/Lists/List/in_eq.con" as lemma.
195 inline procedural "cic:/Coq/Lists/List/in_cons.con" as lemma.
198 Hint Resolve in_cons.
201 inline procedural "cic:/Coq/Lists/List/in_nil.con" as lemma.
203 inline procedural "cic:/Coq/Lists/List/in_inv.con" as lemma.
205 inline procedural "cic:/Coq/Lists/List/In_dec.con" as lemma.
207 inline procedural "cic:/Coq/Lists/List/in_app_or.con" as lemma.
210 Hint Immediate in_app_or.
213 inline procedural "cic:/Coq/Lists/List/in_or_app.con" as lemma.
216 Hint Resolve in_or_app.
219 (*#**************************)
221 (*#* Set inclusion on list *)
223 (*#**************************)
225 inline procedural "cic:/Coq/Lists/List/incl.con" as definition.
231 inline procedural "cic:/Coq/Lists/List/incl_refl.con" as lemma.
234 Hint Resolve incl_refl.
237 inline procedural "cic:/Coq/Lists/List/incl_tl.con" as lemma.
240 Hint Immediate incl_tl.
243 inline procedural "cic:/Coq/Lists/List/incl_tran.con" as lemma.
245 inline procedural "cic:/Coq/Lists/List/incl_appl.con" as lemma.
248 Hint Immediate incl_appl.
251 inline procedural "cic:/Coq/Lists/List/incl_appr.con" as lemma.
254 Hint Immediate incl_appr.
257 inline procedural "cic:/Coq/Lists/List/incl_cons.con" as lemma.
260 Hint Resolve incl_cons.
263 inline procedural "cic:/Coq/Lists/List/incl_app.con" as lemma.
266 Hint Resolve incl_app.
269 (*#*************************)
271 (*#* Nth element of a list *)
273 (*#*************************)
275 inline procedural "cic:/Coq/Lists/List/nth.con" as definition.
277 inline procedural "cic:/Coq/Lists/List/nth_ok.con" as definition.
279 inline procedural "cic:/Coq/Lists/List/nth_in_or_default.con" as lemma.
281 inline procedural "cic:/Coq/Lists/List/nth_S_cons.con" as lemma.
283 inline procedural "cic:/Coq/Lists/List/nth_error.con" as definition.
285 inline procedural "cic:/Coq/Lists/List/nth_default.con" as definition.
287 inline procedural "cic:/Coq/Lists/List/nth_In.con" as lemma.
289 (*#*******************************)
291 (*#* Decidable equality on lists *)
293 (*#*******************************)
295 inline procedural "cic:/Coq/Lists/List/list_eq_dec.con" as lemma.
297 (*#************************)
301 (*#************************)
303 inline procedural "cic:/Coq/Lists/List/rev.con" as definition.
305 inline procedural "cic:/Coq/Lists/List/distr_rev.con" as lemma.
307 inline procedural "cic:/Coq/Lists/List/rev_unit.con" as remark.
309 inline procedural "cic:/Coq/Lists/List/rev_involutive.con" as lemma.
311 (*#********************************************)
313 (*#* Reverse Induction Principle on Lists *)
315 (*#********************************************)
318 Section Reverse_Induction
322 Unset Implicit Arguments.
325 inline procedural "cic:/Coq/Lists/List/rev_list_ind.con" as remark.
328 Set Implicit Arguments.
331 inline procedural "cic:/Coq/Lists/List/rev_ind.con" as lemma.
334 End Reverse_Induction
342 Implicit Arguments nil [A].
346 Hint Resolve nil_cons app_nil_end ass_app app_ass: datatypes v62.
350 Hint Resolve app_comm_cons app_cons_not_nil: datatypes v62.
354 Hint Immediate app_eq_nil: datatypes v62.
358 Hint Resolve app_eq_unit app_inj_tail: datatypes v62.
362 Hint Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons:
367 Hint Resolve in_eq in_cons in_inv in_nil in_app_or in_or_app: datatypes v62.
371 Hint Resolve incl_refl incl_tl incl_tran incl_appl incl_appr incl_cons
372 incl_app: datatypes v62.
376 Section Functions_on_lists
379 (*#***************************************************************)
381 (*#* Some generic functions on lists and basic functions of them *)
383 (*#***************************************************************)
390 cic:/Coq/Lists/List/Functions_on_lists/Map/A.var
394 cic:/Coq/Lists/List/Functions_on_lists/Map/B.var
398 cic:/Coq/Lists/List/Functions_on_lists/Map/f.var
401 inline procedural "cic:/Coq/Lists/List/map.con" as definition.
407 inline procedural "cic:/Coq/Lists/List/in_map.con" as lemma.
409 inline procedural "cic:/Coq/Lists/List/flat_map.con" as definition.
411 inline procedural "cic:/Coq/Lists/List/list_prod.con" as definition.
413 inline procedural "cic:/Coq/Lists/List/in_prod_aux.con" as lemma.
415 inline procedural "cic:/Coq/Lists/List/in_prod.con" as lemma.
417 (*#* [(list_power x y)] is [y^x], or the set of sequences of elts of [y]
418 indexed by elts of [x], sorted in lexicographic order. *)
420 inline procedural "cic:/Coq/Lists/List/list_power.con" as definition.
422 (*#***********************************)
424 (*#* Left-to-right iterator on lists *)
426 (*#***********************************)
429 Section Fold_Left_Recursor
433 cic:/Coq/Lists/List/Functions_on_lists/Fold_Left_Recursor/A.var
437 cic:/Coq/Lists/List/Functions_on_lists/Fold_Left_Recursor/B.var
441 cic:/Coq/Lists/List/Functions_on_lists/Fold_Left_Recursor/f.var
444 inline procedural "cic:/Coq/Lists/List/fold_left.con" as definition.
447 End Fold_Left_Recursor
450 (*#***********************************)
452 (*#* Right-to-left iterator on lists *)
454 (*#***********************************)
457 Section Fold_Right_Recursor
461 cic:/Coq/Lists/List/Functions_on_lists/Fold_Right_Recursor/A.var
465 cic:/Coq/Lists/List/Functions_on_lists/Fold_Right_Recursor/B.var
469 cic:/Coq/Lists/List/Functions_on_lists/Fold_Right_Recursor/f.var
473 cic:/Coq/Lists/List/Functions_on_lists/Fold_Right_Recursor/a0.var
476 inline procedural "cic:/Coq/Lists/List/fold_right.con" as definition.
479 End Fold_Right_Recursor
482 inline procedural "cic:/Coq/Lists/List/fold_symmetric.con" as theorem.
485 End Functions_on_lists
488 (*#* Exporting list notations *)
491 Infix "::" := cons (at level 60, right associativity) : list_scope.
495 Infix "++" := app (right associativity, at level 60) : list_scope.
499 Open Scope list_scope.
502 (*#* Declare Scope list_scope with key list *)
505 Delimit Scope list_scope with list.
509 Bind Scope list_scope with list.