mathlib documentation

data.pfun

structure roption (α : Type u) :
Type u
  • dom : Prop
  • get : c.dom → α

roption α 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 roption.to_option {α : Type u_1} (o : roption α) [decidable o.dom] :

Convert an roption α with a decidable domain to an option

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

roption extensionality

@[simp]
theorem roption.eta {α : Type u_1} (o : roption α) :
{dom := o.dom, get := λ (h : o.dom), o.get h} = o

roption eta expansion

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

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

Equations
@[instance]
def roption.has_mem {α : Type u_1} :
Equations
theorem roption.mem_eq {α : Type u_1} (a : α) (o : roption α) :
a o = ∃ (h : o.dom), o.get h = a
theorem roption.dom_iff_mem {α : Type u_1} {o : roption α} :
o.dom ∃ (y : α), y o
theorem roption.get_mem {α : Type u_1} {o : roption α} (h : o.dom) :
o.get h o
@[ext]
theorem roption.ext {α : Type u_1} {o p : roption α} (H : ∀ (a : α), a o a p) :
o = p

roption extensionality

def roption.none {α : Type u_1} :

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

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

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

Equations
theorem roption.mem_unique {α : Type u_1} {a b : α} {o : roption α} :
a ob oa = b
theorem roption.get_eq_of_mem {α : Type u_1} {o : roption α} {a : α} (h : a o) (h' : o.dom) :
o.get h' = a
@[simp]
theorem roption.get_some {α : Type u_1} {a : α} (ha : (roption.some a).dom) :
(roption.some a).get ha = a
theorem roption.mem_some {α : Type u_1} (a : α) :
@[simp]
theorem roption.mem_some_iff {α : Type u_1} {a b : α} :
theorem roption.eq_some_iff {α : Type u_1} {a : α} {o : roption α} :
theorem roption.eq_none_iff {α : Type u_1} {o : roption α} :
o = roption.none ∀ (a : α), a o
theorem roption.eq_none_iff' {α : Type u_1} {o : roption α} :
theorem roption.some_ne_none {α : Type u_1} (x : α) :
theorem roption.ne_none_iff {α : Type u_1} {o : roption α} :
o roption.none ∃ (x : α), o = roption.some x
theorem roption.eq_none_or_eq_some {α : Type u_1} (o : roption α) :
o = roption.none ∃ (x : α), o = roption.some x
@[simp]
theorem roption.some_inj {α : Type u_1} {a b : α} :
@[simp]
theorem roption.some_get {α : Type u_1} {a : roption α} (ha : a.dom) :
roption.some (a.get ha) = a
theorem roption.get_eq_iff_eq_some {α : Type u_1} {a : roption α} {ha : a.dom} {b : α} :
a.get ha = b a = roption.some b
theorem roption.get_eq_get_of_eq {α : Type u_1} (a : roption α) (ha : a.dom) {b : roption α} (h : a = b) :
a.get ha = b.get _
@[instance]
def roption.some_decidable {α : Type u_1} (a : α) :
Equations
def roption.get_or_else {α : Type u_1} (a : roption α) [decidable a.dom] (d : α) :
α
Equations
@[simp]
theorem roption.get_or_else_none {α : Type u_1} (d : α) :
@[simp]
theorem roption.get_or_else_some {α : Type u_1} (a d : α) :
@[simp]
theorem roption.mem_to_option {α : Type u_1} {o : roption α} [decidable o.dom] {a : α} :
def roption.of_option {α : Type u_1} :
option αroption α

Convert an option α into an roption α

Equations
@[simp]
theorem roption.mem_of_option {α : Type u_1} {a : α} {o : option α} :
@[simp]
theorem roption.of_option_dom {α : Type u_1} (o : option α) :
theorem roption.of_option_eq_get {α : Type u_1} (o : option α) :
@[instance]
def roption.has_coe {α : Type u_1} :
Equations
@[simp]
theorem roption.mem_coe {α : Type u_1} {a : α} {o : option α} :
a o a o
@[simp]
theorem roption.coe_none {α : Type u_1} :
@[simp]
theorem roption.coe_some {α : Type u_1} (a : α) :
theorem roption.induction_on {α : Type u_1} {P : roption α → Prop} (a : roption α) (hnone : P roption.none) (hsome : ∀ (a : α), P (roption.some a)) :
P a
@[simp]
theorem roption.to_of_option {α : Type u_1} (o : option α) :
@[simp]
theorem roption.of_to_option {α : Type u_1} (o : roption α) [decidable o.dom] :
def roption.equiv_option {α : Type u_1} :
Equations
@[instance]
def roption.order_bot {α : Type u_1} :
Equations
@[instance]
def roption.preorder {α : Type u_1} :
Equations
theorem roption.le_total_of_le_of_le {α : Type u_1} {x y : roption α} (z : roption α) (hx : x z) (hy : y z) :
x y y x
def roption.assert {α : Type u_1} (p : Prop) (f : p → roption α) :

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
def roption.bind {α : Type u_1} {β : Type u_2} (f : roption α) (g : α → roption β) :

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

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

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

Equations
theorem roption.mem_map {α : Type u_1} {β : Type u_2} (f : α → β) {o : roption α} {a : α} :
a of a roption.map f o
@[simp]
theorem roption.mem_map_iff {α : Type u_1} {β : Type u_2} (f : α → β) {o : roption α} {b : β} :
b roption.map f o ∃ (a : α) (H : a o), f a = b
@[simp]
theorem roption.map_none {α : Type u_1} {β : Type u_2} (f : α → β) :
@[simp]
theorem roption.map_some {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) :
theorem roption.mem_assert {α : Type u_1} {p : Prop} {f : p → roption α} {a : α} (h : p) :
a f ha roption.assert p f
@[simp]
theorem roption.mem_assert_iff {α : Type u_1} {p : Prop} {f : p → roption α} {a : α} :
a roption.assert p f ∃ (h : p), a f h
theorem roption.assert_pos {α : Type u_1} {p : Prop} {f : p → roption α} (h : p) :
theorem roption.assert_neg {α : Type u_1} {p : Prop} {f : p → roption α} (h : ¬p) :
theorem roption.mem_bind {α : Type u_1} {β : Type u_2} {f : roption α} {g : α → roption β} {a : α} {b : β} :
a fb g ab f.bind g
@[simp]
theorem roption.mem_bind_iff {α : Type u_1} {β : Type u_2} {f : roption α} {g : α → roption β} {b : β} :
b f.bind g ∃ (a : α) (H : a f), b g a
@[simp]
theorem roption.bind_none {α : Type u_1} {β : Type u_2} (f : α → roption β) :
@[simp]
theorem roption.bind_some {α : Type u_1} {β : Type u_2} (a : α) (f : α → roption β) :
(roption.some a).bind f = f a
theorem roption.bind_some_eq_map {α : Type u_1} {β : Type u_2} (f : α → β) (x : roption α) :
theorem roption.bind_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : roption α) (g : α → roption β) (k : β → roption γ) :
(f.bind g).bind k = f.bind (λ (x : α), (g x).bind k)
@[simp]
theorem roption.bind_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (x : roption α) (g : β → roption γ) :
(roption.map f x).bind g = x.bind (λ (y : α), g (f y))
@[simp]
theorem roption.map_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → roption β) (x : roption α) (g : β → γ) :
roption.map g (x.bind f) = x.bind (λ (y : α), roption.map g (f y))
theorem roption.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β → γ) (f : α → β) (o : roption α) :
@[instance]
Equations
theorem roption.map_id' {α : Type u_1} {f : α → α} (H : ∀ (x : α), f x = x) (o : roption α) :
@[simp]
theorem roption.bind_some_right {α : Type u_1} (x : roption α) :
@[simp]
theorem roption.pure_eq_some {α : Type u_1} (a : α) :
@[simp]
theorem roption.ret_eq_some {α : Type u_1} (a : α) :
@[simp]
theorem roption.map_eq_map {α β : Type u_1} (f : α → β) (o : roption α) :
f <$> o = roption.map f o
@[simp]
theorem roption.bind_eq_bind {α β : Type u_1} (f : roption α) (g : α → roption β) :
f >>= g = f.bind g
theorem roption.bind_le {β α : Type u_2} (x : roption α) (f : α → roption β) (y : roption β) :
x >>= f y ∀ (a : α), a xf a y
@[instance]
Equations
def roption.restrict {α : Type u_1} (p : Prop) (o : roption α) :
(p → o.dom)roption α
Equations
@[simp]
theorem roption.mem_restrict {α : Type u_1} (p : Prop) (o : roption α) (h : p → o.dom) (a : α) :
meta def roption.unwrap {α : Type u_1} (o : roption α) :
α

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

theorem roption.assert_defined {α : Type u_1} {p : Prop} {f : p → roption α} (h : p) :
(f h).dom(roption.assert p f).dom
theorem roption.bind_defined {α : Type u_1} {β : Type u_2} {f : roption α} {g : α → roption β} (h : f.dom) :
(g (f.get h)).dom(f.bind g).dom
@[simp]
theorem roption.bind_dom {α : Type u_1} {β : Type u_2} {f : roption α} {g : α → roption β} :
(f.bind g).dom ∃ (h : f.dom), (g (f.get h)).dom
def pfun (α : Type u_1) (β : Type u_2) :
Type (max u_1 u_2)

pfun α β, or α →. β, is the type of partial functions from α to β. It is defined as α → roption β.

Equations
@[instance]
def pfun.inhabited {α : Type u_1} {β : Type u_2} :
inhabited →. β)
Equations
def pfun.dom {α : Type u_1} {β : Type u_2} (f : α →. β) :
set α

The domain of a partial function

Equations
theorem pfun.mem_dom {α : Type u_1} {β : Type u_2} (f : α →. β) (x : α) :
x f.dom ∃ (y : β), y f x
theorem pfun.dom_eq {α : Type u_1} {β : Type u_2} (f : α →. β) :
f.dom = {x : α | ∃ (y : β), y f x}
def pfun.fn {α : Type u_1} {β : Type u_2} (f : α →. β) (x : α) (h : f.dom x) :
β

Evaluate a partial function

Equations
def pfun.eval_opt {α : Type u_1} {β : Type u_2} (f : α →. β) [D : decidable_pred (λ (_x : α), _x f.dom)] (x : α) :

Evaluate a partial function to return an option

Equations
theorem pfun.ext' {α : Type u_1} {β : Type u_2} {f g : α →. β} (H1 : ∀ (a : α), a f.dom a g.dom) (H2 : ∀ (a : α) (p : f.dom a) (q : g.dom a), f.fn a p = g.fn a q) :
f = g

Partial function extensionality

theorem pfun.ext {α : Type u_1} {β : Type u_2} {f g : α →. β} (H : ∀ (a : α) (b : β), b f a b g a) :
f = g
def pfun.as_subtype {α : Type u_1} {β : Type u_2} (f : α →. β) (s : (f.dom)) :
β

Turn a partial function into a function out of a subtype

Equations
def pfun.equiv_subtype {α : Type u_1} {β : Type u_2} :
→. β) Σ (p : α → Prop), subtype p → β

The set of partial functions α →. β is equivalent to the set of pairs (p : α → Prop, f : subtype p → β).

Equations
theorem pfun.as_subtype_eq_of_mem {α : Type u_1} {β : Type u_2} {f : α →. β} {x : α} {y : β} (fxy : y f x) (domx : x f.dom) :
f.as_subtype x, domx⟩ = y
def pfun.lift {α : Type u_1} {β : Type u_2} (f : α → β) :
α →. β

Turn a total function into a partial function

Equations
@[instance]
def pfun.has_coe {α : Type u_1} {β : Type u_2} :
has_coe (α → β) →. β)
Equations
@[simp]
theorem pfun.lift_eq_coe {α : Type u_1} {β : Type u_2} (f : α → β) :
@[simp]
theorem pfun.coe_val {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) :
f a = roption.some (f a)
def pfun.graph {α : Type u_1} {β : Type u_2} (f : α →. β) :
set × β)

The graph of a partial function is the set of pairs (x, f x) where x is in the domain of f.

Equations
def pfun.graph' {α : Type u_1} {β : Type u_2} (f : α →. β) :
rel α β
Equations
def pfun.ran {α : Type u_1} {β : Type u_2} (f : α →. β) :
set β

The range of a partial function is the set of values f x where x is in the domain of f.

Equations
  • f.ran = {b : β | ∃ (a : α), b f a}
def pfun.restrict {α : Type u_1} {β : Type u_2} (f : α →. β) {p : set α} (H : p f.dom) :
α →. β

Restrict a partial function to a smaller domain.

Equations
@[simp]
theorem pfun.mem_restrict {α : Type u_1} {β : Type u_2} {f : α →. β} {s : set α} (h : s f.dom) (a : α) (b : β) :
b f.restrict h a a s b f a
def pfun.res {α : Type u_1} {β : Type u_2} (f : α → β) (s : set α) :
α →. β
Equations
theorem pfun.mem_res {α : Type u_1} {β : Type u_2} (f : α → β) (s : set α) (a : α) (b : β) :
b pfun.res f s a a s f a = b
theorem pfun.res_univ {α : Type u_1} {β : Type u_2} (f : α → β) :
theorem pfun.dom_iff_graph {α : Type u_1} {β : Type u_2} (f : α →. β) (x : α) :
x f.dom ∃ (y : β), (x, y) f.graph
theorem pfun.lift_graph {α : Type u_1} {β : Type u_2} {f : α → β} {a : α} {b : β} :
(a, b) f.graph f a = b
def pfun.pure {α : Type u_1} {β : Type u_2} (x : β) :
α →. β

The monad pure function, the total constant x function

Equations
def pfun.bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α →. β) (g : β → α →. γ) :
α →. γ

The monad bind function, pointwise roption.bind

Equations
  • f.bind g = λ (a : α), (f a).bind (λ (b : β), g b a)
def pfun.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β → γ) (g : α →. β) :
α →. γ

The monad map function, pointwise roption.map

Equations
@[instance]
def pfun.monad {α : Type u_1} :
monad (pfun α)
Equations
@[instance]
def pfun.is_lawful_monad {α : Type u_1} :
theorem pfun.pure_defined {α : Type u_1} {β : Type u_2} (p : set α) (x : β) :
theorem pfun.bind_defined {α : Type u_1} {β γ : Type u_2} (p : set α) {f : α →. β} {g : β → α →. γ} (H1 : p f.dom) (H2 : ∀ (x : β), p (g x).dom) :
p (f >>= g).dom
def pfun.fix {α : Type u_1} {β : Type u_2} (f : α →. β α) :
α →. β
Equations
theorem pfun.dom_of_mem_fix {α : Type u_1} {β : Type u_2} {f : α →. β α} {a : α} {b : β} (h : b f.fix a) :
(f a).dom
theorem pfun.mem_fix_iff {α : Type u_1} {β : Type u_2} {f : α →. β α} {a : α} {b : β} :
b f.fix a sum.inl b f a ∃ (a' : α), sum.inr a' f a b f.fix a'
def pfun.fix_induction {α : Type u_1} {β : Type u_2} {f : α →. β α} {b : β} {C : α → Sort u_3} {a : α} (h : b f.fix a) (H : Π (a : α), b f.fix a(Π (a' : α), b f.fix a'sum.inr a' f aC a')C a) :
C a
Equations
def pfun.image {α : Type u_1} {β : Type u_2} (f : α →. β) (s : set α) :
set β
Equations
theorem pfun.image_def {α : Type u_1} {β : Type u_2} (f : α →. β) (s : set α) :
f.image s = {y : β | ∃ (x : α) (H : x s), y f x}
theorem pfun.mem_image {α : Type u_1} {β : Type u_2} (f : α →. β) (y : β) (s : set α) :
y f.image s ∃ (x : α) (H : x s), y f x
theorem pfun.image_mono {α : Type u_1} {β : Type u_2} (f : α →. β) {s t : set α} (h : s t) :
f.image s f.image t
theorem pfun.image_inter {α : Type u_1} {β : Type u_2} (f : α →. β) (s t : set α) :
f.image (s t) f.image s f.image t
theorem pfun.image_union {α : Type u_1} {β : Type u_2} (f : α →. β) (s t : set α) :
f.image (s t) = f.image s f.image t
def pfun.preimage {α : Type u_1} {β : Type u_2} (f : α →. β) (s : set β) :
set α
Equations
theorem pfun.preimage_def {α : Type u_1} {β : Type u_2} (f : α →. β) (s : set β) :
f.preimage s = {x : α | ∃ (y : β) (H : y s), y f x}
theorem pfun.mem_preimage {α : Type u_1} {β : Type u_2} (f : α →. β) (s : set β) (x : α) :
x f.preimage s ∃ (y : β) (H : y s), y f x
theorem pfun.preimage_subset_dom {α : Type u_1} {β : Type u_2} (f : α →. β) (s : set β) :
theorem pfun.preimage_mono {α : Type u_1} {β : Type u_2} (f : α →. β) {s t : set β} (h : s t) :
theorem pfun.preimage_inter {α : Type u_1} {β : Type u_2} (f : α →. β) (s t : set β) :
theorem pfun.preimage_union {α : Type u_1} {β : Type u_2} (f : α →. β) (s t : set β) :
f.preimage (s t) = f.preimage s f.preimage t
theorem pfun.preimage_univ {α : Type u_1} {β : Type u_2} (f : α →. β) :
def pfun.core {α : Type u_1} {β : Type u_2} (f : α →. β) (s : set β) :
set α
Equations
theorem pfun.core_def {α : Type u_1} {β : Type u_2} (f : α →. β) (s : set β) :
f.core s = {x : α | ∀ (y : β), y f xy s}
theorem pfun.mem_core {α : Type u_1} {β : Type u_2} (f : α →. β) (x : α) (s : set β) :
x f.core s ∀ (y : β), y f xy s
theorem pfun.compl_dom_subset_core {α : Type u_1} {β : Type u_2} (f : α →. β) (s : set β) :
theorem pfun.core_mono {α : Type u_1} {β : Type u_2} (f : α →. β) {s t : set β} (h : s t) :
f.core s f.core t
theorem pfun.core_inter {α : Type u_1} {β : Type u_2} (f : α →. β) (s t : set β) :
f.core (s t) = f.core s f.core t
theorem pfun.mem_core_res {α : Type u_1} {β : Type u_2} (f : α → β) (s : set α) (t : set β) (x : α) :
x (pfun.res f s).core t x sf x t
theorem pfun.core_res {α : Type u_1} {β : Type u_2} (f : α → β) (s : set α) (t : set β) :
(pfun.res f s).core t = s f ⁻¹' t
theorem pfun.core_restrict {α : Type u_1} {β : Type u_2} (f : α → β) (s : set β) :
f.core s = f ⁻¹' s
theorem pfun.preimage_subset_core {α : Type u_1} {β : Type u_2} (f : α →. β) (s : set β) :
f.preimage s f.core s
theorem pfun.preimage_eq {α : Type u_1} {β : Type u_2} (f : α →. β) (s : set β) :
f.preimage s = f.core s f.dom
theorem pfun.core_eq {α : Type u_1} {β : Type u_2} (f : α →. β) (s : set β) :
theorem pfun.preimage_as_subtype {α : Type u_1} {β : Type u_2} (f : α →. β) (s : set β) :