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
+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
+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.
+(* 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) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | @(\ 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 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
]
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 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 -
+(* 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〉
We first write down the function, and then discuss it.*)
]
].
-(* The function is computed by recursion over the input n. If n is 0, then the quotient
-is 0 and the remainder is tt. If n = S a, we start computing the half of a, say 〈q,b〉.
-Then we have two cases according to the possible values of b: if b is tt, then we must return
- 〈q,ff〉, while if b = ff then we must return 〈S q,tt〉.
+(* The function is computed by recursion over the input n. If n is 0, then the
+quotient is 0 and the remainder is tt. If n = S a, we start computing the half
+of a, say 〈q,b〉. Then we have two cases according to the possible values of b:
+if b is tt, then we must return 〈q,ff〉, while if b = ff then we must return 〈S q,tt〉.
It is important to point out the deep, substantial analogy between the algorithm for
computing div2 and the the proof of ex_half. In particular ex_half returns a
qed.
(* 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.
+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] ≝
projects / helm.git / commitdiff