helm/software/matita/nlibrary/basics/list.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 "basics/eq.ma".
  16 include "basics/bool.ma".
  17
  18 ninductive list (A:Type) : Type :=
  19   | nil: list A
  20   | cons: A -> list A -> list A.
  21
  22 notation "hvbox(hd break :: tl)"
  23   right associative with precedence 47
  24   for @{'cons $hd $tl}.
  25
  26 notation "[ list0 x sep ; ]"
  27   non associative with precedence 90
  28   for ${fold right @'nil rec acc @{'cons $x $acc}}.
  29
  30 notation "hvbox(l1 break @ l2)"
  31   right associative with precedence 47
  32   for @{'append $l1 $l2 }.
  33
  34 interpretation "nil" 'nil = (nil ?).
  35 interpretation "cons" 'cons hd tl = (cons ? hd tl).
  36
  37 ndefinition not_nil: ∀A:Type.list A → Prop ≝
  38  λA.λl.match l with [ nil ⇒ True | cons hd tl ⇒ False ].
  39
  40 ntheorem nil_cons:
  41   ∀A:Type.∀l:list A.∀a:A. a::l ≠ [].
  42   #A; #l; #a; napply nmk; #Heq; nchange with (not_nil ? (a::l));
  43   nrewrite > Heq; //;
  44 nqed.
  45
  46 (*
  47 let rec id_list A (l: list A) on l :=
  48   match l with
  49   [ nil => []
  50   | (cons hd tl) => hd :: id_list A tl ]. *)
  51
  52 nlet rec append A (l1: list A) l2 on l1 :=
  53   match l1 with
  54   [ nil ⇒  l2
  55   | cons hd tl ⇒  hd :: append A tl l2 ].
  56
  57 ndefinition hd ≝ λA:Type.λl: list A.λd:A.
  58   match l with
  59   [ nil ⇒ d
  60   | cons a _ ⇒ a].
  61
  62 ndefinition tail ≝  λA:Type.λl: list A.
  63   match l with
  64   [ nil ⇒  []
  65   | cons hd tl ⇒  tl].
  66
  67 interpretation "append" 'append l1 l2 = (append ? l1 l2).
  68
  69 ntheorem append_nil: ∀A:Type.∀l:list A.l @ [] = l.
  70 #A; #l; nelim l; nnormalize;//; nqed.
  71
  72 ntheorem associative_append:
  73  ∀A:Type.associative (list A) (append A).
  74 #A; #l1; #l2; #l3; nelim l1; nnormalize; //; nqed.
  75
  76 (* deleterio per auto
  77 ntheorem cons_append_commute:
  78   ∀A:Type.∀l1,l2:list A.∀a:A.
  79     a :: (l1 @ l2) = (a :: l1) @ l2.
  80 //; nqed. *)
  81
  82 ntheorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1.
  83 #A; #a; #l; #l1; napply sym_eq.
  84 napply associative_append.
  85 (* /2/; *) nqed.
  86
  87 ntheorem nil_append_elim: ∀A.∀l1,l2: list A.∀P: list A → list A → Prop.
  88   l1@l2 = [] → P (nil A) (nil A) → P l1 l2.
  89 #A;#l1; #l2; #P; ncases l1; nnormalize;//;
  90 #a; #l3; #heq; ndestruct;
  91 nqed.
  92
  93 ntheorem nil_to_nil:  ∀A.∀l1,l2:list A.
  94   l1@l2 = [] → l1 = [] ∧ l2 = [].
  95 #A; #l1; #l2; #isnil; napply (nil_append_elim A l1 l2);/2/;
  96 nqed.
  97
  98 (* ierators *)
  99
 100 nlet rec map (A,B:Type) (f: A → B) (l:list A) on l: list B ≝
 101  match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map A B f tl)].
 102
 103 nlet rec foldr (A,B:Type) (f:A → B → B) (b:B) (l:list A) on l :B ≝
 104  match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)].
 105
 106 ndefinition filter ≝
 107   λT:Type.λl:list T.λp:T → bool.
 108   foldr T (list T) (λx,l0.if_then_else ? (p x) (x::l0) l0).
 109
 110 ntheorem eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
 111 #A; #B; #f; #g; #l; #eqfg; nelim l; nnormalize; //; nqed.
 112