(* *)
(**************************************************************************)
+include "ground/notation/functions/verticalbars_1.ma".
include "ground/lib/list.ma".
include "ground/arith/nat_succ.ma".
(* LENGTH FOR LISTS *********************************************************)
-rec definition list_length A (l:list A) on l โ
-match l with
-[ list_nil โ ๐
-| list_cons _ l โ โ(list_length A l)
+rec definition list_length A (l:list A) on l โ match l with
+[ list_empty โ ๐
+| list_lcons _ l โ โ(list_length A l)
].
interpretation
"length (lists)"
- 'card l = (list_length ? l).
+ 'VerticalBars l = (list_length ? l).
(* Basic constructions ******************************************************)
-lemma list_length_nil (A:Type[0]): |list_nil A| = ๐.
+lemma list_length_empty (A:Type[0]):
+ โlist_empty Aโ = ๐.
// qed.
-lemma list_length_cons (A:Type[0]) (l:list A) (a:A): |aโจฎl| = โ|l|.
+lemma list_length_lcons (A:Type[0]) (l:list A) (a:A):
+ โaโจฎlโ = โโlโ.
// qed.
(* Basic inversions *********************************************************)
lemma list_length_inv_zero_dx (A:Type[0]) (l:list A):
- |l| = ๐ โ l = โบ.
-#A * // #a #l >list_length_cons #H
+ โlโ = ๐ โ l = โ.
+#A * // #a #l >list_length_lcons #H
elim (eq_inv_nsucc_zero โฆ H)
qed-.
lemma list_length_inv_zero_sn (A:Type[0]) (l:list A):
- (๐) = |l| โ l = โบ.
+ (๐) = โlโ โ l = โ.
/2 width=1 by list_length_inv_zero_dx/ qed-.
lemma list_length_inv_succ_dx (A:Type[0]) (l:list A) (x):
- |l| = โx โ
- โโtl,a. x = |tl| & l = a โจฎ tl.
+ โlโ = โx โ
+ โโtl,a. x = โtlโ & l = a โจฎ tl.
#A *
-[ #x >list_length_nil #H
+[ #x >list_length_empty #H
elim (eq_inv_zero_nsucc โฆ H)
-| #a #l #x >list_length_cons #H
+| #a #l #x >list_length_lcons #H
/3 width=4 by eq_inv_nsucc_bi, ex2_2_intro/
]
qed-.
lemma list_length_inv_succ_sn (A:Type[0]) (l:list A) (x):
- โx = |l| โ
- โโtl,a. x = |tl| & l = a โจฎ tl.
+ โx = โlโ โ
+ โโtl,a. x = โtlโ & l = a โจฎ tl.
/2 width=1 by list_length_inv_succ_dx/ qed-.