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 ≝ match l with
22 | list_lcons _ l ⇒ ↑(list_length A l)
27 'card l = (list_length ? l).
29 (* Basic constructions ******************************************************)
31 lemma list_length_empty (A:Type[0]): |list_empty A| = 𝟎.
34 lemma list_length_lcons (A:Type[0]) (l:list A) (a:A): |a⨮l| = ↑|l|.
37 (* Basic inversions *********************************************************)
39 lemma list_length_inv_zero_dx (A:Type[0]) (l:list A):
41 #A * // #a #l >list_length_lcons #H
42 elim (eq_inv_nsucc_zero … H)
45 lemma list_length_inv_zero_sn (A:Type[0]) (l:list A):
47 /2 width=1 by list_length_inv_zero_dx/ qed-.
49 lemma list_length_inv_succ_dx (A:Type[0]) (l:list A) (x):
51 ∃∃tl,a. x = |tl| & l = a ⨮ tl.
53 [ #x >list_length_empty #H
54 elim (eq_inv_zero_nsucc … H)
55 | #a #l #x >list_length_lcons #H
56 /3 width=4 by eq_inv_nsucc_bi, ex2_2_intro/
60 lemma list_length_inv_succ_sn (A:Type[0]) (l:list A) (x):
62 ∃∃tl,a. x = |tl| & l = a ⨮ tl.
63 /2 width=1 by list_length_inv_succ_dx/ qed-.