52 lines
1.9 KiB
Text
52 lines
1.9 KiB
Text
|
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
|||
|
|
-- Released under Apache 2.0 license as described in the file LICENSE.
|
|||
|
|
-- Authors: Leonardo de Moura, Jeremy Avigad
|
|||
|
|
import logic hilbert funext
|
|||
|
|
|
|||
|
|
-- Diaconescu’s theorem
|
|||
|
|
-- Show that Excluded middle follows from
|
|||
|
|
-- Hilbert's choice operator, function extensionality and Boolean extensionality
|
|||
|
|
section
|
|||
|
|
hypothesis boolext ⦃a b : Bool⦄ : (a → b) → (b → a) → a = b
|
|||
|
|
|
|||
|
|
parameter p : Bool
|
|||
|
|
|
|||
|
|
definition u [private] := epsilon (λ x, x = true ∨ p)
|
|||
|
|
|
|||
|
|
definition v [private] := epsilon (λ x, x = false ∨ p)
|
|||
|
|
|
|||
|
|
lemma u_def [private] : u = true ∨ p
|
|||
|
|
:= epsilon_ax (exists_intro true (or_intro_left p (refl true)))
|
|||
|
|
|
|||
|
|
lemma v_def [private] : v = false ∨ p
|
|||
|
|
:= epsilon_ax (exists_intro false (or_intro_left p (refl false)))
|
|||
|
|
|
|||
|
|
lemma uv_implies_p [private] : ¬(u = v) ∨ p
|
|||
|
|
:= or_elim u_def
|
|||
|
|
(assume Hut : u = true, or_elim v_def
|
|||
|
|
(assume Hvf : v = false,
|
|||
|
|
have Hne : ¬(u = v), from subst (symm Hvf) (subst (symm Hut) true_ne_false),
|
|||
|
|
or_intro_left p Hne)
|
|||
|
|
(assume Hp : p, or_intro_right (¬u = v) Hp))
|
|||
|
|
(assume Hp : p, or_intro_right (¬u = v) Hp)
|
|||
|
|
|
|||
|
|
lemma p_implies_uv [private] : p → u = v
|
|||
|
|
:= assume Hp : p,
|
|||
|
|
have Hpred : (λ x, x = true ∨ p) = (λ x, x = false ∨ p), from
|
|||
|
|
funext (take x : Bool,
|
|||
|
|
have Hl : (x = true ∨ p) → (x = false ∨ p), from
|
|||
|
|
assume A, or_intro_right (x = false) Hp,
|
|||
|
|
have Hr : (x = false ∨ p) → (x = true ∨ p), from
|
|||
|
|
assume A, or_intro_right (x = true) Hp,
|
|||
|
|
show (x = true ∨ p) = (x = false ∨ p), from
|
|||
|
|
boolext Hl Hr),
|
|||
|
|
show u = v, from
|
|||
|
|
subst Hpred (refl (epsilon (λ x, x = true ∨ p)))
|
|||
|
|
|
|||
|
|
theorem em : p ∨ ¬ p
|
|||
|
|
:= have H : ¬(u = v) → ¬ p, from contrapos p_implies_uv,
|
|||
|
|
or_elim uv_implies_p
|
|||
|
|
(assume Hne : ¬(u = v), or_intro_right p (H Hne))
|
|||
|
|
(assume Hp : p, or_intro_left (¬p) Hp)
|
|||
|
|
end
|