X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftutorial%2Fchapter3.ma;h=c6cb5b8cd8e4c9ac58b3bbaf181789a6ab067a04;hb=c0ac63fead67ea1902e3d923ce877a2779cf501e;hp=51b810beec6309c9440679d76c6e7614c5bcfd26;hpb=7f6235dca57343e63217316b6415599daef7d4aa;p=helm.git

diff --git a/weblib/tutorial/chapter3.ma b/weblib/tutorial/chapter3.ma
index 51b810bee..c6cb5b8cd 100644
--- a/weblib/tutorial/chapter3.ma
+++ b/weblib/tutorial/chapter3.ma
@@ -7,7 +7,7 @@ include "basics/bool.ma".
 (* Matita supports polymorphic data types. The most typical case are polymorphic
 lists, parametric in the type of their elements: *)
 
-inductive list (A:Type[0]) : Type[0] ≝
+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.
 
@@ -64,17 +64,17 @@ specify in the its defintion on which one of them we are recurring: in this case
 If not othewise specified, recursion is supposed to act on the first argument of the
 function.*)
 
-let rec append A (l1: a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A) l2 on l1 ≝ 
+img class="anchor" src="icons/tick.png" id="append"let rec append A (l1: a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A) l2 on l1 ≝ 
   match l1 with
   [ nil ⇒  l2
-  | cons hd tl ⇒  hd a title="cons" href="cic:/fakeuri.def(1)":/aspan class="error" title="Parse error: [sym:] expected after [sym:] (in [term])"/span: append A tl l2 ].
+  | cons hd tl ⇒  hd a title="cons" href="cic:/fakeuri.def(1)":/aspan class="error" title="Parse error: [sym:] expected after [sym:] (in [term])"/spana title="cons" href="cic:/fakeuri.def(1)":/a append A tl l2 ].
 
 interpretation "append" 'append l1 l2 = (append ? l1 l2).
 
 (* As usual, the function is executable. For instance, (append A nil l) reduces to
 l, as shown by the following example: *)
 
-example nil_append: ∀A.∀l:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A. a title="nil" href="cic:/fakeuri.def(1)"[/aspan class="error" title="Parse error: [term] expected after [sym[] (in [term])"/span] a title="append" href="cic:/fakeuri.def(1)"@/a l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l.
+img class="anchor" src="icons/tick.png" id="nil_append"example nil_append: ∀A.∀l:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A. a title="nil" href="cic:/fakeuri.def(1)"[/aspan class="error" title="Parse error: [term] expected after [sym[] (in [term])"/spana 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 l.
 #A #l normalize // qed.
 
 (* Proving that l @ [] = l is just a bit more complex. The situation is exactly 
@@ -82,7 +82,7 @@ the same as for the addition operation of the previous chapter: since append is
 defined by recutsion over the first argument, the computation of l @ [] is stuck, 
 and we must proceed by induction on l *) 
 
-lemma append_nil: ∀A.∀l:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A.l a title="append" href="cic:/fakeuri.def(1)"@/aspan class="error" title="Parse error: [term level 46] expected after [sym@] (in [term])"/spanspan class="error" title="Parse error: [term level 46] expected after [sym@] (in [term])"/span a title="nil" href="cic:/fakeuri.def(1)"[/a] a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l.
+img class="anchor" src="icons/tick.png" id="append_nil"lemma append_nil: ∀A.∀l:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A.l a title="append" href="cic:/fakeuri.def(1)"@/aspan class="error" title="Parse error: [term level 46] expected after [sym@] (in [term])"/spanspan class="error" title="Parse error: [term level 46] expected after [sym@] (in [term])"/span a title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l.
 #A #l (elim l) normalize // qed.
 
 (* similarly, we can define the two functions head and tail. Since we can only define
@@ -90,53 +90,53 @@ total functions, we should decide what to do in case the input list is empty.
 For tl, it is natural to return the empty list; for hd, we take in input a default 
 element d of type A to return in this case. *)
 
-definition head ≝ λA.λl: a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A.λd:A.
+img class="anchor" src="icons/tick.png" id="head"definition head ≝ λA.λl: a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A.λd:A.
   match l with [ nil ⇒ d | cons a _ ⇒ a].
 
-definition tail ≝  λA.λl: a href="cic:/matita/tutorial/chapter3/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].
+img class="anchor" src="icons/tick.png" id="tail"definition tail ≝  λA.λl: a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A.
+  match l with [ nil ⇒  a title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a | cons hd tl ⇒  tl].
 
-example ex_head: ∀A.∀a,d,l. a href="cic:/matita/tutorial/chapter3/head.def(1)"head/a A (aa title="cons" href="cic:/fakeuri.def(1)":/a:l) d a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aspan class="error" title="Parse error: [term] expected after [sym=] (in [term])"/spanspan class="error" title="Parse error: [term] expected after [sym=] (in [term])"/span a.
+img class="anchor" src="icons/tick.png" id="ex_head"example ex_head: ∀A.∀a,d,l. a href="cic:/matita/tutorial/chapter3/head.def(1)"head/a A (aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al) d a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aspan class="error" title="Parse error: [term] expected after [sym=] (in [term])"/spanspan class="error" title="Parse error: [term] expected after [sym=] (in [term])"/span a.
 #A #a #d #l normalize // qed.
 
-example ex_tail: a href="cic:/matita/tutorial/chapter3/tail.def(1)"tail/a ? (a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"cons/a ? a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a a title="nil" href="cic:/fakeuri.def(1)"[/a]) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="nil" href="cic:/fakeuri.def(1)"[/a].
+img class="anchor" src="icons/tick.png" id="ex_tail"example ex_tail: a href="cic:/matita/tutorial/chapter3/tail.def(1)"tail/a ? (a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"cons/a ? a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a a title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a.
 normalize // qed.
 
-theorem associative_append: 
+img class="anchor" src="icons/tick.png" id="associative_append"theorem associative_append: 
 ∀A.∀l1,l2,l3: a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A. (l1 a title="append" href="cic:/fakeuri.def(1)"@/a l2) a title="append" href="cic:/fakeuri.def(1)"@/a l3 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l1 a title="append" href="cic:/fakeuri.def(1)"@/a (l2 a title="append" href="cic:/fakeuri.def(1)"@/a l3).
 #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.
+img class="anchor" src="icons/tick.png" id="a_append"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)":/aa title="cons" href="cic:/fakeuri.def(1)":/aa title="nil" href="cic:/fakeuri.def(1)"[/aa 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)":/aa title="cons" href="cic:/fakeuri.def(1)":/al.
 // 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.
+img class="anchor" src="icons/tick.png" id="append_cons"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)":/aa title="cons" href="cic:/fakeuri.def(1)":/al1)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)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a)) a title="append" href="cic:/fakeuri.def(1)"@/a l1.
 // qed. 
 
 (* Other typical functions over lists are those computing the length 
 of a list, and the function returning the nth element *)
 
-let rec length (A:Type[0]) (l:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A) on l ≝ 
+img class="anchor" src="icons/tick.png" id="length"let rec length (A:Type[0]) (l:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A) on l ≝ 
 match l with 
   [ nil ⇒ a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a
     | cons a tl ⇒ a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a (length A tl)].
 
-let rec nth n (A:Type[0]) (l:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A) (d:A)  ≝  
+img class="anchor" src="icons/tick.png" id="nth"let rec nth n (A:Type[0]) (l:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A) (d:A)  ≝  
   match n with
     [O ⇒ a href="cic:/matita/tutorial/chapter3/head.def(1)"head/a A l d
     |S m ⇒ nth m A (a href="cic:/matita/tutorial/chapter3/tail.def(1)"tail/a A l) d].
 
-example ex_length: a href="cic:/matita/tutorial/chapter3/length.fix(0,1,1)"length/a ? (a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"cons/a ? a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a a title="nil" href="cic:/fakeuri.def(1)"[/a]) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a.
+img class="anchor" src="icons/tick.png" id="ex_length"example ex_length: a href="cic:/matita/tutorial/chapter3/length.fix(0,1,1)"length/a ? (a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"cons/a ? a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a a title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a.
 normalize // qed.
 
-example ex_nth: a href="cic:/matita/tutorial/chapter3/nth.fix(0,0,2)"nth/a (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a) ? (a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"cons/a ? (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a) (a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"cons/a ? a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a a title="nil" href="cic:/fakeuri.def(1)"[/aspan class="error" title="Parse error: [term] expected after [sym[] (in [term])"/span])) a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a.
+img class="anchor" src="icons/tick.png" id="ex_nth"example ex_nth: a href="cic:/matita/tutorial/chapter3/nth.fix(0,0,2)"nth/a (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a) ? (a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"cons/a ? (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a) (a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"cons/a ? a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a a title="nil" href="cic:/fakeuri.def(1)"[/aspan class="error" title="Parse error: [term] expected after [sym[] (in [term])"/spana title="nil" href="cic:/fakeuri.def(1)"]/a)) a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a.
 normalize // qed.
 
 (* Proving that the length of l1@l2 is the sum of the lengths of l1
 and l2 just requires a trivial induction on the first list. *)
 
- lemma  length_add: ∀A.∀l1,l2:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A. 
+ img class="anchor" src="icons/tick.png" id="length_add"lemma  length_add: ∀A.∀l1,l2:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A. 
   a href="cic:/matita/tutorial/chapter3/length.fix(0,1,1)"length/a ? (l1a title="append" href="cic:/fakeuri.def(1)"@/al2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"add/a (a href="cic:/matita/tutorial/chapter3/length.fix(0,1,1)"length/a ? l1) (a href="cic:/matita/tutorial/chapter3/length.fix(0,1,1)"length/a ? l2).
 #A #l1 elim l1 normalize // qed. 
 
@@ -147,22 +147,22 @@ 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 *)
 
-definition is_nil: ∀A:Type[0].a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A → Prop ≝
-λA.λl.match l with [ nil ⇒ l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="nil" href="cic:/fakeuri.def(1)"[/a] | cons hd tl ⇒ (l a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a title="nil" href="cic:/fakeuri.def(1)"[/a])].
+img class="anchor" src="icons/tick.png" id="is_nil"definition is_nil: ∀A:Type[0].a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A → Prop ≝
+λA.λl.match l with [ nil ⇒ l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a | cons hd tl ⇒ (l a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a)].
 
 (* 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 → a title="logical not" href="cic:/fakeuri.def(1)"¬/aP) → a title="logical not" href="cic:/fakeuri.def(1)"¬/aP.
+img class="anchor" src="icons/tick.png" id="neg_aux"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 % /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].
+img class="anchor" src="icons/tick.png" id="diff_cons_nil"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)":/aa 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)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a.
 #A #l #a @a href="cic:/matita/tutorial/chapter3/neg_aux.def(3)"neg_aux/a #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 (a href="cic:/matita/tutorial/chapter3/is_nil.def(1)"is_nil/a ? (aa title="cons" href="cic:/fakeuri.def(1)":/a:l))) 
+(change with (a href="cic:/matita/tutorial/chapter3/is_nil.def(1)"is_nil/a ? (aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al))) 
 (* Now, we rewrite with Heq, obtaining (is_nil A []), that reduces to the trivial 
 goal [] = [] *)
 >Heq // qed.
@@ -177,8 +177,8 @@ False_ind: ∀P.False → P to the current goal, that breaks down to prove False
 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: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].
+img class="anchor" src="icons/tick.png" id="nil_to_nil"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)"[/aa 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)"[/aa 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)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a.
 #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. 
 
 (* 
@@ -188,14 +188,14 @@ acting over lists. A typical example is the map function, taking a function
 f:A → B, a list l = [a1; a2; ... ; an] and returning the list 
 [f a1; f a2; ... ; f an]. *)
 
-let rec map (A,B:Type[0]) (f: A → B) (l:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A) on l: a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a B ≝
- match l with [ nil ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a] | cons x tl ⇒ f x a title="cons" href="cic:/fakeuri.def(1)":/a: (map A B f tl)].
+img class="anchor" src="icons/tick.png" id="map"let rec map (A,B:Type[0]) (f: A → B) (l:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A) on l: a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a B ≝
+ match l with [ nil ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a | cons x tl ⇒ f x a title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/a (map A B f tl)].
 
 (* Another major example is the fold function, that taken a list 
 l = [a1; a2; ... ;an], a base value b:B, and a function f: A → B → B returns 
 (f a1 (f a2 (... (f an b)...))). *)
 
-let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A) on l :B ≝  
+img class="anchor" src="icons/tick.png" id="foldr"let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A) on l :B ≝  
   match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)].
 
 (* As an example of application of foldr, let us use it to define a filter 
@@ -205,21 +205,21 @@ foldr should be (list A), the base value is [], and f: A → list A →list A is
 the function that taken x and l returns x::l, if x satisfies the test, and l 
 otherwise. We use an if_then_else function included from bool.ma to this purpose. *)
 
-definition filter ≝ 
+img class="anchor" src="icons/tick.png" id="filter"definition filter ≝ 
   λT.λp:T → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a.
-  a href="cic:/matita/tutorial/chapter3/foldr.fix(0,4,1)"foldr/a T (a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a T) (λx,l0. if p x then xa title="cons" href="cic:/fakeuri.def(1)":/a:l0 else l0) a title="nil" href="cic:/fakeuri.def(1)"[/a].
+  a href="cic:/matita/tutorial/chapter3/foldr.fix(0,4,1)"foldr/a T (a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a T) (λx,l0. if p x then xa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al0 else l0) a title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a.
 
 (* Here are a couple of simple lemmas on the behaviour of the filter function. 
 It is often convenient to state such lemmas, in order to be able to use rewriting
 as an alternative to reduction in proofs: reduction is a bit difficult to control.
 *)
 
-lemma filter_true : ∀A,l,a,p. p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → 
-  a href="cic:/matita/tutorial/chapter3/filter.def(2)"filter/a A p (aa title="cons" href="cic:/fakeuri.def(1)":/a:l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a a title="cons" href="cic:/fakeuri.def(1)":/a: a href="cic:/matita/tutorial/chapter3/filter.def(2)"filter/a A p l.
+img class="anchor" src="icons/tick.png" id="filter_true"lemma filter_true : ∀A,l,a,p. p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → 
+  a href="cic:/matita/tutorial/chapter3/filter.def(2)"filter/a A p (aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a a title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/a a href="cic:/matita/tutorial/chapter3/filter.def(2)"filter/a A p l.
 #A #l #a #p #pa (elim l) normalize >pa // qed.
 
-lemma filter_false : ∀A,l,a,p. p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → 
-  a href="cic:/matita/tutorial/chapter3/filter.def(2)"filter/a A p (aa title="cons" href="cic:/fakeuri.def(1)":/a:l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter3/filter.def(2)"filter/a A p l.
+img class="anchor" src="icons/tick.png" id="filter_false"lemma filter_false : ∀A,l,a,p. p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → 
+  a href="cic:/matita/tutorial/chapter3/filter.def(2)"filter/a A p (aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter3/filter.def(2)"filter/a A p l.
 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
 
 (* As another example, let us redefine the map function using foldr. The
@@ -227,7 +227,7 @@ result type B is (list B), the base value b is [], and the fold function
 of type A → list B → list B is the function mapping a and l to (f a)::l.
 *)
 
-definition map_again ≝ λA,B,f,l. a href="cic:/matita/tutorial/chapter3/foldr.fix(0,4,1)"foldr/a A (a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a B) (λa,l.f aa title="cons" href="cic:/fakeuri.def(1)":/a:l) a title="nil" href="cic:/fakeuri.def(1)"[/a] l.
+img class="anchor" src="icons/tick.png" id="map_again"definition map_again ≝ λA,B,f,l. a href="cic:/matita/tutorial/chapter3/foldr.fix(0,4,1)"foldr/a A (a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a B) (λa,l.f aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al) a title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a l.
 
 (* 
 h2 class="section"Extensional equality/h2
@@ -240,19 +240,19 @@ and they are clearly different. What we would like to say is that the two
 programs behave in the same way: this is a different, extensional equality 
 that can be defined in the following way. *)
 
-definition ExtEq ≝ λA,B:Type[0].λf,g:A→B.∀a:A.f a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a g a.
+img class="anchor" src="icons/tick.png" id="ExtEq"definition ExtEq ≝ λA,B:Type[0].λf,g:A→B.∀a:A.f a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a g a.
 
 (* Proving that map and map_again are extentionally equal in the 
 previous sense can be proved by a trivial structural induction on the list *)
 
-lemma eq_maps: ∀A,B,f. a href="cic:/matita/tutorial/chapter3/ExtEq.def(1)"ExtEq/a ?? (a href="cic:/matita/tutorial/chapter3/map.fix(0,3,1)"map/a A B f) (a href="cic:/matita/tutorial/chapter3/map_again.def(2)"map_again/a A B f).
+img class="anchor" src="icons/tick.png" id="eq_maps"lemma eq_maps: ∀A,B,f. a href="cic:/matita/tutorial/chapter3/ExtEq.def(1)"ExtEq/a ?? (a href="cic:/matita/tutorial/chapter3/map.fix(0,3,1)"map/a A B f) (a href="cic:/matita/tutorial/chapter3/map_again.def(2)"map_again/a A B f).
 #A #B #f #n (elim n) normalize // qed. 
 
 (* Let us make another remark about extensional equality. It is clear that,
 if f is extensionally equal to g, then (map A B f) is extensionally equal to
 (map A B g). Let us prove it. *)
 
-theorem eq_map : ∀A,B,f,g. a href="cic:/matita/tutorial/chapter3/ExtEq.def(1)"ExtEq/a A B f g → a href="cic:/matita/tutorial/chapter3/ExtEq.def(1)"ExtEq/a ?? (a href="cic:/matita/tutorial/chapter3/map.fix(0,3,1)"map/a span style="text-decoration: underline;"/spanA B f) (a href="cic:/matita/tutorial/chapter3/map.fix(0,3,1)"map/a A B g).
+img class="anchor" src="icons/tick.png" id="eq_map"theorem eq_map : ∀A,B,f,g. a href="cic:/matita/tutorial/chapter3/ExtEq.def(1)"ExtEq/a A B f g → a href="cic:/matita/tutorial/chapter3/ExtEq.def(1)"ExtEq/a ?? (a href="cic:/matita/tutorial/chapter3/map.fix(0,3,1)"map/a span style="text-decoration: underline;"/spanA B f) (a href="cic:/matita/tutorial/chapter3/map.fix(0,3,1)"map/a A B g).
 #A #B #f #g #eqfg
  
 (* the relevant point is that we cannot proceed by rewriting f with g via
@@ -275,7 +275,7 @@ A really convenient tool is the following combination of fold and filter,
 that essentially allow you to iterate on every subset of a given enumerated
 (finite) type, represented as a list. *) 
 
- let rec fold (A,B:Type[0]) (op:B→B→B) (b:B) (p:A→a href="cic:/matita/basics/bool/bool.ind(1,0,0)" title="null"bool/a) (f:A→B) (l:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A) on l:B ≝  
+ img class="anchor" src="icons/tick.png" id="fold"let rec fold (A,B:Type[0]) (op:B→B→B) (b:B) (p:A→a href="cic:/matita/basics/bool/bool.ind(1,0,0)" title="null"bool/a) (f:A→B) (l:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A) on l:B ≝  
  match l with 
   [ nil ⇒ b 
   | cons a l ⇒ if p a then op (f a) (fold A B op b p f l) else
@@ -294,38 +294,38 @@ for @{'fold $op $nil (λ${ident i}.true) (λ${ident i}. $f) $l}.
 
 interpretation "\fold" 'fold op nil p f l = (fold ? ? op nil p f l).
 
-theorem fold_true: 
+img class="anchor" src="icons/tick.png" id="fold_true"theorem fold_true: 
 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → 
-  a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ aa title="cons" href="cic:/fakeuri.def(1)":/a:l| p i} (f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
-    op (f a) a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ l| p i} (f i). 
+  a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al| p ia title="\fold" href="cic:/fakeuri.def(1)"}/a (f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
+    op (f a) a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ l| p ia title="\fold" href="cic:/fakeuri.def(1)"}/a (f i). 
 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
 
-theorem fold_false: 
+img class="anchor" src="icons/tick.png" id="fold_false"theorem fold_false: 
 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f.
-p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ aa title="cons" href="cic:/fakeuri.def(1)":/a:l| p i} (f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
-  a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ l| p i} (f i).
+p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al| p ia title="\fold" href="cic:/fakeuri.def(1)"}/a (f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
+  a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ l| p ia title="\fold" href="cic:/fakeuri.def(1)"}/a (f i).
 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
 
-theorem fold_filter: 
+img class="anchor" src="icons/tick.png" id="fold_filter"theorem fold_filter: 
 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A →B.
-  a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ l| p i} (f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
-    a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ (a href="cic:/matita/tutorial/chapter3/filter.def(2)"filter/a A p l)} (f i).
+  a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ l| p ia title="\fold" href="cic:/fakeuri.def(1)"}/a (f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
+    a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ (a href="cic:/matita/tutorial/chapter3/filter.def(2)"filter/a A p l)a title="\fold" href="cic:/fakeuri.def(1)"}/a (f i).
 #A #B #a #l #p #op #nil #f elim l //  
 #a #tl #Hind cases(a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (p a)) #pa 
   [ >a href="cic:/matita/tutorial/chapter3/filter_true.def(3)"filter_true/a // > a href="cic:/matita/tutorial/chapter3/fold_true.def(3)"fold_true/a // >a href="cic:/matita/tutorial/chapter3/fold_true.def(3)"fold_true/a //
   | >a href="cic:/matita/tutorial/chapter3/filter_false.def(3)"filter_false/a // >a href="cic:/matita/tutorial/chapter3/fold_false.def(3)"fold_false/a // ]
 qed.
 
-record Aop (A:Type[0]) (nil:A) : Type[0] ≝
+img class="anchor" src="icons/tick.png" id="Aop"record Aop (A:Type[0]) (nil:A) : Type[0] ≝
 {op :2> A → A → A; 
   nill:∀a. op nil a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a; 
   nilr:∀a. op a nil a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a;
   assoc: ∀a,b,c.op a (op b c) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a op (op a b) c
 }.
 
-theorem fold_sum: ∀A,B. ∀I,J:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A.∀nil.∀op:a href="cic:/matita/tutorial/chapter3/Aop.ind(1,0,2)"Aop/a B nil.∀f:A → B.
- op (a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ I} (f i)) (a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ J} (f i)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
-   a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ (Ia title="append" href="cic:/fakeuri.def(1)"@/aJ)} (f i).
+img class="anchor" src="icons/tick.png" id="fold_sum"theorem fold_sum: ∀A,B. ∀I,J:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A.∀nil.∀op:a href="cic:/matita/tutorial/chapter3/Aop.ind(1,0,2)"Aop/a B nil.∀f:A → B.
+ op (a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ Ia title="\fold" href="cic:/fakeuri.def(1)"}/a (f i)) (a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ Ja title="\fold" href="cic:/fakeuri.def(1)"}/a (f i)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
+   a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ (Ia title="append" href="cic:/fakeuri.def(1)"@/aJ)a title="\fold" href="cic:/fakeuri.def(1)"}/a (f i).
 #A #B #I #J #nil #op #f (elim I) normalize 
   [>a href="cic:/matita/tutorial/chapter3/nill.fix(0,2,2)"nill/a//|#a #tl #Hind <a href="cic:/matita/tutorial/chapter3/assoc.fix(0,2,2)"assoc/a //]
 qed.
\ No newline at end of file