How to do inductive type cases in Coq

Question

I wanted to use destruct tactics to prove affirmation by deeds. I read a few examples on the Internet and I am confused. Can anyone explain this 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 online examples suggest doing the following:

 intros. destruct a. 

In this 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 sub-goals and wants me to PROVE them ... which is impossible.

Summary: How to accurately refuse impossible cases?

I have seen some examples using inversion , but I do not understand this procedure.

Finally, what happens if my lemma depends on several inductive types, and I still want to cover ALL cases?

Answer 1

How to refuse impossible cases? Well, it is true that the first two obligations cannot be proved, but note that they contradict the assumptions ( zero <> zero and one <> one , respectively). This way you can prove these goals with tauto (there is also a more primitive tactic that will do the trick if you're interested).

inversion is a more advanced version of destruct. In addition to the “destruction” of inductance, it sometimes generates some equalities (which you may need). This in itself is a simple version of induction that will additionally create the induction hypothesis for you.

If you have several inductive types for your purpose, you can destruct/invert them in turn.

More detailed walkthrough:

 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. 

Answer 2

If you see an impossible goal, there are two possibilities: either you made a mistake in your proof strategy (perhaps your lemma is incorrect), or the hypotheses are contradictory.

If you think the hypotheses are contradictory, you can set a False goal to get a little complexity. elimtype False achieves this. Often you prove False by proving the sentence P and its negation ~P ; absurd P tactics draws any goal from P and ~P If there is a certain hypothesis that is contradictory, contradict H will set the goal ~H , or if the hypothesis is a negation of ~A , then the goal will be A (stronger than ~ ~A , but usually more convenient), If one particular hypothesis is obviously contradictory, contradiction H or simply contradiction will prove any goal.

There are many tactics related to hypotheses of inductive types. Finding out which one to use mainly depends on experience. Here are the main ones (but you will soon come across cases that are not covered here):

• destruct simply decomposes the hypothesis into several parts. It loses information about dependencies and recursion. A typical example is destruct H where H is the conjunction of H : A /\ B , which splits H into two independent hypotheses of types A and B ; or dally destruct H , where H is the disjunction of H : A \/ B , which splits the proof into two different defendants, one with hypothesis A and one with hypothesis B
• case_eq is similar to destruct , but retains the connections that the hypothesis has with other hypotheses. For example, destruct n , where n : nat splits the proof into two clients, one for n = 0 and one for n = S m . If other hypotheses use n (i.e., you have H : P n ), you may need to remember that the n that you destroyed is the same n that is used in these hypotheses: case_eq n does this.
• inversion performs case analysis as a hypothesis. This is especially useful when there are dependencies in the type of hypothesis that destruct would forget. Usually you use case_eq for hypotheses in Set (where equality matters) and inversion for hypotheses in Prop (which have very dependent types). Inversion tactics leave a lot of equal behind, and often subst follows to simplify hypotheses. The inversion_clear tactic is a simple alternative to inversion; subst inversion; subst , but loses some information.
• induction means that you are going to prove the goal by induction (= recursion) on this hypothesis. For example, induction n where n : nat means that you perform integer induction and prove the base case ( n replaced by 0 ), and the inductive register ( n replaced by m+1 ).

Your example is simple enough that you can prove it as an “obvious case analysis on A ”.

 Lemma has2b2: forall a:three, a<>zero/\a<>one ->a=two. Proof. destruct a; tauto. Qed. 

But look at the cases created by destruct tactics, i.e. after just intros; destruct a. intros; destruct a. . (The case when A is equal to one is symmetric; the last case when A is equal to two is obvious by reflexivity.)

 H : zero <> zero /\ zero <> one ============================ zero = two 

The goal seems impossible. We can say this Coq, and here he can automatically detect a contradiction ( zero=zero obvious, and the rest is a first-order tautology processed by tauto tactics).

 elimtype False. tauto. 

Actually, tauto works even if you don’t start by telling Coq to not worry about the goal, and wrote tauto without elimtype False in the first place (IIRC it was not in older versions of Coq). You can see what Coq does with tauto tactics by writing info tauto . Coq will tell you what kind of proof of script tauto tactics tauto . It is not very easy to follow, so let's look at a manual proof of this case. First, divide the hypothesis (which is a conjunction) into two.

 destruct H as [H0 H1]. 

Now we have two hypotheses, one of which is zero <> zero . This is clearly false because it is clearly the negation of zero = zero .

 contradiction H0. reflexivity. 

We can take a closer look at what contradiction tactics do. ( info contradiction will tell you what is going on under the stage, but again not a beginner). We argue that the goal is true because the hypotheses are contradictory, so we can prove anything. Therefore, set the intermediate target to False .

 assert (F : False). 

Launch red in H0. to see that zero <> zero is really the designation for ~(zero=zero) , which in turn is defined as the value zero=zero -> False . So False is the conclusion of H0 :

 apply H0. 

And now we need to prove that zero=zero , which

 reflexivity. 

Now we have proved our statement False . It remains to be proved that False implies our goal. Well, False implies any purpose that defines it ( False is defined as an inductive type with 0 case).

 destruct F.