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/notation/constructors/nil_0.ma".
16 include "ground_2/notation/constructors/cons_2.ma".
17 include "ground_2/lib/arith.ma".
19 (* LISTS ********************************************************************)
21 inductive list (A:Type[0]) : Type[0] :=
23 | cons: A → list A → list A.
25 interpretation "nil (list)" 'Nil = (nil ?).
27 interpretation "cons (list)" 'Cons hd tl = (cons ? hd tl).
29 rec definition length (A:Type[0]) (l:list A) on l ≝ match l with
31 | cons _ l ⇒ ⫯(length A l)
34 interpretation "length (list)"
35 'card l = (length ? l).
37 rec definition all A (R:predicate A) (l:list A) on l ≝
40 | cons hd tl ⇒ R hd ∧ all A R tl
43 (* Basic properties on length ***********************************************)
45 lemma length_nil (A:Type[0]): |nil A| = 0.
48 lemma length_cons (A:Type[0]) (l:list A) (a:A): |a@l| = ⫯|l|.
51 (* Basic inversion lemmas on length *****************************************)
53 lemma length_inv_zero_dx (A:Type[0]) (l:list A): |l| = 0 → l = ◊.
54 #A * // #a #l >length_cons #H destruct
57 lemma length_inv_zero_sn (A:Type[0]) (l:list A): 0 = |l| → l = ◊.
58 /2 width=1 by length_inv_zero_dx/ qed-.
60 lemma length_inv_succ_dx (A:Type[0]) (l:list A) (x): |l| = ⫯x →
61 ∃∃tl,a. x = |tl| & l = a @ tl.
62 #A * /2 width=4 by ex2_2_intro/
63 >length_nil #x #H destruct
66 lemma length_inv_succ_sn (A:Type[0]) (l:list A) (x): ⫯x = |l| →
67 ∃∃tl,a. x = |tl| & l = a @ tl.
68 /2 width=1 by length_inv_succ_dx/ qed.