michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/logic/axioms/prop_decidable.lean): simplify proof of prop_decidable (using arbitrary instead of epsilon)

Browse source
This commit is contained in:
Jeremy Avigad 2015-04-08 19:28:13 -04:00 committed by Leonardo de Moura
parent cc63a40a01
commit 53919699bc
1 changed files with 3 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
library/logic/axioms/prop_decidable.lean
View file

@ -4,20 +4,17 @@ Released under Apache 2.0 license as described in the file LICENSE.
Module: logic.axioms.prop_decidable Module: logic.axioms.prop_decidable
Author: Leonardo de Moura Author: Leonardo de Moura
Excluded middle + Hilbert implies every proposition is decidable.
-/ -/
import logic.axioms.prop_complete logic.axioms.hilbert import logic.axioms.prop_complete logic.axioms.hilbert
open decidable inhabited nonempty open decidable inhabited nonempty
-- Excluded middle + Hilbert implies every proposition is decidable
-- First, we show that (decidable a) is inhabited for any 'a' using the excluded middle
theorem decidable_inhabited [instance] (a : Prop) : inhabited (decidable a) := theorem decidable_inhabited [instance] (a : Prop) : inhabited (decidable a) :=
inhabited_of_nonempty inhabited_of_nonempty
(or.elim (em a) (or.elim (em a)
(assume Ha, nonempty.intro (inl Ha)) (assume Ha, nonempty.intro (inl Ha))
(assume Hna, nonempty.intro (inr Hna))) (assume Hna, nonempty.intro (inr Hna)))
-- Note that decidable_inhabited is marked as an instance, and it is silently used
-- for synthesizing the implicit argument in the following 'epsilon'
theorem prop_decidable [instance] (a : Prop) : decidable a := theorem prop_decidable [instance] (a : Prop) : decidable a :=
epsilon (λd, true) arbitrary (decidable a)