lean2/library/logic/decidable.lean

101 lines
3.9 KiB
Text
Raw Normal View History

-- 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 logic.connectives data.empty
inductive decidable [class] (p : Prop) : Type :=
inl : p → decidable p,
inr : ¬p → decidable p
namespace decidable
definition true_decidable [instance] : decidable true :=
inl trivial
definition false_decidable [instance] : decidable false :=
inr not_false_trivial
variables {p q : Prop}
definition rec_on_true [H : decidable p] {H1 : p → Type} {H2 : ¬p → Type} (H3 : p) (H4 : H1 H3)
: rec_on H H1 H2 :=
rec_on H (λh, H4) (λh, false.rec_type _ (h H3))
definition rec_on_false [H : decidable p] {H1 : p → Type} {H2 : ¬p → Type} (H3 : ¬p) (H4 : H2 H3)
: rec_on H H1 H2 :=
rec_on H (λh, false.rec_type _ (H3 h)) (λh, H4)
theorem irrelevant [instance] : subsingleton (decidable p) :=
subsingleton.intro (fun d1 d2,
decidable.rec
(assume Hp1 : p, decidable.rec
(assume Hp2 : p, congr_arg inl (eq.refl Hp1)) -- using proof irrelevance for Prop
(assume Hnp2 : ¬p, absurd Hp1 Hnp2)
d2)
(assume Hnp1 : ¬p, decidable.rec
(assume Hp2 : p, absurd Hp2 Hnp1)
(assume Hnp2 : ¬p, congr_arg inr (eq.refl Hnp1)) -- using proof irrelevance for Prop
d2)
d1)
theorem em (p : Prop) [H : decidable p] : p ¬p :=
induction_on H (λ Hp, or.inl Hp) (λ Hnp, or.inr Hnp)
definition by_cases {q : Type} [C : decidable p] (Hpq : p → q) (Hnpq : ¬p → q) : q :=
rec_on C (assume Hp, Hpq Hp) (assume Hnp, Hnpq Hnp)
theorem by_contradiction [Hp : decidable p] (H : ¬p → false) : p :=
or.elim (em p)
(assume H1 : p, H1)
(assume H1 : ¬p, false_elim (H H1))
definition and_decidable [instance] (Hp : decidable p) (Hq : decidable q) : decidable (p ∧ q) :=
rec_on Hp
(assume Hp : p, rec_on Hq
(assume Hq : q, inl (and.intro Hp Hq))
(assume Hnq : ¬q, inr (and.not_right p Hnq)))
(assume Hnp : ¬p, inr (and.not_left q Hnp))
definition or_decidable [instance] (Hp : decidable p) (Hq : decidable q) : decidable (p q) :=
rec_on Hp
(assume Hp : p, inl (or.inl Hp))
(assume Hnp : ¬p, rec_on Hq
(assume Hq : q, inl (or.inr Hq))
(assume Hnq : ¬q, inr (or.not_intro Hnp Hnq)))
definition not_decidable [instance] (Hp : decidable p) : decidable (¬p) :=
rec_on Hp
(assume Hp, inr (not_not_intro Hp))
(assume Hnp, inl Hnp)
definition implies_decidable [instance] (Hp : decidable p) (Hq : decidable q) : decidable (p → q) :=
rec_on Hp
(assume Hp : p, rec_on Hq
(assume Hq : q, inl (assume H, Hq))
(assume Hnq : ¬q, inr (assume H : p → q, absurd (H Hp) Hnq)))
(assume Hnp : ¬p, inl (assume Hp, absurd Hp Hnp))
definition iff_decidable [instance] (Hp : decidable p) (Hq : decidable q) : decidable (p ↔ q) := _
definition decidable_iff_equiv (Hp : decidable p) (H : p ↔ q) : decidable q :=
rec_on Hp
(assume Hp : p, inl (iff.elim_left H Hp))
(assume Hnp : ¬p, inr (iff.elim_left (iff.flip_sign H) Hnp))
definition decidable_eq_equiv (Hp : decidable p) (H : p = q) : decidable q :=
decidable_iff_equiv Hp (eq_to_iff H)
protected theorem rec_subsingleton [instance] [H : decidable p] {H1 : p → Type} {H2 : ¬p → Type}
(H3 : Π(h : p), subsingleton (H1 h)) (H4 : Π(h : ¬p), subsingleton (H2 h))
: subsingleton (rec_on H H1 H2) :=
rec_on H (λh, H3 h) (λh, H4 h) --this can be proven using dependent version of "by_cases"
end decidable
definition decidable_rel {A : Type} (R : A → Prop) := Π (a : A), decidable (R a)
definition decidable_rel2 {A : Type} (R : A → A → Prop) := Π (a b : A), decidable (R a b)
definition decidable_eq (A : Type) := decidable_rel2 (@eq A)
--empty cannot depend on decidable
protected definition empty.has_decidable_eq [instance] : decidable_eq empty :=
take (a b : empty), decidable.inl (!empty.elim a)