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 *)
+(* 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 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 *)
+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
| 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.
+(* 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
+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.
normalize // qed.
- (* In a similar way, it is convenient to state a lemma about the behaviour of add when the
+(* 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).
(* 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.
+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.
IH: ∃m. x = add m m ∨ x = S (add m m)
At this point we should assume the existence of m enjoying the inductive hypothesis. To
eliminate the existential from the context we can just use the case tactic. This situation where
-we introduce something into the context and immediately eliminate it by case analysis is
-so frequent that Matita provides a convenient shorthand: you can just type a single "*".
+we introduce something into the context and immediately eliminate it by case analysis is so
+frequent that Matita provides a convenient shorthand: you can just type a single "*".
The star symbol should be reminiscent of an explosion: the idea is that you have a structured
hypothesis, and you ask to explode it into its constituents. In the case of the existential,
it allows to pass from a goal of the shape
projects / helm.git / commitdiff