feat(library): add definition of subsingleton and some other minor changes

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

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 :=

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

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
 

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)

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)