data.part

# Partial values of a type #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 part_enat, is used to move decidability of the order to decidability of part_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) :
• 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.

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

Convert a part α with a decidable domain to an option

Equations
@[simp]
theorem part.to_option_is_some {α : Type u_1} (o : part α) [decidable o.dom] :
@[simp]
theorem part.to_option_is_none {α : Type u_1} (o : part α) [decidable o.dom] :
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
@[protected, 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
@[simp]
theorem part.mem_mk_iff {α : Type u_1} {p : Prop} {o : p α} {a : α} :
a {dom := p, get := o} (h : p), o h = a
@[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
@[protected, 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
@[simp]
theorem part.some_dom {α : Type u_1} (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} :
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
@[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.not_none_dom {α : Type u_1} :
@[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 =
theorem part.some_injective {α : Type u_1} :
@[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] :
@[protected, instance]
def part.none_decidable {α : Type u_1} :
Equations
@[protected, 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
theorem part.get_or_else_of_dom {α : Type u_1} (a : part α) (h : a.dom) [decidable a.dom] (d : α) :
a.get_or_else d = a.get h
theorem part.get_or_else_of_not_dom {α : Type u_1} (a : part α) (h : ¬a.dom) [decidable a.dom] (d : α) :
@[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 : α} :
@[protected]
theorem part.dom.to_option {α : Type u_1} {o : part α} [decidable o.dom] (h : o.dom) :
theorem part.to_option_eq_none_iff {α : Type u_1} {a : part α} [decidable a.dom] :
@[simp]
theorem part.elim_to_option {α : Type u_1} {β : Type u_2} (a : part α) [decidable a.dom] (b : β) (f : α β) :
f a.to_option = dite a.dom (λ (h : a.dom), f (a.get h)) (λ (h : ¬a.dom), b)
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 :=
@[protected, 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 : α) :
@[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 α) :
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] :
noncomputable def part.equiv_option {α : Type u_1} :
part α

part α is (classically) equivalent to option α.

Equations
@[protected, instance]
def part.partial_order {α : Type u_1} :

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

Equations
@[protected, instance]
def part.order_bot {α : 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
@[protected]
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 o f 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 h a 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 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
@[protected]
theorem part.dom.bind {α : Type u_1} {β : Type u_2} {o : part α} (h : o.dom) (f : α part β) :
o.bind f = f (o.get h)
theorem part.dom.of_bind {α : Type u_1} {β : Type u_2} {f : α part β} {a : part α} (h : (a.bind f).dom) :
a.dom
@[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_to_option {α : Type u_1} {β : Type u_2} (f : α part β) (o : part α) [decidable o.dom] [Π (a : α), decidable (f a).dom] [decidable (o.bind f).dom] :
(o.bind f).to_option = (λ (a : α), (f a).to_option) o.to_option
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
@[protected, instance]
Equations
@[protected, 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 : α) :
@[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 x f a y
@[protected, 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
@[protected, instance]
def part.has_zero {α : Type u_1} [has_zero α] :
Equations
@[protected, instance]
def part.has_one {α : Type u_1} [has_one α] :
Equations
@[protected, instance]
def part.has_mul {α : Type u_1} [has_mul α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def part.has_neg {α : Type u_1} [has_neg α] :
Equations
@[protected, instance]
def part.has_inv {α : Type u_1} [has_inv α] :
Equations
@[protected, instance]
def part.has_div {α : Type u_1} [has_div α] :
Equations
@[protected, instance]
def part.has_sub {α : Type u_1} [has_sub α] :
Equations
@[protected, instance]
def part.has_mod {α : Type u_1} [has_mod α] :
Equations
@[protected, instance]
def part.has_append {α : Type u_1} [has_append α] :
Equations
@[protected, instance]
def part.has_inter {α : Type u_1} [has_inter α] :
Equations
@[protected, instance]
def part.has_union {α : Type u_1} [has_union α] :
Equations
@[protected, instance]
def part.has_sdiff {α : Type u_1} [has_sdiff α] :
Equations
theorem part.zero_mem_zero {α : Type u_1} [has_zero α] :
0 0
theorem part.one_mem_one {α : Type u_1} [has_one α] :
1 1
theorem part.add_mem_add {α : Type u_1} [has_add α] (a b : part α) (ma mb : α) (ha : ma a) (hb : mb b) :
ma + mb a + b
theorem part.mul_mem_mul {α : Type u_1} [has_mul α] (a b : part α) (ma mb : α) (ha : ma a) (hb : mb b) :
ma * mb a * b
theorem part.left_dom_of_add_dom {α : Type u_1} [has_add α] {a b : part α} (hab : (a + b).dom) :
a.dom
theorem part.left_dom_of_mul_dom {α : Type u_1} [has_mul α] {a b : part α} (hab : (a * b).dom) :
a.dom
theorem part.right_dom_of_mul_dom {α : Type u_1} [has_mul α] {a b : part α} (hab : (a * b).dom) :
b.dom
theorem part.right_dom_of_add_dom {α : Type u_1} [has_add α] {a b : part α} (hab : (a + b).dom) :
b.dom
@[simp]
theorem part.mul_get_eq {α : Type u_1} [has_mul α] (a b : part α) (hab : (a * b).dom) :
(a * b).get hab = a.get _ * b.get _
@[simp]
theorem part.add_get_eq {α : Type u_1} [has_add α] (a b : part α) (hab : (a + b).dom) :
(a + b).get hab = a.get _ + b.get _
theorem part.some_add_some {α : Type u_1} [has_add α] (a b : α) :
= part.some (a + b)
theorem part.some_mul_some {α : Type u_1} [has_mul α] (a b : α) :
= part.some (a * b)
theorem part.neg_mem_neg {α : Type u_1} [has_neg α] (a : part α) (ma : α) (ha : ma a) :
-ma -a
theorem part.inv_mem_inv {α : Type u_1} [has_inv α] (a : part α) (ma : α) (ha : ma a) :
theorem part.inv_some {α : Type u_1} [has_inv α] (a : α) :
theorem part.neg_some {α : Type u_1} [has_neg α] (a : α) :
theorem part.div_mem_div {α : Type u_1} [has_div α] (a b : part α) (ma mb : α) (ha : ma a) (hb : mb b) :
ma / mb a / b
theorem part.sub_mem_sub {α : Type u_1} [has_sub α] (a b : part α) (ma mb : α) (ha : ma a) (hb : mb b) :
ma - mb a - b
theorem part.left_dom_of_div_dom {α : Type u_1} [has_div α] {a b : part α} (hab : (a / b).dom) :
a.dom
theorem part.left_dom_of_sub_dom {α : Type u_1} [has_sub α] {a b : part α} (hab : (a - b).dom) :
a.dom
theorem part.right_dom_of_sub_dom {α : Type u_1} [has_sub α] {a b : part α} (hab : (a - b).dom) :
b.dom
theorem part.right_dom_of_div_dom {α : Type u_1} [has_div α] {a b : part α} (hab : (a / b).dom) :
b.dom
@[simp]
theorem part.sub_get_eq {α : Type u_1} [has_sub α] (a b : part α) (hab : (a - b).dom) :
(a - b).get hab = a.get _ - b.get _
@[simp]
theorem part.div_get_eq {α : Type u_1} [has_div α] (a b : part α) (hab : (a / b).dom) :
(a / b).get hab = a.get _ / b.get _
theorem part.some_div_some {α : Type u_1} [has_div α] (a b : α) :
= part.some (a / b)
theorem part.some_sub_some {α : Type u_1} [has_sub α] (a b : α) :
= part.some (a - b)
theorem part.mod_mem_mod {α : Type u_1} [has_mod α] (a b : part α) (ma mb : α) (ha : ma a) (hb : mb b) :
ma % mb a % b
theorem part.left_dom_of_mod_dom {α : Type u_1} [has_mod α] {a b : part α} (hab : (a % b).dom) :
a.dom
theorem part.right_dom_of_mod_dom {α : Type u_1} [has_mod α] {a b : part α} (hab : (a % b).dom) :
b.dom
@[simp]
theorem part.mod_get_eq {α : Type u_1} [has_mod α] (a b : part α) (hab : (a % b).dom) :
(a % b).get hab = a.get _ % b.get _
theorem part.some_mod_some {α : Type u_1} [has_mod α] (a b : α) :
= part.some (a % b)
theorem part.append_mem_append {α : Type u_1} [has_append α] (a b : part α) (ma mb : α) (ha : ma a) (hb : mb b) :
ma ++ mb a ++ b
theorem part.left_dom_of_append_dom {α : Type u_1} [has_append α] {a b : part α} (hab : (a ++ b).dom) :
a.dom
theorem part.right_dom_of_append_dom {α : Type u_1} [has_append α] {a b : part α} (hab : (a ++ b).dom) :
b.dom
@[simp]
theorem part.append_get_eq {α : Type u_1} [has_append α] (a b : part α) (hab : (a ++ b).dom) :
(a ++ b).get hab = a.get _ ++ b.get _
theorem part.some_append_some {α : Type u_1} [has_append α] (a b : α) :
= part.some (a ++ b)
theorem part.inter_mem_inter {α : Type u_1} [has_inter α] (a b : part α) (ma mb : α) (ha : ma a) (hb : mb b) :
ma mb a b
theorem part.left_dom_of_inter_dom {α : Type u_1} [has_inter α] {a b : part α} (hab : (a b).dom) :
a.dom
theorem part.right_dom_of_inter_dom {α : Type u_1} [has_inter α] {a b : part α} (hab : (a b).dom) :
b.dom
@[simp]
theorem part.inter_get_eq {α : Type u_1} [has_inter α] (a b : part α) (hab : (a b).dom) :
(a b).get hab = a.get _ b.get _
theorem part.some_inter_some {α : Type u_1} [has_inter α] (a b : α) :
= part.some (a b)
theorem part.union_mem_union {α : Type u_1} [has_union α] (a b : part α) (ma mb : α) (ha : ma a) (hb : mb b) :
ma mb a b
theorem part.left_dom_of_union_dom {α : Type u_1} [has_union α] {a b : part α} (hab : (a b).dom) :
a.dom
theorem part.right_dom_of_union_dom {α : Type u_1} [has_union α] {a b : part α} (hab : (a b).dom) :
b.dom
@[simp]
theorem part.union_get_eq {α : Type u_1} [has_union α] (a b : part α) (hab : (a b).dom) :
(a b).get hab = a.get _ b.get _
theorem part.some_union_some {α : Type u_1} [has_union α] (a b : α) :
= part.some (a b)
theorem part.sdiff_mem_sdiff {α : Type u_1} [has_sdiff α] (a b : part α) (ma mb : α) (ha : ma a) (hb : mb b) :
ma \ mb a \ b
theorem part.left_dom_of_sdiff_dom {α : Type u_1} [has_sdiff α] {a b : part α} (hab : (a \ b).dom) :
a.dom
theorem part.right_dom_of_sdiff_dom {α : Type u_1} [has_sdiff α] {a b : part α} (hab : (a \ b).dom) :
b.dom
@[simp]
theorem part.sdiff_get_eq {α : Type u_1} [has_sdiff α] (a b : part α) (hab : (a \ b).dom) :
(a \ b).get hab = a.get _ \ b.get _
theorem part.some_sdiff_some {α : Type u_1} [has_sdiff α] (a b : α) :
= part.some (a \ b)