mathlib documentation

data.part

Partial values of a type #

This file defines part α, the partial values of a type.

o : part α carries a proposition o.dom, its domain, along with a function get : o.dom → α, its value. The rule is then that every partial value has a value but, to access it, you need to provide a proof of the domain.

part α behaves the same as option α except that o : option α is decidably none or some a for some a : α, while the domain of o : part α doesn't have to be decidable. That means you can translate back and forth between a partial value with a decidable domain and an option, and option α and part α are classically equivalent. In general, part α is bigger than option α.

In current mathlib, part ℕ, aka enat, is used to move decidability of the order to decidability of enat.find (which is the smallest natural satisfying a predicate, or ∞ if there's none).

Main declarations #

option-like declarations:

part.none: The partial value whose domain is false.
part.some a: The partial value whose domain is true and whose value is a.
part.of_option: Converts an option α to a part α by sending none to none and some a to some a.
part.to_option: Converts a part α with a decidable domain to an option α.
part.equiv_option: Classical equivalence between part α and option α.

Monadic structure:

part.bind: o.bind f has value (f (o.get _)).get _ (f o morally) and is defined when o and f (o.get _) are defined.
part.map: Maps the value and keeps the same domain.

Other:

part.restrict: part.restrict p o replaces the domain of o : part α by p : Prop so long as p → o.dom.
part.assert: assert p f appends p to the domains of the values of a partial function.
part.unwrap: Gets the value of a partial value regardless of its domain. Unsound.

Notation #

For a : α, o : part α, a ∈ o means that o is defined and equal to a. Formally, it means o.dom and o.get _ = a.

structure part (α : Type u) :

Type u

dom : Prop
get : self.dom → α

part α is the type of "partial values" of type α. It is similar to option α except the domain condition can be an arbitrary proposition, not necessarily decidable.

def part.to_option {α : Type u_1} (o : part α) [decidable o.dom] :

Convert a part α with a decidable domain to an option

Equations

o.to_option = dite o.dom (λ (h : o.dom), some (o.get h)) (λ (h : ¬o.dom), none)

theorem part.ext' {α : Type u_1} {o p : part α} (H1 : o.dom ↔ p.dom) (H2 : ∀ (h₁ : o.dom) (h₂ : p.dom), o.get h₁ = p.get h₂) :

o = p

part extensionality

@[simp]

theorem part.eta {α : Type u_1} (o : part α) :

{dom := o.dom, get := λ (h : o.dom), o.get h} = o

part eta expansion

@[protected]

def part.mem {α : Type u_1} (a : α) (o : part α) :

Prop

a ∈ o means that o is defined and equal to a

Equations

part.mem a o = ∃ (h : o.dom), o.get h = a

@[protected, instance]

def part.has_mem {α : Type u_1} :

has_mem α (part α)

Equations

part.has_mem = {mem := part.mem α}

theorem part.mem_eq {α : Type u_1} (a : α) (o : part α) :

a ∈ o = ∃ (h : o.dom), o.get h = a

theorem part.dom_iff_mem {α : Type u_1} {o : part α} :

o.dom ↔ ∃ (y : α), y ∈ o

theorem part.get_mem {α : Type u_1} {o : part α} (h : o.dom) :

o.get h ∈ o

@[ext]

theorem part.ext {α : Type u_1} {o p : part α} (H : ∀ (a : α), a ∈ o ↔ a ∈ p) :

o = p

part extensionality

def part.none {α : Type u_1} :

The none value in part has a false domain and an empty function.

Equations

part.none = {dom := false, get := false.rec α}

@[protected, instance]

def part.inhabited {α : Type u_1} :

inhabited (part α)

Equations

part.inhabited = {default := part.none α}

@[simp]

theorem part.not_mem_none {α : Type u_1} (a : α) :

a ∉ part.none

def part.some {α : Type u_1} (a : α) :

The some a value in part has a true domain and the function returns a.

Equations

part.some a = {dom := true, get := λ (_x : true), a}

theorem part.mem_unique {α : Type u_1} {a b : α} {o : part α} :

a ∈ o → b ∈ o → a = b

theorem part.mem.left_unique {α : Type u_1} :

relator.left_unique has_mem.mem

theorem part.get_eq_of_mem {α : Type u_1} {o : part α} {a : α} (h : a ∈ o) (h' : o.dom) :

o.get h' = a

@[protected]

theorem part.subsingleton {α : Type u_1} (o : part α) :

{a : α | a ∈ o}.subsingleton

@[simp]

theorem part.get_some {α : Type u_1} {a : α} (ha : (part.some a).dom) :

(part.some a).get ha = a

theorem part.mem_some {α : Type u_1} (a : α) :

a ∈ part.some a

@[simp]

theorem part.mem_some_iff {α : Type u_1} {a b : α} :

b ∈ part.some a ↔ b = a

theorem part.eq_some_iff {α : Type u_1} {a : α} {o : part α} :

o = part.some a ↔ a ∈ o

theorem part.eq_none_iff {α : Type u_1} {o : part α} :

o = part.none ↔ ∀ (a : α), a ∉ o

theorem part.eq_none_iff' {α : Type u_1} {o : part α} :

o = part.none ↔ ¬o.dom

@[simp]

theorem part.some_ne_none {α : Type u_1} (x : α) :

part.some x ≠ part.none

@[simp]

theorem part.none_ne_some {α : Type u_1} (x : α) :

part.none ≠ part.some x

theorem part.ne_none_iff {α : Type u_1} {o : part α} :

o ≠ part.none ↔ ∃ (x : α), o = part.some x

theorem part.eq_none_or_eq_some {α : Type u_1} (o : part α) :

o = part.none ∨ ∃ (x : α), o = part.some x

@[simp]

theorem part.some_inj {α : Type u_1} {a b : α} :

part.some a = part.some b ↔ a = b

@[simp]

theorem part.some_get {α : Type u_1} {a : part α} (ha : a.dom) :

part.some (a.get ha) = a

theorem part.get_eq_iff_eq_some {α : Type u_1} {a : part α} {ha : a.dom} {b : α} :

a.get ha = b ↔ a = part.some b

theorem part.get_eq_get_of_eq {α : Type u_1} (a : part α) (ha : a.dom) {b : part α} (h : a = b) :

a.get ha = b.get _

theorem part.get_eq_iff_mem {α : Type u_1} {o : part α} {a : α} (h : o.dom) :

o.get h = a ↔ a ∈ o

theorem part.eq_get_iff_mem {α : Type u_1} {o : part α} {a : α} (h : o.dom) :

a = o.get h ↔ a ∈ o

@[simp]

theorem part.none_to_option {α : Type u_1} [decidable part.none.dom] :

part.none.to_option = none

@[simp]

theorem part.some_to_option {α : Type u_1} (a : α) [decidable (part.some a).dom] :

(part.some a).to_option = some a

@[protected, instance]

def part.none_decidable {α : Type u_1} :

decidable part.none.dom

Equations

part.none_decidable = decidable.false

@[protected, instance]

def part.some_decidable {α : Type u_1} (a : α) :

decidable (part.some a).dom

Equations

part.some_decidable a = decidable.true

def part.get_or_else {α : Type u_1} (a : part α) [decidable a.dom] (d : α) :

α

Retrieves the value of a : part α if it exists, and return the provided default value otherwise.

Equations

a.get_or_else d = dite a.dom (λ (ha : a.dom), a.get ha) (λ (ha : ¬a.dom), d)

@[simp]

theorem part.get_or_else_none {α : Type u_1} (d : α) [decidable part.none.dom] :

part.none.get_or_else d = d

@[simp]

theorem part.get_or_else_some {α : Type u_1} (a d : α) [decidable (part.some a).dom] :

(part.some a).get_or_else d = a

@[simp]

theorem part.mem_to_option {α : Type u_1} {o : part α} [decidable o.dom] {a : α} :

a ∈ o.to_option ↔ a ∈ o

def part.of_option {α : Type u_1} :

option α → part α

Converts an option α into a part α.

Equations

part.of_option (some a) = part.some a
part.of_option none = part.none

@[simp]

theorem part.mem_of_option {α : Type u_1} {a : α} {o : option α} :

a ∈ part.of_option o ↔ a ∈ o

@[simp]

theorem part.of_option_dom {α : Type u_1} (o : option α) :

(part.of_option o).dom ↔ ↥(o.is_some)

theorem part.of_option_eq_get {α : Type u_1} (o : option α) :

part.of_option o = {dom := ↥(o.is_some), get := option.get o}

@[protected, instance]

def part.has_coe {α : Type u_1} :

has_coe (option α) (part α)

Equations

part.has_coe = {coe := part.of_option α}

@[simp]

theorem part.mem_coe {α : Type u_1} {a : α} {o : option α} :

a ∈ ↑o ↔ a ∈ o

@[simp]

theorem part.coe_none {α : Type u_1} :

↑none = part.none

@[simp]

theorem part.coe_some {α : Type u_1} (a : α) :

↑(some a) = part.some a

@[protected]

theorem part.induction_on {α : Type u_1} {P : part α → Prop} (a : part α) (hnone : P part.none) (hsome : ∀ (a : α), P (part.some a)) :

P a

@[protected, instance]

def part.of_option_decidable {α : Type u_1} (o : option α) :

decidable (part.of_option o).dom

Equations

@[simp]

theorem part.to_of_option {α : Type u_1} (o : option α) :

(part.of_option o).to_option = o

@[simp]

theorem part.of_to_option {α : Type u_1} (o : part α) [decidable o.dom] :

part.of_option o.to_option = o

noncomputable def part.equiv_option {α : Type u_1} :

part α ≃ option α

part α is (classically) equivalent to option α.

Equations

part.equiv_option = {to_fun := λ (o : part α), o.to_option, inv_fun := part.of_option α, left_inv := _, right_inv := _}

@[protected, instance]

def part.partial_order {α : Type u_1} :

partial_order (part α)

We give part α the order where everything is greater than none.

Equations

part.partial_order = {le := λ (x y : part α), ∀ (i : α), i ∈ x → i ∈ y, lt := preorder.lt._default (λ (x y : part α), ∀ (i : α), i ∈ x → i ∈ y), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

@[protected, instance]

def part.order_bot {α : Type u_1} :

order_bot (part α)

Equations

part.order_bot = {bot := part.none α, bot_le := _}

theorem part.le_total_of_le_of_le {α : Type u_1} {x y : part α} (z : part α) (hx : x ≤ z) (hy : y ≤ z) :

x ≤ y ∨ y ≤ x

def part.assert {α : Type u_1} (p : Prop) (f : p → part α) :

assert p f is a bind-like operation which appends an additional condition p to the domain and uses f to produce the value.

Equations

part.assert p f = {dom := ∃ (h : p), (f h).dom, get := λ (ha : ∃ (h : p), (f h).dom), (f _).get _}

@[protected]

def part.bind {α : Type u_1} {β : Type u_2} (f : part α) (g : α → part β) :

The bind operation has value g (f.get), and is defined when all the parts are defined.

Equations

f.bind g = part.assert f.dom (λ (b : f.dom), g (f.get b))

@[simp]

theorem part.map_get {α : Type u_1} {β : Type u_2} (f : α → β) (o : part α) (ᾰ : o.dom) :

(part.map f o).get ᾰ = (f ∘ o.get) ᾰ

def part.map {α : Type u_1} {β : Type u_2} (f : α → β) (o : part α) :

The map operation for part just maps the value and maintains the same domain.

Equations

part.map f o = {dom := o.dom, get := f ∘ o.get}

@[simp]

theorem part.map_dom {α : Type u_1} {β : Type u_2} (f : α → β) (o : part α) :

(part.map f o).dom = o.dom

theorem part.mem_map {α : Type u_1} {β : Type u_2} (f : α → β) {o : part α} {a : α} :

a ∈ o → f a ∈ part.map f o

@[simp]

theorem part.mem_map_iff {α : Type u_1} {β : Type u_2} (f : α → β) {o : part α} {b : β} :

b ∈ part.map f o ↔ ∃ (a : α) (H : a ∈ o), f a = b

@[simp]

theorem part.map_none {α : Type u_1} {β : Type u_2} (f : α → β) :

part.map f part.none = part.none

@[simp]

theorem part.map_some {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) :

part.map f (part.some a) = part.some (f a)

theorem part.mem_assert {α : Type u_1} {p : Prop} {f : p → part α} {a : α} (h : p) :

a ∈ f h → a ∈ part.assert p f

@[simp]

theorem part.mem_assert_iff {α : Type u_1} {p : Prop} {f : p → part α} {a : α} :

a ∈ part.assert p f ↔ ∃ (h : p), a ∈ f h

theorem part.assert_pos {α : Type u_1} {p : Prop} {f : p → part α} (h : p) :

part.assert p f = f h

theorem part.assert_neg {α : Type u_1} {p : Prop} {f : p → part α} (h : ¬p) :

part.assert p f = part.none

theorem part.mem_bind {α : Type u_1} {β : Type u_2} {f : part α} {g : α → part β} {a : α} {b : β} :

a ∈ f → b ∈ g a → b ∈ f.bind g

@[simp]

theorem part.mem_bind_iff {α : Type u_1} {β : Type u_2} {f : part α} {g : α → part β} {b : β} :

b ∈ f.bind g ↔ ∃ (a : α) (H : a ∈ f), b ∈ g a

@[simp]

theorem part.bind_none {α : Type u_1} {β : Type u_2} (f : α → part β) :

part.none.bind f = part.none

@[simp]

theorem part.bind_some {α : Type u_1} {β : Type u_2} (a : α) (f : α → part β) :

(part.some a).bind f = f a

theorem part.bind_of_mem {α : Type u_1} {β : Type u_2} {o : part α} {a : α} (h : a ∈ o) (f : α → part β) :

o.bind f = f a

theorem part.bind_some_eq_map {α : Type u_1} {β : Type u_2} (f : α → β) (x : part α) :

x.bind (part.some ∘ f) = part.map f x

theorem part.bind_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : part α) (g : α → part β) (k : β → part γ) :

(f.bind g).bind k = f.bind (λ (x : α), (g x).bind k)

@[simp]

theorem part.bind_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (x : part α) (g : β → part γ) :

(part.map f x).bind g = x.bind (λ (y : α), g (f y))

@[simp]

theorem part.map_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → part β) (x : part α) (g : β → γ) :

part.map g (x.bind f) = x.bind (λ (y : α), part.map g (f y))

theorem part.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β → γ) (f : α → β) (o : part α) :

part.map g (part.map f o) = part.map (g ∘ f) o

@[protected, instance]

def part.monad :

Equations

part.monad = monad.mk

@[protected, instance]

def part.is_lawful_monad :

is_lawful_monad part

theorem part.map_id' {α : Type u_1} {f : α → α} (H : ∀ (x : α), f x = x) (o : part α) :

part.map f o = o

@[simp]

theorem part.bind_some_right {α : Type u_1} (x : part α) :

x.bind part.some = x

@[simp]

theorem part.pure_eq_some {α : Type u_1} (a : α) :

pure a = part.some a

@[simp]

theorem part.ret_eq_some {α : Type u_1} (a : α) :

return a = part.some a

@[simp]

theorem part.map_eq_map {α β : Type u_1} (f : α → β) (o : part α) :

f <$> o = part.map f o

@[simp]

theorem part.bind_eq_bind {α β : Type u_1} (f : part α) (g : α → part β) :

f >>= g = f.bind g

theorem part.bind_le {β α : Type u_2} (x : part α) (f : α → part β) (y : part β) :

x >>= f ≤ y ↔ ∀ (a : α), a ∈ x → f a ≤ y

@[protected, instance]

def part.monad_fail :

monad_fail part

Equations

part.monad_fail = {fail := λ (_x : Type u_1) (_x_1 : string), part.none}

def part.restrict {α : Type u_1} (p : Prop) (o : part α) (H : p → o.dom) :

restrict p o h replaces the domain of o with p, and is well defined when p implies o is defined.

Equations

part.restrict p o H = {dom := p, get := λ (h : p), o.get _}

@[simp]

theorem part.mem_restrict {α : Type u_1} (p : Prop) (o : part α) (h : p → o.dom) (a : α) :

a ∈ part.restrict p o h ↔ p ∧ a ∈ o

meta def part.unwrap {α : Type u_1} (o : part α) :

α

unwrap o gets the value at o, ignoring the condition. This function is unsound.

theorem part.assert_defined {α : Type u_1} {p : Prop} {f : p → part α} (h : p) :

(f h).dom → (part.assert p f).dom

theorem part.bind_defined {α : Type u_1} {β : Type u_2} {f : part α} {g : α → part β} (h : f.dom) :

(g (f.get h)).dom → (f.bind g).dom

@[simp]

theorem part.bind_dom {α : Type u_1} {β : Type u_2} {f : part α} {g : α → part β} :

(f.bind g).dom ↔ ∃ (h : f.dom), (g (f.get h)).dom