commit by user andrea

diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma
index a32e29ba64e634709c6ed9acf9d04384e4d0ac7d..fba2b61ca904072bd5f2d8e700d3cf96a5b7ef49 100644 (file)
--- a/weblib/tutorial/chapter2.ma
+++ b/weblib/tutorial/chapter2.ma
@@ -1,15 +1,99 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department of the University of Bologna, Italy.                     
-    ||I||                                                                 
-    ||T||  
-    ||A||  This file is distributed under the terms of the 
-    \   /  GNU General Public License Version 2        
-     \ /      
-      V_______________________________________________________________ *)
-
-include "arithmetics/nat.ma".
+include "basics/logic.ma".
+
+(* Most of the types we have seen so far are enumerated types, composed by 
+a finite set of alternatives, and records, composed by tuples of
+heteregoneous elements. A more interesting case of type definition is
+when some of the rules defining its elements are recursive, i.e. they
+allow the formation of more elements of the type in terms of the already
+defined ones. The most typical case is provided by the natural numbers,
+that can be defined as the smallest set generated by a constant 0 and a
+successor function from natural numbers to natural numbers *)
+
+inductive nat : Type[0] ≝ 
+| O :nat
+| S: nat →nat.
+
+(* The two terms O and S are called constructors: they define the
+signature of the type, whose objects are the elements freely generated
+by means of them. So, examples of natural numbers are O, S O, S (S O), 
+S (S (S O)) and so on. 
+
+The language of Matita allows the definition of well founded recursive functions
+over inductive types; in order to guarantee termination of recursion you are
+only allowed to make recursive calls on structurally smaller arguments than the 
+ones your received in input. 
+Most mathematical functions can be naturally defined in this way. For instance, 
+the sum of two natural numbers can be defined as follows *)
+
+let rec add n m ≝ 
+match n with
+[ O ⇒ m
+| S a ⇒ \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (add a m)
+].
+
+(* It is worth to observe that the previous algorithm works by recursion over the
+first argument. This means that, for instance, (add 0 x) will reduce to x, as expected, 
+but (add x 0) is stack. How can we prove that, for a generic x, (add x 0) = x? The 
+mathematical tool do it is called induction. The induction principle states that, 
+given a property P(n) over natural numbers, if we prove P(0) and prove that, for any 
+m, P(m) implies P(S m), than we can conclude P(n) for any n. 
+
+The elim tactic, allow you to apply induction in a vcery simple way. If your
+goal is P(n), the invocation of
+  elim n
+will break down your task to prove the two subgoals P(0) and ∀m.P(m) → P(S m).
+Let us apply it to our case *)
+
+lemma add_0: ∀a. \ 5a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"\ 6add\ 5/a\ 6 a \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a.
+#a elim a
+
+(* If you stop the computation here, you will see on the right the two subgoals 
+    - add O O = O
+    - ∀x. add x 0 = x → add (S x) O = S x
+After normalization, both goals are trivial.
+*)
+
+normalize // qed.
+
+ (* In a similar way, it is convenient to state a lemma about the behaviour of add when the 
+second argument is not zero. *)
+
+lemma add_S : ∀a,b. \ 5a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"\ 6add\ 5/a\ 6 a (\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 b) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"\ 6add\ 5/a\ 6 a b).
+
+(* In the same way as before, we proceed by induction over a. *)
+
+#a #b elim a normalize //
+qed. 
+
+(* We are now in the position to prove the commutativity of the sum *)
+
+theorem add_comm : ∀a,b. \ 5a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"\ 6add\ 5/a\ 6 a b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"\ 6add\ 5/a\ 6 b a.
+#a elim a normalize
+
+(* We have two sub goals:
+  G1: ∀b. b = add b O
+  G2: ∀x.(∀b. add x b = add b x) → ∀b. S (add x b) = add b (S x). 
+G1 is just our lemma add_O. For G2, we start introducing x and the induction
+hypothesis IH; then, the goal is proved by rewriting using add_S and IH.
+For Matita, the task is trivial and we can simply close the goal with // *)
+
+// qed.
+
+(* Let us now define the following function: *)
+
+definition twice ≝ λn.\ 5a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"\ 6add\ 5/a\ 6 n n. 
+
+(* We are interested to prove that for any natural number m there 
+exists a natural number m that is the integer half of m. This
+will give us the opportunity to introduce new connectives
+and quantifiers, and later on to make some interesting consideration
+on proofs and computations. *)
+
+theorem ex_half: ∀n.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6m. n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/twice.def(2)"\ 6twice\ 5/a\ 6 m \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter2/twice.def(2)"\ 6twice\ 5/a\ 6 m).
+
+
+
+ include "basics.ma".
 include "basics/list.ma".
 
 interpretation "iff" 'iff a b = (iff a b).