From: matitaweb Date: Wed, 7 Mar 2012 10:01:30 +0000 (+0000) Subject: Added sections in chapter 1. X-Git-Tag: make_still_working~1886 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=10b08809fd7b78ff21f020911b7ec383eb4f1f0d;p=helm.git Added sections in chapter 1. --- diff --git a/weblib/tutorial/chapter1.ma b/weblib/tutorial/chapter1.ma index 9043bdad7..c46004f24 100644 --- a/weblib/tutorial/chapter1.ma +++ b/weblib/tutorial/chapter1.ma @@ -1,4 +1,5 @@ -(* +(* +h1Matita Interactive Tutorial/h1 This is an interactive tutorial. To let you interact on line with the system, you must first of all register yourself. @@ -15,15 +16,19 @@ a file. The play button is meant to process the script up to a position previously selected by the user; the bottom button execute the whole script. That's it: we arespan style="font-family: Verdana,sans-serif;" /spannow ready to start. -The first thing to say is that in a system like Matita's very few things are -built-in: not even booleans or logical connectives. The main philosophy of the -system is to let you define your own data-types and functions using a powerful -computational mechanism based on the declaration of inductive types. +h2 class="section"Data types, functions and theorems/h2 +Matita is both a programming language and a theorem proving environment: +you define datatypes and programs, and then prove properties on them. +Very few things are built-in: not even booleans or logical connectives +(but you may of course use libraries, as in normal programming languages). +The main philosophy of the system is to let you define your own data-types +and functions using a powerful computational mechanism based on the +declaration of inductive types. Let us start this tutorial with a simple example based on the following well known problem. -h2 class="section"The goat, the wolf and the cabbage/h2 +bThe goat, the wolf and the cabbage/b A farmer need to transfer a goat, a wolf and a cabbage across a river, but there is only one place available on his boat. Furthermore, the goat will eat the cabbage if they are left alone on the same bank, and similarly the wolf will eat @@ -98,8 +103,9 @@ it. *) 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. -(* A slightly more complex problem consists in proving that opposite is -idempotent *) +(* +h2 class="section"Case analysis/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. @@ -135,7 +141,9 @@ them in turn, in a way that will be described at the end of this section. // qed. -(* Instead of working with functions, it is sometimes convenient to work with +(* +h2 class="section"Predicates/h2 +Instead of working with functions, it is sometimes convenient to work with predicates. For instance, instead of defining a function computing the opposite bank, we could declare a predicate stating when two banks are opposite to each other. Only two cases are possible, leading naturally to the following @@ -169,7 +177,9 @@ automation *) cases oppab // qed. -(* Let us come to the opposite direction. *) +(* +h2 class="section"Rewriting/h2 +Let us come to the opposite direction. *) 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. @@ -189,6 +199,7 @@ opposite b into a, we would have typed "