-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
+(******************************** Induction ***********************************)
include "basics/types.ma".
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 *)
+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,
+(* 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
-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 *)
+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 ⇒ S (add a m)
].
-(*
-Elimination
+(* Observe that the definition of a recursive function requires the keyword
+"let rec" instead of "definition". The specification of formal parameters is
+different too. In this case, they come before the body, and do not require a λ.
+If you need to specify the type of some argument, you need to enclose it in
+brackets, as follows: (n:nat).
-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 stuck.
-How can we prove that, for a generic x, (add x O) = x? The mathematical tool to 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.
+By convention, recursion is supposed to operate over the first argument (that
+means that this is the only argument that is supposed to decrease in the
+recursive calls). In case you need to work on a different argument, say foo, you
+can specify it by explicitly mention "on foo" just after the declaration of all
+parameters. *)
-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).
+(******************************* Elimination **********************************)
+
+(* 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 stuck.
+How can we prove that, for a generic x, (add x O) = x? The mathematical tool to
+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 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 *)
].
(* coercion nat_of_bool. ?? *)
-
-(* Let us now define the following function: *)
-definition twice ≝ λn.add n n.
+(******************************** Existential *********************************)
-(*
-Existential
+(* We are interested to prove that for any natural number n there exists a
+natural number m that is the integer half of n. This will give us the
+opportunity to introduce new connectives and quantifiers and, later on, to make
+some interesting consideration on proofs and computations.
+Here is the formal statement of the theorem we are interested in: *)
-We are interested to prove that for any natural number n there exists a natural
-number m that is the integer half of n. This will give us the opportunity to
-introduce new connectives and quantifiers and, later on, to make some interesting
-consideration on proofs and computations. *)
+definition twice ≝ λn.add n n.
theorem ex_half: ∀n.∃m. n = twice m ∨ n = S (twice 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)
+ 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
+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
[@(ex_intro … O) %1 //
-(*
-Destructuration
+(******************************* Decomposition ********************************)
-The case of G2 is more complex. We should start introducing x and the
+(* 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
#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.
-*)
+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. *)
[@(ex_intro … m) /2/ | @(ex_intro … (S m)) normalize /2/
]
qed.
-(*
-Computing vs. Proving
+(**************************** Computing vs. Proving ***************************)
-Instead of proving the existence of a number corresponding to the half of n,
+(* 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 in our case is just a
boolean value: tt if the input term is even, and ff 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 nat × bool, defined in the basic library. The product type
-is just a sort of general purpose record, with standard fields fst and snd, called
-projections.
-A pair of values n and m is written (pair … m n) or \langle n,m \rangle - visually
-rendered as 〈n,m〉
-
+is just a sort of general purpose record, with standard fields fst and snd,
+called projections.
+A pair of values n and m is written (pair … m n) or \langle n,m \rangle -
+visually rendered as 〈n,m〉.
We first write down the function, and then discuss it.*)
let rec div2 n ≝
proof of the kind ∃n.A(n)∨B(n): the really informative content in it is the
witness n and a boolean indicating which one between the two conditions A(n) and
B(n) is met. This is precisely the quotient-remainder pair returned by div2.
-In both cases we proceed by recurrence (respectively, induction or recursion) over
-the input argument n. In case n = 0, we conclude the proof in ex_half by providing
-the witness O and a proof of A(O); this corresponds to returning the pair 〈O,ff〉 in
-div2. Similarly, in the inductive case n = S a, we must exploit the inductive
-hypothesis for a (i.e. the result of the recursive call), distinguishing two subcases
-according to the the two possibilites A(a) or B(a) (i.e. the two possibile values of
-the remainder for a). The reader is strongly invited to check all remaining details.
-
-Let us now prove that our div2 function has the expected behaviour.
+In both cases we proceed by recurrence (respectively, induction or recursion)
+over the input argument n. In case n = 0, we conclude the proof in ex_half by
+providing the witness O and a proof of A(O); this corresponds to returning the
+pair 〈O,ff〉 in div2. Similarly, in the inductive case n = S a, we must exploit
+the inductive hypothesis for a (i.e. the result of the recursive call),
+distinguishing two subcases according to the the two possibilites A(a) or B(a)
+(i.e. the two possibile values of the remainder for a). The reader is strongly
+invited to check all remaining details. *)
+
+(****************************** Destruct **************************************)
+
+(* Let us now prove that our div2 function has the expected behaviour.
+We start proving a few easy lemmas:
*)
lemma div2SO: ∀n,q. div2 n = 〈q,ff〉 → div2 (S n) = 〈q,tt〉.
lemma div2S1: ∀n,q. div2 n = 〈q,tt〉 → div2 (S n) = 〈S q,ff〉.
#n #q #H normalize >H normalize // qed.
+(* Here is our statement, where $\mathit{nat\_of\_bool}$ is the above coercions:
+*)
+
lemma div2_ok: ∀n,q,r. div2 n = 〈q,r〉 → n = add (nat_of_bool r) (twice q).
-#n elim n
- [#q #r #H normalize in H; destruct //
+
+(* We proceed by induction on $n$, that produces two subgoals. *)
+
+#n elim n
+ [#q #r #H
+
+(* After introducing the hypothesis q,r and H, the first subgoal looks like the
+following:
+
+ n : nat
+ q : nat
+ r : bool
+ H : (div2 O=〈q,r〉)
+ ---------------------------
+
+ (O=add (nat_of_bool r) (twice q))
+
+Note that the right hand side of equation H is not in normal form, and we would
+like to reduce it. We can do it by specifying a pattern for the normalize
+tactic, introduced by the ``in'' keyword, and delimited by a semicolon. In this
+case, the pattern is just the name of the hypothesis and we should write *)
+
+ normalize in H;
+
+(* that transforms H as follows:
+
+ H : (〈O,ff〉=〈q,r〉)
+
+From such an hypothesis we expect to be able to conclude that q=O$ and r=false.
+The tactic that provides this functionality is called "destruct". The tactic
+decomposes an equality between structured terms in smaller components: if an
+absurd situation is recognized (like an equality between 0 and (S n)) the
+current goal is automatically closed; otherwise, all derived equations where one
+of the sides is a variable are automatically substituted in the proof, and the
+remaining equations are added to the context (replacing the original equation).
+
+In the above case, by invoking destruct we would get the two equations q=O and
+r=false; these are immediately substituted in the goal, that can now be solved
+by direct computation. *)
+
+ destruct //
+
+(********************************** Cut ***************************************)
+
+(* Let's come to the second subgoal *)
|#a #Hind #q #r
+(* After performing the previous introductions, the current goal looks like the
+following:
+
+ n : nat
+ a : nat
+ Hind : (∀q:nat.∀r:bool.div2 a=〈q,r〉→a=add (nat_of_bool r) (twice q))
+ q : nat
+ r : bool
+ ---------------------------
+ div2 (S a)=〈q,r〉→S a=add (nat_of_bool r) (twice q)
+
+We should proceed by cases on the remainder of (div2 a), but before doing it we
+should emphasize the fact that (div2 a) can be expressed as a pair of its two
+projections. The tactics that allows to introduce a new hypothesis, splitting a
+complex proofs into smaller components is called "cut".
+The invocation of "cut A" transforms the current goal G into the two subgoals A
+and A→G (A is called the cut formula).
+
+In our case, the cut formula is
+ div2 a = 〈fst … (div2 a), snd … (div2 a)〉
+whose proof is trivial
+*)
+
cut (div2 a = 〈fst … (div2 a), snd … (div2 a)〉) [//]
+
+(* We now proceed by induction on (snd … (div2 a)); the two subgoals are
+respectively closed using the two lemmas div2SO and div2S1 in conjunction with
+the inductive hypothesis, and do not contain additional challenges. *)
+
cases (snd … (div2 a))
[#H >(div2S1 … H) #H1 destruct normalize @eq_f >add_S @(Hind … H)
|#H >(div2SO … H) #H1 destruct normalize @eq_f @(Hind … H)
]
qed.
-(*
-Mixing proofs and computations
-
-There is still another possibility, however, namely to mix the program and its
-specification into a single entity. The idea is to refine the output type of the
-div2 function: it should not be just a generic pair 〈q,r〉 of natural numbers but a
-specific pair satisfying the specification of the function. In other words, we need
-the possibility to define, for a type A and a property P over A, the subset type
-{a:A|P(a)} of all elements a of type A that satisfy the property P. Subset types
-are just a particular case of the so called dependent types, that is types that
-can depend over arguments (such as arrays of a specified length, taken as a
-parameter).These kind of types are quite unusual in traditional programming
-languages, and their study is one of the new frontiers of the current research on
-type systems.
-
-There is nothing special in a subset type {a:A|P(a)}: it is just a record composed
-by an element of a of type A and a proof of P(a). The crucial point is to have a
-language reach enough to comprise proofs among its expressions.
+(********************** Mixing proofs and computations ************************)
+
+(* There is still another possibility, however, namely to mix the program and
+its specification into a single entity. The idea is to refine the output type of
+the div2 function: it should not be just a generic pair 〈q,r〉 of natural numbers
+but a specific pair satisfying the specification of the function. In other
+words, we need the possibility to define, for a type A and a property P over A,
+the subset type {a:A|P(a)} of all elements a of type A that satisfy the property
+P. Subset types are just a particular case of the so called dependent types,
+that is types that can depend over arguments (such as arrays of a specified
+length, taken as a parameter).These kind of types are quite unusual in
+traditional programming languages, and their study is one of the new frontiers
+of the current research on type systems.
+
+There is nothing special in a subset type {a:A|P(a)}: it is just a record
+composed by an element of a of type A and a proof of P(a). The crucial point is
+to have a language reach enough to comprise proofs among its expressions.
*)
record Sub (A:Type[0]) (P:A → Prop) : Type[0] ≝
definition qr_spec ≝ λn.λp.∀q,r. p = 〈q,r〉 → n = add (nat_of_bool r) (twice q).
-(* We can now construct a function from n to {p|qr_spec n p} by composing the objects
-we already have *)
+(* We can now construct a function from n to {p|qr_spec n p} by composing the
+objects we already have *)
definition div2P: ∀n. Sub (nat×bool) (qr_spec n) ≝ λn.
mk_Sub ?? (div2 n) (div2_ok n).
qed.
example full7: (div2Pagain (S(S(S(S(S(S(S O)))))))) = ?.
-[normalize
-// qed.
+[normalize //] qed.
example quotient7: witness … (div2Pagain (S(S(S(S(S(S(S O)))))))) = ?.
normalize // qed.
projects / helm.git / commitdiff