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/lib/list.ma".
16 include "ground/arith/nat_succ.ma".
18 (* LENGTH FOR LISTS *********************************************************)
20 rec definition list_length A (l:list A) on l ≝
23 | list_cons _ l ⇒ ↑(list_length A l)
28 'card l = (list_length ? l).
30 (* Basic constructions ******************************************************)
32 lemma list_length_nil (A:Type[0]): |list_nil A| = 𝟎.
35 lemma list_length_cons (A:Type[0]) (l:list A) (a:A): |a⨮l| = ↑|l|.
38 (* Basic inversions *********************************************************)
40 lemma list_length_inv_zero_dx (A:Type[0]) (l:list A):
42 #A * // #a #l >list_length_cons #H
43 elim (eq_inv_nsucc_zero … H)
46 lemma list_length_inv_zero_sn (A:Type[0]) (l:list A):
48 /2 width=1 by list_length_inv_zero_dx/ qed-.
50 lemma list_length_inv_succ_dx (A:Type[0]) (l:list A) (x):
52 ∃∃tl,a. x = |tl| & l = a ⨮ tl.
54 [ #x >list_length_nil #H
55 elim (eq_inv_zero_nsucc … H)
56 | #a #l #x >list_length_cons #H
57 /3 width=4 by eq_inv_nsucc_bi, ex2_2_intro/
61 lemma list_length_inv_succ_sn (A:Type[0]) (l:list A) (x):
63 ∃∃tl,a. x = |tl| & l = a ⨮ tl.
64 /2 width=1 by list_length_inv_succ_dx/ qed-.