Library UniMath.MoreFoundations.DoubleNegation

Require Import UniMath.Foundations.All.

When proving a negation, we may undo a double negation.
Lemma wma_dneg {X:Type} (P:Type) : ¬¬ P -> (P -> ¬ X) -> ¬ X.
Show proof.
  intros dnp p.
  apply dnegnegtoneg.
  assert (q := dnegf p); clear p.
  apply q; clear q.
  apply dnp.

It's not false that a type is decidable.
Lemma dneg_decidable (P:Type) : ¬¬ decidable P.
Show proof.
  intros ndec.
  unfold decidable in ndec.
  assert (q := fromnegcoprod ndec); clear ndec.
  contradicts (pr1 q) (pr2 q).

When proving a negation, we may assume a type is decidable.
Lemma wma_decidable {X:Type} (P:Type) : (decidable P -> ¬ X) -> ¬ X.
Show proof.
  apply (wma_dneg (decidable P)).
  apply dneg_decidable.

Local Open Scope logic.

Compare with negforall_to_existsneg, which uses LEM instead.
Lemma negforall_to_existsneg' {X:Type} (P:X->Type) : (¬ ∏ x, ¬¬ (P x)) -> ¬¬ (∃ x, ¬ (P x)).
Show proof.
  intros nf c. use nf; clear nf. intro x.
  assert (q := neghexisttoforallneg _ c x); clear c; simpl in q.
  exact q.