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 α.

• 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
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

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

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

Equations
@[instance]
def part.has_mem {α : Type u_1} :
(part α)
Equations
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} :
part α

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

Equations
@[instance]
def part.inhabited {α : Type u_1} :
Equations
@[simp]
theorem part.not_mem_none {α : Type u_1} (a : α) :
def part.some {α : Type u_1} (a : α) :
part α

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

Equations
theorem part.mem_unique {α : Type u_1} {a b : α} {o : part α} :
a ob oa = b
theorem part.mem.left_unique {α : Type u_1} :
theorem part.get_eq_of_mem {α : Type u_1} {o : part α} {a : α} (h : a o) (h' : o.dom) :
o.get h' = a
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
@[simp]
theorem part.mem_some_iff {α : Type u_1} {a b : α} :
b b = a
theorem part.eq_some_iff {α : Type u_1} {a : α} {o : part α} :
o = a o
theorem part.eq_none_iff {α : Type u_1} {o : part α} :
∀ (a : α), a o
theorem part.eq_none_iff' {α : Type u_1} {o : part α} :
@[simp]
theorem part.some_ne_none {α : Type u_1} (x : α) :
@[simp]
theorem part.none_ne_some {α : Type u_1} (x : α) :
theorem part.ne_none_iff {α : Type u_1} {o : part α} :
∃ (x : α), o =
theorem part.eq_none_or_eq_some {α : Type u_1} (o : part α) :
∃ (x : α), o =
@[simp]
theorem part.some_inj {α : Type u_1} {a 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 =
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}  :
@[simp]
theorem part.some_to_option {α : Type u_1} (a : α) [decidable (part.some a).dom] :
@[instance]
def part.none_decidable {α : Type u_1} :
Equations
@[instance]
def part.some_decidable {α : Type u_1} (a : α) :
Equations
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
@[simp]
theorem part.get_or_else_none {α : Type u_1} (d : α)  :
@[simp]
theorem part.get_or_else_some {α : Type u_1} (a d : α) [decidable (part.some a).dom] :
@[simp]
theorem part.mem_to_option {α : Type u_1} {o : part α} [decidable o.dom] {a : α} :
def part.of_option {α : Type u_1} :
part α

Converts an option α into a part α.

Equations
@[simp]
theorem part.mem_of_option {α : Type u_1} {a : α} {o : option α} :
a o
@[simp]
theorem part.of_option_dom {α : Type u_1} (o : option α) :
theorem part.of_option_eq_get {α : Type u_1} (o : option α) :
= {dom := (o.is_some), get :=
@[instance]
def part.has_coe {α : Type u_1} :
has_coe (option α) (part α)
Equations
@[simp]
theorem part.mem_coe {α : Type u_1} {a : α} {o : option α} :
a o a o
@[simp]
theorem part.coe_none {α : Type u_1} :
@[simp]
theorem part.coe_some {α : Type u_1} (a : α) :
(some a) =
theorem part.induction_on {α : Type u_1} {P : part α → Prop} (a : part α) (hnone : P part.none) (hsome : ∀ (a : α), P (part.some a)) :
P a
@[instance]
def part.of_option_decidable {α : Type u_1} (o : option α) :
Equations
@[simp]
theorem part.to_of_option {α : Type u_1} (o : option α) :
= o
@[simp]
theorem part.of_to_option {α : Type u_1} (o : part α) [decidable o.dom] :
def part.equiv_option {α : Type u_1} :
part α

part α is (classically) equivalent to option α.

Equations
@[instance]
def part.order_bot {α : Type u_1} :

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

Equations
@[instance]
def part.preorder {α : Type u_1} :
Equations
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 α) :
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
• f = {dom := ∃ (h : p), (f h).dom, get := λ (ha : ∃ (h : p), (f h).dom), (f _).get _}
def part.bind {α : Type u_1} {β : Type u_2} (f : part α) (g : α → part β) :
part β

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

Equations
@[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 α) :
part β

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

Equations
@[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 of a o
@[simp]
theorem part.mem_map_iff {α : Type u_1} {β : Type u_2} (f : α → β) {o : part α} {b : β} :
b o ∃ (a : α) (H : a o), f a = b
@[simp]
theorem part.map_none {α : Type u_1} {β : Type u_2} (f : α → β) :
@[simp]
theorem part.map_some {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) :
(part.some a) = part.some (f a)
theorem part.mem_assert {α : Type u_1} {p : Prop} {f : p → part α} {a : α} (h : p) :
a f ha f
@[simp]
theorem part.mem_assert_iff {α : Type u_1} {p : Prop} {f : p → part α} {a : α} :
a f ∃ (h : p), a f h
theorem part.assert_pos {α : Type u_1} {p : Prop} {f : p → part α} (h : p) :
f = f h
theorem part.assert_neg {α : Type u_1} {p : Prop} {f : p → part α} (h : ¬p) :
theorem part.mem_bind {α : Type u_1} {β : Type u_2} {f : part α} {g : α → part β} {a : α} {b : β} :
a fb g ab 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 β) :
@[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 α) :
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 : β → γ) :
(x.bind f) = x.bind (λ (y : α), (f y))
theorem part.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β → γ) (f : α → β) (o : part α) :
(part.map f o) = part.map (g f) o
@[instance]
Equations
@[instance]
theorem part.map_id' {α : Type u_1} {f : α → α} (H : ∀ (x : α), f x = x) (o : part α) :
o = o
@[simp]
theorem part.bind_some_right {α : Type u_1} (x : part α) :
= x
@[simp]
theorem part.pure_eq_some {α : Type u_1} (a : α) :
pure a =
@[simp]
theorem part.ret_eq_some {α : Type u_1} (a : α) :
=
@[simp]
theorem part.map_eq_map {α β : Type u_1} (f : α → β) (o : part α) :
f <\$> o = 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 xf a y
@[instance]
Equations
def part.restrict {α : Type u_1} (p : Prop) (o : part α) (H : p → o.dom) :
part α

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

Equations
@[simp]
theorem part.mem_restrict {α : Type u_1} (p : Prop) (o : part α) (h : p → o.dom) (a : α) :
a 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 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