(* *)
(**************************************************************************)
+include "ground/notation/functions/verticalbars_1.ma".
include "ground/lib/list.ma".
include "ground/arith/nat_succ.ma".
interpretation
"length (lists)"
- 'card l = (list_length ? l).
+ 'VerticalBars l = (list_length ? l).
(* Basic constructions ******************************************************)
-lemma list_length_empty (A:Type[0]): |list_empty A| = ๐.
+lemma list_length_empty (A:Type[0]):
+ โlist_empty Aโ = ๐.
// qed.
-lemma list_length_lcons (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 = โ.
+ โ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_empty #H
elim (eq_inv_zero_nsucc โฆ H)
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-.