From 53919699bcb16bec08dd8f2a1e75b3d50babb10b Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Wed, 8 Apr 2015 19:28:13 -0400 Subject: [PATCH] refactor(library/logic/axioms/prop_decidable.lean): simplify proof of prop_decidable (using arbitrary instead of epsilon) --- library/logic/axioms/prop_decidable.lean | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/library/logic/axioms/prop_decidable.lean b/library/logic/axioms/prop_decidable.lean index c1d723b04..14daeeb83 100644 --- a/library/logic/axioms/prop_decidable.lean +++ b/library/logic/axioms/prop_decidable.lean @@ -4,20 +4,17 @@ Released under Apache 2.0 license as described in the file LICENSE. Module: logic.axioms.prop_decidable Author: Leonardo de Moura + +Excluded middle + Hilbert implies every proposition is decidable. -/ import logic.axioms.prop_complete logic.axioms.hilbert 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) := inhabited_of_nonempty (or.elim (em a) (assume Ha, nonempty.intro (inl Ha)) (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 := -epsilon (λd, true) +arbitrary (decidable a)