weblib/tutorial/chapter2.ma

   1 include "basics/logic.ma".
   2
   3 (* Most of the types we have seen so far are enumerated types, composed by
   4 a finite set of alternatives, and records, composed by tuples of
   5 heteregoneous elements. A more interesting case of type definition is
   6 when some of the rules defining its elements are recursive, i.e. they
   7 allow the formation of more elements of the type in terms of the already
   8 defined ones. The most typical case is provided by the natural numbers,
   9 that can be defined as the smallest set generated by a constant 0 and a
  10 successor function from natural numbers to natural numbers *)
  11
  12 inductive nat : Type[0] ≝
  13 | O :nat
  14 | S: nat →nat.
  15
  16 (* The two terms O and S are called constructors: they define the
  17 signature of the type, whose objects are the elements freely generated
  18 by means of them. So, examples of natural numbers are O, S O, S (S O),
  19 S (S (S O)) and so on.
  20
  21 The language of Matita allows the definition of well founded recursive functions
  22 over inductive types; in order to guarantee termination of recursion you are
  23 only allowed to make recursive calls on structurally smaller arguments than the
  24 ones your received in input.
  25 Most mathematical functions can be naturally defined in this way. For instance,
  26 the sum of two natural numbers can be defined as follows *)
  27
  28 let rec add n m ≝
  29 match n with
  30 [ O ⇒ m
  31 | S a ⇒ \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (add a m)
  32 ].
  33
  34 (* It is worth to observe that the previous algorithm works by recursion over the
  35 first argument. This means that, for instance, (add 0 x) will reduce to x, as expected,
  36 but (add x 0) is stack. How can we prove that, for a generic x, (add x 0) = x? The
  37 mathematical tool do it is called induction. The induction principle states that,
  38 given a property P(n) over natural numbers, if we prove P(0) and prove that, for any
  39 m, P(m) implies P(S m), than we can conclude P(n) for any n.
  40
  41 The elim tactic, allow you to apply induction in a vcery simple way. If your
  42 goal is P(n), the invocation of
  43   elim n
  44 will break down your task to prove the two subgoals P(0) and ∀m.P(m) → P(S m).
  45 Let us apply it to our case *)
  46
  47 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.
  48 #a elim a
  49
  50 (* If you stop the computation here, you will see on the right the two subgoals
  51     - add O O = O
  52     - ∀x. add x 0 = x → add (S x) O = S x
  53 After normalization, both goals are trivial.
  54 *)
  55
  56 normalize // qed.
  57
  58  (* In a similar way, it is convenient to state a lemma about the behaviour of add when the
  59 second argument is not zero. *)
  60
  61 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).
  62
  63 (* In the same way as before, we proceed by induction over a. *)
  64
  65 #a #b elim a normalize //
  66 qed.
  67
  68 (* We are now in the position to prove the commutativity of the sum *)
  69
  70 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.
  71 #a elim a normalize
  72
  73 (* We have two sub goals:
  74   G1: ∀b. b = add b O
  75   G2: ∀x.(∀b. add x b = add b x) → ∀b. S (add x b) = add b (S x).
  76 G1 is just our lemma add_O. For G2, we start introducing x and the induction
  77 hypothesis IH; then, the goal is proved by rewriting using add_S and IH.
  78 For Matita, the task is trivial and we can simply close the goal with // *)
  79
  80 // qed.
  81
  82 (* Let us now define the following function: *)
  83
  84 definition twice ≝ λn.\ 5a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"\ 6add\ 5/a\ 6 n n.
  85
  86 (* We are interested to prove that for any natural number m there
  87 exists a natural number m that is the integer half of m. This
  88 will give us the opportunity to introduce new connectives
  89 and quantifiers, and later on to make some interesting consideration
  90 on proofs and computations. *)
  91
  92 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).
  93 #n elim n normalize
  94
  95 (* *)
  96   [@(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6) %1 //
  97 (* *)
  98  |#x * #m * #eqx
  99     [@(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … m) /2/ | @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m)) normalize /2/
 100   ]
 101 qed.