d8a616fa70
I made some major changes in the library. I wanted to wait with pushing until I had finished the formalization of the slice functor, but for some reason that is very hard to formalize, requiring a lot of casts and manipulation of casts. So I've not finished that yet. Changes: - in multiple files make more use of variables - move dependent congr_arg theorems to logic.cast and proof them using heq (which doesn't involve nested inductions and fewer casts). - prove some more theorems involving heq, e.g. hcongr_arg3 (which do not require piext) - in theorems where casts are used in the statement use eq.rec_on instead of eq.drec_on - in category split basic into basic, functor and natural_transformation - change the definition of functor to use fully bundled categories. @avigad: this means that the file semisimplicial.lean will also need changes (but I'm quite sure nothing major). You want to define the fully bundled category Delta, and use only fully bundled categories (type and ᵒᵖ are notations for the fully bundled Type_category and Opposite if you open namespace category.ops). If you want I can make the changes. - lots of minor changes
100 lines
3.9 KiB
Text
100 lines
3.9 KiB
Text
-- 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 _ (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 _ (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)
|
||
|
||
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 em (p : Prop) [H : decidable p] : p ∨ ¬p :=
|
||
by_cases (λ Hp, or.inl Hp) (λ Hnp, or.inr Hnp)
|
||
|
||
theorem by_contradiction [Hp : decidable p] (H : ¬p → false) : p :=
|
||
by_cases
|
||
(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, so we prove this here
|
||
protected definition empty.has_decidable_eq [instance] : decidable_eq empty :=
|
||
take (a b : empty), decidable.inl (!empty.elim a)
|