Menu
I wan to use the destruct tactic to prove a statement by cases. I have read a couple of examples online and I'm confused. Could someone explain it better?
Here is a small example (there are other ways to solve it but try using destruct):
Inductive three := zero
| one
| two.
Lemma has2b2: forall a:three, a<>zero /\ a<>one -> a=two.
Now some examples online suggest doing the following:
intros. destruct a.
In which case I get:
3 subgoals H : zero <> zero /\ zero <> one
______________________________________(1/3)
zero = two
______________________________________(2/3)
one = two
______________________________________(3/3)
two = two
So, I want to prove that the first two cases are impossible. But the machine lists them as subgoals and wants me to PROVE them... which is impossible.
Summary: How to exactly discard the impossible cases?
I have seen some examples using inversion but I don't understand the procedure.
Finally, what happens if my lemma depends on several inductive types and I still want to cover ALL cases?
990
simpl: Simplifies the goal or hypotheses in the context. unfold: Unfolds the definitions of terms. apply: Uses implications to transform goals and hypotheses. rewrite: Replaces a term with an equivalent term if the equivalence of the terms has already been proven.
This tactic applies to any goal. The argument term is a term well-formed in the local context. The tactic apply tries to match the current goal against the conclusion of the type of term . If it succeeds, then the tactic returns as many subgoals as the number of non-dependent premises of the type of term.
reflexivity. Use reflexivity when your goal is to prove that something equals itself. In this example we will prove that any term x of type Set is equal to itself.
How to discard impossible cases? Well, it's true that the first two obligations are impossible to prove, but note they have contradicting assumptions (zero <> zero and one <> one, respectively). So you will be able to prove those goals with tauto (there are also more primitive tactics that will do the trick, if you are interested).
inversion is a more advanced version of destruct. Additional to 'destructing' the inductive, it will sometimes generate some equalities (that you may need). It itself is a simple version of induction, which will additionally generate an induction hypothesis for you.
If you have several inductive types in your goal, you can destruct/invert them one by one.
More detailed walk-through:
Inductive three := zero | one | two .
Lemma test : forall a, a <> zero /\ a <> one -> a = two.
Proof.
intros a H.
destruct H. (* to get two parts of conjunction *)
destruct a. (* case analysis on 'a' *)
(* low-level proof *)
compute in H. (* to see through the '<>' notation *)
elimtype False. (* meaning: assumptions are contradictory, I can prove False from them *)
apply H.
reflexivity.
(* can as well be handled with more high-level tactics *)
firstorder.
(* the "proper" case *)
reflexivity.
Qed.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
