X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Fbasics%2Flists%2Flists.ma;fp=weblib%2Fbasics%2Flists%2Flists.ma;h=ba7e48477d5db5abe24b65a2f7fc86d6a0c0514b;hb=adfe42bbd5aaa4130a4133f345930e79444f0f3e;hp=0000000000000000000000000000000000000000;hpb=4672640dc168a3adcbea86887c38d895358288e8;p=helm.git

diff --git a/weblib/basics/lists/lists.ma b/weblib/basics/lists/lists.ma
new file mode 100644
index 000000000..ba7e48477
--- /dev/null
+++ b/weblib/basics/lists/lists.ma
@@ -0,0 +1,47 @@
+(* Definition of list *)
+
+include "basics/logic.ma".
+
+img class="anchor" src="icons/tick.png" id="list"inductive 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).
+
+img class="anchor" src="icons/tick.png" id="is_nil"definition is_nil: ∀A:Type[0].a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A → Prop ≝
+ λA.λl.match l with [ nil ⇒ a href="cic:/matita/basics/logic/True.ind(1,0,0)"True/a | cons hd tl ⇒ a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a ].
+
+img class="anchor" src="icons/tick.png" id="nil_cons"theorem nil_cons:
+  ∀A:Type[0].∀l:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A.∀a:A. a:a title="cons" href="cic:/fakeuri.def(1)":/al a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a [a title="nil" href="cic:/fakeuri.def(1)"]/a.
+  #A #l #a @a href="cic:/matita/basics/logic/Not.con(0,1,1)"nmk/a #Heq (change with (a href="cic:/matita/basics/lists/lists/is_nil.def(1)"is_nil/a ? (a:a title="cons" href="cic:/fakeuri.def(1)":/al))) >Heq //
+qed.
+
+(* hd and tail *)
+img class="anchor" src="icons/tick.png" id="hd"definition hd ≝ λA.λl: a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A.λd:A.
+  match l with [ nil ⇒ d | cons a _ ⇒ a].
+
+img class="anchor" src="icons/tick.png" id="tail"definition tail ≝  λA.λl: a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A.
+  match l with [ nil ⇒  [a title="nil" href="cic:/fakeuri.def(1)"]/a | cons hd tl ⇒  tl].
+
+(* injectivity *) 
+
+img class="anchor" src="icons/tick.png" id="cons_injective_l"lemma cons_injective_l : ∀A.∀a1,a2:A.∀l1,l2.a1:a title="cons" href="cic:/fakeuri.def(1)":/al1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a2:a title="cons" href="cic:/fakeuri.def(1)":/al2 → a1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a2.
+#A #a1 #a2 #l1 #l2 #Heq destruct //
+qed.
+
+img class="anchor" src="icons/tick.png" id="cons_injective_r"lemma cons_injective_r : ∀A.∀a1,a2:A.∀l1,l2.a1:a title="cons" href="cic:/fakeuri.def(1)":/al1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a2:a title="cons" href="cic:/fakeuri.def(1)":/al2 → l1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l2.
+#A #a1 #a2 #l1 #l2 #Heq destruct //
+qed.