coq proof : tactic absurd, how does it works?

Question

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)

Answer 1

• 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.