From 29b6d1081c8d33ee41d6ce3cf3793b35a5247ada Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 21 Jul 2014 02:42:11 +0100 Subject: [PATCH] feat(library/standard/bool_decidable): cleanup bool_decidable, and remove the artificial dependency to bit Signed-off-by: Leonardo de Moura --- library/standard/bool_decidable.lean | 26 +++++++++----------------- 1 file changed, 9 insertions(+), 17 deletions(-) diff --git a/library/standard/bool_decidable.lean b/library/standard/bool_decidable.lean index f2b9040f4..2f4f27318 100644 --- a/library/standard/bool_decidable.lean +++ b/library/standard/bool_decidable.lean @@ -1,26 +1,18 @@ -- Copyright (c) 2014 Microsoft Corporation. All rights reserved. -- Released under Apache 2.0 license as described in the file LICENSE. -- Author: Leonardo de Moura -import classical hilbert bit decidable -using bit decidable +import classical hilbert decidable +using decidable -- Excluded middle + Hilbert implies every proposition is decidable -definition to_bit (a : Bool) : bit -:= epsilon (λ b : bit, (b = '1) ↔ a) -theorem to_bit_def (a : Bool) : (to_bit a) = '1 ↔ a +-- First, we show that (decidable a) is inhabited for any 'a' using the excluded middle +theorem inhabited_decidable [instance] (a : Bool) : inhabited (decidable a) := or_elim (em a) - (assume Hp, epsilon_ax (exists_intro '1 (iff_intro (assume H, Hp) (assume H, refl b1)))) - (assume Hn, epsilon_ax (exists_intro '0 (iff_intro (assume H, absurd_elim a H b0_ne_b1) (assume H, absurd_elim ('0 = '1) H Hn)))) + (assume Ha, inhabited_intro (inl Ha)) + (assume Hna, inhabited_intro (inr Hna)) +-- Note that inhabited_decidable is marked as an instance, and it is silently used +-- for synthesizing the implicit argument in the following 'epsilon' theorem bool_decidable [instance] (a : Bool) : decidable a -:= bit_rec - (assume H0 : to_bit a = '0, - have e1 : ¬ to_bit a = '1, from subst (symm H0) b0_ne_b1, - have Hna : ¬a, from iff_mp_left (iff_flip_sign (to_bit_def a)) e1, - inr Hna) - (assume H1 : to_bit a = '1, - have Ha : a, from iff_mp_left (to_bit_def a) H1, - inl Ha) - (to_bit a) - (refl (to_bit a)) +:= epsilon (λ d, true)