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)