CODEWITHSUNDEEP
coq
edelagnier
edelagnier

Reputation: 1535

coq proof : tactic absurd, how does it works?

I am trying to understand a proof in coq. I wrote it long ago during a course but now I'm blocked by the absurd command. Here is the proof : 

Theorem Thm_2 : (~psi -> ~phi) -> (phi -> psi).
Proof.
intro.
intro.
cut (psi \/ ~psi).
intro.
elim H1.
intro.
exact H2.
intro.
absurd phi.
cut (~psi).
exact H.
exact H2.
exact H0.
apply classic.
Qed.

When I use the absurd phi tactic, my current goal is psi. And the absurd command transforms it in two goals : ~ phi and phi. My problem is I can't figure nor remember the logic behind this step...

Thank you for your help ! (it seems I can't add a Hello at the beginning of my message... sorry)

Upvotes: 4

Views: 2836

Answers (1)

Ptival
Ptival

Reputation: 9437

  • If you can prove phi and ~ phi, then you can prove False (remember, ~ phi := phi -> False)
  • If you can prove False, then you can prove anything, including your goal at that point

So absurd phi applies False elimination, and have you prove False by means of proving both phi and ~ phi.

Upvotes: 5

Related Questions