Tactic to apply double negation elimination or excluded middle when goal is False

Using Coq
1

Somehow the following fact seems not often taught in proof assistant tutorials, in spite of being incredibly useful: when your current goal is False, you can, while remaining in intuitionistic logic, transform a hypothesis ~~P into P, and get a hypothesis P \/ ~P for free.

I have the following tactics to apply this.

  • Did I miss some built-in tactics that do this?
  • If not: in dneg_elim, how can I avoid changing the order of hypotheses in the context?
Ltac dneg_elim :=
  repeat match goal with
    | [ H : ~~?P |- False ] => apply H; clear H; intro H
    end.

Example dneg_over_implication A B : ~~(A -> B) -> (~~A -> ~~B).
Proof.
  intros HAB HA HB. dneg_elim. apply HB, HAB, HA.
Qed.

Lemma double_neg_lem P : ~~(P \/ ~P).
Proof. tauto. Qed.

Tactic Notation "lem" constr(term) "as" simple_intropattern(pat) :=
  apply (double_neg_lem term); intros pat.

Example dneg_over_implication_converse A B : (~~A -> ~~B) -> ~~(A -> B).
Proof.
  intros H H'. lem A as [HA | HnA].
  * lem B as [HB | HnB].
    ** apply H'. intros _. exact HB.
    ** apply H, HnB. intro HnA. apply HnA, HA.
  * apply H'. intro HA. exfalso. apply HnA, HA.
Qed.
2

To preserve the order of variables, you can use this trick:

Ltac dneg_elim :=
  repeat match goal with
    | [ H : ~~?P |- False ] => apply H; let H' := fresh in intro H' after H; clear H; rename H' into H
    end.

You might be right that this is not often taught in tutorials. Providing this tactic as a standard one looks indeed pretty relevant.

PS: That might be interesting also to provide an Ltac2 version of dneg_elim.

2 Likes