# mathlib3documentation

data.seq.computation

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
Instances for `computation`
def computation.return {α : Type u} (a : α) :

`return a` is the computation that immediately terminates with result `a`.

Equations
Instances for `computation.return`
@[protected, instance]
def computation.has_coe_t {α : Type u} :
Equations
def computation.think {α : Type u} (c : computation α) :

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

Equations
Instances for `computation.think`
def computation.thinkN {α : Type u} (c : computation α) :

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

Equations
Instances for `computation.thinkN`
def computation.head {α : Type u} (c : computation α) :

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

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

`tail c` is the remainder of computation, either `c` if `c = return 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 `think`s.

Equations
@[protected, instance]
def computation.inhabited {α : Type u} :
Equations
def computation.run_for {α : 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
def computation.destruct {α : Type u} (c : computation α) :
α

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

Equations
meta 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.

theorem computation.destruct_eq_ret {α : Type u} {s : computation α} {a : α} :
theorem computation.destruct_eq_think {α : Type u} {s s' : computation α} :
@[simp]
theorem computation.destruct_ret {α : Type u} (a : α) :
@[simp]
theorem computation.destruct_think {α : Type u} (s : computation α) :
@[simp]
theorem computation.destruct_empty {α : Type u} :
@[simp]
theorem computation.head_ret {α : Type u} (a : α) :
@[simp]
theorem computation.head_think {α : Type u} (s : computation α) :
@[simp]
theorem computation.head_empty {α : Type u} :
@[simp]
theorem computation.tail_ret {α : Type u} (a : α) :
@[simp]
theorem computation.tail_think {α : Type u} (s : computation α) :
@[simp]
theorem computation.tail_empty {α : Type u} :
theorem computation.think_empty {α : Type u} :
def computation.rec_on {α : Type u} {C : Sort v} (s : computation α) (h1 : Π (a : α), C ) (h2 : Π (s : , C s.think) :
C s

Recursion principle for computations, compare with `list.rec_on`.

Equations
def computation.corec.F {α : Type u} {β : Type v} (f : β α β) :
α β × β)
Equations
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 = return a`, and if `f b = inl b'` then `corec f b = think (corec f b')`.

Equations
@[simp]
def computation.lmap {α : Type u} {β : Type v} {γ : Type w} (f : α β) :
α γ β γ

left map of `⊕`

Equations
@[simp]
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 : β) :
b).destruct = (f b)
@[simp]
def computation.bisim_o {α : Type u} (R : Prop) :
α α Prop
Equations
def computation.is_bisimulation {α : Type u} (R : Prop) :
Prop
Equations
theorem computation.eq_of_bisim {α : Type u} (R : Prop) (bisim : computation.is_bisimulation R) {s₁ s₂ : computation α} (r : R s₁ s₂) :
s₁ = s₂
@[protected]
def computation.mem {α : Type u} (a : α) (s : computation α) :
Prop
Equations
@[protected, instance]
def computation.has_mem {α : Type u} :
Equations
theorem computation.le_stable {α : Type u} (s : computation α) {a : α} {m n : } (h : m n) :
s.val m = s.val n =
theorem computation.mem_unique {α : Type u} {s : computation α} {a b : α} :
a s b s a = b
@[class]
structure computation.terminates {α : Type u} (s : computation α) :
Prop

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

Instances of this typeclass
theorem computation.terminates_iff {α : Type u} (s : computation α) :
s.terminates (a : α), a s
theorem computation.terminates_of_mem {α : Type u} {s : computation α} {a : α} (h : a s) :
theorem computation.terminates_def {α : Type u} (s : computation α) :
theorem computation.ret_mem {α : Type u} (a : α) :
theorem computation.eq_of_ret_mem {α : Type u} {a a' : α} (h : a' ) :
a' = a
@[protected, instance]
def computation.ret_terminates {α : Type u} (a : α) :
theorem computation.think_mem {α : Type u} {s : computation α} {a : α} :
a s a s.think
@[protected, instance]
theorem computation.of_think_mem {α : Type u} {s : computation α} {a : α} :
a s.think a s
theorem computation.not_mem_empty {α : Type u} (a : α) :
theorem computation.thinkN_mem {α : Type u} {s : computation α} {a : α} (n : ) :
a s.thinkN n a s
@[protected, instance]
def computation.thinkN_terminates {α : Type u} (s : computation α) [s.terminates] (n : ) :
def computation.promises {α : Type u} (s : computation α) (a : α) :
Prop

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

Equations
theorem computation.mem_promises {α : Type u} {s : computation α} {a : α} :
a s s ~> a
theorem computation.empty_promises {α : Type u} (a : α) :
def computation.length {α : Type u} (s : computation α) [h : s.terminates] :

`length s` gets the number of steps of a terminating computation

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

`get s` returns the result of a terminating computation

Equations
theorem computation.get_mem {α : Type u} (s : computation α) [h : s.terminates] :
s.get s
theorem computation.get_eq_of_mem {α : Type u} (s : computation α) [h : s.terminates] {a : α} :
a s s.get = a
theorem computation.mem_of_get_eq {α : Type u} (s : computation α) [h : s.terminates] {a : α} :
s.get = a a s
@[simp]
theorem computation.get_think {α : Type u} (s : computation α) [h : s.terminates] :
@[simp]
theorem computation.get_thinkN {α : Type u} (s : computation α) [h : s.terminates] (n : ) :
(s.thinkN n).get = s.get
theorem computation.get_promises {α : Type u} (s : computation α) [h : s.terminates] :
s ~> s.get
theorem computation.mem_of_promises {α : Type u} (s : computation α) [h : s.terminates] {a : α} (p : s ~> a) :
a s
theorem computation.get_eq_of_promises {α : Type u} (s : computation α) [h : s.terminates] {a : α} :
s ~> a s.get = a
def computation.results {α : Type u} (s : computation α) (a : α) (n : ) :
Prop

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

Equations
theorem computation.results_of_terminates' {α : Type u} (s : computation α) [T : s.terminates] {a : α} (h : a s) :
theorem computation.results.mem {α : Type u} {s : computation α} {a : α} {n : } :
s.results a n a s
theorem computation.results.terminates {α : Type u} {s : computation α} {a : α} {n : } (h : s.results a n) :
theorem computation.results.length {α : Type u} {s : computation α} {a : α} {n : } [T : s.terminates] :
s.results a n s.length = n
theorem computation.results.val_unique {α : Type u} {s : computation α} {a b : α} {m n : } (h1 : s.results a m) (h2 : s.results b n) :
a = b
theorem computation.results.len_unique {α : Type u} {s : computation α} {a b : α} {m n : } (h1 : s.results a m) (h2 : s.results b n) :
m = n
theorem computation.exists_results_of_mem {α : Type u} {s : computation α} {a : α} (h : a s) :
(n : ), s.results a n
@[simp]
theorem computation.get_ret {α : Type u} (a : α) :
= a
@[simp]
theorem computation.length_ret {α : Type u} (a : α) :
theorem computation.results_ret {α : Type u} (a : α) :
0
@[simp]
theorem computation.length_think {α : Type u} (s : computation α) [h : s.terminates] :
theorem computation.results_think {α : Type u} {s : computation α} {a : α} {n : } (h : s.results a n) :
s.think.results a (n + 1)
theorem computation.of_results_think {α : Type u} {s : computation α} {a : α} {n : } (h : s.think.results a n) :
(m : ), s.results a m n = m + 1
@[simp]
theorem computation.results_think_iff {α : Type u} {s : computation α} {a : α} {n : } :
s.think.results a (n + 1) s.results a n
theorem computation.results_thinkN {α : Type u} {s : computation α} {a : α} {m : } (n : ) :
s.results a m (s.thinkN n).results a (m + n)
theorem computation.results_thinkN_ret {α : Type u} (a : α) (n : ) :
.thinkN n).results a n
@[simp]
theorem computation.length_thinkN {α : Type u} (s : computation α) [h : s.terminates] (n : ) :
(s.thinkN n).length = s.length + n
theorem computation.eq_thinkN {α : Type u} {s : computation α} {a : α} {n : } (h : s.results a n) :
s = n
theorem computation.eq_thinkN' {α : Type u} (s : computation α) [h : s.terminates] :
s =
def computation.mem_rec_on {α : Type u} {C : Sort v} {a : α} {s : computation α} (M : a s) (h1 : C ) (h2 : Π (s : , C s C s.think) :
C s
Equations
def computation.terminates_rec_on {α : Type u} {C : Sort v} (s : computation α) [s.terminates] (h1 : Π (a : α), C ) (h2 : Π (s : , C s C s.think) :
C s
Equations
• h2 = (h1 s.get) h2
def computation.map {α : Type u} {β : Type v} (f : α β) :

Map a function on the result of a computation.

Equations
Instances for `computation.map`
def computation.bind.G {α : Type u} {β : Type v} :
β β
Equations
def computation.bind.F {α : Type u} {β : Type v} (f : α ) :
β
Equations
def computation.bind {α : Type u} {β : Type v} (c : computation α) (f : α ) :

Compose two computations into a monadic `bind` operation.

Equations
Instances for `computation.bind`
@[protected, instance]
Equations
theorem computation.has_bind_eq_bind {α β : Type u} (c : computation α) (f : α ) :
c >>= f = c.bind f
def computation.join {α : Type u} (c : computation (computation α)) :

Flatten a computation of computations into a single computation.

Equations
@[simp]
theorem computation.map_ret {α : Type u} {β : Type v} (f : α β) (a : α) :
@[simp]
theorem computation.map_think {α : Type u} {β : Type v} (f : α β) (s : computation α) :
= s).think
@[simp]
theorem computation.destruct_map {α : Type u} {β : Type v} (f : α β) (s : computation α) :
s).destruct =
@[simp]
theorem computation.map_id {α : Type u} (s : computation α) :
theorem computation.map_comp {α : Type u} {β : Type v} {γ : Type w} (f : α β) (g : β γ) (s : computation α) :
computation.map (g f) s = s)
@[simp]
theorem computation.ret_bind {α : Type u} {β : Type v} (a : α) (f : α ) :
f = f a
@[simp]
theorem computation.think_bind {α : Type u} {β : Type v} (c : computation α) (f : α ) :
c.think.bind f = (c.bind f).think
@[simp]
theorem computation.bind_ret {α : Type u} {β : Type v} (f : α β) (s : computation α) :
s.bind =
@[simp]
theorem computation.bind_ret' {α : Type u} (s : computation α) :
@[simp]
theorem computation.bind_assoc {α : Type u} {β : Type v} {γ : Type w} (s : computation α) (f : α ) (g : β ) :
(s.bind f).bind g = s.bind (λ (x : α), (f x).bind g)
theorem computation.results_bind {α : Type u} {β : Type v} {s : computation α} {f : α } {a : α} {b : β} {m n : } (h1 : s.results a m) (h2 : (f a).results b n) :
(s.bind f).results b (n + m)
theorem computation.mem_bind {α : Type u} {β : Type v} {s : computation α} {f : α } {a : α} {b : β} (h1 : a s) (h2 : b f a) :
b s.bind f
@[protected, instance]
def computation.terminates_bind {α : Type u} {β : Type v} (s : computation α) (f : α ) [s.terminates] [(f s.get).terminates] :
@[simp]
theorem computation.get_bind {α : Type u} {β : Type v} (s : computation α) (f : α ) [s.terminates] [(f s.get).terminates] :
(s.bind f).get = (f s.get).get
@[simp]
theorem computation.length_bind {α : Type u} {β : Type v} (s : computation α) (f : α ) [T1 : s.terminates] [T2 : (f s.get).terminates] :
(s.bind f).length = (f s.get).length + s.length
theorem computation.of_results_bind {α : Type u} {β : Type v} {s : computation α} {f : α } {b : β} {k : } :
(s.bind f).results b k ( (a : α) (m n : ), s.results a m (f a).results b n k = n + m)
theorem computation.exists_of_mem_bind {α : Type u} {β : Type v} {s : computation α} {f : α } {b : β} (h : b s.bind f) :
(a : α) (H : a s), b f a
theorem computation.bind_promises {α : Type u} {β : Type v} {s : computation α} {f : α } {a : α} {b : β} (h1 : s ~> a) (h2 : f a ~> b) :
s.bind f ~> b
@[protected, instance]
Equations
@[protected, instance]
theorem computation.has_map_eq_map {α β : Type u} (f : α β) (c : computation α) :
f <\$> c =
@[simp]
theorem computation.return_def {α : Type u} (a : α) :
@[simp]
theorem computation.map_ret' {α β : Type u_1} (f : α β) (a : α) :
@[simp]
theorem computation.map_think' {α β : Type u_1} (f : α β) (s : computation α) :
f <\$> s.think = (f <\$> s).think
theorem computation.mem_map {α : Type u} {β : Type v} (f : α β) {a : α} {s : computation α} (m : a s) :
f a
theorem computation.exists_of_mem_map {α : Type u} {β : Type v} {f : α β} {b : β} {s : computation α} (h : b ) :
(a : α), a s f a = b
@[protected, instance]
def computation.terminates_map {α : Type u} {β : Type v} (f : α β) (s : computation α) [s.terminates] :
theorem computation.terminates_map_iff {α : Type u} {β : Type v} (f : α β) (s : computation α) :
def computation.orelse {α : Type u} (c₁ c₂ : computation α) :

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

Equations
• c₁.orelse c₂ = computation.corec (λ (_x : , computation.orelse._match_3 _x) (c₁, c₂)
• computation.orelse._match_3 (c₁, c₂) = computation.orelse._match_1 c₂ c₁.destruct
• computation.orelse._match_1 c₂ (sum.inr c₁') = computation.orelse._match_2 c₁' c₂.destruct
• computation.orelse._match_1 c₂ (sum.inl a) =
• computation.orelse._match_2 c₁' (sum.inr c₂') = sum.inr (c₁', c₂')
• computation.orelse._match_2 c₁' (sum.inl a) =
@[protected, instance]
Equations
@[simp]
theorem computation.ret_orelse {α : Type u} (a : α) (c₂ : computation α) :
<|> c₂) =
@[simp]
theorem computation.orelse_ret {α : Type u} (c₁ : computation α) (a : α) :
@[simp]
theorem computation.orelse_think {α : Type u} (c₁ c₂ : computation α) :
(c₁.think <|> c₂.think) = (c₁ <|> c₂).think
@[simp]
theorem computation.empty_orelse {α : Type u} (c : computation α) :
<|> c) = c
@[simp]
theorem computation.orelse_empty {α : Type u} (c : computation α) :
(c <|> = c
def computation.equiv {α : Type u} (c₁ c₂ : computation α) :
Prop

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

Equations
@[refl]
theorem computation.equiv.refl {α : Type u} (s : computation α) :
s ~ s
@[symm]
theorem computation.equiv.symm {α : Type u} {s t : computation α} :
s ~ t t ~ s
@[trans]
theorem computation.equiv.trans {α : Type u} {s t u : computation α} :
s ~ t t ~ u s ~ u
theorem computation.equiv_of_mem {α : Type u} {s t : computation α} {a : α} (h1 : a s) (h2 : a t) :
s ~ t
theorem computation.terminates_congr {α : Type u} {c₁ c₂ : computation α} (h : c₁ ~ c₂) :
theorem computation.promises_congr {α : Type u} {c₁ c₂ : computation α} (h : c₁ ~ c₂) (a : α) :
c₁ ~> a c₂ ~> a
theorem computation.get_equiv {α : Type u} {c₁ c₂ : computation α} (h : c₁ ~ c₂) [c₁.terminates] [c₂.terminates] :
c₁.get = c₂.get
theorem computation.think_equiv {α : Type u} (s : computation α) :
s.think ~ s
theorem computation.thinkN_equiv {α : Type u} (s : computation α) (n : ) :
s.thinkN n ~ s
theorem computation.bind_congr {α : Type u} {β : Type v} {s1 s2 : computation α} {f1 f2 : α } (h1 : s1 ~ s2) (h2 : (a : α), f1 a ~ f2 a) :
s1.bind f1 ~ s2.bind f2
theorem computation.equiv_ret_of_mem {α : Type u} {s : computation α} {a : α} (h : a s) :
def computation.lift_rel {α : Type u} {β : Type v} (R : α β Prop) (ca : computation α) (cb : computation β) :
Prop

`lift_rel 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.lift_rel.swap {α : Type u} {β : Type v} (R : α β Prop) (ca : computation α) (cb : computation β) :
ca cb
theorem computation.lift_eq_iff_equiv {α : Type u} (c₁ c₂ : computation α) :
c₂ c₁ ~ c₂
theorem computation.lift_rel.refl {α : Type u} (R : α α Prop) (H : reflexive R) :
theorem computation.lift_rel.symm {α : Type u} (R : α α Prop) (H : symmetric R) :
theorem computation.lift_rel.trans {α : Type u} (R : α α Prop) (H : transitive R) :
theorem computation.lift_rel.equiv {α : Type u} (R : α α Prop) :
theorem computation.lift_rel.imp {α : Type u} {β : Type v} {R S : α β Prop} (H : {a : α} {b : β}, R a b S a b) (s : computation α) (t : computation β) :
t t
theorem computation.terminates_of_lift_rel {α : Type u} {β : Type v} {R : α β Prop} {s : computation α} {t : computation β} :
theorem computation.rel_of_lift_rel {α : Type u} {β : Type v} {R : α β Prop} {ca : computation α} {cb : computation β} :
cb {a : α} {b : β}, a ca b cb R a b
theorem computation.lift_rel_of_mem {α : Type u} {β : Type v} {R : α β Prop} {a : α} {b : β} {ca : computation α} {cb : computation β} (ma : a ca) (mb : b cb) (ab : R a b) :
cb
theorem computation.exists_of_lift_rel_left {α : Type u} {β : Type v} {R : α β Prop} {ca : computation α} {cb : computation β} (H : cb) {a : α} (h : a ca) :
{b : β}, b cb R a b
theorem computation.exists_of_lift_rel_right {α : Type u} {β : Type v} {R : α β Prop} {ca : computation α} {cb : computation β} (H : cb) {b : β} (h : b cb) :
{a : α}, a ca R a b
theorem computation.lift_rel_def {α : Type u} {β : Type v} {R : α β Prop} {ca : computation α} {cb : computation β} :
cb (ca.terminates cb.terminates) {a : α} {b : β}, a ca b cb R a b
theorem computation.lift_rel_bind {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} (R : α β Prop) (S : γ δ Prop) {s1 : computation α} {s2 : computation β} {f1 : α } {f2 : β } (h1 : s2) (h2 : {a : α} {b : β}, R a b (f1 a) (f2 b)) :
(s1.bind f1) (s2.bind f2)
@[simp]
theorem computation.lift_rel_return_left {α : Type u} {β : Type v} (R : α β Prop) (a : α) (cb : computation β) :
{b : β}, b cb R a b
@[simp]
theorem computation.lift_rel_return_right {α : Type u} {β : Type v} (R : α β Prop) (ca : computation α) (b : β) :
{a : α}, a ca R a b
@[simp]
theorem computation.lift_rel_return {α : Type u} {β : Type v} (R : α β Prop) (a : α) (b : β) :
R a b
@[simp]
theorem computation.lift_rel_think_left {α : Type u} {β : Type v} (R : α β Prop) (ca : computation α) (cb : computation β) :
cb cb
@[simp]
theorem computation.lift_rel_think_right {α : Type u} {β : Type v} (R : α β Prop) (ca : computation α) (cb : computation β) :
cb.think cb
theorem computation.lift_rel_mem_cases {α : Type u} {β : Type v} {R : α β Prop} {ca : computation α} {cb : computation β} (Ha : (a : α), a ca cb) (Hb : (b : β), b cb cb) :
cb
theorem computation.lift_rel_congr {α : Type u} {β : Type v} {R : α β Prop} {ca ca' : computation α} {cb cb' : computation β} (ha : ca ~ ca') (hb : cb ~ cb') :
cb ca' cb'
theorem computation.lift_rel_map {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} (R : α β Prop) (S : γ δ Prop) {s1 : computation α} {s2 : computation β} {f1 : α γ} {f2 : β δ} (h1 : s2) (h2 : {a : α} {b : β}, R a b S (f1 a) (f2 b)) :
s1) s2)
theorem computation.map_congr {α : Type u} {β : Type v} (R : α α Prop) (S : β β Prop) {s1 s2 : computation α} {f : α β} (h1 : s1 ~ s2) :
s1 ~ s2
@[simp]
def computation.lift_rel_aux {α : Type u} {β : Type v} (R : α β Prop) (C : Prop) :
α β Prop
Equations
@[simp]
theorem computation.lift_rel_aux.ret_left {α : Type u} {β : Type v} (R : α β Prop) (C : Prop) (a : α) (cb : computation β) :
(sum.inl a) cb.destruct {b : β}, b cb R a b
theorem computation.lift_rel_aux.swap {α : Type u} {β : Type v} (R : α β Prop) (C : Prop) (a : α ) (b : β ) :
a = b
@[simp]
theorem computation.lift_rel_aux.ret_right {α : Type u} {β : Type v} (R : α β Prop) (C : Prop) (b : β) (ca : computation α) :
(sum.inl b) {a : α}, a ca R a b
theorem computation.lift_rel_rec.lem {α : Type u} {β : Type v} {R : α β Prop} (C : Prop) (H : {ca : {cb : , C ca cb cb.destruct) (ca : computation α) (cb : computation β) (Hc : C ca cb) (a : α) (ha : a ca) :
cb
theorem computation.lift_rel_rec {α : Type u} {β : Type v} {R : α β Prop} (C : Prop) (H : {ca : {cb : , C ca cb cb.destruct) (ca : computation α) (cb : computation β) (Hc : C ca cb) :
cb