From ff5022c2f4035c21bf69039cb492dd2d55f58d3e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 14 Jun 2015 17:33:22 -0700 Subject: [PATCH] feat(library/data/axioms): add 'type_decidable' In Lean standard mode, Hilbert choice implies that all types are decidable. --- library/logic/axioms/prop_decidable.lean | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/library/logic/axioms/prop_decidable.lean b/library/logic/axioms/prop_decidable.lean index 02e73171b..01d4f443f 100644 --- a/library/logic/axioms/prop_decidable.lean +++ b/library/logic/axioms/prop_decidable.lean @@ -5,8 +5,8 @@ Author: Leonardo de Moura Excluded middle + Hilbert implies every proposition is decidable. -/ -import logic.axioms.prop_complete logic.axioms.hilbert -open decidable inhabited nonempty +import logic.axioms.prop_complete logic.axioms.hilbert data.sum +open decidable inhabited nonempty sum theorem decidable_inhabited [instance] (a : Prop) : inhabited (decidable a) := inhabited_of_nonempty @@ -16,3 +16,9 @@ inhabited_of_nonempty theorem prop_decidable [instance] (a : Prop) : decidable a := arbitrary (decidable a) + +theorem type_decidable (A : Type) : A + (A → false) := +match prop_decidable (nonempty A) with +| inl Hp := sum.inl (inhabited.value (inhabited_of_nonempty Hp)) +| inr Hn := sum.inr (λ a, absurd (nonempty.intro a) Hn) +end