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

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

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

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

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

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

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

Equations

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

Equations
Equations
def Computation.runFor {α : 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
  • Computation.runFor = Subtype.val
def Computation.destruct {α : Type u} (c : Computation α) :

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

Equations
def Computation.recOn {α : Type u} {C : Computation αSort v} (s : Computation α) (h1 : (a : α) → C (Computation.pure a)) (h2 : (s : Computation α) → C (Computation.think s)) :
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 : βα β) :
α βOption α × (α β)

Corecursor constructor for corec

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 = 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
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 : Computation αComputation αProp) :
α Computation αα Computation αProp

Bisimilarity over a sum of Computations

Equations

Attribute expressing bisimilarity over two Computations

Equations
theorem Computation.eq_of_bisim {α : Type u} (R : Computation αComputation αProp) (bisim : Computation.IsBisimulation R) {s₁ : Computation α} {s₂ : Computation α} (r : R s₁ s₂) :
s₁ = s₂
def Computation.Mem {α : Type u} (a : α) (s : Computation α) :

Assertion that a Computation limits to a given value

Equations
Equations
  • Computation.instMembershipComputation = { mem := Computation.Mem }
theorem Computation.le_stable {α : Type u} (s : Computation α) {a : α} {m : } {n : } (h : m n) :
s m = some as n = some a
theorem Computation.mem_unique {α : Type u} {s : Computation α} {a : α} {b : α} :
a sb sa = b
class Computation.Terminates {α : Type u} (s : Computation α) :
  • 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_of_mem {α : Type u} {s : Computation α} {a : α} (h : a s) :
    theorem Computation.ret_mem {α : Type u} (a : α) :
    theorem Computation.eq_of_pure_mem {α : Type u} {a : α} {a' : α} (h : a' Computation.pure a) :
    a' = a
    theorem Computation.think_mem {α : Type u} {s : Computation α} {a : α} :
    theorem Computation.of_think_mem {α : Type u} {s : Computation α} {a : α} :
    theorem Computation.thinkN_mem {α : Type u} {s : Computation α} {a : α} (n : ) :
    def Computation.Promises {α : Type u} (s : Computation α) (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

    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 : Computation α} {a : α} :

    length s gets the number of steps of a terminating computation

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

    get s returns the result of a terminating computation

    Equations
    theorem Computation.get_eq_of_mem {α : Type u} (s : Computation α) [h : Computation.Terminates s] {a : α} :
    a sComputation.get s = a
    theorem Computation.mem_of_get_eq {α : Type u} (s : Computation α) [h : Computation.Terminates s] {a : α} :
    Computation.get s = aa s
    def Computation.Results {α : Type u} (s : Computation α) (a : α) (n : ) :

    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.mem {α : Type u} {s : Computation α} {a : α} {n : } :
    Computation.Results s a na s
    theorem Computation.Results.val_unique {α : Type u} {s : Computation α} {a : α} {b : α} {m : } {n : } (h1 : Computation.Results s a m) (h2 : Computation.Results s b n) :
    a = b
    theorem Computation.Results.len_unique {α : Type u} {s : Computation α} {a : α} {b : α} {m : } {n : } (h1 : Computation.Results s a m) (h2 : Computation.Results s b n) :
    m = n
    theorem Computation.exists_results_of_mem {α : Type u} {s : Computation α} {a : α} (h : a s) :
    n, Computation.Results s a n
    @[simp]
    theorem Computation.results_think {α : Type u} {s : Computation α} {a : α} {n : } (h : Computation.Results s a n) :
    theorem Computation.of_results_think {α : Type u} {s : Computation α} {a : α} {n : } (h : Computation.Results (Computation.think s) a n) :
    m, Computation.Results s a m n = m + 1
    theorem Computation.results_thinkN {α : Type u} {s : Computation α} {a : α} {m : } (n : ) :
    theorem Computation.eq_thinkN {α : Type u} {s : Computation α} {a : α} {n : } (h : Computation.Results s a n) :
    def Computation.memRecOn {α : Type u} {C : Computation αSort v} {a : α} {s : Computation α} (M : a s) (h1 : C (Computation.pure a)) (h2 : (s : Computation α) → C sC (Computation.think s)) :
    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 : Computation αSort v} (s : Computation α) [inst : Computation.Terminates s] (h1 : (a : α) → C (Computation.pure a)) (h2 : (s : Computation α) → C sC (Computation.think s)) :
    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 : αComputation β) :

    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 : Computation α) (f : αComputation β) :

    Compose two computations into a monadic bind operation.

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

    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 : 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.bind_pure {α : Type u} {β : Type v} (f : αβ) (s : Computation α) :
    Computation.bind s (Computation.pure f) = Computation.map f s
    @[simp]
    theorem Computation.bind_pure' {α : Type u} (s : Computation α) :
    Computation.bind s Computation.pure = s
    @[simp]
    theorem Computation.bind_assoc {α : Type u} {β : Type v} {γ : Type w} (s : Computation α) (f : αComputation β) (g : βComputation γ) :
    theorem Computation.results_bind {α : Type u} {β : Type v} {s : Computation α} {f : αComputation β} {a : α} {b : β} {m : } {n : } (h1 : Computation.Results s a m) (h2 : Computation.Results (f a) b n) :
    theorem Computation.mem_bind {α : Type u} {β : Type v} {s : Computation α} {f : αComputation β} {a : α} {b : β} (h1 : a s) (h2 : b f a) :
    theorem Computation.of_results_bind {α : Type u} {β : Type v} {s : Computation α} {f : αComputation β} {b : β} {k : } :
    Computation.Results (Computation.bind s f) b ka m n, Computation.Results s a m Computation.Results (f a) b n k = n + m
    theorem Computation.exists_of_mem_bind {α : Type u} {β : Type v} {s : Computation α} {f : αComputation β} {b : β} (h : b Computation.bind s f) :
    a, a s b f a
    theorem Computation.bind_promises {α : Type u} {β : Type v} {s : Computation α} {f : αComputation β} {a : α} {b : β} (h1 : Computation.Promises s a) (h2 : Computation.Promises (f a) b) :
    theorem Computation.has_map_eq_map {α : Type u} {β : Type u} (f : αβ) (c : Computation α) :
    @[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 : Computation α) :
    theorem Computation.mem_map {α : Type u} {β : Type v} (f : αβ) {a : α} {s : Computation α} (m : a s) :
    theorem Computation.exists_of_mem_map {α : Type u} {β : Type v} {f : αβ} {b : β} {s : Computation α} (h : b Computation.map f s) :
    a, a s f a = b
    def Computation.orElse {α : Type u} (c₁ : Computation α) (c₂ : UnitComputation α) :

    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₂ : Computation α) :
    @[simp]
    @[simp]
    theorem Computation.orelse_think {α : Type u} (c₁ : Computation α) (c₂ : Computation α) :
    @[simp]
    theorem Computation.empty_orelse {α : Type u} (c : Computation α) :
    (HOrElse.hOrElse (Computation.empty α) fun x => c) = c
    @[simp]
    theorem Computation.orelse_empty {α : Type u} (c : Computation α) :
    def Computation.Equiv {α : Type u} (c₁ : Computation α) (c₂ : Computation α) :

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

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

    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 : Computation α) (cb : Computation β) :
    theorem Computation.lift_eq_iff_equiv {α : Type u} (c₁ : Computation α) (c₂ : Computation α) :
    Computation.LiftRel (fun x x_1 => x = x_1) c₁ c₂ Computation.Equiv c₁ c₂
    theorem Computation.LiftRel.refl {α : Type u} (R : ααProp) (H : Reflexive R) :
    theorem Computation.LiftRel.symm {α : Type u} (R : ααProp) (H : Symmetric R) :
    theorem Computation.LiftRel.trans {α : Type u} (R : ααProp) (H : Transitive R) :
    theorem Computation.LiftRel.imp {α : Type u} {β : Type v} {R : αβProp} {S : αβProp} (H : {a : α} → {b : β} → R a bS a b) (s : Computation α) (t : Computation β) :
    theorem Computation.rel_of_LiftRel {α : Type u} {β : Type v} {R : αβProp} {ca : Computation α} {cb : Computation β} :
    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 : Computation α} {cb : Computation β} (ma : a ca) (mb : b cb) (ab : R a b) :
    theorem Computation.exists_of_LiftRel_left {α : Type u} {β : Type v} {R : αβProp} {ca : Computation α} {cb : Computation β} (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 : Computation α} {cb : Computation β} (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 : Computation α} {cb : Computation β} :
    Computation.LiftRel R ca cb (Computation.Terminates ca Computation.Terminates 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 : Computation α} {s2 : Computation β} {f1 : αComputation γ} {f2 : βComputation δ} (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 : Computation β) :
    Computation.LiftRel R (Computation.pure a) cb b, b cb R a b
    @[simp]
    theorem Computation.liftRel_pure_right {α : Type u} {β : Type v} (R : αβProp) (ca : Computation α) (b : β) :
    Computation.LiftRel R ca (Computation.pure b) a, a ca R a b
    @[simp]
    theorem Computation.liftRel_pure {α : Type u} {β : Type v} (R : αβProp) (a : α) (b : β) :
    @[simp]
    theorem Computation.liftRel_think_left {α : Type u} {β : Type v} (R : αβProp) (ca : Computation α) (cb : Computation β) :
    @[simp]
    theorem Computation.liftRel_think_right {α : Type u} {β : Type v} (R : αβProp) (ca : Computation α) (cb : Computation β) :
    theorem Computation.liftRel_mem_cases {α : Type u} {β : Type v} {R : αβProp} {ca : Computation α} {cb : Computation β} (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 : Computation α} {ca' : Computation α} {cb : Computation β} {cb' : Computation β} (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 : Computation α} {s2 : Computation β} {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 : Computation α} {s2 : Computation α} {f : αβ} (h1 : Computation.Equiv s1 s2) :
    def Computation.LiftRelAux {α : Type u} {β : Type v} (R : αβProp) (C : Computation αComputation βProp) :
    α Computation αβ Computation β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 αComputation α_1Prop} {a : α} {b : α_1}, Computation.LiftRelAux R C (Sum.inl a) (Sum.inl b) = R a b
    @[simp]
    theorem Computation.LiftRelAux_inl_inr :
    ∀ {α : Type u_1} {α_1 : Type u_2} {R : αα_1Prop} {C : Computation αComputation α_1Prop} {a : α} {cb : Computation α_1}, Computation.LiftRelAux R C (Sum.inl a) (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 αComputation α_1Prop} {ca : Computation α} {b : α_1}, Computation.LiftRelAux R C (Sum.inr ca) (Sum.inl b) = a, a ca R a b
    @[simp]
    theorem Computation.LiftRelAux_inr_inr :
    ∀ {α : Type u_1} {α_1 : Type u_2} {R : αα_1Prop} {C : Computation αComputation α_1Prop} {ca : Computation α} {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 : Computation αComputation βProp) (a : α) (cb : Computation β) :
    theorem Computation.LiftRelAux.swap {α : Type u} {β : Type v} (R : αβProp) (C : Computation αComputation βProp) (a : α Computation α) (b : β Computation β) :
    @[simp]
    theorem Computation.LiftRelAux.ret_right {α : Type u} {β : Type v} (R : αβProp) (C : Computation αComputation βProp) (b : β) (ca : Computation α) :
    theorem Computation.LiftRelRec.lem {α : Type u} {β : Type v} {R : αβProp} (C : Computation αComputation βProp) (H : ∀ {ca : Computation α} {cb : Computation β}, C ca cbComputation.LiftRelAux R C (Computation.destruct ca) (Computation.destruct cb)) (ca : Computation α) (cb : Computation β) (Hc : C ca cb) (a : α) (ha : a ca) :
    theorem Computation.lift_rel_rec {α : Type u} {β : Type v} {R : αβProp} (C : Computation αComputation βProp) (H : ∀ {ca : Computation α} {cb : Computation β}, C ca cbComputation.LiftRelAux R C (Computation.destruct ca) (Computation.destruct cb)) (ca : Computation α) (cb : Computation β) (Hc : C ca cb) :