1 (* Definition of list *)
3 include "basics/logic.ma".
5 \ 5img class="anchor" src="icons/tick.png" id="list"
\ 6inductive list (A:Type[0]) : Type[0] :=
7 | cons: A -> list A -> list A.
9 notation "hvbox(hd break :: tl)"
10 right associative with precedence 47
13 notation "[ list0 term 19 x sep ; ]"
14 non associative with precedence 90
15 for ${fold right @'nil rec acc @{'cons $x $acc}}.
17 notation "hvbox(l1 break @ l2)"
18 right associative with precedence 47
19 for @{'append $l1 $l2 }.
21 interpretation "nil" 'nil = (nil ?).
22 interpretation "cons" 'cons hd tl = (cons ? hd tl).
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 ].
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 //
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].
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].
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 //
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 //