# Documentation

Mathlib.Data.Seq.Computation

# Coinductive formalization of unbounded computations. #

This file provides a Computation type where Computation α is the type of unbounded computations returning α.

def Computation (α : Type u) :

Computation α is the type of unbounded computations returning α. An element of Computation α is an infinite sequence of Option α such that if f n = some a for some n then it is constantly some a after that.

Equations
• = { f // ∀ ⦃n : ⦄ ⦃a : α⦄, f n = some af (n + 1) = some a }
def Computation.pure {α : Type u} (a : α) :

pure a is the computation that immediately terminates with result a.

Equations
Equations
• Computation.instCoeTCComputation = { coe := Computation.pure }
def Computation.think {α : Type u} (c : ) :

think c is the computation that delays for one "tick" and then performs computation c.

Equations
def Computation.thinkN {α : Type u} (c : ) :

thinkN c n is the computation that delays for n ticks and then performs computation c.

Equations
def Computation.head {α : Type u} (c : ) :

head c is the first step of computation, either some a if c = pure a or none if c = think c'.

Equations
def Computation.tail {α : Type u} (c : ) :

tail c is the remainder of computation, either c if c = pure a or c' if c = think c'.

Equations
def Computation.empty (α : Type u_1) :

empty α is the computation that never returns, an infinite sequence of thinks.

Equations
Equations
• Computation.instInhabitedComputation = { default := }
def Computation.runFor {α : Type u} :

run_for c n evaluates c for n steps and returns the result, or none if it did not terminate after n steps.

Equations
• Computation.runFor = Subtype.val
def Computation.destruct {α : Type u} (c : ) :
α

destruct c is the destructor for Computation α as a coinductive type. It returns inl a if c = pure a and inr c' if c = think c'.

Equations
• = match c 0 with | none => | some a =>
unsafe def Computation.run {α : Type u} :
α

run c is an unsound meta function that runs c to completion, possibly resulting in an infinite loop in the VM.

Equations
• = let c := x; match with | => a | Sum.inr ca =>
theorem Computation.destruct_eq_pure {α : Type u} {s : } {a : α} :
theorem Computation.destruct_eq_think {α : Type u} {s : } {s' : } :
@[simp]
theorem Computation.destruct_pure {α : Type u} (a : α) :
@[simp]
theorem Computation.destruct_think {α : Type u} (s : ) :
@[simp]
theorem Computation.destruct_empty {α : Type u} :
@[simp]
theorem Computation.head_pure {α : Type u} (a : α) :
@[simp]
theorem Computation.head_think {α : Type u} (s : ) :
= none
@[simp]
theorem Computation.head_empty {α : Type u} :
= none
@[simp]
theorem Computation.tail_pure {α : Type u} (a : α) :
@[simp]
theorem Computation.tail_think {α : Type u} (s : ) :
@[simp]
theorem Computation.tail_empty {α : Type u} :
def Computation.recOn {α : Type u} {C : Sort v} (s : ) (h1 : (a : α) → C ()) (h2 : (s : ) → C ()) :
C s

Recursion principle for computations, compare with List.recOn.

Equations
• One or more equations did not get rendered due to their size.
def Computation.Corec.f {α : Type u} {β : Type v} (f : βα β) :
α β × (α β)

Corecursor constructor for corec

Equations
• = match x with | => (some a, ) | => (match f b with | => some a | Sum.inr val => none, f b)
def Computation.corec {α : Type u} {β : Type v} (f : βα β) (b : β) :

corec f b is the corecursor for Computation α as a coinductive type. If f b = inl a then corec f b = pure a, and if f b = inl b' then corec f b = think (corec f b').

Equations
• One or more equations did not get rendered due to their size.
def Computation.lmap {α : Type u} {β : Type v} {γ : Type w} (f : αβ) :
α γβ γ

left map of ⊕⊕

Equations
• = match x with | => Sum.inl (f a) | =>
def Computation.rmap {α : Type u} {β : Type v} {γ : Type w} (f : βγ) :
α βα γ

right map of ⊕⊕

Equations
@[simp]
theorem Computation.corec_eq {α : Type u} {β : Type v} (f : βα β) (b : β) :
def Computation.BisimO {α : Type u} (R : ) :
α α Prop

Bisimilarity over a sum of Computations

Equations
• = match x, x with | , Sum.inl a' => a = a' | , Sum.inr s' => R s s' | x, x_1 => False
def Computation.IsBisimulation {α : Type u} (R : ) :

Attribute expressing bisimilarity over two Computations

Equations
• = ∀ ⦃s₁ s₂ : ⦄, R s₁ s₂
theorem Computation.eq_of_bisim {α : Type u} (R : ) (bisim : ) {s₁ : } {s₂ : } (r : R s₁ s₂) :
s₁ = s₂
def Computation.Mem {α : Type u} (a : α) (s : ) :

Assertion that a Computation limits to a given value

Equations
Equations
• Computation.instMembershipComputation = { mem := Computation.Mem }
theorem Computation.le_stable {α : Type u} (s : ) {a : α} {m : } {n : } (h : m n) :
s m = some as n = some a
theorem Computation.mem_unique {α : Type u} {s : } {a : α} {b : α} :
a sb sa = b
class Computation.Terminates {α : Type u} (s : ) :
• assertion that there is some term a such that the Computation terminates

term : a, a s

Terminates s asserts that the computation s eventually terminates with some value.

Instances
theorem Computation.terminates_iff {α : Type u} (s : ) :
a, a s
theorem Computation.terminates_of_mem {α : Type u} {s : } {a : α} (h : a s) :
theorem Computation.terminates_def {α : Type u} (s : ) :
n, Option.isSome (s n) = true
theorem Computation.ret_mem {α : Type u} (a : α) :
theorem Computation.eq_of_pure_mem {α : Type u} {a : α} {a' : α} (h : ) :
a' = a
instance Computation.ret_terminates {α : Type u} (a : α) :
Equations
theorem Computation.think_mem {α : Type u} {s : } {a : α} :
a s
instance Computation.think_terminates {α : Type u} (s : ) [inst : ] :
Equations
theorem Computation.of_think_mem {α : Type u} {s : } {a : α} :
a s
theorem Computation.not_mem_empty {α : Type u} (a : α) :
theorem Computation.eq_empty_of_not_terminates {α : Type u} {s : } (H : ) :
theorem Computation.thinkN_mem {α : Type u} {s : } {a : α} (n : ) :
a a s
instance Computation.thinkN_terminates {α : Type u} (s : ) [inst : ] (n : ) :
Equations
theorem Computation.of_thinkN_terminates {α : Type u} (s : ) (n : ) :
def Computation.Promises {α : Type u} (s : ) (a : α) :

Promises s a, or s ~> a, asserts that although the computation s may not terminate, if it does, then the result is a.

Equations
• = ∀ ⦃a' : α⦄, a' sa = a'

Promises s a, or s ~> a, asserts that although the computation s may not terminate, if it does, then the result is a.

Equations
• One or more equations did not get rendered due to their size.
theorem Computation.mem_promises {α : Type u} {s : } {a : α} :
a s
theorem Computation.empty_promises {α : Type u} (a : α) :
def Computation.length {α : Type u} (s : ) [h : ] :

length s gets the number of steps of a terminating computation

Equations
def Computation.get {α : Type u} (s : ) [h : ] :
α

get s returns the result of a terminating computation

Equations
theorem Computation.get_mem {α : Type u} (s : ) [h : ] :
theorem Computation.get_eq_of_mem {α : Type u} (s : ) [h : ] {a : α} :
a s
theorem Computation.mem_of_get_eq {α : Type u} (s : ) [h : ] {a : α} :
a s
@[simp]
theorem Computation.get_think {α : Type u} (s : ) [h : ] :
@[simp]
theorem Computation.get_thinkN {α : Type u} (s : ) [h : ] (n : ) :
theorem Computation.get_promises {α : Type u} (s : ) [h : ] :
theorem Computation.mem_of_promises {α : Type u} (s : ) [h : ] {a : α} (p : ) :
a s
theorem Computation.get_eq_of_promises {α : Type u} (s : ) [h : ] {a : α} :
def Computation.Results {α : Type u} (s : ) (a : α) (n : ) :

Results s a n completely characterizes a terminating computation: it asserts that s terminates after exactly n steps, with result a.

Equations
• = h,
theorem Computation.results_of_terminates {α : Type u} (s : ) [_T : ] :
theorem Computation.results_of_terminates' {α : Type u} (s : ) [T : ] {a : α} (h : a s) :
theorem Computation.Results.mem {α : Type u} {s : } {a : α} {n : } :
a s
theorem Computation.Results.terminates {α : Type u} {s : } {a : α} {n : } (h : ) :
theorem Computation.Results.length {α : Type u} {s : } {a : α} {n : } [_T : ] :
theorem Computation.Results.val_unique {α : Type u} {s : } {a : α} {b : α} {m : } {n : } (h1 : ) (h2 : ) :
a = b
theorem Computation.Results.len_unique {α : Type u} {s : } {a : α} {b : α} {m : } {n : } (h1 : ) (h2 : ) :
m = n
theorem Computation.exists_results_of_mem {α : Type u} {s : } {a : α} (h : a s) :
n,
@[simp]
theorem Computation.get_pure {α : Type u} (a : α) :
@[simp]
theorem Computation.length_pure {α : Type u} (a : α) :
theorem Computation.results_pure {α : Type u} (a : α) :
@[simp]
theorem Computation.length_think {α : Type u} (s : ) [h : ] :
theorem Computation.results_think {α : Type u} {s : } {a : α} {n : } (h : ) :
theorem Computation.of_results_think {α : Type u} {s : } {a : α} {n : } (h : ) :
m, n = m + 1
@[simp]
theorem Computation.results_think_iff {α : Type u} {s : } {a : α} {n : } :
theorem Computation.results_thinkN {α : Type u} {s : } {a : α} {m : } (n : ) :
Computation.Results () a (m + n)
theorem Computation.results_thinkN_pure {α : Type u} (a : α) (n : ) :
@[simp]
theorem Computation.length_thinkN {α : Type u} (s : ) [_h : ] (n : ) :
theorem Computation.eq_thinkN {α : Type u} {s : } {a : α} {n : } (h : ) :
theorem Computation.eq_thinkN' {α : Type u} (s : ) [_h : ] :
def Computation.memRecOn {α : Type u} {C : Sort v} {a : α} {s : } (M : a s) (h1 : C ()) (h2 : (s : ) → C sC ()) :
C s

Recursor based on memberhip

Equations
• One or more equations did not get rendered due to their size.
def Computation.terminatesRecOn {α : Type u} {C : Sort v} (s : ) [inst : ] (h1 : (a : α) → C ()) (h2 : (s : ) → C sC ()) :
C s

Recursor based on assertion of Terminates

Equations
def Computation.map {α : Type u} {β : Type v} (f : αβ) :

Map a function on the result of a computation.

Equations
• One or more equations did not get rendered due to their size.
def Computation.Bind.g {α : Type u} {β : Type v} :
β β

bind over a Sum of Computation

Equations
def Computation.Bind.f {α : Type u} {β : Type v} (f : α) :
β

bind over a function mapping α to a Computation

Equations
• One or more equations did not get rendered due to their size.
def Computation.bind {α : Type u} {β : Type v} (c : ) (f : α) :

Compose two computations into a monadic bind operation.

Equations
Equations
theorem Computation.has_bind_eq_bind {α : Type u} {β : Type u} (c : ) (f : α) :
c >>= f =
def Computation.join {α : Type u} (c : ) :

Flatten a computation of computations into a single computation.

Equations
@[simp]
theorem Computation.map_pure {α : Type u} {β : Type v} (f : αβ) (a : α) :
@[simp]
theorem Computation.map_think {α : Type u} {β : Type v} (f : αβ) (s : ) :
@[simp]
theorem Computation.destruct_map {α : Type u} {β : Type v} (f : αβ) (s : ) :
@[simp]
theorem Computation.map_id {α : Type u} (s : ) :
= s
theorem Computation.map_comp {α : Type u} {β : Type v} {γ : Type w} (f : αβ) (g : βγ) (s : ) :
@[simp]
theorem Computation.ret_bind {α : Type u} {β : Type v} (a : α) (f : α) :
= f a
@[simp]
theorem Computation.think_bind {α : Type u} {β : Type v} (c : ) (f : α) :
@[simp]
theorem Computation.bind_pure {α : Type u} {β : Type v} (f : αβ) (s : ) :
Computation.bind s (Computation.pure f) =
@[simp]
theorem Computation.bind_pure' {α : Type u} (s : ) :
Computation.bind s Computation.pure = s
@[simp]
theorem Computation.bind_assoc {α : Type u} {β : Type v} {γ : Type w} (s : ) (f : α) (g : β) :
= Computation.bind s fun x => Computation.bind (f x) g
theorem Computation.results_bind {α : Type u} {β : Type v} {s : } {f : α} {a : α} {b : β} {m : } {n : } (h1 : ) (h2 : Computation.Results (f a) b n) :
theorem Computation.mem_bind {α : Type u} {β : Type v} {s : } {f : α} {a : α} {b : β} (h1 : a s) (h2 : b f a) :
b
instance Computation.terminates_bind {α : Type u} {β : Type v} (s : ) (f : α) [inst : ] [inst : ] :
Equations
@[simp]
theorem Computation.get_bind {α : Type u} {β : Type v} (s : ) (f : α) [inst : ] [inst : ] :
@[simp]
theorem Computation.length_bind {α : Type u} {β : Type v} (s : ) (f : α) [_T1 : ] [_T2 : ] :
theorem Computation.of_results_bind {α : Type u} {β : Type v} {s : } {f : α} {b : β} {k : } :
a m n, Computation.Results (f a) b n k = n + m
theorem Computation.exists_of_mem_bind {α : Type u} {β : Type v} {s : } {f : α} {b : β} (h : b ) :
a, a s b f a
theorem Computation.bind_promises {α : Type u} {β : Type v} {s : } {f : α} {a : α} {b : β} (h1 : ) (h2 : Computation.Promises (f a) b) :
Equations
theorem Computation.has_map_eq_map {α : Type u} {β : Type u} (f : αβ) (c : ) :
f <\$> c =
@[simp]
theorem Computation.pure_def {α : Type u} (a : α) :
@[simp]
theorem Computation.map_pure' {α : Type u_1} {β : Type u_1} (f : αβ) (a : α) :
@[simp]
theorem Computation.map_think' {α : Type u_1} {β : Type u_1} (f : αβ) (s : ) :
theorem Computation.mem_map {α : Type u} {β : Type v} (f : αβ) {a : α} {s : } (m : a s) :
f a
theorem Computation.exists_of_mem_map {α : Type u} {β : Type v} {f : αβ} {b : β} {s : } (h : b ) :
a, a s f a = b
instance Computation.terminates_map {α : Type u} {β : Type v} (f : αβ) (s : ) [inst : ] :
Equations
theorem Computation.terminates_map_iff {α : Type u} {β : Type v} (f : αβ) (s : ) :
def Computation.orElse {α : Type u} (c₁ : ) (c₂ : ) :

c₁ <|> c₂ calculates c₁ and c₂ simultaneously, returning the first one that gives a result.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Computation.ret_orElse {α : Type u} (a : α) (c₂ : ) :
(HOrElse.hOrElse () fun x => c₂) =
@[simp]
theorem Computation.orelse_pure {α : Type u} (c₁ : ) (a : α) :
(HOrElse.hOrElse () fun x => ) =
@[simp]
theorem Computation.orelse_think {α : Type u} (c₁ : ) (c₂ : ) :
(HOrElse.hOrElse () fun x => ) = Computation.think (HOrElse.hOrElse c₁ fun x => c₂)
@[simp]
theorem Computation.empty_orelse {α : Type u} (c : ) :
(HOrElse.hOrElse () fun x => c) = c
@[simp]
theorem Computation.orelse_empty {α : Type u} (c : ) :
(HOrElse.hOrElse c fun x => ) = c
def Computation.Equiv {α : Type u} (c₁ : ) (c₂ : ) :

c₁ ~ c₂ asserts that c₁ and c₂ either both terminate with the same result, or both loop forever.

Equations

equivalence relation for computations

Equations
theorem Computation.Equiv.refl {α : Type u} (s : ) :
theorem Computation.Equiv.symm {α : Type u} {s : } {t : } :
theorem Computation.Equiv.trans {α : Type u} {s : } {t : } {u : } :
theorem Computation.Equiv.equivalence {α : Type u} :
Equivalence Computation.Equiv
theorem Computation.equiv_of_mem {α : Type u} {s : } {t : } {a : α} (h1 : a s) (h2 : a t) :
theorem Computation.terminates_congr {α : Type u} {c₁ : } {c₂ : } (h : ) :
theorem Computation.promises_congr {α : Type u} {c₁ : } {c₂ : } (h : ) (a : α) :
theorem Computation.get_equiv {α : Type u} {c₁ : } {c₂ : } (h : ) [inst : ] [inst : ] :
theorem Computation.think_equiv {α : Type u} (s : ) :
theorem Computation.thinkN_equiv {α : Type u} (s : ) (n : ) :
theorem Computation.bind_congr {α : Type u} {β : Type v} {s1 : } {s2 : } {f1 : α} {f2 : α} (h1 : ) (h2 : ∀ (a : α), Computation.Equiv (f1 a) (f2 a)) :
theorem Computation.equiv_pure_of_mem {α : Type u} {s : } {a : α} (h : a s) :
def Computation.LiftRel {α : Type u} {β : Type v} (R : αβProp) (ca : ) (cb : ) :

LiftRel R ca cb is a generalization of Equiv to relations other than equality. It asserts that if ca terminates with a, then cb terminates with some b such that R a b, and if cb terminates with b then ca terminates with some a such that R a b.

Equations
theorem Computation.LiftRel.swap {α : Type u} {β : Type v} (R : αβProp) (ca : ) (cb : ) :
theorem Computation.lift_eq_iff_equiv {α : Type u} (c₁ : ) (c₂ : ) :
Computation.LiftRel (fun x x_1 => x = x_1) c₁ c₂
theorem Computation.LiftRel.refl {α : Type u} (R : ααProp) (H : ) :
theorem Computation.LiftRel.symm {α : Type u} (R : ααProp) (H : ) :
theorem Computation.LiftRel.trans {α : Type u} (R : ααProp) (H : ) :
theorem Computation.LiftRel.equiv {α : Type u} (R : ααProp) :
theorem Computation.LiftRel.imp {α : Type u} {β : Type v} {R : αβProp} {S : αβProp} (H : {a : α} → {b : β} → R a bS a b) (s : ) (t : ) :
theorem Computation.terminates_of_LiftRel {α : Type u} {β : Type v} {R : αβProp} {s : } {t : } :
→ ()
theorem Computation.rel_of_LiftRel {α : Type u} {β : Type v} {R : αβProp} {ca : } {cb : } :
Computation.LiftRel R ca cb{a : α} → {b : β} → a cab cbR a b
theorem Computation.liftRel_of_mem {α : Type u} {β : Type v} {R : αβProp} {a : α} {b : β} {ca : } {cb : } (ma : a ca) (mb : b cb) (ab : R a b) :
theorem Computation.exists_of_LiftRel_left {α : Type u} {β : Type v} {R : αβProp} {ca : } {cb : } (H : Computation.LiftRel R ca cb) {a : α} (h : a ca) :
b, b cb R a b
theorem Computation.exists_of_LiftRel_right {α : Type u} {β : Type v} {R : αβProp} {ca : } {cb : } (H : Computation.LiftRel R ca cb) {b : β} (h : b cb) :
a, a ca R a b
theorem Computation.liftRel_def {α : Type u} {β : Type v} {R : αβProp} {ca : } {cb : } :
Computation.LiftRel R ca cb () ({a : α} → {b : β} → a cab cbR a b)
theorem Computation.liftRel_bind {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} (R : αβProp) (S : γδProp) {s1 : } {s2 : } {f1 : α} {f2 : β} (h1 : Computation.LiftRel R s1 s2) (h2 : ∀ {a : α} {b : β}, R a bComputation.LiftRel S (f1 a) (f2 b)) :
@[simp]
theorem Computation.liftRel_pure_left {α : Type u} {β : Type v} (R : αβProp) (a : α) (cb : ) :
b, b cb R a b
@[simp]
theorem Computation.liftRel_pure_right {α : Type u} {β : Type v} (R : αβProp) (ca : ) (b : β) :
a, a ca R a b
@[simp]
theorem Computation.liftRel_pure {α : Type u} {β : Type v} (R : αβProp) (a : α) (b : β) :
R a b
@[simp]
theorem Computation.liftRel_think_left {α : Type u} {β : Type v} (R : αβProp) (ca : ) (cb : ) :
@[simp]
theorem Computation.liftRel_think_right {α : Type u} {β : Type v} (R : αβProp) (ca : ) (cb : ) :
theorem Computation.liftRel_mem_cases {α : Type u} {β : Type v} {R : αβProp} {ca : } {cb : } (Ha : ∀ (a : α), a caComputation.LiftRel R ca cb) (Hb : ∀ (b : β), b cbComputation.LiftRel R ca cb) :
theorem Computation.liftRel_congr {α : Type u} {β : Type v} {R : αβProp} {ca : } {ca' : } {cb : } {cb' : } (ha : Computation.Equiv ca ca') (hb : Computation.Equiv cb cb') :
theorem Computation.liftRel_map {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} (R : αβProp) (S : γδProp) {s1 : } {s2 : } {f1 : αγ} {f2 : βδ} (h1 : Computation.LiftRel R s1 s2) (h2 : {a : α} → {b : β} → R a bS (f1 a) (f2 b)) :
theorem Computation.map_congr {α : Type u} {β : Type v} {s1 : } {s2 : } {f : αβ} (h1 : ) :
def Computation.LiftRelAux {α : Type u} {β : Type v} (R : αβProp) (C : ) :
α β Prop

Alternate defintion of LiftRel over relations between Computations

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Computation.LiftRelAux_inl_inl :
∀ {α : Type u_1} {α_1 : Type u_2} {R : αα_1Prop} {C : Computation α_1Prop} {a : α} {b : α_1}, Computation.LiftRelAux R C () () = R a b
@[simp]
theorem Computation.LiftRelAux_inl_inr :
∀ {α : Type u_1} {α_1 : Type u_2} {R : αα_1Prop} {C : Computation α_1Prop} {a : α} {cb : Computation α_1}, Computation.LiftRelAux R C () (Sum.inr cb) = b, b cb R a b
@[simp]
theorem Computation.LiftRelAux_inr_inl :
∀ {α : Type u_1} {α_1 : Type u_2} {R : αα_1Prop} {C : Computation α_1Prop} {ca : } {b : α_1}, Computation.LiftRelAux R C (Sum.inr ca) () = a, a ca R a b
@[simp]
theorem Computation.LiftRelAux_inr_inr :
∀ {α : Type u_1} {α_1 : Type u_2} {R : αα_1Prop} {C : Computation α_1Prop} {ca : } {cb : Computation α_1}, Computation.LiftRelAux R C (Sum.inr ca) (Sum.inr cb) = C ca cb
@[simp]
theorem Computation.LiftRelAux.ret_left {α : Type u} {β : Type v} (R : αβProp) (C : ) (a : α) (cb : ) :
b, b cb R a b
theorem Computation.LiftRelAux.swap {α : Type u} {β : Type v} (R : αβProp) (C : ) (a : α ) (b : β ) :
=
@[simp]
theorem Computation.LiftRelAux.ret_right {α : Type u} {β : Type v} (R : αβProp) (C : ) (b : β) (ca : ) :
a, a ca R a b
theorem Computation.LiftRelRec.lem {α : Type u} {β : Type v} {R : αβProp} (C : ) (H : ∀ {ca : } {cb : }, C ca cb) (ca : ) (cb : ) (Hc : C ca cb) (a : α) (ha : a ca) :
theorem Computation.lift_rel_rec {α : Type u} {β : Type v} {R : αβProp} (C : ) (H : ∀ {ca : } {cb : }, C ca cb) (ca : ) (cb : ) (Hc : C ca cb) :