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)

Accepted Answer

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

coq proof : tactic absurd, how does it works?

Solution

Problem