commit by user andrea

diff --git a/weblib/tutorial/chapter3.ma b/weblib/tutorial/chapter3.ma
index 4ce43679d7c498e59b28f075dd2f0c080c1bf7bb..849b067e7f587d49175a3fad3abffbaf8ec6a493 100644 (file)
--- a/weblib/tutorial/chapter3.ma
+++ b/weblib/tutorial/chapter3.ma
@@ -103,19 +103,66 @@ theorem append_cons:
 ∀A.∀a:A.∀l,l1: \ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.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 (\ 5a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"\ 6cons\ 5/a\ 6 ? a \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6])) \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 l1.
 /2/ qed. 
 
+(* Other typical functions over lists are those computing the length 
+of a list, and the function returning the nth element *)
 
-theorem nil_to_nil:  ∀A.∀l1,l2:\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 \ 5span style="text-decoration: underline;"\ 6\ 5/span\ 6A.
-  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].
-#A #l1 #l2 #isnil @(\ 5a href="cic:/matita/tutorial/chapter3/nil_append_elim.def(3)"\ 6nil_append_elim\ 5/a\ 6 A l1 l2) /2/
-qed.
+let rec length (A:Type[0]) (l:\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l ≝ 
+match l with 
+  [ nil ⇒ \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6
+    | cons a tl ⇒ \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (length A tl)].
+
+let rec nth n (A:Type[0]) (l:\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (d:A)  ≝  
+  match n with
+    [O ⇒ \ 5a href="cic:/matita/tutorial/chapter3/hd.def(1)"\ 6hd\ 5/a\ 6 A l d
+    |S m ⇒ nth m A (\ 5a href="cic:/matita/tutorial/chapter3/tail.def(1)"\ 6tail\ 5/a\ 6 A l) d].
+
+example ex_length: \ 5a href="cic:/matita/tutorial/chapter3/length.fix(0,1,1)"\ 6length\ 5/a\ 6 ? (\ 5a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"\ 6cons\ 5/a\ 6 ? \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 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 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6.
+normalize // qed.
+
+example ex_nth: \ 5a href="cic:/matita/tutorial/chapter3/nth.fix(0,0,2)"\ 6nth\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6) ? (\ 5a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"\ 6cons\ 5/a\ 6 ? (\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6) (\ 5a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"\ 6cons\ 5/a\ 6 ? \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6])) \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6.
+normalize // qed.
+
+lemma  length_add: ∀A.∀l1,l2:\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A. 
+  \ 5a href="cic:/matita/tutorial/chapter3/length.fix(0,1,1)"\ 6length\ 5/a\ 6 ? (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 href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"\ 6add\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter3/length.fix(0,1,1)"\ 6length\ 5/a\ 6 ? l1) (\ 5a href="cic:/matita/tutorial/chapter3/length.fix(0,1,1)"\ 6length\ 5/a\ 6 ? l2).
+#A #l1 elim l1 normalize // qed. 
 
-definition not_nil: ∀A:Type[0].\ 5a href="cic:/matita/tutorial/chapter3/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].
+(* Let us come to a more interesting question. How can we prove that the empty list is 
+different from any list with at least one element, that is from any list of the kind (a::l)?
+We start defining a simple predicate stating if a list is empty or not. The predicate
+is computed by inspection over the list *)
 
-theorem nil_cons:
+definition is_nil: ∀A:Type[0].\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A → Prop ≝
+λA.λl.match l with [ nil ⇒ l \ 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] | cons hd tl ⇒ (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])].
+
+(* Next we need a simple result about negation: if you wish to prove ¬P you are
+authorized to add P to your hypothesis: *)
+
+lemma neg_aux : ∀P:Prop. (P → \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6P) → \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6P.
+#P #PtonegP % /3/ qed. 
+
+theorem diff_cons_nil:
 ∀A:Type[0].∀l:\ 5a href="cic:/matita/tutorial/chapter3/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].
-#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/tutorial/chapter3/not_nil.def(1)"\ 6not_nil\ 5/a\ 6 ? (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l))) >Heq //
-qed.
+#A #l #a @\ 5a href="cic:/matita/tutorial/chapter3/neg_aux.def(3)"\ 6neg_aux\ 5/a\ 6 #Heq 
+(* we start assuming the new hypothesis Heq of type a::l = [] using neg_aux. 
+Next we use the change tactic to pass from the current goal a::l≠ [] to the expression 
+is_nil a::l, convertible with it. *)
+(change with (\ 5a href="cic:/matita/tutorial/chapter3/is_nil.def(1)"\ 6is_nil\ 5/a\ 6 ? (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l))) 
+(* Now, we rewrite with Heq, obtaining (is_nil A []), that reduces to the trivial 
+goal [] = [] *)
+>Heq // qed.
+
+(* As an application of the previous result let us prove that l1@l2 is empty if and 
+only if both l1 and l2 are empty. The idea is to proceed by cases on l1: if l1=[] the
+statement is trivial; on the other side, if l1 = a::tl, then the hypothesis 
+(a::tl)@l2 = [] is absurd, hence we can prove anything from it. When we know we can
+prove both A and ¬A, a sensible way to proceed is to apply False_ind: ∀P.False → P to the 
+current goal, that breaks down to prove False, and then absurd: ∀A:Prop. A → ¬A → False 
+to reduce to the contradictory cases. Usually, you may invoke automation to take care 
+to solve the absurd case. *)
+
+lemma nil_to_nil:  ∀A.∀l1,l2:\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 \ 5span style="text-decoration: underline;"\ 6\ 5/span\ 6A.
+  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].
+#A #l1 cases l1 normalize /2/ #a #tl #l2 #H @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /2/ qed. 
 
 (* iterators *)
 
@@ -147,18 +194,6 @@ match l1 with
   | cons a tl ⇒ (map ??(dp ?? a) (g a)) @ dprodl A f tl g
   ]. *)
 
-(**************************** length ******************************)
-
-let rec length (A:Type[0]) (l:\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l ≝ 
-  match l with 
-    [ nil ⇒ \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6
-    | cons a tl ⇒ \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (length A tl)].
-
-let rec nth n (A:Type[0]) (l:\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (d:A)  ≝  
-  match n with
-    [O ⇒ \ 5a href="cic:/matita/tutorial/chapter3/hd.def(1)"\ 6hd\ 5/a\ 6 A l d
-    |S m ⇒ nth m A (\ 5a href="cic:/matita/tutorial/chapter3/tail.def(1)"\ 6tail\ 5/a\ 6 A l) d].
-
 (**************************** fold *******************************)
 
 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/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l :B ≝