commit by user andrea

[helm.git] / weblib / basics / lists / lists.ma

diff --git a/weblib/basics/lists/lists.ma b/weblib/basics/lists/lists.ma
new file mode 100644 (file)
index 0000000..ba7e484
--- /dev/null
+++ b/weblib/basics/lists/lists.ma
@@ -0,0 +1,47 @@
+(* Definition of list *)
+
+include "basics/logic.ma".
+
+\ 5img class="anchor" src="icons/tick.png" id="list"\ 6inductive list (A:Type[0]) : Type[0] :=
+  | nil: list A
+  | cons: A -> list A -> list A.
+
+notation "hvbox(hd break :: tl)"
+  right associative with precedence 47
+  for @{'cons $hd $tl}.
+
+notation "[ list0 term 19 x sep ; ]"
+  non associative with precedence 90
+  for ${fold right @'nil rec acc @{'cons $x $acc}}.
+
+notation "hvbox(l1 break @ l2)"
+  right associative with precedence 47
+  for @{'append $l1 $l2 }.
+
+interpretation "nil" 'nil = (nil ?).
+interpretation "cons" 'cons hd tl = (cons ? hd tl).
+
+\ 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 ≝
+ λ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 ].
+
+\ 5img class="anchor" src="icons/tick.png" id="nil_cons"\ 6theorem nil_cons:
+  ∀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.
+  #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 //
+qed.
+
+(* hd and tail *)
+\ 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.
+  match l with [ nil ⇒ d | cons a _ ⇒ a].
+
+\ 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.
+  match l with [ nil ⇒  [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 | cons hd tl ⇒  tl].
+
+(* injectivity *) 
+
+\ 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.
+#A #a1 #a2 #l1 #l2 #Heq destruct //
+qed.
+
+\ 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.
+#A #a1 #a2 #l1 #l2 #Heq destruct //
+qed.