weblib/basics/lists/lists.ma

   1 (* Definition of list *)
   2
   3 include "basics/logic.ma".
   4
   5 \ 5img class="anchor" src="icons/tick.png" id="list"\ 6inductive list (A:Type[0]) : Type[0] :=
   6   | nil: list A
   7   | cons: A -> list A -> list A.
   8
   9 notation "hvbox(hd break :: tl)"
  10   right associative with precedence 47
  11   for @{'cons $hd $tl}.
  12
  13 notation "[ list0 term 19 x sep ; ]"
  14   non associative with precedence 90
  15   for ${fold right @'nil rec acc @{'cons $x $acc}}.
  16
  17 notation "hvbox(l1 break @ l2)"
  18   right associative with precedence 47
  19   for @{'append $l1 $l2 }.
  20
  21 interpretation "nil" 'nil = (nil ?).
  22 interpretation "cons" 'cons hd tl = (cons ? hd tl).
  23
  24 \ 5img class="anchor" src="icons/tick.png" id="is_nil"\ 6definition is_nil: ∀A:Type[0].\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A → Prop ≝
  25  λ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 ].
  26
  27 \ 5img class="anchor" src="icons/tick.png" id="nil_cons"\ 6theorem nil_cons:
  28   ∀A:Type[0].∀l:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀a:A. a:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l \ 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.
  29   #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/lists/lists/is_nil.def(1)"\ 6is_nil\ 5/a\ 6 ? (a:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l))) >Heq //
  30 qed.
  31
  32 (* hd and tail *)
  33 \ 5img class="anchor" src="icons/tick.png" id="hd"\ 6definition hd ≝ λA.λl: \ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.λd:A.
  34   match l with [ nil ⇒ d | cons a _ ⇒ a].
  35
  36 \ 5img class="anchor" src="icons/tick.png" id="tail"\ 6definition tail ≝  λA.λl: \ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
  37   match l with [ nil ⇒  [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 | cons hd tl ⇒  tl].
  38
  39 (* injectivity *)
  40
  41 \ 5img class="anchor" src="icons/tick.png" id="cons_injective_l"\ 6lemma cons_injective_l : ∀A.∀a1,a2:A.∀l1,l2.a1:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a2:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l2 → a1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a2.
  42 #A #a1 #a2 #l1 #l2 #Heq destruct //
  43 qed.
  44
  45 \ 5img class="anchor" src="icons/tick.png" id="cons_injective_r"\ 6lemma cons_injective_r : ∀A.∀a1,a2:A.∀l1,l2.a1:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a2:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l2 → l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l2.
  46 #A #a1 #a2 #l1 #l2 #Heq destruct //
  47 qed.