Skip to content

Instantly share code, notes, and snippets.

@codyroux

codyroux/is_a_neg_implies_em.v

Created September 3, 2022 15:44
Show Gist options
  • Save codyroux/ecc94914fc507fcdb86c12eea0b79e7c to your computer and use it in GitHub Desktop.
Save codyroux/ecc94914fc507fcdb86c12eea0b79e7c to your computer and use it in GitHub Desktop.
Download ZIP
Raw
is_a_neg_implies_em.v
Require Import Setoid.
Axiom is_a_neg : forall (P : Prop), exists (Q : Prop), P <-> ~Q.
Lemma not_not : forall P, ~~P -> P.
Proof.
intros P.
assert (h := is_a_neg P); destruct h as [Q h].
rewrite h.
tauto.
Qed.
Theorem em: forall P, P \/ ~P.
Proof.
intro P.
apply not_not.
tauto.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment