matita/matita/contribs/lambdadelta/ground/lib/list_length.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "ground/notation/functions/verticalbars_1.ma".
  16 include "ground/lib/list.ma".
  17 include "ground/arith/nat_succ.ma".
  18
  19 (* LENGTH FOR LISTS *********************************************************)
  20
  21 rec definition list_length A (l:list A) on l ≝ match l with
  22 [ list_empty     ⇒ 𝟎
  23 | list_lcons _ l ⇒ ↑(list_length A l)
  24 ].
  25
  26 interpretation
  27   "length (lists)"
  28   'VerticalBars l = (list_length ? l).
  29
  30 (* Basic constructions ******************************************************)
  31
  32 lemma list_length_empty (A:Type[0]):
  33       ❘list_empty A❘ = 𝟎.
  34 // qed.
  35
  36 lemma list_length_lcons (A:Type[0]) (l:list A) (a:A):
  37       ❘a⨮l❘ = ↑❘l❘.
  38 // qed.
  39
  40 (* Basic inversions *********************************************************)
  41
  42 lemma list_length_inv_zero_dx (A:Type[0]) (l:list A):
  43       ❘l❘ = 𝟎 → l = ⓔ.
  44 #A * // #a #l >list_length_lcons #H
  45 elim (eq_inv_nsucc_zero … H)
  46 qed-.
  47
  48 lemma list_length_inv_zero_sn (A:Type[0]) (l:list A):
  49       (𝟎) = ❘l❘ → l = ⓔ.
  50 /2 width=1 by list_length_inv_zero_dx/ qed-.
  51
  52 lemma list_length_inv_succ_dx (A:Type[0]) (l:list A) (x):
  53       ❘l❘ = ↑x →
  54       ∃∃tl,a. x = ❘tl❘ & l = a ⨮ tl.
  55 #A *
  56 [ #x >list_length_empty #H
  57   elim (eq_inv_zero_nsucc … H)
  58 | #a #l #x >list_length_lcons #H
  59   /3 width=4 by eq_inv_nsucc_bi, ex2_2_intro/
  60 ]
  61 qed-.
  62
  63 lemma list_length_inv_succ_sn (A:Type[0]) (l:list A) (x):
  64       ↑x = ❘l❘ →
  65       ∃∃tl,a. x = ❘tl❘ & l = a ⨮ tl.
  66 /2 width=1 by list_length_inv_succ_dx/ qed-.