0
$\begingroup$

I am relatively new to Coq. Can anyone show me how to prove the following in Coq?

(P -> (Q /\ R)) -> (~Q) -> ~P
$\endgroup$

1 Answer 1

1
$\begingroup$

You've asked a few of these and haven't really gotten any real help since it's clear you are completely lost, and it's hard to help someone climb a whole learning curve in the span of a single question (the real solution is for you to go through a tutorial). I'm not sure what situation has brought you here, but I'll try to give a guide through this proof.. hope it helps.

First, when you're starting out, it's best to run "unfold not." right at the beginning in order to eliminate the defined not operation, replacing $\lnot A$ with $A\to \bot.$ This will make things easier. So our statement is actually $$ (P\to (Q\land R))\to (Q\to \bot)\to P\to \bot$$

We can peel off the premises of the implications successively with intros. If you simply run "intros." you will be left with a goal of $\bot$ and assumptions $$H_0:(P\to (Q\land R))\\ H_1:Q\to \bot\\H_2:P.$$ This makes sense: the way that you show $\phi\to \psi$ is to take $\phi$ as an assumption and use it to prove $\psi$ (this is the implication introduction rule in natural deduction).

So what can we do here to prove our goal $\bot$? First off, we see that we have $Q\to \bot,$ so if we can prove $Q,$ then we're done. The way we do this in Coq is with the "apply" tactic. If you just type "apply H_1." it will apply $H_1$ to the goal producing a new goal. Here, this will change the goal to $Q,$ which makes sense: as we said, if we can show $Q$ then since we have $Q\to \bot,$ we can prove $\bot$ by proving $Q.$ Formally, we are using implication elimination. The reason it is called "apply" because function application is the type theory analogue of implication elimination under the Curry-Howard correspondence.

So where were we? $Q$ is our goal and we have the same hypotheses as above. How can we make some more progress? Well, if you look at $H_2$ and $H_0,$ we have $P$ and $P\to (Q\land R).$ Great, that means we have $Q\land R.$ Again, this is using implication elimination, so we use the apply tactic. This time we're not applying it to the goal but to one of our assumptions. The way to do this is "apply H_0 in H_2 as H_3." (The "as H_3" part just makes sure you get a new assumption... otherwise it would replace $H_2$ with $Q\land R.$) Now we have $$H_3: Q\land R$$ at our disposal.

Well, great, cause our goal is $Q$ and clearly if we have $Q\land R$ then we have $Q.$ To make it official we have to break apart the $\land$ into its two assumptions. So run "destruct H_3." and you'll see that you have $$ H_4: Q\\ H_5 : R$$ as assumptions. Great, H_4 is our goal. So go head and "apply H_4" or "refine H_4" and you're done. (Actually, apply is smart enough that you can just do "apply H_3" instead of destructing. But it's probably best to do things as much by hand as possible. After all, this proof can be completed with a single tactic "tauto." if all we care about is getting the term defined.)

$\endgroup$
2
  • $\begingroup$ I got Error: Statement without assumptions for "apply H_0 in H_2 as H_3." $\endgroup$
    – user643202
    Feb 25, 2019 at 4:45
  • $\begingroup$ @Anonymous I'm not going to troubleshoot your code for you. It's really telling that you wrote literally what I wrote and expected it to work with no modification whatsoever. I gave the ideas behind a proof here and if you want to use it you actually need to think about it. If you're getting an error, do what you do if you get an error you don't understand in any programming language: squint and see if there's a typo or you can parse what's going on. Otherwise, google it. As I said in the first paragraph, you really need to go through a tutorial. $\endgroup$ Feb 25, 2019 at 4:49

You must log in to answer this question.