From: matitaweb Date: Wed, 7 Mar 2012 10:13:47 +0000 (+0000) Subject: commit by user andrea X-Git-Tag: make_still_working~1885 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=2979a29642a4b0b16834ec69177813a6c6051e7e commit by user andrea --- diff --git a/weblib/tutorial/chapter1.ma b/weblib/tutorial/chapter1.ma index c46004f24..7a961d4d2 100644 --- a/weblib/tutorial/chapter1.ma +++ b/weblib/tutorial/chapter1.ma @@ -63,7 +63,9 @@ name for further reference, and we call it "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. -(* If you stop the execution here you will see a new window on the right side +(* +h2 class="section"The goal window/h2 +If you stop the execution here you will see a new window on the right side of the screen: it is the goal window, providing a sequent like representation of the form @@ -104,7 +106,7 @@ lemma west_to_east : a href="cic:/matita/tutorial/chapter1/opposite.def(1)"opp // qed. (* -h2 class="section"Case analysis/h2 +h2 class="section"Introduction/h2 A slightly more complex problem consists in proving that opposite is idempotent *) 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. @@ -120,7 +122,10 @@ wish to rename x into b (since it is a bank), we just type #b. *) (* See the effect of the execution in the goal window on the right: b has been added to the context (replacing x in the conclusion); moreover its implicit type "bank" has been made explicit. +*) +(* +h2 class="section"Case analysis/h2 But how are we supposed to proceed, now? Simplification cannot help us, since b is a variable: just try to call normalize and you will see that it has no effect. The point is that we must proceed by cases according to the possible values of b, @@ -265,8 +270,9 @@ expect to need several moves to transfer all items from a bank to the other, so we should start our proof by applying "more". Matita syntax for invoking the application of a property named foo is to write "@foo". In general, the philosophy of Matita is to describe each proof of a property P as a structured collection of -results required for proving P, prefixed by simple modalities (<,@,...) explaining -the way the result is used (e.g. for rewriting, in an applicative step, and so on). +objects involved in the proof, prefixed by simple modalities (#,<,@,...) explaining +the way it is actually used (e.g. for introduction, rewriting, in an applicative +step, and so on). *) 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.