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: TheoryList.v,v 1.15.2.1 2004/07/16 19:31:06 herbelin Exp $ i*)
35 (*#* Some programs and results about lists following CAML Manual *)
37 include "Lists/List.ma".
40 Set Implicit Arguments.
48 cic:/Coq/Lists/TheoryList/Lists/A.var
51 (*#*********************)
53 (*#* The null function *)
55 (*#*********************)
57 inline procedural "cic:/Coq/Lists/TheoryList/Isnil.con" as definition.
59 inline procedural "cic:/Coq/Lists/TheoryList/Isnil_nil.con" as lemma.
62 Hint Resolve Isnil_nil.
65 inline procedural "cic:/Coq/Lists/TheoryList/not_Isnil_cons.con" as lemma.
68 Hint Resolve Isnil_nil not_Isnil_cons.
71 inline procedural "cic:/Coq/Lists/TheoryList/Isnil_dec.con" as lemma.
73 (*#***********************)
75 (*#* The Uncons function *)
77 (*#***********************)
79 inline procedural "cic:/Coq/Lists/TheoryList/Uncons.con" as lemma.
81 (*#*******************************)
83 (*#* The head function *)
85 (*#*******************************)
87 inline procedural "cic:/Coq/Lists/TheoryList/Hd.con" as lemma.
89 inline procedural "cic:/Coq/Lists/TheoryList/Tl.con" as lemma.
91 (*#***************************************)
93 (*#* Length of lists *)
95 (*#***************************************)
97 (* length is defined in List *)
99 inline procedural "cic:/Coq/Lists/TheoryList/Length_l.con" as definition.
101 (* A tail recursive version *)
103 inline procedural "cic:/Coq/Lists/TheoryList/Length_l_pf.con" as lemma.
105 inline procedural "cic:/Coq/Lists/TheoryList/Length.con" as lemma.
107 (*#******************************)
109 (*#* Members of lists *)
111 (*#******************************)
113 inline procedural "cic:/Coq/Lists/TheoryList/In_spec.ind".
116 Hint Resolve in_hd in_tl.
124 Hint Resolve in_cons.
127 inline procedural "cic:/Coq/Lists/TheoryList/In_In_spec.con" as theorem.
129 inline procedural "cic:/Coq/Lists/TheoryList/AllS.ind".
132 Hint Resolve allS_nil allS_cons.
136 cic:/Coq/Lists/TheoryList/Lists/eqA_dec.var
139 inline procedural "cic:/Coq/Lists/TheoryList/mem.con" as definition.
145 inline procedural "cic:/Coq/Lists/TheoryList/Mem.con" as lemma.
147 (*#********************************)
149 (*#* Index of elements *)
151 (*#********************************)
153 include "Arith/Le.ma".
155 include "Arith/Lt.ma".
157 inline procedural "cic:/Coq/Lists/TheoryList/nth_spec.ind".
160 Hint Resolve nth_spec_O nth_spec_S.
163 inline procedural "cic:/Coq/Lists/TheoryList/fst_nth_spec.ind".
166 Hint Resolve fst_nth_O fst_nth_S.
169 inline procedural "cic:/Coq/Lists/TheoryList/fst_nth_nth.con" as lemma.
172 Hint Immediate fst_nth_nth.
175 inline procedural "cic:/Coq/Lists/TheoryList/nth_lt_O.con" as lemma.
177 inline procedural "cic:/Coq/Lists/TheoryList/nth_le_length.con" as lemma.
179 inline procedural "cic:/Coq/Lists/TheoryList/Nth_func.con" as definition.
181 inline procedural "cic:/Coq/Lists/TheoryList/Nth.con" as lemma.
183 inline procedural "cic:/Coq/Lists/TheoryList/Item.con" as lemma.
185 include "Arith/Minus.ma".
187 include "Bool/DecBool.ma".
189 inline procedural "cic:/Coq/Lists/TheoryList/index_p.con" as definition.
191 inline procedural "cic:/Coq/Lists/TheoryList/Index_p.con" as lemma.
193 inline procedural "cic:/Coq/Lists/TheoryList/Index.con" as lemma.
200 cic:/Coq/Lists/TheoryList/Lists/Find_sec/R.var
204 cic:/Coq/Lists/TheoryList/Lists/Find_sec/P.var
207 inline procedural "cic:/Coq/Lists/TheoryList/InR.ind".
210 Hint Resolve inR_hd inR_tl.
213 inline procedural "cic:/Coq/Lists/TheoryList/InR_inv.con" as definition.
215 inline procedural "cic:/Coq/Lists/TheoryList/InR_INV.con" as lemma.
217 inline procedural "cic:/Coq/Lists/TheoryList/InR_cons_inv.con" as lemma.
219 inline procedural "cic:/Coq/Lists/TheoryList/InR_or_app.con" as lemma.
221 inline procedural "cic:/Coq/Lists/TheoryList/InR_app_or.con" as lemma.
224 cic:/Coq/Lists/TheoryList/Lists/Find_sec/RS_dec.var
227 inline procedural "cic:/Coq/Lists/TheoryList/find.con" as definition.
229 inline procedural "cic:/Coq/Lists/TheoryList/Find.con" as lemma.
232 cic:/Coq/Lists/TheoryList/Lists/Find_sec/B.var
236 cic:/Coq/Lists/TheoryList/Lists/Find_sec/T.var
240 cic:/Coq/Lists/TheoryList/Lists/Find_sec/TS_dec.var
243 inline procedural "cic:/Coq/Lists/TheoryList/try_find.con" as definition.
245 inline procedural "cic:/Coq/Lists/TheoryList/Try_find.con" as lemma.
256 cic:/Coq/Lists/TheoryList/Lists/Assoc_sec/B.var
259 inline procedural "cic:/Coq/Lists/TheoryList/assoc.con" as definition.
261 inline procedural "cic:/Coq/Lists/TheoryList/AllS_assoc.ind".
264 Hint Resolve allS_assoc_nil allS_assoc_cons.
267 (* The specification seems too weak: it is enough to return b if the
268 list has at least an element (a,b); probably the intention is to have
271 (a:A)(l:(list A*B)){b:B|(In_spec (a,b) l)}+{(AllS_assoc [a':A]~(a=a') l)}.
274 inline procedural "cic:/Coq/Lists/TheoryList/Assoc.con" as lemma.
285 Hint Resolve Isnil_nil not_Isnil_cons in_hd in_tl in_cons allS_nil allS_cons:
290 Hint Immediate fst_nth_nth: datatypes.