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 include "ground/notation/functions/verticalbars_1.ma".
16 include "ground/lib/list.ma".
17 include "ground/arith/nat_succ.ma".
19 (* LENGTH FOR LISTS *********************************************************)
21 rec definition list_length A (l:list A) on l โ match l with
23 | list_lcons _ l โ โ(list_length A l)
28 'VerticalBars l = (list_length ? l).
30 (* Basic constructions ******************************************************)
32 lemma list_length_empty (A:Type[0]):
33 โlist_empty Aโ = ๐.
36 lemma list_length_lcons (A:Type[0]) (l:list A) (a:A):
37 โaโจฎlโ = โโlโ.
40 (* Basic inversions *********************************************************)
42 lemma list_length_inv_zero_dx (A:Type[0]) (l:list A):
43 โlโ = ๐ โ l = โ.
44 #A * // #a #l >list_length_lcons #H
45 elim (eq_inv_nsucc_zero โฆ H)
48 lemma list_length_inv_zero_sn (A:Type[0]) (l:list A):
49 (๐) = โlโ โ l = โ.
50 /2 width=1 by list_length_inv_zero_dx/ qed-.
52 lemma list_length_inv_succ_dx (A:Type[0]) (l:list A) (x):
54 โโtl,a. x = โtlโ & l = a โจฎ tl.
56 [ #x >list_length_empty #H
57 elim (eq_inv_zero_nsucc โฆ H)
58 | #a #l #x >list_length_lcons #H
59 /3 width=4 by eq_inv_nsucc_bi, ex2_2_intro/
63 lemma list_length_inv_succ_sn (A:Type[0]) (l:list A) (x):
65 โโtl,a. x = โtlโ & l = a โจฎ tl.
66 /2 width=1 by list_length_inv_succ_dx/ qed-.