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_2/lib/arith.ma".
16 include "ground_2/lib/list.ma".
18 (* LENGTH OF A LIST *********************************************************)
20 rec definition length A (l:list A) on l ≝ match l with
22 | cons _ l ⇒ ↑(length A l)
25 interpretation "length (list)"
26 'card l = (length ? l).
28 (* Basic properties *********************************************************)
30 lemma length_nil (A:Type[0]): |nil A| = 0.
33 lemma length_cons (A:Type[0]) (l:list A) (a:A): |a⨮l| = ↑|l|.
36 (* Basic inversion lemmas ***************************************************)
38 lemma length_inv_zero_dx (A:Type[0]) (l:list A): |l| = 0 → l = Ⓔ.
39 #A * // #a #l >length_cons #H destruct
42 lemma length_inv_zero_sn (A:Type[0]) (l:list A): 0 = |l| → l = Ⓔ.
43 /2 width=1 by length_inv_zero_dx/ qed-.
45 lemma length_inv_succ_dx (A:Type[0]) (l:list A) (x): |l| = ↑x →
46 ∃∃tl,a. x = |tl| & l = a ⨮ tl.
47 #A * /2 width=4 by ex2_2_intro/
48 >length_nil #x #H destruct
51 lemma length_inv_succ_sn (A:Type[0]) (l:list A) (x): ↑x = |l| →
52 ∃∃tl,a. x = |tl| & l = a ⨮ tl.
53 /2 width=1 by length_inv_succ_dx/ qed.