Skip to content

Instantly share code, notes, and snippets.

@fetburner
Created February 12, 2020 11:05
Show Gist options
  • Save fetburner/3193ae919afda9a479a1ada4f4b24e80 to your computer and use it in GitHub Desktop.
Save fetburner/3193ae919afda9a479a1ada4f4b24e80 to your computer and use it in GitHub Desktop.
Drinker paradox
Require Import Classical.
From mathcomp Require Import all_ssreflect.
Section Drinker.
Variable P : Type.
Variable p : P.
Variable D : P -> Prop.
Theorem drinker : exists (x : P), D x -> forall y, D y.
Proof.
case (classic (exists x, ~ D x)) => [ [ x H ] | H ].
- by exists x => /H.
- exists p => ? x.
case (classic (D x)) => // ?.
case H. by exists x.
Qed.
End Drinker.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment