Mathlib.Logic.Unique

Unique structure

(α : Sort u) extends Inhabited α

Full source

/-- `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. -/
@[ext]
structure Unique (α : Sort u) extends Inhabited α where
  /-- In a `Unique` type, every term is equal to the default element (from `Inhabited`). -/
  uniq : ∀ a : α, a = default

Type with a unique element

Informal description

The structure `Unique α` expresses that the type `α` has exactly one element, called `default`. This combines the properties of being inhabited (having at least one element) and being a subsingleton (having at most one element).

unique_iff_existsUnique theorem

(α : Sort u) : Nonempty (Unique α) ↔ ∃! _ : α, True

Full source

theorem unique_iff_existsUnique (α : Sort u) : NonemptyNonempty (Unique α) ↔ ∃! _ : α, True :=
  ⟨fun ⟨u⟩ ↦ ⟨u.default, trivial, fun a _ ↦ u.uniq a⟩,
   fun ⟨a, _, h⟩ ↦ ⟨⟨⟨a⟩, fun _ ↦ h _ trivial⟩⟩⟩

Equivalence of Unique Type and Unique Element Existence

Informal description

For any type $\alpha$, the following are equivalent: 1. There exists a unique instance of the `Unique` structure on $\alpha$. 2. There exists a unique element $a$ in $\alpha$ (i.e., $\exists! a : \alpha, \text{True}$).

unique_subtype_iff_existsUnique theorem

{α} (p : α → Prop) : Nonempty (Unique (Subtype p)) ↔ ∃! a, p a

Full source

theorem unique_subtype_iff_existsUnique {α} (p : α → Prop) :
    NonemptyNonempty (Unique (Subtype p)) ↔ ∃! a, p a :=
  ⟨fun ⟨u⟩ ↦ ⟨u.default.1, u.default.2, fun a h ↦ congr_arg Subtype.val (u.uniq ⟨a, h⟩)⟩,
   fun ⟨a, ha, he⟩ ↦ ⟨⟨⟨⟨a, ha⟩⟩, fun ⟨b, hb⟩ ↦ by
      congr
      exact he b hb⟩⟩⟩

Subtype is Unique iff Predicate has Unique Solution

Informal description

For any type $\alpha$ and predicate $p : \alpha \to \mathrm{Prop}$, the subtype $\{x : \alpha \mid p(x)\}$ is nonempty and unique (i.e., has exactly one element) if and only if there exists a unique element $a \in \alpha$ satisfying $p(a)$.

uniqueOfSubsingleton abbrev

{α : Sort*} [Subsingleton α] (a : α) : Unique α

Full source

/-- 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]. -/
abbrev uniqueOfSubsingleton {α : Sort*} [Subsingleton α] (a : α) : Unique α where
  default := a
  uniq _ := Subsingleton.elim _ _

Construction of Unique Instance from Subsingleton and Element

Informal description

Given a type $\alpha$ that is a subsingleton (i.e., any two elements are equal) and an explicit element $a : \alpha$, we can construct a `Unique \alpha$ instance, which asserts that $\alpha$ has exactly one element (namely $a$).

PUnit.instUnique instance

: Unique PUnit.{u}

Full source

instance PUnit.instUnique : Unique PUnitPUnit.{u} where
  default := PUnit.unit
  uniq x := subsingleton x _

The Unit Type is Unique

Informal description

The type `PUnit` has exactly one element, which is `PUnit.unit`.

PUnit.default_eq_unit theorem

: (default : PUnit) = PUnit.unit

Full source

@[simp]
theorem PUnit.default_eq_unit : (default : PUnit) = PUnit.unit :=
  rfl

Default Element of PUnit is Unit

Informal description

The default element of the type `PUnit` is equal to its unique element `PUnit.unit`.

uniqueProp definition

{p : Prop} (h : p) : Unique.{0} p

Full source

/-- Every provable proposition is unique, as all proofs are equal. -/
def uniqueProp {p : Prop} (h : p) : Unique.{0} p where
  default := h
  uniq _ := rfl

Unique element of a provable proposition

Informal description

For any proposition $ p $ that is provable (i.e., $ h : p $ is given), the type $ p $ has a unique element. This is because all proofs of $ p $ are equal by proof irrelevance.

instUniqueTrue instance

: Unique True

Full source

instance : Unique True :=
  uniqueProp trivial

Uniqueness of the True Proposition

Informal description

The proposition `True` has a unique element.

Unique.instInhabited instance

: Inhabited α

Full source

instance (priority := 100) : Inhabited α :=
  toInhabited ‹Unique α›

Unique Types are Inhabited

Informal description

For any type $\alpha$ with a unique element, $\alpha$ is inhabited (has at least one element).

Unique.default_eq theorem

(a : α) : default = a

Full source

theorem default_eq (a : α) : default = a :=
  (uniq _ a).symm

Default Element Equals Any Element in Unique Types

Informal description

For any element $a$ of a type $\alpha$ with a unique element, the default element of $\alpha$ is equal to $a$.

Unique.instSubsingleton instance

: Subsingleton α

Full source

instance (priority := 100) instSubsingleton : Subsingleton α :=
  subsingleton_of_forall_eq _ eq_default

Unique Types are Subsingletons

Informal description

For any type $\alpha$ with a unique element, $\alpha$ is a subsingleton (has at most one element).

Unique.forall_iff theorem

{p : α → Prop} : (∀ a, p a) ↔ p default

Full source

theorem forall_iff {p : α → Prop} : (∀ a, p a) ↔ p default :=
  ⟨fun h ↦ h _, fun h x ↦ by rwa [Unique.eq_default x]⟩

Universal Quantification in Unique Types is Equivalent to Default Element Satisfying Predicate

Informal description

For any predicate $p$ on a type $\alpha$ with a unique element, the universal quantification $\forall a, p(a)$ holds if and only if $p$ holds for the default element of $\alpha$.

Unique.exists_iff theorem

{p : α → Prop} : Exists p ↔ p default

Full source

theorem exists_iff {p : α → Prop} : ExistsExists p ↔ p default :=
  ⟨fun ⟨a, ha⟩ ↦ eq_default a ▸ ha, Exists.intro default⟩

Existence in Unique Types is Equivalent to Default Element Satisfying Predicate

Informal description

For any predicate $p$ on a type $\alpha$ with a unique element, the existence of an element $a \in \alpha$ satisfying $p(a)$ is equivalent to the default element of $\alpha$ satisfying $p$. In other words, $\exists a, p(a) \leftrightarrow p(\text{default})$.

Unique.subsingleton_unique' theorem

: ∀ h₁ h₂ : Unique α, h₁ = h₂

Full source

@[ext]
protected theorem subsingleton_unique' : ∀ h₁ h₂ : Unique α, h₁ = h₂
  | ⟨⟨x⟩, h⟩, ⟨⟨y⟩, _⟩ => by congr; rw [h x, h y]

Uniqueness of the Unique Instance

Informal description

For any two instances `h₁` and `h₂` of the `Unique α` structure on a type `α`, we have `h₁ = h₂`.

Unique.subsingleton_unique instance

: Subsingleton (Unique α)

Full source

instance subsingleton_unique : Subsingleton (Unique α) :=
  ⟨Unique.subsingleton_unique'⟩

Uniqueness of Unique Instances

Informal description

For any type $\alpha$, the type `Unique α` is a subsingleton. In other words, there is at most one way to construct a `Unique` instance for a given type $\alpha$.

Unique.mk' abbrev

(α : Sort u) [h₁ : Inhabited α] [Subsingleton α] : Unique α

Full source

/-- Construct `Unique` from `Inhabited` and `Subsingleton`. Making this an instance would create
a loop in the class inheritance graph. -/
abbrev mk' (α : Sort u) [h₁ : Inhabited α] [Subsingleton α] : Unique α :=
  { h₁ with uniq := fun _ ↦ Subsingleton.elim _ _ }

Construction of Unique Type from Inhabited Subsingleton

Informal description

Given a type $\alpha$ that is inhabited (has at least one element) and is a subsingleton (has at most one element), then $\alpha$ has a unique element (i.e., is a `Unique` type).

nonempty_unique theorem

(α : Sort u) [Subsingleton α] [Nonempty α] : Nonempty (Unique α)

Full source

theorem nonempty_unique (α : Sort u) [Subsingleton α] [Nonempty α] : Nonempty (Unique α) := by
  inhabit α
  exact ⟨Unique.mk' α⟩

Existence of Unique Element in Nonempty Subsingleton Types

Informal description

For any type $\alpha$ that is a subsingleton (has at most one element) and is nonempty (has at least one element), there exists a unique element of type $\alpha$.

unique_iff_subsingleton_and_nonempty theorem

(α : Sort u) : Nonempty (Unique α) ↔ Subsingleton α ∧ Nonempty α

Full source

theorem unique_iff_subsingleton_and_nonempty (α : Sort u) :
    NonemptyNonempty (Unique α) ↔ Subsingleton α ∧ Nonempty α :=
  ⟨fun ⟨u⟩ ↦ by constructor <;> exact inferInstance,
   fun ⟨hs, hn⟩ ↦ nonempty_unique α⟩

Characterization of Unique Types via Subsingleton and Nonempty Properties

Informal description

For any type $\alpha$, the existence of a unique element (i.e., $\alpha$ is a `Unique` type) is equivalent to $\alpha$ being a subsingleton (having at most one element) and nonempty (having at least one element). In other words, $\text{Nonempty (Unique $\alpha$)} \leftrightarrow \text{Subsingleton $\alpha$} \land \text{Nonempty $\alpha$}$.

Pi.default_def theorem

{β : α → Sort v} [∀ a, Inhabited (β a)] : @default (∀ a, β a) _ = fun a : α ↦ @default (β a) _

Full source

@[simp]
theorem Pi.default_def {β : α → Sort v} [∀ a, Inhabited (β a)] :
    @default (∀ a, β a) _ = fun a : α ↦ @default (β a) _ :=
  rfl

Default Value of Product Type as Pointwise Defaults

Informal description

For any family of types $\beta : \alpha \to \text{Sort } v$ where each $\beta(a)$ is inhabited, the default value of the product type $\forall a, \beta(a)$ is the function that maps each $a \in \alpha$ to the default value of $\beta(a)$.

Pi.default_apply theorem

{β : α → Sort v} [∀ a, Inhabited (β a)] (a : α) : @default (∀ a, β a) _ a = default

Full source

theorem Pi.default_apply {β : α → Sort v} [∀ a, Inhabited (β a)] (a : α) :
    @default (∀ a, β a) _ a = default :=
  rfl

Default Value of Dependent Function at Point Equals Default Value of Component

Informal description

For any family of types $\beta : \alpha \to \text{Sort } v$ where each $\beta(a)$ is inhabited, the default value of the dependent function type $\forall a, \beta(a)$ evaluated at any $a : \alpha$ equals the default value of $\beta(a)$. In other words, $(\text{default} : \forall a, \beta(a))(a) = \text{default} : \beta(a)$.

Pi.unique instance

{β : α → Sort v} [∀ a, Unique (β a)] : Unique (∀ a, β a)

Full source

instance Pi.unique {β : α → Sort v} [∀ a, Unique (β a)] : Unique (∀ a, β a) where
  uniq := fun _ ↦ funext fun _ ↦ Unique.eq_default _

Uniqueness of Dependent Functions with Unique Components

Informal description

For any family of types $\beta : \alpha \to \text{Sort } v$ where each $\beta(a)$ has a unique element, the dependent function type $\forall a, \beta(a)$ also has a unique element.

Pi.uniqueOfIsEmpty instance

[IsEmpty α] (β : α → Sort v) : Unique (∀ a, β a)

Full source

/-- There is a unique function on an empty domain. -/
instance Pi.uniqueOfIsEmpty [IsEmpty α] (β : α → Sort v) : Unique (∀ a, β a) where
  default := isEmptyElim
  uniq _ := funext isEmptyElim

Uniqueness of Functions on Empty Domains

Informal description

For any empty type $\alpha$ and any family of types $\beta : \alpha \to \text{Sort } v$, the dependent function type $\forall a, \beta(a)$ has a unique element (the empty function).

heq_const_of_unique theorem

[Unique α] {β : α → Sort v} (f : ∀ a, β a) : HEq f (Function.const α (f default))

Full source

theorem heq_const_of_unique [Unique α] {β : α → Sort v} (f : ∀ a, β a) :
    HEq f (Function.const α (f default)) :=
  (Function.hfunext rfl) fun i _ _ ↦ by rw [Subsingleton.elim i default]; rfl

Heterogeneous Equality of Dependent Functions on Unique Types with Constant Functions

Informal description

For any type $\alpha$ with a unique element and any type family $\beta : \alpha \to \Sort v$, a dependent function $f : \forall a, \beta a$ is heterogeneously equal to the constant function that maps every element of $\alpha$ to $f(\text{default})$.

Function.Injective.subsingleton theorem

(hf : Injective f) [Subsingleton β] : Subsingleton α

Full source

/-- If the codomain of an injective function is a subsingleton, then the domain
is a subsingleton as well. -/
protected theorem Injective.subsingleton (hf : Injective f) [Subsingleton β] : Subsingleton α :=
  ⟨fun _ _ ↦ hf <| Subsingleton.elim _ _⟩

Injective Functions Preserve Subsingleton Property

Informal description

If $ f : \alpha \to \beta $ is an injective function and $ \beta $ is a subsingleton (i.e., all elements of $ \beta $ are equal), then $ \alpha $ is also a subsingleton.

Function.Surjective.subsingleton theorem

[Subsingleton α] (hf : Surjective f) : Subsingleton β

Full source

/-- If the domain of a surjective function is a subsingleton, then the codomain is a subsingleton as
well. -/
protected theorem Surjective.subsingleton [Subsingleton α] (hf : Surjective f) : Subsingleton β :=
  ⟨hf.forall₂.2 fun x y ↦ congr_arg f <| Subsingleton.elim x y⟩

Surjective Functions Preserve Subsingleton Property

Informal description

If $\alpha$ is a subsingleton (i.e., all elements of $\alpha$ are equal) and $f : \alpha \to \beta$ is a surjective function, then $\beta$ is also a subsingleton.

Function.Surjective.unique definition

{α : Sort u} (f : α → β) (hf : Surjective f) [Unique.{u} α] : Unique β

Full source

/-- If the domain of a surjective function is a singleton,
then the codomain is a singleton as well. -/
protected def Surjective.unique {α : Sort u} (f : α → β) (hf : Surjective f) [Unique.{u} α] :
    Unique β :=
  @Unique.mk' _ ⟨f default⟩ hf.subsingleton

Surjective function from unique domain implies unique codomain

Informal description

If $ f : \alpha \to \beta $ is a surjective function and the domain $\alpha$ has a unique element, then the codomain $\beta$ also has a unique element.

Function.Injective.unique definition

[Inhabited α] [Subsingleton β] (hf : Injective f) : Unique α

Full source

/-- If `α` is inhabited and admits an injective map to a subsingleton type, then `α` is `Unique`. -/
protected def Injective.unique [Inhabited α] [Subsingleton β] (hf : Injective f) : Unique α :=
  @Unique.mk' _ _ hf.subsingleton

Injective function from inhabited type to subsingleton implies uniqueness

Informal description

If a type $\alpha$ is inhabited and there exists an injective function $f : \alpha \to \beta$ where $\beta$ is a subsingleton, then $\alpha$ has exactly one element (i.e., $\alpha$ is `Unique`).

Function.Surjective.uniqueOfSurjectiveConst definition

(α : Type*) {β : Type*} (b : β) (h : Function.Surjective (Function.const α b)) : Unique β

Full source

/-- If a constant function is surjective, then the codomain is a singleton. -/
def Surjective.uniqueOfSurjectiveConst (α : Type*) {β : Type*} (b : β)
    (h : Function.Surjective (Function.const α b)) : Unique β :=
  @uniqueOfSubsingleton _ (subsingleton_of_forall_eq b <| h.forall.mpr fun _ ↦ rfl) b

Uniqueness of codomain of a surjective constant function

Informal description

Given a type $\beta$ and an element $b \in \beta$, if the constant function $\alpha \to \beta$ sending every element of $\alpha$ to $b$ is surjective, then $\beta$ has exactly one element (namely $b$).

uniqueElim definition

[Unique ι] (x : α (default : ι)) (i : ι) : α i

Full source

/-- Given one value over a unique, we get a dependent function. -/
def uniqueElim [Unique ι] (x : α (default : ι)) (i : ι) : α i := by
  rw [Unique.eq_default i]
  exact x

Dependent elimination for unique types

Informal description

Given a type $\iota$ with a unique element (default) and a family of types $\alpha$ indexed by $\iota$, the function `uniqueElim` takes an element $x$ of $\alpha$ at the default index and any index $i$, and returns $x$ as an element of $\alpha i$. This works because in a unique type, any index $i$ is equal to the default index.

uniqueElim_default theorem

{_ : Unique ι} (x : α (default : ι)) : uniqueElim x (default : ι) = x

Full source

@[simp]
theorem uniqueElim_default {_ : Unique ι} (x : α (default : ι)) : uniqueElim x (default : ι) = x :=
  rfl

Default Element Property in Unique Types

Informal description

For any type $\iota$ with a unique element (default) and any family of types $\alpha$ indexed by $\iota$, the function `uniqueElim` satisfies $\text{uniqueElim}\,x\,(\text{default}) = x$ for any $x \in \alpha(\text{default})$.

uniqueElim_const theorem

{β : Sort*} {_ : Unique ι} (x : β) (i : ι) : uniqueElim (α := fun _ ↦ β) x i = x

Full source

@[simp]
theorem uniqueElim_const {β : Sort*} {_ : Unique ι} (x : β) (i : ι) :
    uniqueElim (α := fun _ ↦ β) x i = x :=
  rfl

Constant Elimination in Unique Types

Informal description

For any type $\beta$ and any unique type $\iota$ (i.e., a type with exactly one element), the function `uniqueElim` applied to a constant family $\alpha := \lambda \_, \beta$ satisfies $\text{uniqueElim}\,x\,i = x$ for any $x : \beta$ and $i : \iota$.

Unique.bijective theorem

{A B} [Unique A] [Unique B] {f : A → B} : Function.Bijective f

Full source

theorem Unique.bijective {A B} [Unique A] [Unique B] {f : A → B} : Function.Bijective f := by
  rw [Function.bijective_iff_has_inverse]
  refine ⟨default, ?_, ?_⟩ <;> intro x <;> simp

Bijectivity of Functions Between Unique Types

Informal description

Let $A$ and $B$ be types with unique elements, and let $f : A \to B$ be a function. Then $f$ is bijective.

Option.subsingleton_iff_isEmpty theorem

{α : Type u} : Subsingleton (Option α) ↔ IsEmpty α

Full source

/-- `Option α` is a `Subsingleton` if and only if `α` is empty. -/
theorem subsingleton_iff_isEmpty {α : Type u} : SubsingletonSubsingleton (Option α) ↔ IsEmpty α :=
  ⟨fun h ↦ ⟨fun x ↦ Option.noConfusion <| @Subsingleton.elim _ h x none⟩,
   fun h ↦ ⟨fun x y ↦
     Option.casesOn x (Option.casesOn y rfl fun x ↦ h.elim x) fun x ↦ h.elim x⟩⟩

Subsingleton Property of `Option α` and Emptiness of $\alpha$

Informal description

For any type $\alpha$, the type `Option α` (which adds a "none" element to $\alpha$) is a subsingleton (i.e., has at most one element) if and only if $\alpha$ is empty (i.e., has no elements).

Option.instUniqueOfIsEmpty instance

{α} [IsEmpty α] : Unique (Option α)

Full source

instance {α} [IsEmpty α] : Unique (Option α) :=
  @Unique.mk' _ _ (subsingleton_iff_isEmpty.2 ‹_›)

Uniqueness of `Option α` for Empty $\alpha$

Informal description

For any type $\alpha$ that is empty, the type `Option α` (which adds a distinguished "none" element to $\alpha$) has exactly one element.

Unique.subtypeEq instance

(y : α) : Unique { x // x = y }

Full source

instance Unique.subtypeEq (y : α) : Unique { x // x = y } where
  default := ⟨y, rfl⟩
  uniq := fun ⟨x, hx⟩ ↦ by congr

Uniqueness of the Subtype $\{x \mid x = y\}$

Informal description

For any element $y$ in a type $\alpha$, the subtype $\{x \mid x = y\}$ has exactly one element.

Unique.subtypeEq' instance

(y : α) : Unique { x // y = x }

Full source

instance Unique.subtypeEq' (y : α) : Unique { x // y = x } where
  default := ⟨y, rfl⟩
  uniq := fun ⟨x, hx⟩ ↦ by subst hx; congr

Uniqueness of the Subtype $\{x \mid y = x\}$

Informal description

For any element $y$ in a type $\alpha$, the subtype $\{x \mid y = x\}$ has exactly one element.

Fin.instUnique instance

: Unique (Fin 1)

Full source

instance Fin.instUnique : Unique (Fin 1) where uniq _ := Subsingleton.elim _ _

Uniqueness of $\text{Fin}(1)$

Informal description

The finite type $\text{Fin}(1)$ has exactly one element.

Mathlib.Logic.Unique

Main declaration

Main statements

Implementation details