Partial functions #
This file defines partial functions. Partial functions are like functions, except they can also be
"undefined" on some inputs. We define them as functions α → Part β
.
Definitions #
PFun α β
: Type of partial functions fromα
toβ
. Defined asα → Part β
and denotedα →. β
.PFun.Dom
: Domain of a partial function. Set of values on which it is defined. Not to be confused with the domain of a functionα → β
, which is a type (α
presently).PFun.fn
: Evaluation of a partial function. Takes in an element and a proof it belongs to the partial function'sDom
.PFun.asSubtype
: Returns a partial function as a function from itsDom
.PFun.toSubtype
: Restricts the codomain of a function to a subtype.PFun.evalOpt
: Returns a partial function with a decidableDom
as a functiona → Option β
.PFun.lift
: Turns a function into a partial function.PFun.id
: The identity as a partial function.PFun.comp
: Composition of partial functions.PFun.restrict
: Restriction of a partial function to a smallerDom
.PFun.res
: Turns a function into a partial function with a prescribed domain.PFun.fix
: First return map of a partial functionf : α →. β ⊕ α
.PFun.fix_induction
: A recursion principle forPFun.fix
.
Partial functions as relations #
Partial functions can be considered as relations, so we specialize some Rel
definitions to PFun
:
PFun.image
: Image of a set under a partial function.PFun.ran
: Range of a partial function.PFun.preimage
: Preimage of a set under a partial function.PFun.core
: Core of a set under a partial function.PFun.graph
: Graph of a partial functiona →. β
as aSet (α × β)
.PFun.graph'
: Graph of a partial functiona →. β
as aRel α β
.
PFun α
as a monad #
Monad operations:
α →. β
is notation for the type PFun α β
of partial functions from α
to β
.
Equations
- «term_→._» = Lean.ParserDescr.trailingNode `term_→._ 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →. ") (Lean.ParserDescr.cat `term 25))
Instances For
Evaluate a partial function to return an Option
Equations
- f.evalOpt x = (f x).toOption
Instances For
First return map. Transforms a partial function f : α →. β ⊕ α
into the partial function
α →. β
which sends a : α
to the first value in β
it hits by iterating f
, if such a value
exists. By abusing notation to illustrate, either f a
is in the β
part of β ⊕ α
(in which
case f.fix a
returns f a
), or it is undefined (in which case f.fix a
is undefined as well), or
it is in the α
part of β ⊕ α
(in which case we repeat the procedure, so f.fix a
will return
f.fix (f a)
).
Equations
- One or more equations did not get rendered due to their size.
Instances For
A recursion principle for PFun.fix
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Another induction lemma for b ∈ f.fix a
which allows one to prove a predicate P
holds for
a
given that f a
inherits P
from a
and P
holds for preimages of b
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Turns a function into a partial function to a subtype.
Equations
- PFun.toSubtype p f a = { Dom := p (f a), get := Subtype.mk (f a) }