weblib/basics/list.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||
   8     \   /  This file is distributed under the terms of the
   9      \ /   GNU General Public License Version 2
  10       V_______________________________________________________________ *)
  11
  12 include "arithmetics/nat.ma".
  13
  14 inductive list (A:Type[0]) : Type[0] :=
  15   | nil: list A
  16   | cons: A -> list A -> list A.
  17
  18 notation "hvbox(hd break :: tl)"
  19   right associative with precedence 47
  20   for @{'cons $hd $tl}.
  21
  22 notation "[ list0 x sep ; ]"
  23   non associative with precedence 90
  24   for ${fold right @'nil rec acc @{'cons $x $acc}}.
  25
  26 notation "hvbox(l1 break @ l2)"
  27   right associative with precedence 47
  28   for @{'append $l1 $l2 }.
  29
  30 interpretation "nil" 'nil = (nil ?).
  31 interpretation "cons" 'cons hd tl = (cons ? hd tl).
  32
  33 definition not_nil: ∀A:Type[0].\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A → Prop ≝
  34  λA.λl.match l with [ nil ⇒ \ 5a href="cic:/matita/basics/logic/True.ind(1,0,0)"\ 6True\ 5/a\ 6 | cons hd tl ⇒ \ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6 ].
  35
  36 theorem nil_cons:
  37   ∀A:Type[0].∀l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀a:A. a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6].
  38   #A #l #a @\ 5a href="cic:/matita/basics/logic/Not.con(0,1,1)"\ 6nmk\ 5/a\ 6 #Heq (change with (\ 5a href="cic:/matita/basics/list/not_nil.def(1)"\ 6not_nil\ 5/a\ 6 ? (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l))) >Heq //
  39 qed.
  40
  41 (*
  42 let rec id_list A (l: list A) on l :=
  43   match l with
  44   [ nil => []
  45   | (cons hd tl) => hd :: id_list A tl ]. *)
  46
  47 let rec append A (l1: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) l2 on l1 ≝
  48   match l1 with
  49   [ nil ⇒  l2
  50   | cons hd tl ⇒  hd \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: append A tl l2 ].
  51
  52 definition hd ≝ λA.λl: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.λd:A.
  53   match l with [ nil ⇒ d | cons a _ ⇒ a].
  54
  55 definition tail ≝  λA.λl: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
  56   match l with [ nil ⇒  \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] | cons hd tl ⇒  tl].
  57
  58 interpretation "append" 'append l1 l2 = (append ? l1 l2).
  59
  60 theorem append_nil: ∀A.∀l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.l \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l.
  61 #A #l (elim l) normalize // qed.
  62
  63 theorem associative_append:
  64  ∀A.\ 5a href="cic:/matita/basics/relations/associative.def(1)"\ 6associative\ 5/a\ 6 (\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (\ 5a href="cic:/matita/basics/list/append.fix(0,1,1)"\ 6append\ 5/a\ 6 A).
  65 #A #l1 #l2 #l3 (elim l1) normalize // qed.
  66
  67 (* deleterio per auto
  68 ntheorem cons_append_commute:
  69   ∀A:Type.∀l1,l2:list A.∀a:A.
  70     a :: (l1 @ l2) = (a :: l1) @ l2.
  71 //; nqed. *)
  72
  73 theorem append_cons:∀A.∀a:A.∀l,l1.l\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l1)\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6(l\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]))\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l1.\ 5span style="text-decoration: underline;"\ 6\ 5/span\ 6\ 5span class="autotactic"\ 6\ 5/span\ 6
  74 #A #a #l1 #l2 >\ 5a href="cic:/matita/basics/list/associative_append.def(4)"\ 6associative_append\ 5/a\ 6 // qed.
  75
  76 theorem nil_append_elim: ∀A.∀l1,l2: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀P:?→?→Prop.
  77   l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] → P (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 A) (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 A) → P l1 l2.
  78 #A #l1 #l2 #P (cases l1) normalize //
  79 #a #l3 #heq destruct
  80 qed.
  81
  82 theorem nil_to_nil:  ∀A.∀l1,l2:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
  83   l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] → l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6].
  84 #A #l1 #l2 #isnil @(\ 5a href="cic:/matita/basics/list/nil_append_elim.def(4)"\ 6nil_append_elim\ 5/a\ 6 A l1 l2) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
  85 qed.
  86
  87 (* iterators *)
  88
  89 let rec map (A,B:Type[0]) (f: A → B) (l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 B ≝
  90  match l with [ nil ⇒ \ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 ? | cons x tl ⇒ f x \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: (map A B f tl)].
  91
  92 lemma map_append : ∀A,B,f,l1,l2.
  93   (\ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B f l1) \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 (\ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B f l2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B f (l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2).
  94 #A #B #f #l1 elim l1
  95 [ #l2 @\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6
  96 | #h #t #IH #l2 normalize //
  97 ] qed.
  98
  99 let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l :B ≝
 100  match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)].
 101
 102 definition filter ≝
 103   λT.λp:T → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6.
 104   \ 5a href="cic:/matita/basics/list/foldr.fix(0,4,1)"\ 6foldr\ 5/a\ 6 T (\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 T) (λx,l0.if (p x) then (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l0) else l0) (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 T).
 105
 106 definition compose ≝ λA,B,C.λf:A→B→C.λl1,l2.
 107     \ 5a href="cic:/matita/basics/list/foldr.fix(0,4,1)"\ 6foldr\ 5/a\ 6 ?? (λi,acc.(\ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 ?? (f i) l2)\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6acc) \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ] l1.
 108
 109 lemma filter_true : ∀A,l,a,p. p a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 →
 110   \ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: \ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p l.
 111 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
 112
 113 lemma filter_false : ∀A,l,a,p. p a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 →
 114   \ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p l.
 115 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
 116
 117 theorem eq_map : ∀A,B,f,g,l. (∀x.f x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 g x) → \ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B f l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B g l.
 118 #A #B #f #g #l #eqfg (elim l) normalize // qed.
 119
 120 (*
 121 let rec dprodl (A:Type[0]) (f:A→Type[0]) (l1:list A) (g:(∀a:A.list (f a))) on l1 ≝
 122 match l1 with
 123   [ nil ⇒ nil ?
 124   | cons a tl ⇒ (map ??(dp ?? a) (g a)) @ dprodl A f tl g
 125   ]. *)
 126
 127 (**************************** length *******************************)
 128
 129 let rec length (A:Type[0]) (l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l ≝
 130   match l with
 131     [ nil ⇒ \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6
 132     | cons a tl ⇒ \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (length A tl)].
 133
 134 notation "|M|" non associative with precedence 60 for @{'norm $M}.
 135 interpretation "norm" 'norm l = (length ? l).
 136
 137 lemma length_append: ∀A.∀l1,l2:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
 138   \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2| \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6l1|\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6\ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6l2|.
 139 #A #l1 elim l1 // normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
 140 qed.
 141
 142 let rec nth n (A:Type[0]) (l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (d:A)  ≝
 143   match n with
 144     [O ⇒ \ 5a href="cic:/matita/basics/list/hd.def(1)"\ 6hd\ 5/a\ 6 A l d
 145     |S m ⇒ nth m A (\ 5a href="cic:/matita/basics/list/tail.def(1)"\ 6tail\ 5/a\ 6 A l) d].
 146
 147 (***************************** fold *******************************)
 148
 149 let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6) (f:A→B) (l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l :B ≝
 150  match l with
 151   [ nil ⇒ b
 152   | cons a l ⇒ if (p a) then (op (f a) (fold A B op b p f l))
 153       else (fold A B op b p f l)
 154   ].
 155
 156 notation "\fold  [ op , nil ]_{ ident i ∈ l | p} f"
 157   with precedence 80
 158 for @{'fold $op $nil (λ${ident i}. $p) (λ${ident i}. $f) $l}.
 159
 160 notation "\fold [ op , nil ]_{ident i ∈ l } f"
 161   with precedence 80
 162 for @{'fold $op $nil (λ${ident i}.true) (λ${ident i}. $f) $l}.
 163
 164 interpretation "\fold" 'fold op nil p f l = (fold ? ? op nil p f l).
 165
 166 theorem fold_true:
 167 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. p a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 →
 168   \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l| p i} (f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
 169     op (f a) \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ l| p i} (f i).
 170 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
 171
 172 theorem fold_false:
 173 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f.
 174 p a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 → \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l| p i} (f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
 175   \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ l| p i} (f i).
 176 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
 177
 178 theorem fold_filter:
 179 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A →B.
 180   \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ l| p i} (f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
 181     \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ (\ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p l)} (f i).
 182 #A #B #a #l #p #op #nil #f elim l //
 183 #a #tl #Hind cases(\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (p a)) #pa
 184   [ >\ 5a href="cic:/matita/basics/list/filter_true.def(3)"\ 6filter_true\ 5/a\ 6 // > \ 5a href="cic:/matita/basics/list/fold_true.def(3)"\ 6fold_true\ 5/a\ 6 // >\ 5a href="cic:/matita/basics/list/fold_true.def(3)"\ 6fold_true\ 5/a\ 6 //
 185   | >\ 5a href="cic:/matita/basics/list/filter_false.def(3)"\ 6filter_false\ 5/a\ 6 // >\ 5a href="cic:/matita/basics/list/fold_false.def(3)"\ 6fold_false\ 5/a\ 6 // ]
 186 qed.
 187
 188 record Aop (A:Type[0]) (nil:A) : Type[0] ≝
 189   {op :2> A → A → A;
 190    nill:∀a. op nil a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a;
 191    nilr:∀a. op a nil \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a;
 192    assoc: ∀a,b,c.op a (op b c) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 op (op a b) c
 193   }.
 194
 195 theorem fold_sum: ∀A,B. ∀I,J:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀nil.∀op:\ 5a href="cic:/matita/basics/list/Aop.ind(1,0,2)"\ 6Aop\ 5/a\ 6 B nil.∀f.
 196   op (\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i∈I} (f i)) (\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i∈J} (f i)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
 197     \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i∈(I\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6J)} (f i).
 198 #A #B #I #J #nil #op #f (elim I) normalize
 199   [>\ 5a href="cic:/matita/basics/list/nill.fix(0,2,2)"\ 6nill\ 5/a\ 6 //|#a #tl #Hind <\ 5a href="cic:/matita/basics/list/assoc.fix(0,2,2)"\ 6assoc\ 5/a\ 6 //]
 200 qed.