X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftutorial%2Fchapter1.ma;h=4cf145d60f53f72c70b08846444700cd9b1afc7e;hb=84b38ac86f1f92b91ae8913cd0dbcb5c3485dc3a;hp=ef764ceae2aa5bff3b8e1375c6a9c84290d498c4;hpb=d08155a49dea388057f68f8f81c8bdf9b0b98d7b;p=helm.git

diff --git a/weblib/tutorial/chapter1.ma b/weblib/tutorial/chapter1.ma
index ef764ceae..4cf145d60 100644
--- a/weblib/tutorial/chapter1.ma
+++ b/weblib/tutorial/chapter1.ma
@@ -44,24 +44,24 @@ few preliminary notions not worth discussing for the moment.
 
 include "basics/logic.ma".
 
-inductive bank: Type[0] ≝
+img class="anchor" src="icons/tick.png" id="bank"inductive bank: Type[0] ≝
 | east : bank 
 | west : bank.
 
 (* We can now define a simple function computing, for each bank of the river, the
 opposite one. *)
 
-definition opposite ≝ λs.
+img class="anchor" src="icons/tick.png" id="opposite"definition opposite ≝ λs.
 match s with
-  [ east ⇒ west
-  | west ⇒ east
+  [ east ⇒ a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a
+  | west ⇒ a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a
   ].
 
 (* Functions are live entities, and can be actually computed. To check this, let
 us state the property that the opposite bank of east is west; every lemma needs a 
 name for further reference, and we call it "east_to_west". *)
  
-lemma east_to_west : opposite east = west.
+img class="anchor" src="icons/tick.png" id="east_to_west"lemma east_to_west : a href="cic:/matita/tutorial/chapter1/opposite.def(1)"opposite/a a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a.
 
 (* 
 h2 class="section"The goal window/h2
@@ -102,14 +102,14 @@ lemma performing some book-keeping operations.
 In this case, we avoid the unnecessary simplification step: // will take care of 
 it. *) 
 
-lemma west_to_east : opposite west = east.
+img class="anchor" src="icons/tick.png" id="west_to_east"lemma west_to_east : a href="cic:/matita/tutorial/chapter1/opposite.def(1)"opposite/a a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a.
 // qed.
 
 (*
 h2 class="section"Introduction/h2
 A slightly more complex problem consists in proving that opposite is idempotent *)
 
-lemma idempotent_opposite : ∀x. opposite (opposite x) = x.
+img class="anchor" src="icons/tick.png" id="idempotent_opposite"lemma idempotent_opposite : ∀x. a href="cic:/matita/tutorial/chapter1/opposite.def(1)"opposite/a (a href="cic:/matita/tutorial/chapter1/opposite.def(1)"opposite/a x) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a x.
 
 (* we start the proof moving x from the conclusion into the context, that is a 
 (backward) introduction step. Matita syntax for an introduction step is simply 
@@ -155,9 +155,9 @@ other. Only two cases are possible, leading naturally to the following
 definition:
 *)
 
-inductive opp : bank → bank → Prop ≝ 
-| east_west : opp east west
-| west_east : opp west east.
+img class="anchor" src="icons/tick.png" id="opp"inductive opp : a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"bank/a → a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"bank/a → Prop ≝ 
+| east_west : opp a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a
+| west_east : opp a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a.
 
 (* In precisely the same way as "bank" is the smallest type containing east and
 west, opp is the smallest predicate containing the two sub-cases east_west and
@@ -169,7 +169,7 @@ Between opp and opposite we have the following relation:
     opp a b iff a = opposite b
 Let us prove it, starting from the left to right implication, first *)
 
-lemma opp_to_opposite: ∀a,b. opp a b → a = opposite b.
+img class="anchor" src="icons/tick.png" id="opp_to_opposite"lemma opp_to_opposite: ∀a,b. a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"opp/a a b → a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter1/opposite.def(1)"opposite/a b.
  
 (* We start the proof introducing a, b and the hypothesis opp a b, that we
 call oppab. *)
@@ -186,7 +186,7 @@ cases oppab // qed.
 h2 class="section"Rewriting/h2
 Let us come to the opposite direction. *)
 
-lemma opposite_to_opp: ∀a,b. a = opposite b → opp a b.
+img class="anchor" src="icons/tick.png" id="opposite_to_opp"lemma opposite_to_opp: ∀a,b. a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter1/opposite.def(1)"opposite/a b → a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"opp/a a b.
 
 (* As usual, we start introducing a, b and the hypothesis (a = opposite b), 
 that we call eqa. *)
@@ -211,44 +211,44 @@ wolf, the cabbage, and the boat. The simplest way to declare such a data type
 is to use a record.
 *)
 
-record state : Type[0] ≝
-  {goat_pos : bank;
-   wolf_pos : bank;
-   cabbage_pos: bank;
-   boat_pos : bank}.
+img class="anchor" src="icons/tick.png" id="state"record state : Type[0] ≝
+  {goat_pos : a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"bank/a;
+   wolf_pos : a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"bank/a;
+   cabbage_pos: a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"bank/a;
+   boat_pos : a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"bank/a}.
 
 (* When you define a record named foo, the system automatically defines a record 
 constructor named mk_foo. To construct a new record you pass as arguments to 
 mk_foo the values of the record fields *)
 
-definition start ≝ mk_state east east east east.
-definition end ≝ mk_state west west west west.
+img class="anchor" src="icons/tick.png" id="start"definition start ≝ a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a.
+img class="anchor" src="icons/tick.png" id="end"definition end ≝ a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a.
 
 (* We must now define the possible moves. A natural way to do it is in the form 
 of a relation (a binary predicate) over states. *)
 
-inductive move : state → state → Prop ≝
-| move_goat: ∀g,g1,w,c. opp g g1 → move (mk_state g w c g) (mk_state g1 w c g1)
+img class="anchor" src="icons/tick.png" id="move"inductive move : a href="cic:/matita/tutorial/chapter1/state.ind(1,0,0)"state/a → a href="cic:/matita/tutorial/chapter1/state.ind(1,0,0)"state/a → Prop ≝
+| move_goat: ∀g,g1,w,c. a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"opp/a g g1 → move (a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a g w c g) (a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a g1 w c g1)
   (* We can move the goat from a bank g to the opposite bank g1 if and only if the
      boat is on the same bank g of the goat and we move the boat along with it. *)
-| move_wolf: ∀g,w,w1,c. opp w w1 → move (mk_state g w c w) (mk_state g w1 c w1)
-| move_cabbage: ∀g,w,c,c1.opp c c1 → move (mk_state g w c c) (mk_state g w c1 c1)
-| move_boat: ∀g,w,c,b,b1. opp b b1 → move (mk_state g w c b) (mk_state g w c b1).
+| move_wolf: ∀g,w,w1,c. a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"opp/a w w1 → move (a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a g w c w) (a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a g w1 c w1)
+| move_cabbage: ∀g,w,c,c1.a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"opp/a c c1 → move (a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a g w c c) (a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a g w c1 c1)
+| move_boat: ∀g,w,c,b,b1. a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"opp/a b b1 → move (a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a g w c b) (a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a g w c b1).
 
 (* A state is safe if either the goat is on the same bank of the boat, or both 
 the wolf and the cabbage are on the opposite bank of the goat. *)
 
-inductive safe_state : state → Prop ≝
-| with_boat : ∀g,w,c.safe_state (mk_state g w c g)
-| opposite_side : ∀g,g1,b.opp g g1 → safe_state (mk_state g g1 g1 b).
+img class="anchor" src="icons/tick.png" id="safe_state"inductive safe_state : a href="cic:/matita/tutorial/chapter1/state.ind(1,0,0)"state/a → Prop ≝
+| with_boat : ∀g,w,c.safe_state (a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a g w c g)
+| opposite_side : ∀g,g1,b.a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"opp/a g g1 → safe_state (a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a g g1 g1 b).
 
 (* Finally, a state y is reachable from x if either there is a single move 
 leading from x to y, or there is a safe state z such that z is reachable from x 
 and there is a move leading from z to y *)
 
-inductive reachable : state → state → Prop ≝
-| one : ∀x,y.move x y → reachable x y
-| more : ∀x,z,y. span style="text-decoration: underline;"/spanreachable x z → safe_state z → span style="text-decoration: underline;"/spanmove z y → reachable x y.
+img class="anchor" src="icons/tick.png" id="reachable"inductive reachable : a href="cic:/matita/tutorial/chapter1/state.ind(1,0,0)"state/a → a href="cic:/matita/tutorial/chapter1/state.ind(1,0,0)"state/a → Prop ≝
+| one : ∀x,y.a href="cic:/matita/tutorial/chapter1/move.ind(1,0,0)"move/a x y → reachable x y
+| more : ∀x,z,y. span style="text-decoration: underline;"/spanreachable x z → a href="cic:/matita/tutorial/chapter1/safe_state.ind(1,0,0)"safe_state/a z → span style="text-decoration: underline;"/spana href="cic:/matita/tutorial/chapter1/move.ind(1,0,0)"move/a z y → reachable x y.
 
 (* 
 h2 class="section"Automation/h2
@@ -260,8 +260,8 @@ applicative nodes). In this case, there is a solution in six moves, and we
 need a few more applications to handle reachability, and side conditions. 
 The magic number to let automation work is, in this case, 9.  *)
 
-lemma problem: reachable start end.
-normalize /span class="autotactic"9span class="autotrace" trace one, more, with_boat, opposite_side, move_goat, move_wolf, move_cabbage, move_boat, east_west, west_east/span/span/ qed. 
+img class="anchor" src="icons/tick.png" id="problem"lemma problem: a href="cic:/matita/tutorial/chapter1/reachable.ind(1,0,0)"reachable/a a href="cic:/matita/tutorial/chapter1/start.def(1)"start/a a href="cic:/matita/tutorial/chapter1/end.def(1)"end/a.
+normalize /span class="autotactic"9span class="autotrace" trace a href="cic:/matita/tutorial/chapter1/reachable.con(0,1,0)"one/a, a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"more/a, a href="cic:/matita/tutorial/chapter1/safe_state.con(0,1,0)"with_boat/a, a href="cic:/matita/tutorial/chapter1/safe_state.con(0,2,0)"opposite_side/a, a href="cic:/matita/tutorial/chapter1/move.con(0,1,0)"move_goat/a, a href="cic:/matita/tutorial/chapter1/move.con(0,2,0)"move_wolf/a, a href="cic:/matita/tutorial/chapter1/move.con(0,3,0)"move_cabbage/a, a href="cic:/matita/tutorial/chapter1/move.con(0,4,0)"move_boat/a, a href="cic:/matita/tutorial/chapter1/opp.con(0,1,0)"east_west/a, a href="cic:/matita/tutorial/chapter1/opp.con(0,2,0)"west_east/a/span/span/ qed. 
 
 (* 
 h2 class="section"Application/h2
@@ -275,8 +275,8 @@ the way it is actually used (e.g. for introduction, rewriting, in an applicative
 step, and so on).
 *)
 
-lemma problem1: reachable start end.
-normalize @more
+img class="anchor" src="icons/tick.png" id="problem1"lemma problem1: a href="cic:/matita/tutorial/chapter1/reachable.ind(1,0,0)"reachable/a a href="cic:/matita/tutorial/chapter1/start.def(1)"start/a a href="cic:/matita/tutorial/chapter1/end.def(1)"end/a.
+normalize @a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"more/a
 
 (* 
 h2 class="section"Focusing/h2
@@ -314,7 +314,7 @@ We can now proceed in several possible ways. The most straightforward way is to
 provide the intermediate state, that is [east,west,west,east]. We can do it, by 
 just applying this term. *)
 
-   @(mk_state east west west east) 
+   @(a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a) 
 
 (* This application closes the goal; at present, no goal has the focus on.
 In order to act on the next goal, we must focus on it using the "|" operator. In
@@ -331,7 +331,7 @@ requires /2/ since move_goat opens an additional subgoal. By applying "]" we
 refocus on the skipped goal, going back to a situation similar to the one we
 started with. *)
 
-  | /span class="autotactic"2span class="autotrace" trace move_goat, east_west/span/span/ ] 
+  | /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/tutorial/chapter1/move.con(0,1,0)"move_goat/a, a href="cic:/matita/tutorial/chapter1/opp.con(0,1,0)"east_west/a/span/span/ ] 
 
 (* 
 h2 class="section"Implicit arguments/h2
@@ -342,20 +342,20 @@ already instatated on the next intermediate state. As first argument, we
 type a question mark that stands for an implicit argument to be guessed by
 the system. *)
 
-@(more ? (mk_state east west west west))
+@(a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"more/a ? (a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a))
 
 (* We now get three independent subgoals, all actives, and two of them are 
 trivial. Wespan style="font-family: Verdana,sans-serif;" /spancan just apply automation to all of them, and it will close the two
 trivial goals. *)
 
-/span class="autotactic"2span class="autotrace" trace opposite_side, move_boat, east_west, west_east/span/span/
+/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/tutorial/chapter1/safe_state.con(0,2,0)"opposite_side/a, a href="cic:/matita/tutorial/chapter1/move.con(0,4,0)"move_boat/a, a href="cic:/matita/tutorial/chapter1/opp.con(0,1,0)"east_west/a, a href="cic:/matita/tutorial/chapter1/opp.con(0,2,0)"west_east/a/span/span/
 
 (* Let us come to the next step, that consists in moving the wolf. Suppose that 
 instead of specifying the next intermediate state, we prefer to specify the next 
 move. In the spirit of the previous example, we can do it in the following way 
 *)
 
-@(more … (move_wolf … ))
+@(a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"more/a … (a href="cic:/matita/tutorial/chapter1/move.con(0,2,0)"move_wolf/a … ))
 
 (* The dots stand here for an arbitrary number of implicit arguments, to be 
 guessed by the system. 
@@ -367,12 +367,12 @@ be arbitrary). The simplest way to proceed is to focus on the bank, that is
 the fourth subgoal, and explicitly instatiate it. Instead of repeatedly using "|",
 we can perform focusing by typing "4:" as described by the following command. *)
 
-[4: @east] /span class="autotactic"2span class="autotrace" trace with_boat, east_west/span/span/
+[4: @a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a] /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/tutorial/chapter1/safe_state.con(0,1,0)"with_boat/a, a href="cic:/matita/tutorial/chapter1/opp.con(0,1,0)"east_west/a/span/span/
 
 (* Alternatively, we can directly instantiate the bank into the move. Let
 us complete the proof in this, very readable way. *)
 
-@(more … (move_goat west … )) /span class="autotactic"2span class="autotrace" trace with_boat, west_east/span/span/
-@(more … (move_cabbage ?? east … )) /span class="autotactic"2span class="autotrace" trace opposite_side, east_west, west_east/span/span/
-@(more … (move_boat ??? west … )) /span class="autotactic"2span class="autotrace" trace with_boat, west_east/span/span/
-@one /span class="autotactic"2span class="autotrace" trace move_goat, east_west/span/span/ qed.
\ No newline at end of file
+@(a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"more/a … (a href="cic:/matita/tutorial/chapter1/move.con(0,1,0)"move_goat/a a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a … )) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/tutorial/chapter1/safe_state.con(0,1,0)"with_boat/a, a href="cic:/matita/tutorial/chapter1/opp.con(0,2,0)"west_east/a/span/span/
+@(a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"more/a … (a href="cic:/matita/tutorial/chapter1/move.con(0,3,0)"move_cabbage/a ?? a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a … )) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/tutorial/chapter1/safe_state.con(0,2,0)"opposite_side/a, a href="cic:/matita/tutorial/chapter1/opp.con(0,1,0)"east_west/a, a href="cic:/matita/tutorial/chapter1/opp.con(0,2,0)"west_east/a/span/span/
+@(a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"more/a … (a href="cic:/matita/tutorial/chapter1/move.con(0,4,0)"move_boat/a ??? a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a … )) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/tutorial/chapter1/safe_state.con(0,1,0)"with_boat/a, a href="cic:/matita/tutorial/chapter1/opp.con(0,2,0)"west_east/a/span/span/
+@a href="cic:/matita/tutorial/chapter1/reachable.con(0,1,0)"one/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/tutorial/chapter1/move.con(0,1,0)"move_goat/a, a href="cic:/matita/tutorial/chapter1/opp.con(0,1,0)"east_west/a/span/span/ qed.
\ No newline at end of file