mathlib documentation

data.seq.computation

def computation  :
Type uType 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
def computation.return {α : Type u} :
α → computation α

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

Equations
@[instance]
def computation.has_coe_t {α : Type u} :

Equations
def computation.think {α : Type u} :

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

Equations
def computation.thinkN {α : Type u} :

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

Equations
def computation.head {α : Type u} :

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} :

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 thinks.

Equations
@[instance]
def computation.inhabited {α : Type u} :

Equations
def computation.run_for {α : Type u} :
computation αoption α

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} :

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} :
computation α → α

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 α} :
s.destruct = sum.inr s's = s'.think

@[simp]
theorem computation.destruct_ret {α : Type u} (a : α) :

@[simp]
theorem computation.destruct_think {α : Type u} (s : computation α) :

@[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]

def computation.cases_on {α : Type u} {C : computation αSort v} (s : computation α) :
(Π (a : α), C (computation.return a))(Π (s : computation α), C s.think)C s

Equations
def computation.corec.F {α : Type u} {β : Type v} :
(β → α β)α βoption α × β)

Equations
def computation.corec {α : Type u} {β : Type v} :
(β → α β)β → computation α

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} :
(α → β)α γβ γ

left map of

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

right map of

Equations
@[simp]
theorem computation.corec_eq {α : Type u} {β : Type v} (f : β → α β) (b : β) :

@[simp]
def computation.bisim_o {α : Type u} :
(computation αcomputation α → Prop)α computation αα computation α → Prop

Equations
def computation.is_bisimulation {α : Type u} :
(computation αcomputation α → Prop) → Prop

Equations
theorem computation.eq_of_bisim {α : Type u} (R : computation αcomputation α → Prop) (bisim : computation.is_bisimulation R) {s₁ s₂ : computation α} :
R s₁ s₂s₁ = s₂

def computation.mem {α : Type u} :
α → computation α → Prop

Equations
@[instance]
def computation.has_mem {α : Type u} :

Equations
theorem computation.le_stable {α : Type u} (s : computation α) {a : α} {m n : } :
m ns.val m = some as.val n = some a

@[class]
def computation.terminates {α : Type u} :
computation α → Prop

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

Equations
Instances
theorem computation.terminates_of_mem {α : Type u} {s : computation α} {a : α} :
a s → s.terminates

theorem computation.terminates_def {α : Type u} (s : computation α) :
s.terminates ∃ (n : ), ((s.val n).is_some)

theorem computation.ret_mem {α : Type u} (a : α) :

theorem computation.eq_of_ret_mem {α : Type u} {a a' : α} :
a' computation.return aa' = a

@[instance]
def computation.ret_terminates {α : Type u} (a : α) :

theorem computation.think_mem {α : Type u} {s : computation α} {a : α} :
a sa s.think

@[instance]

theorem computation.of_think_mem {α : Type u} {s : computation α} {a : α} :
a s.thinka s

theorem computation.of_think_terminates {α : Type u} {s : computation α} :

theorem computation.not_mem_empty {α : Type u} (a : α) :

theorem computation.thinkN_mem {α : Type u} {s : computation α} {a : α} (n : ) :
a s.thinkN n a s

@[instance]
def computation.thinkN_terminates {α : Type u} (s : computation α) [s.terminates] (n : ) :

theorem computation.of_thinkN_terminates {α : Type u} (s : computation α) (n : ) :

def computation.promises {α : Type u} :
computation αα → 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
  • s ~> a = ∀ ⦃a' : α⦄, a' sa = a'
theorem computation.mem_promises {α : Type u} {s : computation α} {a : α} :
a ss ~> 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 ss.get = a

theorem computation.mem_of_get_eq {α : Type u} (s : computation α) [h : s.terminates] {a : α} :
s.get = aa 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 : α} :
s ~> aa s

theorem computation.get_eq_of_promises {α : Type u} (s : computation α) [h : s.terminates] {a : α} :
s ~> as.get = a

def computation.results {α : Type u} :
computation αα → → 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] :

theorem computation.results_of_terminates' {α : Type u} (s : computation α) [T : s.terminates] {a : α} :
a ss.results a s.length

theorem computation.results.mem {α : Type u} {s : computation α} {a : α} {n : } :
s.results a na s

theorem computation.results.terminates {α : Type u} {s : computation α} {a : α} {n : } :
s.results a n → s.terminates

theorem computation.results.length {α : Type u} {s : computation α} {a : α} {n : } [T : s.terminates] :
s.results a ns.length = n

theorem computation.results.val_unique {α : Type u} {s : computation α} {a b : α} {m n : } :
s.results a ms.results b na = b

theorem computation.results.len_unique {α : Type u} {s : computation α} {a b : α} {m n : } :
s.results a ms.results b nm = n

theorem computation.exists_results_of_mem {α : Type u} {s : computation α} {a : α} :
a s(∃ (n : ), s.results a n)

@[simp]
theorem computation.get_ret {α : Type u} (a : α) :

@[simp]
theorem computation.length_ret {α : Type u} (a : α) :

theorem computation.results_ret {α : Type u} (a : α) :

@[simp]
theorem computation.length_think {α : Type u} (s : computation α) [h : s.terminates] :

theorem computation.results_think {α : Type u} {s : computation α} {a : α} {n : } :
s.results a ns.think.results a (n + 1)

theorem computation.of_results_think {α : Type u} {s : computation α} {a : α} {n : } :
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 : ) :

@[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 : } :

theorem computation.eq_thinkN' {α : Type u} (s : computation α) [h : s.terminates] :

def computation.mem_rec_on {α : Type u} {C : computation αSort v} {a : α} {s : computation α} :
a sC (computation.return a)(Π (s : computation α), C sC s.think)C s

Equations
def computation.terminates_rec_on {α : Type u} {C : computation αSort v} (s : computation α) [s.terminates] :
(Π (a : α), C (computation.return a))(Π (s : computation α), C sC s.think)C s

Equations
def computation.map {α : Type u} {β : Type v} :
(α → β)computation αcomputation β

Map a function on the result of a computation.

Equations
def computation.bind.G {α : Type u} {β : Type v} :

Equations
def computation.bind.F {α : Type u} {β : Type v} :

Equations
def computation.bind {α : Type u} {β : Type v} :
computation α(α → computation β)computation β

Compose two computations into a monadic bind operation.

Equations
theorem computation.has_bind_eq_bind {α β : Type u} (c : computation α) (f : α → computation β) :
c >>= f = c.bind f

def computation.join {α : Type u} :

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 α) :

@[simp]
theorem computation.destruct_map {α : Type u} {β : Type v} (f : α → β) (s : computation α) :

@[simp]
theorem computation.map_id {α : Type u} (s : computation α) :

theorem computation.map_comp {α : Type u} {β : Type v} {γ : Type w} (f : α → β) (g : β → γ) (s : computation α) :

@[simp]
theorem computation.ret_bind {α : Type u} {β : Type v} (a : α) (f : α → computation β) :

@[simp]
theorem computation.think_bind {α : Type u} {β : Type v} (c : computation α) (f : α → computation β) :
c.think.bind f = (c.bind f).think

@[simp]
theorem computation.bind_ret {α : Type u} {β : Type v} (f : α → β) (s : computation α) :

@[simp]
theorem computation.bind_ret' {α : Type u} (s : computation α) :

@[simp]
theorem computation.bind_assoc {α : Type u} {β : Type v} {γ : Type w} (s : computation α) (f : α → computation β) (g : β → computation γ) :
(s.bind f).bind g = s.bind (λ (x : α), (f x).bind g)

theorem computation.results_bind {α : Type u} {β : Type v} {s : computation α} {f : α → computation β} {a : α} {b : β} {m n : } :
s.results a m(f a).results b n(s.bind f).results b (n + m)

theorem computation.mem_bind {α : Type u} {β : Type v} {s : computation α} {f : α → computation β} {a : α} {b : β} :
a sb f ab s.bind f

@[instance]
def computation.terminates_bind {α : Type u} {β : Type v} (s : computation α) (f : α → computation β) [s.terminates] [(f s.get).terminates] :

@[simp]
theorem computation.get_bind {α : Type u} {β : Type v} (s : computation α) (f : α → computation β) [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 : α → computation β) [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 : α → computation β} {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 : α → computation β} {b : β} :
b s.bind f(∃ (a : α) (H : a s), b f a)

theorem computation.bind_promises {α : Type u} {β : Type v} {s : computation α} {f : α → computation β} {a : α} {b : β} :
s ~> af a ~> bs.bind f ~> b

theorem computation.has_map_eq_map {α β : Type u} (f : α → β) (c : computation α) :

@[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 α} :
a sf a computation.map f s

theorem computation.exists_of_mem_map {α : Type u} {β : Type v} {f : α → β} {b : β} {s : computation α} :
b computation.map f s(∃ (a : α), a s f a = b)

@[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₂ calculates c₁ and c₂ simultaneously, returning the first one that gives a result.

Equations
@[simp]
theorem computation.ret_orelse {α : Type u} (a : α) (c₂ : computation α) :

@[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 α) :

@[simp]
theorem computation.orelse_empty {α : Type u} (c : computation α) :

def computation.equiv {α : Type u} :
computation αcomputation α → Prop

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

Equations
  • c₁ ~ c₂ = ∀ (a : α), a c₁ a c₂
theorem computation.equiv.refl {α : Type u} (s : computation α) :
s ~ s

theorem computation.equiv.symm {α : Type u} {s t : computation α} :
s ~ tt ~ s

theorem computation.equiv.trans {α : Type u} {s t u : computation α} :
s ~ tt ~ us ~ u

theorem computation.equiv_of_mem {α : Type u} {s t : computation α} {a : α} :
a sa ts ~ t

theorem computation.terminates_congr {α : Type u} {c₁ c₂ : computation α} :
c₁ ~ c₂(c₁.terminates c₂.terminates)

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 : α → computation β} :
s1 ~ s2(∀ (a : α), f1 a ~ f2 a)s1.bind f1 ~ s2.bind f2

theorem computation.equiv_ret_of_mem {α : Type u} {s : computation α} {a : α} :

def computation.lift_rel {α : Type u} {β : Type v} :
(α → β → Prop)computation α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 β) :

theorem computation.lift_eq_iff_equiv {α : Type u} (c₁ c₂ : computation α) :
computation.lift_rel eq c₁ c₂ c₁ ~ c₂

theorem computation.lift_rel.refl {α : Type u} (R : α → α → Prop) :

theorem computation.lift_rel.symm {α : Type u} (R : α → α → Prop) :

theorem computation.lift_rel.trans {α : Type u} (R : α → α → Prop) :

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 bS a b) (s : computation α) (t : computation β) :

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 β} (a : computation.lift_rel R ca cb) {a_1 : α} {b : β} :
a_1 cab cbR a_1 b

theorem computation.lift_rel_of_mem {α : Type u} {β : Type v} {R : α → β → Prop} {a : α} {b : β} {ca : computation α} {cb : computation β} :
a cab cbR a bcomputation.lift_rel R ca cb

theorem computation.exists_of_lift_rel_left {α : Type u} {β : Type v} {R : α → β → Prop} {ca : computation α} {cb : computation β} (H : computation.lift_rel R ca cb) {a : α} :
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 : computation.lift_rel R ca cb) {b : β} :
b cb(∃ {a : α}, a ca R a b)

theorem computation.lift_rel_def {α : Type u} {β : Type v} {R : α → β → Prop} {ca : computation α} {cb : computation β} :
computation.lift_rel R ca cb (ca.terminates cb.terminates) ∀ {a : α} {b : β}, a cab cbR 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 : α → computation γ} {f2 : β → computation δ} :
computation.lift_rel R s1 s2(∀ {a : α} {b : β}, R a bcomputation.lift_rel S (f1 a) (f2 b))computation.lift_rel S (s1.bind f1) (s2.bind f2)

@[simp]
theorem computation.lift_rel_return_left {α : Type u} {β : Type v} (R : α → β → Prop) (a : α) (cb : computation β) :
computation.lift_rel R (computation.return a) cb ∃ {b : β}, b cb R a b

@[simp]
theorem computation.lift_rel_return_right {α : Type u} {β : Type v} (R : α → β → Prop) (ca : computation α) (b : β) :
computation.lift_rel R ca (computation.return b) ∃ {a : α}, a ca R a b

@[simp]
theorem computation.lift_rel_return {α : Type u} {β : Type v} (R : α → β → Prop) (a : α) (b : β) :

@[simp]
theorem computation.lift_rel_think_left {α : Type u} {β : Type v} (R : α → β → Prop) (ca : computation α) (cb : computation β) :

@[simp]
theorem computation.lift_rel_think_right {α : Type u} {β : Type v} (R : α → β → Prop) (ca : computation α) (cb : computation β) :

theorem computation.lift_rel_mem_cases {α : Type u} {β : Type v} {R : α → β → Prop} {ca : computation α} {cb : computation β} :
(∀ (a : α), a cacomputation.lift_rel R ca cb)(∀ (b : β), b cbcomputation.lift_rel R ca cb)computation.lift_rel R ca cb

theorem computation.lift_rel_congr {α : Type u} {β : Type v} {R : α → β → Prop} {ca ca' : computation α} {cb cb' : computation β} :
ca ~ ca'cb ~ cb'(computation.lift_rel R ca cb computation.lift_rel R 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 : β → δ} :
computation.lift_rel R s1 s2(∀ {a : α} {b : β}, R a bS (f1 a) (f2 b))computation.lift_rel S (computation.map f1 s1) (computation.map f2 s2)

theorem computation.map_congr {α : Type u} {β : Type v} (R : α → α → Prop) (S : β → β → Prop) {s1 s2 : computation α} {f : α → β} :
s1 ~ s2computation.map f s1 ~ computation.map f s2

@[simp]
def computation.lift_rel_aux {α : Type u} {β : Type v} :
(α → β → Prop)(computation αcomputation β → Prop)α computation αβ computation β → Prop

Equations
@[simp]
theorem computation.lift_rel_aux.ret_left {α : Type u} {β : Type v} (R : α → β → Prop) (C : computation αcomputation β → Prop) (a : α) (cb : computation β) :
computation.lift_rel_aux R C (sum.inl a) cb.destruct ∃ {b : β}, b cb R a b

theorem computation.lift_rel_aux.swap {α : Type u} {β : Type v} (R : α → β → Prop) (C : computation αcomputation β → Prop) (a : α computation α) (b : β computation β) :

@[simp]
theorem computation.lift_rel_aux.ret_right {α : Type u} {β : Type v} (R : α → β → Prop) (C : computation αcomputation β → Prop) (b : β) (ca : computation α) :
computation.lift_rel_aux R C ca.destruct (sum.inl b) ∃ {a : α}, a ca R a b

theorem computation.lift_rel_rec.lem {α : Type u} {β : Type v} {R : α → β → Prop} (C : computation αcomputation β → Prop) (H : ∀ {ca : computation α} {cb : computation β}, C ca cbcomputation.lift_rel_aux R C ca.destruct cb.destruct) (ca : computation α) (cb : computation β) (Hc : C ca cb) (a : α) :
a cacomputation.lift_rel R ca cb

theorem computation.lift_rel_rec {α : Type u} {β : Type v} {R : α → β → Prop} (C : computation αcomputation β → Prop) (H : ∀ {ca : computation α} {cb : computation β}, C ca cbcomputation.lift_rel_aux R C ca.destruct cb.destruct) (ca : computation α) (cb : computation β) :
C ca cbcomputation.lift_rel R ca cb