2014-07-19 19:09:47 +00:00
|
|
|
|
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
|
|
|
|
-- Released under Apache 2.0 license as described in the file LICENSE.
|
|
|
|
|
-- Author: Leonardo de Moura
|
2014-08-01 00:48:51 +00:00
|
|
|
|
|
2014-10-09 01:41:18 +00:00
|
|
|
|
import logic.connectives data.empty
|
2014-07-19 19:09:47 +00:00
|
|
|
|
|
2014-10-08 01:02:15 +00:00
|
|
|
|
inductive decidable [class] (p : Prop) : Type :=
|
2014-08-22 22:46:10 +00:00
|
|
|
|
inl : p → decidable p,
|
|
|
|
|
inr : ¬p → decidable p
|
2014-07-19 19:09:47 +00:00
|
|
|
|
|
2014-09-04 22:03:59 +00:00
|
|
|
|
namespace decidable
|
|
|
|
|
|
2014-10-09 01:41:18 +00:00
|
|
|
|
definition true_decidable [instance] : decidable true :=
|
|
|
|
|
inl trivial
|
|
|
|
|
|
|
|
|
|
definition false_decidable [instance] : decidable false :=
|
|
|
|
|
inr not_false_trivial
|
|
|
|
|
|
|
|
|
|
section
|
|
|
|
|
variables {p q : Prop}
|
|
|
|
|
protected theorem induction_on {C : Prop} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C :=
|
|
|
|
|
decidable.rec H1 H2 H
|
|
|
|
|
|
|
|
|
|
protected definition rec_on {C : decidable p → Type} (H : decidable p)
|
|
|
|
|
(H1 : Π(a : p), C (inl a)) (H2 : Π(a : ¬p), C (inr a)) :
|
|
|
|
|
C H :=
|
|
|
|
|
decidable.rec H1 H2 H
|
|
|
|
|
|
|
|
|
|
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
|
2014-08-20 02:32:44 +00:00
|
|
|
|
end decidable
|
2014-09-08 05:22:04 +00:00
|
|
|
|
|
2014-10-09 01:41:18 +00:00
|
|
|
|
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)
|