From 0fdf8cd395b21ec003569383aee1449a6fe4b35a Mon Sep 17 00:00:00 2001 From: matitaweb Date: Tue, 11 Oct 2011 15:39:38 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter2.ma | 50 +++++++++++++++++++++++++++++++++---- 1 file changed, 45 insertions(+), 5 deletions(-) diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma index d6e5a82b8..b1292601a 100644 --- a/weblib/tutorial/chapter2.ma +++ b/weblib/tutorial/chapter2.ma @@ -92,10 +92,50 @@ on proofs and computations. *) theorem ex_half: ∀n.a title="exists" href="cic:/fakeuri.def(1)"∃/am. n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a m a title="logical or" href="cic:/fakeuri.def(1)"∨/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a 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. +*) [@(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a) %1 // -(* *) - |#x * #m * #eqx - [@(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … m) /2/ | @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a 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. +*) + [@(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … m) /2/ | @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a m)) normalize /2/ ] -qed. +qed. \ No newline at end of file -- 2.39.2