From 1e595e80274abb639d02d003fe2fbddd49df3b50 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 22 Jul 2014 03:54:28 -0700 Subject: [PATCH] feat(library/standard/decidable): decidable is proof irrelevant Signed-off-by: Leonardo de Moura --- library/standard/decidable.lean | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/library/standard/decidable.lean b/library/standard/decidable.lean index ff2332838..a4f3a1ad6 100644 --- a/library/standard/decidable.lean +++ b/library/standard/decidable.lean @@ -17,6 +17,18 @@ theorem em (p : Bool) (H : decidable p) : p ∨ ¬p definition rec [inline] {p : Bool} {C : Type} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C := decidable_rec H1 H2 H +theorem irrelevant {p : Bool} (d1 d2 : decidable p) : d1 = d2 +:= decidable_rec + (assume Hp1 : p, decidable_rec + (assume Hp2 : p, congr2 inl (refl Hp1)) -- using proof irrelevance for Bool + (assume Hnp2 : ¬p, absurd_elim (inl Hp1 = inr Hnp2) Hp1 Hnp2) + d2) + (assume Hnp1 : ¬p, decidable_rec + (assume Hp2 : p, absurd_elim (inr Hnp1 = inl Hp2) Hp2 Hnp1) + (assume Hnp2 : ¬p, congr2 inr (refl Hnp1)) -- using proof irrelevance for Bool + d2) + d1 + theorem decidable_true [instance] : decidable true := inl trivial