CODEWITHSUNDEEP
coq
nss
nss

Reputation: 9

how do I prove forall P Q : Prop, ((((P -> Q) -> P) -> P) -> Q) ->Q. in coq?

I am very new to coq so if you only say intros. I don't know what to introduce. So being specific like (Ex. intros p q.) would be very helpful.

Upvotes: 0

Views: 90

Answers (1)

Pierre Castéran
Pierre Castéran

Reputation: 916

Fortunately, your goal can be automatically solved by the auto tactic. If you use its variant info_auto, Coq tells you which steps lead to the solution .

Goal  forall P Q : Prop, ((((P -> Q) -> P) -> P) -> Q) -> Q.
  info_auto.

Then, you may replay the proof by yourself, and add comments and explicit variables names to the introstactics, and you will understand the strategy used by auto (what to do when the conclusion is a forall or an implication, or an atomic proposition).

 Restart. 
  intros P Q H.
  apply H (* no-choice ! *).
  intro H0.         
  apply H0.  (* no other possibility ! *)
  intro p. 
  apply H. (* no alternative ! *)
  intros _. 
  assumption. 
Qed.

Upvotes: 3

Related Questions