feat(logic/basic): introduce pempty

Author: kim-em

data/equiv/basic.lean

@@ -159,6 +159,15 @@ def equiv_empty (h : α → false) : α ≃ empty :=
 def false_equiv_empty : false ≃ empty :=
 equiv_empty _root_.id
 
+def equiv_pempty (h : α → false) : α ≃ pempty :=
+⟨λ x, (h x).elim, λ e, e.rec _, λ x, (h x).elim, λ e, e.rec _⟩
+
+def false_equiv_pempty : false ≃ pempty :=
+equiv_pempty _root_.id
+
+def pempty_equiv_pempty : pempty.{v} ≃ pempty.{w} :=
+equiv_pempty (pempty.elim)
+
 def empty_of_not_nonempty {α : Sort*} (h : ¬ nonempty α) : α ≃ empty :=
 ⟨assume a, (h ⟨a⟩).elim, assume e, e.rec_on _, assume a, (h ⟨a⟩).elim, assume e, e.rec_on _⟩
 
@@ -188,13 +197,13 @@ section
 @[simp] def empty_arrow_equiv_unit (α : Sort*) : (empty → α) ≃ punit.{u} :=
 ⟨λ f, punit.star, λ u e, e.rec _, λ f, funext $ λ x, x.rec _, λ u, by cases u; refl⟩
 
+@[simp] def pempty_arrow_equiv_unit (α : Sort*) : (pempty → α) ≃ punit.{u} :=
+⟨λ f, punit.star, λ u e, e.rec _, λ f, funext $ λ x, x.rec _, λ u, by cases u; refl⟩
+
 @[simp] def false_arrow_equiv_unit (α : Sort*) : (false → α) ≃ punit.{u} :=
 calc (false → α) ≃ (empty → α) : arrow_congr false_equiv_empty (equiv.refl _)
              ... ≃ punit       : empty_arrow_equiv_unit _
 
-def arrow_empty_unit {α : Sort*} : (empty → α) ≃ punit.{u} :=
-⟨λf, punit.star, λu e, e.rec_on _, assume f, funext $ assume e, e.rec_on _, assume u, punit_eq _ _⟩
-
 end
 
 @[congr] def prod_congr {α₁ β₁ α₂ β₂ : Sort*} : α₁ ≃ α₂ → β₁ ≃ β₂ → (α₁ × β₁) ≃ (α₂ × β₂)
@@ -233,6 +242,12 @@ equiv_empty (λ ⟨_, e⟩, e.rec _)
 
 @[simp] def empty_prod (α : Sort*) : (empty × α) ≃ empty :=
 equiv_empty (λ ⟨e, _⟩, e.rec _)
+
+@[simp] def prod_pempty (α : Sort*) : (α × pempty) ≃ pempty :=
+equiv_pempty (λ ⟨_, e⟩, e.rec _)
+
+@[simp] def pempty_prod (α : Sort*) : (pempty × α) ≃ pempty :=
+equiv_pempty (λ ⟨e, _⟩, e.rec _)
 end
 
 section
@@ -293,6 +308,15 @@ noncomputable def Prop_equiv_bool : Prop ≃ bool :=
 @[simp] def empty_sum (α : Sort*) : (empty ⊕ α) ≃ α :=
 (sum_comm _ _).trans $ sum_empty _
 
+@[simp] def sum_pempty (α : Sort*) : (α ⊕ pempty) ≃ α :=
+⟨λ s, match s with inl a := a | inr e := pempty.rec _ e end,
+ inl,
+ λ s, by rcases s with _ | ⟨⟨⟩⟩; refl,
+ λ a, rfl⟩
+
+@[simp] def pempty_sum (α : Sort*) : (pempty ⊕ α) ≃ α :=
+(sum_comm _ _).trans $ sum_pempty _
+
 @[simp] def option_equiv_sum_unit (α : Sort*) : option α ≃ (α ⊕ punit.{u+1}) :=
 ⟨λ o, match o with none := inr punit.star | some a := inl a end,
  λ s, match s with inr _ := none | inl a := some a end,
@@ -450,6 +474,9 @@ protected def univ (α) : @univ α ≃ α :=
 protected def empty (α) : (∅ : set α) ≃ empty :=
 equiv_empty $ λ ⟨x, h⟩, not_mem_empty x h
 
+protected def pempty (α) : (∅ : set α) ≃ pempty :=
+equiv_pempty $ λ ⟨x, h⟩, not_mem_empty x h
+
 protected def union {α} {s t : set α} [decidable_pred s] (H : s ∩ t = ∅) :
   (s ∪ t : set α) ≃ (s ⊕ t) :=
 ⟨λ ⟨x, h⟩, if hs : x ∈ s then sum.inl ⟨_, hs⟩ else sum.inr ⟨_, h.resolve_left hs⟩,

data/fintype.lean

@@ -169,6 +169,12 @@ instance : fintype empty := ⟨∅, empty.rec _⟩
 
 @[simp] theorem fintype.card_empty : fintype.card empty = 0 := rfl
 
+instance : fintype pempty := ⟨∅, pempty.rec _⟩
+
+@[simp] theorem fintype.univ_pempty : @univ pempty _ = ∅ := rfl
+
+@[simp] theorem fintype.card_pempty : fintype.card pempty = 0 := rfl
+
 instance : fintype unit := ⟨⟨()::0, by simp⟩, λ ⟨⟩, by simp⟩
 
 @[simp] theorem fintype.univ_unit : @univ unit _ = {()} := rfl

logic/basic.lean

@@ -37,6 +37,14 @@ instance : decidable_eq empty := λa, a.elim
 @[simp] theorem coe_coe {α β γ} [has_coe α β] [has_coe_t β γ]
   (a : α) : (a : γ) = (a : β) := rfl
 
+/-- `pempty` is the universe-polymorphic analogue of `empty`. -/
+@[derive decidable_eq]
+inductive {u} pempty : Sort u
+
+def pempty.elim {C : Sort*} : pempty → C.
+
+instance subsingleton_pempty : subsingleton pempty := ⟨λa, a.elim⟩
+
 end miscellany
 
 /-

set_theory/cardinal.lean

@@ -146,7 +146,7 @@ local infixr ^ := @has_pow.pow cardinal cardinal cardinal.has_pow
 @[simp] theorem power_zero {a : cardinal} : a ^ 0 = 1 :=
 quotient.induction_on a $ assume α, quotient.sound ⟨
   equiv.trans (equiv.arrow_congr equiv.ulift (equiv.refl α)) $
-  equiv.trans equiv.arrow_empty_unit $
+  equiv.trans (equiv.empty_arrow_equiv_unit α) $
   equiv.ulift.symm⟩
 
 @[simp] theorem power_one {a : cardinal} : a ^ 1 = a :=

tactic/auto_cases.lean

@@ -2,17 +2,18 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Authors: Scott Morrison
 
+import logic.basic
 import tactic.basic
 import data.option
 
 open tactic
 
--- FIXME we need to be able to add more cases here...
--- Alternatively, just put `pempty` into mathlib and I'll survive.
 meta def auto_cases_at (h : expr) : tactic string :=
 do t' ← infer_type h,
   t' ← whnf t',
   let use_cases := match t' with
+  | `(empty)     := tt
+  | `(pempty)    := tt
   | `(unit)      := tt
   | `(punit)     := tt
   | `(ulift _)   := tt