Documentation

Mathlib.Logic.Unique

Types with a unique term #

In this file we define a typeclass Unique, which expresses that a type has a unique term. In other words, a type that is Inhabited and a Subsingleton.

Main declaration #

Unique: a typeclass that expresses that a type has a unique term.

Main statements #

Unique.mk': an inhabited subsingleton type is Unique. This can not be an instance because it would lead to loops in typeclass inference.
Function.Surjective.unique: if the domain of a surjective function is Unique, then its codomain is unique as well.
Function.Injective.subsingleton: if the codomain of an injective function is Subsingleton, then its domain is Subsingleton as well.
Function.Injective.unique: if the codomain of an injective function is Subsingleton and its domain is Inhabited, then its domain is Unique.

Implementation details #

The typeclass Unique α is implemented as a type, rather than a Prop-valued predicate, for good definitional properties of the default term.

theorem Unique.ext {α : Sort u} (x : Unique α) (y : Unique α) (default : default = default) :

x = y

theorem Unique.ext_iff {α : Sort u} (x : Unique α) (y : Unique α) :

x = y ↔ default = default

class Unique (α : Sort u) extends Inhabited :

Sort (max1u)

In a Unique type, every term is equal to the default element (from Inhabited).
uniq : ∀ (a : α), a = default

Unique α expresses that α is a type with a unique term default.

This is implemented as a type, rather than a Prop-valued predicate, for good definitional properties of the default term.

Instances

theorem unique_iff_exists_unique (α : Sort u) :

Nonempty (Unique α) ↔ ∃! x, True

theorem unique_subtype_iff_exists_unique {α : Sort u_1} (p : α → Prop) :

Nonempty (Unique (Subtype p)) ↔ ∃! a, p a

def uniqueOfSubsingleton {α : Sort u_1} [inst : Subsingleton α] (a : α) :

Given an explicit a : α with Subsingleton α, we can construct a Unique α instance. This is a def because the typeclass search cannot arbitrarily invent the a : α term. Nevertheless, these instances are all equivalent by Unique.Subsingleton.unique.

See note [reducible non-instances].

Equations

uniqueOfSubsingleton a = { toInhabited := { default := a }, uniq := (_ : ∀ (x : α), x = default) }

instance PUnit.unique :

Equations

PUnit.unique = { toInhabited := { default := PUnit.unit }, uniq := PUnit.unique.proof_1 }

@[simp]

theorem PUnit.default_eq_unit :

default = PUnit.unit

def uniqueProp {p : Prop} (h : p) :

Every provable proposition is unique, as all proofs are equal.

Equations

uniqueProp h = { toInhabited := { default := h }, uniq := (_ : ∀ (x : p), x = x) }

instance instUniqueTrue :

Equations

instUniqueTrue = uniqueProp trivial

theorem Fin.eq_zero (n : Fin 1) :

n = 0

instance instInhabitedFinSucc {n : ℕ} :

Inhabited (Fin (Nat.succ n))

Equations

instInhabitedFinSucc = { default := 0 }

instance inhabitedFinOneAdd (n : ℕ) :

Inhabited (Fin (1 + n))

Equations

inhabitedFinOneAdd n = { default := { val := 0, isLt := (_ : 0 < 1 + n) } }

@[simp]

theorem Fin.default_eq_zero (n : ℕ) :

default = 0

instance Fin.unique :

Equations

Fin.unique = { toInhabited := instInhabitedFinSucc, uniq := Fin.eq_zero }

instance Unique.instInhabited {α : Sort u_1} [inst : Unique α] :

Equations

Unique.instInhabited = inst.toInhabited

theorem Unique.eq_default {α : Sort u_1} [inst : Unique α] (a : α) :

a = default

theorem Unique.default_eq {α : Sort u_1} [inst : Unique α] (a : α) :

default = a

instance Unique.instSubsingleton {α : Sort u_1} [inst : Unique α] :

Subsingleton α

Equations

@Unique.instSubsingleton = @Unique.instSubsingleton.proof_1

theorem Unique.forall_iff {α : Sort u_1} [inst : Unique α] {p : α → Prop} :

((a : α) → p a) ↔ p default

theorem Unique.exists_iff {α : Sort u_1} [inst : Unique α] {p : α → Prop} :

Exists p ↔ p default

theorem Unique.subsingleton_unique' {α : Sort u_1} (h₁ : Unique α) (h₂ : Unique α) :

h₁ = h₂

instance Unique.subsingleton_unique {α : Sort u_1} :

Subsingleton (Unique α)

Equations

@Unique.subsingleton_unique = @Unique.subsingleton_unique.proof_1

def Unique.mk' (α : Sort u) [h₁ : Inhabited α] [inst : Subsingleton α] :

Construct Unique from Inhabited and Subsingleton. Making this an instance would create a loop in the class inheritance graph.

Equations

Unique.mk' α = { toInhabited := { default := default }, uniq := (_ : ∀ (x : α), x = default) }

theorem unique_iff_subsingleton_and_nonempty (α : Sort u) :

Nonempty (Unique α) ↔ Subsingleton α ∧ Nonempty α

@[simp]

theorem Pi.default_def {α : Sort u_1} {β : α → Sort v} [inst : (a : α) → Inhabited (β a)] :

default = fun a => default

theorem Pi.default_apply {α : Sort u_1} {β : α → Sort v} [inst : (a : α) → Inhabited (β a)] (a : α) :

default ((a : α) → β a) (instInhabitedForAll_1 α) a = default

instance Pi.unique {α : Sort u_1} {β : α → Sort v} [inst : (a : α) → Unique (β a)] :

Unique ((a : α) → β a)

Equations

Pi.unique = { toInhabited := instInhabitedForAll_1 α, uniq := (_ : ∀ (x : (a : α) → β a), x = default) }

instance Pi.uniqueOfIsEmpty {α : Sort u_1} [inst : IsEmpty α] (β : α → Sort v) :

Unique ((a : α) → β a)

There is a unique function on an empty domain.

Equations

Pi.uniqueOfIsEmpty β = { toInhabited := { default := fun a => isEmptyElim a }, uniq := (_ : ∀ (x : (a : α) → β a), x = default) }

theorem eq_const_of_unique {α : Sort u_1} {β : Sort u_2} [inst : Unique α] (f : α → β) :

f = Function.const α (f default)

theorem heq_const_of_unique {α : Sort u_1} [inst : Unique α] {β : α → Sort v} (f : (a : α) → β a) :

HEq f (Function.const α (f default))

theorem Function.Injective.subsingleton {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Function.Injective f) [inst : Subsingleton β] :

Subsingleton α

If the codomain of an injective function is a subsingleton, then the domain is a subsingleton as well.

theorem Function.Surjective.subsingleton {α : Sort u_1} {β : Sort u_2} {f : α → β} [inst : Subsingleton α] (hf : Function.Surjective f) :

Subsingleton β

If the domain of a surjective function is a subsingleton, then the codomain is a subsingleton as well.

def Function.Surjective.unique {α : Sort u} {β : Sort u_1} (f : α → β) (hf : Function.Surjective f) [inst : Unique α] :

If the domain of a surjective function is a singleton, then the codomain is a singleton as well.

Equations

Function.Surjective.unique f hf = Unique.mk' β

def Function.Injective.unique {α : Sort u_1} {β : Sort u_2} {f : α → β} [inst : Inhabited α] [inst : Subsingleton β] (hf : Function.Injective f) :

If α is inhabited and admits an injective map to a subsingleton type, then α is Unique.

Equations

Function.Injective.unique hf = Unique.mk' α

def Function.Surjective.uniqueOfSurjectiveConst (α : Type u_1) {β : Type u_2} (b : β) (h : Function.Surjective (Function.const α b)) :

If a constant function is surjective, then the codomain is a singleton.

Equations

Function.Surjective.uniqueOfSurjectiveConst α b h = uniqueOfSubsingleton b

theorem Unique.bijective {A : Sort u_1} {B : Sort u_2} [inst : Unique A] [inst : Unique B] {f : A → B} :

Function.Bijective f

theorem Option.subsingleton_iff_isEmpty {α : Type u} :

Subsingleton (Option α) ↔ IsEmpty α

Option α is a Subsingleton if and only if α is empty.

instance Option.instUniqueOption {α : Type u_1} [inst : IsEmpty α] :

Unique (Option α)

Equations

Option.instUniqueOption = Unique.mk' (Option α)

instance Unique.subtypeEq {α : Sort u} (y : α) :

Unique { x // x = y }

Equations

Unique.subtypeEq y = { toInhabited := { default := { val := y, property := (_ : y = y) } }, uniq := (_ : ∀ (x : { x // x = y }), x = default) }

instance Unique.subtypeEq' {α : Sort u} (y : α) :

Unique { x // y = x }

Equations

Unique.subtypeEq' y = { toInhabited := { default := { val := y, property := (_ : y = y) } }, uniq := (_ : ∀ (x : { x // y = x }), x = default) }