X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftutorial%2Fchapter3.ma;h=20e545e37cff1a6fa90ef11852151c25bebdfa28;hb=7aa41e02e64bd09df253cc4267a44b4f49b16e03;hp=c42e1887f892428f61ae4834dda4ae0f6f37c6c4;hpb=b5f54d2815f446a999736abd0ffe80641596a5f6;p=helm.git

diff --git a/weblib/tutorial/chapter3.ma b/weblib/tutorial/chapter3.ma
index c42e1887f..20e545e37 100644
--- a/weblib/tutorial/chapter3.ma
+++ b/weblib/tutorial/chapter3.ma
@@ -99,9 +99,12 @@ theorem associative_append:
 #A #l1 #l2 #l3 (elim l1) normalize // qed.
 
 (* Problemi con la notazione *)
+lemma a_append: ∀A.∀a.∀l:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A. (aa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]) a title="append" href="cic:/fakeuri.def(1)"@/a l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a aa title="cons" href="cic:/fakeuri.def(1)":/a:l.
+// qed.
+
 theorem append_cons:
 ∀A.∀a:A.∀l,l1: a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A.la title="append" href="cic:/fakeuri.def(1)"@/a(aa title="cons" href="cic:/fakeuri.def(1)":/a:l1)a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (l a title="append" href="cic:/fakeuri.def(1)"@/a (a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"cons/a ? a a title="nil" href="cic:/fakeuri.def(1)"[/a])) a title="append" href="cic:/fakeuri.def(1)"@/a l1.
-/2/ qed. 
+// qed. 
 
 (* Other typical functions over lists are those computing the length 
 of a list, and the function returning the nth element *)
@@ -141,7 +144,7 @@ definition is_nil: ∀A:Type[0].a href="cic:/matita/tutorial/chapter3/list.ind(
 authorized to add P to your hypothesis: *)
 
 lemma neg_aux : ∀P:Prop. (P → a title="logical not" href="cic:/fakeuri.def(1)"¬/aP) → a title="logical not" href="cic:/fakeuri.def(1)"¬/aP.
-#P #PtonegP % /3/ qed. 
+#P #PtonegP % /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ qed. 
 
 theorem diff_cons_nil:
 ∀A:Type[0].∀l:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A.∀a:A. aa title="cons" href="cic:/fakeuri.def(1)":/a:l a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a title="nil" href="cic:/fakeuri.def(1)"[/a].
@@ -165,7 +168,7 @@ to solve the absurd case. *)
 
 lemma nil_to_nil:  ∀A.∀l1,l2:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a span style="text-decoration: underline;"/spanA.
   l1a title="append" href="cic:/fakeuri.def(1)"@/al2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="nil" href="cic:/fakeuri.def(1)"[/a] → l1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="nil" href="cic:/fakeuri.def(1)"[/a] a title="logical and" href="cic:/fakeuri.def(1)"∧/a l2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="nil" href="cic:/fakeuri.def(1)"[/a].
-#A #l1 cases l1 normalize /2/ #a #tl #l2 #H @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /2/ qed. 
+#A #l1 cases l1 normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/ #a #tl #l2 #H @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ qed. 
 
 (* Let us come to some important, higher order, polymorphic functionals 
 acting over lists. A typical example is the map function, taking a function