From ae3419f82f2e7b1f5e1099d22dc508cfe341af54 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Wed, 8 Oct 2014 21:41:18 -0400 Subject: [PATCH] feat(library): add definition of subsingleton and some other minor changes --- library/data/empty.lean | 5 +- library/data/prod.lean | 3 +- library/data/sigma.lean | 5 +- library/data/unit.lean | 4 + library/logic/decidable.lean | 154 +++++++++++++++++++---------------- library/logic/eq.lean | 43 ++++++++-- 6 files changed, 130 insertions(+), 84 deletions(-) diff --git a/library/data/empty.lean b/library/data/empty.lean index beb7e6e91..9f4f44e7e 100644 --- a/library/data/empty.lean +++ b/library/data/empty.lean @@ -12,6 +12,9 @@ inductive empty : Type namespace empty protected theorem elim (A : Type) (H : empty) : A := rec (λe, A) H + + protected theorem subsingleton [instance] : subsingleton empty := + subsingleton.intro (λ a b, !elim a) end empty namespace false @@ -19,5 +22,5 @@ namespace false cast (false_elim H) true theorem rec_type (A : Type) (H : false) : A := - empty.rec (λx,A) (to_empty H) + !empty.elim (to_empty H) end false diff --git a/library/data/prod.lean b/library/data/prod.lean index 3b78f571b..96c70a47b 100644 --- a/library/data/prod.lean +++ b/library/data/prod.lean @@ -13,12 +13,13 @@ inductive prod (A B : Type) : Type := mk : A → B → prod A B definition pair := @prod.mk + +namespace prod infixr `×` := prod -- notation for n-ary tuples notation `(` h `,` t:(foldl `,` (e r, prod.mk r e) h) `)` := t -namespace prod section parameters {A B : Type} protected theorem destruct {P : A × B → Prop} (p : A × B) (H : ∀a b, P (a, b)) : P p := diff --git a/library/data/sigma.lean b/library/data/sigma.lean index 6c4ee4a5d..2ae838b17 100644 --- a/library/data/sigma.lean +++ b/library/data/sigma.lean @@ -13,8 +13,9 @@ namespace sigma section parameters {A : Type} {B : A → Type} - definition dpr1 (p : Σ x, B x) : A := rec (λ a b, a) p - definition dpr2 (p : Σ x, B x) : B (dpr1 p) := rec (λ a b, b) p + --without reducible tag, slice.composition_functor in algebra.category.constructions fails + definition dpr1 [reducible] (p : Σ x, B x) : A := rec (λ a b, a) p + definition dpr2 [reducible] (p : Σ x, B x) : B (dpr1 p) := rec (λ a b, b) p theorem dpr1_dpair (a : A) (b : B a) : dpr1 (dpair a b) = a := rfl theorem dpr2_dpair (a : A) (b : B a) : dpr2 (dpair a b) = b := rfl diff --git a/library/data/unit.lean b/library/data/unit.lean index 4cca0914b..3de08a28f 100644 --- a/library/data/unit.lean +++ b/library/data/unit.lean @@ -9,9 +9,13 @@ inductive unit : Type := namespace unit notation `⋆`:max := star + -- remove duplication? protected theorem equal (a b : unit) : a = b := rec (rec rfl b) a + protected theorem subsingleton [instance] : subsingleton unit := + subsingleton.intro (λ a b, equal a b) + theorem eq_star (a : unit) : a = star := equal a star diff --git a/library/logic/decidable.lean b/library/logic/decidable.lean index 76cf4eb4b..ff7f57493 100644 --- a/library/logic/decidable.lean +++ b/library/logic/decidable.lean @@ -2,7 +2,7 @@ -- Released under Apache 2.0 license as described in the file LICENSE. -- Author: Leonardo de Moura -import logic.connectives +import logic.connectives data.empty inductive decidable [class] (p : Prop) : Type := inl : p → decidable p, @@ -10,90 +10,102 @@ inr : ¬p → decidable p namespace decidable -definition true_decidable [instance] : decidable true := -inl trivial + definition true_decidable [instance] : decidable true := + inl trivial -definition false_decidable [instance] : decidable false := -inr not_false_trivial + definition false_decidable [instance] : decidable false := + inr not_false_trivial -protected theorem induction_on {p : Prop} {C : Prop} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C := -decidable.rec H1 H2 H + 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 {p : Prop} {C : Type} (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 -theorem irrelevant {p : Prop} (d1 d2 : decidable p) : 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 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)) -theorem em (p : Prop) {H : decidable p} : p ∨ ¬p := -induction_on H (λ Hp, or.inl Hp) (λ Hnp, or.inr Hnp) + 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) -definition by_cases {a : Prop} {b : Type} {C : decidable a} (Hab : a → b) (Hnab : ¬a → b) : b := -rec_on C (assume Ha, Hab Ha) (assume Hna, Hnab Hna) + 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 by_contradiction {p : Prop} {Hp : decidable p} (H : ¬p → false) : p := -or.elim (em p) - (assume H1 : p, H1) - (assume H1 : ¬p, false_elim (H H1)) + theorem em (p : Prop) {H : decidable p} : p ∨ ¬p := + induction_on H (λ Hp, or.inl Hp) (λ Hnp, or.inr Hnp) -definition and_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : - decidable (a ∧ b) := -rec_on Ha - (assume Ha : a, rec_on Hb - (assume Hb : b, inl (and.intro Ha Hb)) - (assume Hnb : ¬b, inr (and.not_right a Hnb))) - (assume Hna : ¬a, inr (and.not_left b Hna)) + 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) -definition or_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : - decidable (a ∨ b) := -rec_on Ha - (assume Ha : a, inl (or.inl Ha)) - (assume Hna : ¬a, rec_on Hb - (assume Hb : b, inl (or.inr Hb)) - (assume Hnb : ¬b, inr (or.not_intro Hna Hnb))) + 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 not_decidable [instance] {a : Prop} (Ha : decidable a) : decidable (¬a) := -rec_on Ha - (assume Ha, inr (not_not_intro Ha)) - (assume Hna, inl Hna) + 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 iff_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : - decidable (a ↔ b) := -rec_on Ha - (assume Ha, rec_on Hb - (assume Hb : b, inl (iff.intro (assume H, Hb) (assume H, Ha))) - (assume Hnb : ¬b, inr (assume H : a ↔ b, absurd (iff.elim_left H Ha) Hnb))) - (assume Hna, rec_on Hb - (assume Hb : b, inr (assume H : a ↔ b, absurd (iff.elim_right H Hb) Hna)) - (assume Hnb : ¬b, inl - (iff.intro (assume Ha, absurd Ha Hna) (assume Hb, absurd Hb Hnb)))) + 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 implies_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : - decidable (a → b) := -rec_on Ha - (assume Ha : a, rec_on Hb - (assume Hb : b, inl (assume H, Hb)) - (assume Hnb : ¬b, inr (assume H : a → b, absurd (H Ha) Hnb))) - (assume Hna : ¬a, inl (assume Ha, absurd Ha Hna)) + definition not_decidable [instance] (Hp : decidable p) : decidable (¬p) := + rec_on Hp + (assume Hp, inr (not_not_intro Hp)) + (assume Hnp, inl Hnp) -definition decidable_iff_equiv {a b : Prop} (Ha : decidable a) (H : a ↔ b) : decidable b := -rec_on Ha - (assume Ha : a, inl (iff.elim_left H Ha)) - (assume Hna : ¬a, inr (iff.elim_left (iff.flip_sign H) Hna)) + 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 decidable_eq_equiv {a b : Prop} (Ha : decidable a) (H : a = b) : decidable b := -decidable_iff_equiv Ha (eq_to_iff H) + 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 end decidable -definition decidable_eq (A : Type) := Π (a b : A), decidable (a = b) +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) diff --git a/library/logic/eq.lean b/library/logic/eq.lean index 760394d97..e8722e2e3 100644 --- a/library/logic/eq.lean +++ b/library/logic/eq.lean @@ -18,7 +18,7 @@ infix `=` := eq definition rfl {A : Type} {a : A} := eq.refl a -- proof irrelevance is built in -theorem proof_irrel {a : Prop} {H₁ H₂ : a} : H₁ = H₂ := +theorem proof_irrel {a : Prop} (H₁ H₂ : a) : H₁ = H₂ := rfl namespace eq @@ -26,10 +26,10 @@ section variables {A : Type} variables {a b c : A} theorem id_refl (H₁ : a = a) : H₁ = (eq.refl a) := - proof_irrel + !proof_irrel theorem irrel (H₁ H₂ : a = b) : H₁ = H₂ := - proof_irrel + !proof_irrel theorem subst {P : A → Prop} (H₁ : a = b) (H₂ : P a) : P b := rec H₂ H₁ @@ -126,10 +126,14 @@ section end section - variables {A : Type} {B : A → Type} {C : Πa, B a → Type} {R : Type} - variables {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} {c₁ : C a₁ b₁} {c₂ : C a₂ b₂} + variables {A : Type} {B : A → Type} {C : Πa, B a → Type} {D : Πa b, C a b → Type} {R : Type} + variables {a₁ a₂ : A} + {b₁ : B a₁} {b₂ : B a₂} + {c₁ : C a₁ b₁} {c₂ : C a₂ b₂} + {d₁ : D a₁ b₁ c₁} {d₂ : D a₂ b₂ c₂} - theorem congr_arg2_dep (f : Πa, B a → R) (H₁ : a₁ = a₂) (H₂ : eq.rec_on H₁ b₁ = b₂) : f a₁ b₁ = f a₂ b₂ := + theorem congr_arg2_dep (f : Πa, B a → R) (H₁ : a₁ = a₂) (H₂ : eq.rec_on H₁ b₁ = b₂) + : f a₁ b₁ = f a₂ b₂ := eq.rec_on H₁ (λ (b₂ : B a₁) (H₁ : a₁ = a₁) (H₂ : eq.rec_on H₁ b₁ = b₂), calc @@ -138,14 +142,24 @@ section b₂ H₁ H₂ theorem congr_arg3_dep (f : Πa b, C a b → R) (H₁ : a₁ = a₂) (H₂ : eq.rec_on H₁ b₁ = b₂) - (H₃ : eq.rec_on (congr_arg2_dep C H₁ H₂) c₁ = c₂) : f a₁ b₁ c₁ = f a₂ b₂ c₂ := + (H₃ : eq.rec_on (congr_arg2_dep C H₁ H₂) c₁ = c₂) : f a₁ b₁ c₁ = f a₂ b₂ c₂ := eq.rec_on H₁ (λ (b₂ : B a₁) (H₂ : b₁ = b₂) (c₂ : C a₁ b₂) (H₃ : (rec_on (congr_arg2_dep C (refl a₁) H₂) c₁) = c₂), - have H₃' : eq.rec_on H₂ c₁ = c₂, - from (rec_on_irrel H₂ (congr_arg2_dep C (refl a₁) H₂) c₁⁻¹) ▸ H₃, + have H₃' : eq.rec_on H₂ c₁ = c₂, from rec_on_irrel H₂ _ c₁ ⬝ H₃, congr_arg2_dep (f a₁) H₂ H₃') b₂ H₂ c₂ H₃ + + -- for the moment the following theorem is commented out, because it takes long to prove + -- theorem congr_arg4_dep (f : Πa b c, D a b c → R) (H₁ : a₁ = a₂) (H₂ : eq.rec_on H₁ b₁ = b₂) + -- (H₃ : eq.rec_on (congr_arg2_dep C H₁ H₂) c₁ = c₂) + -- (H₄ : eq.rec_on (congr_arg3_dep D H₁ H₂ H₃) d₁ = d₂) : f a₁ b₁ c₁ d₁ = f a₂ b₂ c₂ d₂ := + -- eq.rec_on H₁ + -- (λ b₂ H₂ c₂ H₃ d₂ (H₄ : _), + -- have H₃' [visible] : eq.rec_on H₂ c₁ = c₂, from rec_on_irrel H₂ _ c₁ ⬝ H₃, + -- have H₄' : rec_on (congr_arg2_dep (D a₁) H₂ H₃') d₁ = d₂, from rec_on_irrel _ _ d₁ ⬝ H₄, + -- congr_arg3_dep (f a₁) H₂ H₃' H₄') + -- b₂ H₂ c₂ H₃ d₂ H₄ end section @@ -238,3 +252,14 @@ end theorem true_ne_false : ¬true = false := assume H : true = false, H ▸ trivial + +inductive subsingleton [class] (A : Type) : Prop := +intro : (∀ a b : A, a = b) -> subsingleton A + +namespace subsingleton +definition elim {A : Type} (H : subsingleton A) : ∀(a b : A), a = b := +rec (fun p, p) H +end subsingleton + +protected definition prop.subsingleton [instance] (P : Prop) : subsingleton P := +subsingleton.intro (λa b, !proof_irrel)