-include "basics/logic.ma".
+include "basics/types.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 you 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 O x) will reduce to x, as expected, but (add x O)
+is stack. How can we prove that, for a generic x, (add x O) = 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 very 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.
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. *)
+(* 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).
#n elim n normalize
-(* *)
+(* We proceed by induction on n, that breaks down to the following goals:
+ G1: ∃m.O = add O O ∨ O = S (add m m)
+ G2: ∀x.(∃m. x = add m m ∨ x = S (add m m))→ ∃m. S x = add m m ∨ S x = S (add m m)
+The only way we have to prove an existential goal is by exhibiting the witness, that in the case
+of first goal is O. We do it by apply the term called ex_intro instantiated by the witness.
+Then, it is clear that we must follow the left branch of the disjunction. One way to do it is by
+applying the term or_introl, that is the first constructor of the disjunction. However,
+remembering the names of constructors can be annyoing: we can invoke the application of the n-th
+constructor of an inductive type (inferred by the current goal) by typing %n. At this point
+we are left with the subgoal O = add O O, that is closed by computation.
+It is worth to observe that invoking automation at depth /3/ would also automatically close G1.
+*)
[@(\ 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 //
-(* *)
- |#x * #m * #eqx
- [@(\ 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/
+
+(* The case of G2 is more complex. We should start introducing x and the inductive hypothesis
+ 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 "*".
+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
+ (∃x.P x) → Q
+to a goal of the shape
+ ∀x.P x → Q
+*)
+ |#x *
+(* At this point we are left with a new goal with the following shape
+ G3: ∀m. x = add m m ∨ x = S (add m m) → ....
+We should introduce m, the hypothesis H: x = add m m ∨ x = S (add m m), and then reason by
+cases on this hypothesis. It is the same situation as before: we explode the disjunctive
+hypothesis into its possible consituents. In the case of a disjunction, the * tactic allows
+to pass from a goal of the form
+ A∨B → Q
+to two subgoals of the form
+ A → Q and B → Q
+*)
+ #m * #eqx
+(* In the first subgoal, we are under the assumption that x = add m m. The half of (S x)
+is hence m, and we have to prove the right branch of the disjunction.
+In the second subgoal, we are under the assumption that x = S (add m m). The halh of (S x)
+is hence (S m), and have to follow the left branch of the disjunction.
+*)
+ [@(\ 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/
]
qed.
+
+(* Instead of proving the existence of a number corresponding to the half of n, we could
+be interested in computing it. The best way to do it is to define this division operation
+together with the remainder, that is 0 if the input term is even, and 1 if the input term
+is odd. Since we must return a pair, we could use a suitably defined record type, or simply
+a product type N × N, defined in the basic library. The product type is just a sort of
+general purpose record, with standard fields fst and snd, called projections. *)
+
+let rec div2 n ≝
+match n with
+[ O ⇒ <O,O>
+| S a ⇒ <O,O>
+].
+
+ let p \def(div2 a) in
+ match (snd p) with
+ [ O ⇒ <fst p,1>
+ | S b \Rightarrow <S(fst p),O>
+ ]
+].
\ No newline at end of file
projects / helm.git / blobdiff