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.
+qed.
\ No newline at end of file
projects / helm.git / commitdiff