Coinductive formalization of unbounded computations.

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

def Computation (α : Type u) : 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

• Computation α = { f : Stream' (Option α) // ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a }

def Computation.pure {α : Type u} (a : α) : Computation α

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

Equations

• Computation.pure a = ⟨Stream'.const (some a), ⋯⟩

instance Computation.instCoeTC {α : Type u} : CoeTC α (Computation α)

Equations

• Computation.instCoeTC = { coe := Computation.pure }

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

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

Equations

• c.think = ⟨Stream'.cons none ↑c, ⋯⟩

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

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

Equations

• c.thinkN 0 = c
• c.thinkN n.succ = (c.thinkN n).think

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

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

Equations

• c.head = (↑c).head

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

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

Equations

• c.tail = ⟨(↑c).tail, ⋯⟩

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

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

Equations

• Computation.empty α = ⟨Stream'.const none, ⋯⟩

instance Computation.instInhabited {α : Type u} : Inhabited (Computation α)

Equations

• Computation.instInhabited = { default := Computation.empty α }

def Computation.runFor {α : Type u} : Computation α → ℕ → Option α

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

• c.destruct = match ↑c 0 with | none => Sum.inr c.tail | some a => Sum.inl a

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.

theorem Computation.destruct_eq_pure {α : Type u} {s : Computation α} {a : α} : s.destruct = Sum.inl a → s = Computation.pure a

theorem Computation.destruct_eq_think {α : Type u} {s s' : Computation α} : s.destruct = Sum.inr s' → s = s'.think

@[simp]

theorem Computation.destruct_pure {α : Type u} (a : α) : (Computation.pure a).destruct = Sum.inl a

@[simp]

theorem Computation.destruct_think {α : Type u} (s : Computation α) : s.think.destruct = Sum.inr s

@[simp]

theorem Computation.destruct_empty {α : Type u} : (Computation.empty α).destruct = Sum.inr (Computation.empty α)

@[simp]

theorem Computation.head_pure {α : Type u} (a : α) : (Computation.pure a).head = some a

@[simp]

theorem Computation.head_think {α : Type u} (s : Computation α) : s.think.head = none

@[simp]

theorem Computation.head_empty {α : Type u} : (Computation.empty α).head = none

@[simp]

theorem Computation.tail_pure {α : Type u} (a : α) : (Computation.pure a).tail = Computation.pure a

@[simp]

theorem Computation.tail_think {α : Type u} (s : Computation α) : s.think.tail = s

@[simp]

theorem Computation.tail_empty {α : Type u} : (Computation.empty α).tail = Computation.empty α

theorem Computation.think_empty {α : Type u} : Computation.empty α = (Computation.empty α).think

def Computation.recOn {α : Type u} {C : Computation α → Sort v} (s : Computation α) (h1 : (a : α) → C (Computation.pure a)) (h2 : (s : Computation α) → C s.think) : C s

Recursion principle for computations, compare with List.recOn.

Equations

• s.recOn h1 h2 = match H : s.destruct with | Sum.inl v => ⋯.mpr (h1 v) | Sum.inr v => match v, H with | ⟨a, s'⟩, H => ⋯.mpr (h2 ⟨a, s'⟩)

def Computation.Corec.f {α : Type u} {β : Type v} (f : β → α ⊕ β) : α ⊕ β → Option α × (α ⊕ β)

Corecursor constructor for corec

Equations

• Computation.Corec.f f (Sum.inl a) = (some a, Sum.inl a)
• Computation.Corec.f f (Sum.inr val) = (match f val with | Sum.inl a => some a | Sum.inr val => none, f val)

def Computation.corec {α : Type u} {β : Type v} (f : β → α ⊕ β) (b : β) : Computation α

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

• Computation.corec f b = ⟨Stream'.corec' (Computation.Corec.f f) (Sum.inr b), ⋯⟩

def Computation.lmap {α : Type u} {β : Type v} {γ : Type w} (f : α → β) : α ⊕ γ → β ⊕ γ

left map of ⊕

Equations

• Computation.lmap f (Sum.inl a) = Sum.inl (f a)
• Computation.lmap f (Sum.inr val) = Sum.inr val

def Computation.rmap {α : Type u} {β : Type v} {γ : Type w} (f : β → γ) : α ⊕ β → α ⊕ γ

right map of ⊕

Equations

• Computation.rmap f (Sum.inl a) = Sum.inl a
• Computation.rmap f (Sum.inr val) = Sum.inr (f val)

@[simp]

theorem Computation.corec_eq {α : Type u} {β : Type v} (f : β → α ⊕ β) (b : β) : (Computation.corec f b).destruct = Computation.rmap (Computation.corec f) (f b)

def Computation.BisimO {α : Type u} (R : Computation α → Computation α → Prop) : α ⊕ Computation α → α ⊕ Computation α → Prop

Bisimilarity over a sum of Computations

Equations

• Computation.BisimO R (Sum.inl a) (Sum.inl a') = (a = a')
• Computation.BisimO R (Sum.inr s) (Sum.inr s') = R s s'
• Computation.BisimO R x✝ x = False

def Computation.IsBisimulation {α : Type u} (R : Computation α → Computation α → Prop) : Prop

Attribute expressing bisimilarity over two Computations

Equations

• Computation.IsBisimulation R = ∀ ⦃s₁ s₂ : Computation α⦄, R s₁ s₂ → Computation.BisimO R s₁.destruct s₂.destruct

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

def Computation.Mem {α : Type u} (s : Computation α) (a : α) : Prop

Assertion that a Computation limits to a given value

Equations

• s.Mem a = (some a ∈ ↑s)

instance Computation.instMembership {α : Type u} : Membership α (Computation α)

Equations

• Computation.instMembership = { mem := Computation.Mem }

theorem Computation.le_stable {α : Type u} (s : Computation α) {a : α} {m n : ℕ} (h : m ≤ n) : ↑s m = some a → ↑s n = some a

theorem Computation.mem_unique {α : Type u} {s : Computation α} {a b : α} : a ∈ s → b ∈ s → a = b

theorem Computation.Mem.left_unique {α : Type u} : Relator.LeftUnique fun (x1 : α) (x2 : Computation α) => x1 ∈ x2

class Computation.Terminates {α : Type u} (s : Computation α) : Prop

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

• term : ∃ (a : α), a ∈ s

  assertion that there is some term a such that the Computation terminates

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) : s.Terminates

theorem Computation.terminates_def {α : Type u} (s : Computation α) : s.Terminates ↔ ∃ (n : ℕ), (↑s n).isSome = true

theorem Computation.ret_mem {α : Type u} (a : α) : a ∈ Computation.pure a

theorem Computation.eq_of_pure_mem {α : Type u} {a a' : α} (h : a' ∈ Computation.pure a) : a' = a

instance Computation.ret_terminates {α : Type u} (a : α) : (Computation.pure a).Terminates

Equations

• ⋯ = ⋯

theorem Computation.think_mem {α : Type u} {s : Computation α} {a : α} : a ∈ s → a ∈ s.think

instance Computation.think_terminates {α : Type u} (s : Computation α) [s.Terminates] : s.think.Terminates

Equations

• ⋯ = ⋯

theorem Computation.of_think_mem {α : Type u} {s : Computation α} {a : α} : a ∈ s.think → a ∈ s

theorem Computation.of_think_terminates {α : Type u} {s : Computation α} : s.think.Terminates → s.Terminates

theorem Computation.not_mem_empty {α : Type u} (a : α) : ¬a ∈ Computation.empty α

theorem Computation.not_terminates_empty {α : Type u} : ¬(Computation.empty α).Terminates

theorem Computation.eq_empty_of_not_terminates {α : Type u} {s : Computation α} (H : ¬s.Terminates) : s = Computation.empty α

theorem Computation.thinkN_mem {α : Type u} {s : Computation α} {a : α} (n : ℕ) : a ∈ s.thinkN n ↔ a ∈ s

instance Computation.thinkN_terminates {α : Type u} (s : Computation α) [s.Terminates] (n : ℕ) : (s.thinkN n).Terminates

Equations

• ⋯ = ⋯

theorem Computation.of_thinkN_terminates {α : Type u} (s : Computation α) (n : ℕ) : (s.thinkN n).Terminates → s.Terminates

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

• s.Promises a = ∀ ⦃a' : α⦄, a' ∈ s → a = a'

def Computation.«term_~>_» : Lean.TrailingParserDescr

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

Equations

• Computation.«term_~>_» = Lean.ParserDescr.trailingNode `Computation.«term_~>_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ~> ") (Lean.ParserDescr.cat `term 51))

theorem Computation.mem_promises {α : Type u} {s : Computation α} {a : α} : a ∈ s → s.Promises a

theorem Computation.empty_promises {α : Type u} (a : α) : (Computation.empty α).Promises a

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

length s gets the number of steps of a terminating computation

Equations

• s.length = Nat.find ⋯

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

get s returns the result of a terminating computation

Equations

• s.get = (↑s (Nat.find ⋯)).get ⋯

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] : s.think.get = s.get

@[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.Promises s.get

theorem Computation.mem_of_promises {α : Type u} (s : Computation α) [h : s.Terminates] {a : α} (p : s.Promises a) : a ∈ s

theorem Computation.get_eq_of_promises {α : Type u} (s : Computation α) [h : s.Terminates] {a : α} : s.Promises 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

• s.Results a n = ∃ (h : a ∈ s), s.length = n

theorem Computation.results_of_terminates {α : Type u} (s : Computation α) [_T : s.Terminates] : s.Results s.get s.length

theorem Computation.results_of_terminates' {α : Type u} (s : Computation α) [T : s.Terminates] {a : α} (h : a ∈ s) : s.Results a s.length

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) : s.Terminates

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_pure {α : Type u} (a : α) : (Computation.pure a).get = a

@[simp]

theorem Computation.length_pure {α : Type u} (a : α) : (Computation.pure a).length = 0

theorem Computation.results_pure {α : Type u} (a : α) : (Computation.pure a).Results a 0

@[simp]

theorem Computation.length_think {α : Type u} (s : Computation α) [h : s.Terminates] : s.think.length = s.length + 1

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_pure {α : Type u} (a : α) (n : ℕ) : ((Computation.pure a).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 = (Computation.pure a).thinkN n

theorem Computation.eq_thinkN' {α : Type u} (s : Computation α) [_h : s.Terminates] : s = (Computation.pure s.get).thinkN s.length

def Computation.memRecOn {α : Type u} {C : Computation α → Sort v} {a : α} {s : Computation α} (M : a ∈ s) (h1 : C (Computation.pure a)) (h2 : (s : Computation α) → C s → C s.think) : C s

Recursor based on membership

Equations

• Computation.memRecOn M h1 h2 = ⋯.mpr (⋯.mpr (Nat.recAux h1 (fun (n : ℕ) (IH : C ((Computation.pure a).thinkN n)) => h2 ((Computation.pure a).thinkN n) IH) s.length))

def Computation.terminatesRecOn {α : Type u} {C : Computation α → Sort v} (s : Computation α) [s.Terminates] (h1 : (a : α) → C (Computation.pure a)) (h2 : (s : Computation α) → C s → C s.think) : C s

Recursor based on assertion of Terminates

Equations

• s.terminatesRecOn h1 h2 = Computation.memRecOn ⋯ (h1 s.get) h2

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

Map a function on the result of a computation.

Equations

• Computation.map f ⟨s, al⟩ = ⟨Stream'.map (fun (o : Option α) => Option.casesOn o none (some ∘ f)) s, ⋯⟩

def Computation.Bind.g {α : Type u} {β : Type v} : β ⊕ Computation β → β ⊕ Computation α ⊕ Computation β

bind over a Sum of Computation

Equations

• Computation.Bind.g (Sum.inl a) = Sum.inl a
• Computation.Bind.g (Sum.inr ca) = Sum.inr (Sum.inr ca)

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

bind over a function mapping α to a Computation

Equations

• Computation.Bind.f f (Sum.inl ca) = match ca.destruct with | Sum.inl a => Computation.Bind.g (f a).destruct | Sum.inr ca' => Sum.inr (Sum.inl ca')
• Computation.Bind.f f (Sum.inr cb) = Computation.Bind.g cb.destruct

def Computation.bind {α : Type u} {β : Type v} (c : Computation α) (f : α → Computation β) : Computation β

Compose two computations into a monadic bind operation.

Equations

• c.bind f = Computation.corec (Computation.Bind.f f) (Sum.inl c)

instance Computation.instBind : Bind Computation

Equations

• Computation.instBind = { bind := @Computation.bind }

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

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

Flatten a computation of computations into a single computation.

Equations

• c.join = c >>= id

@[simp]

theorem Computation.map_pure {α : Type u} {β : Type v} (f : α → β) (a : α) : Computation.map f (Computation.pure a) = Computation.pure (f a)

@[simp]

theorem Computation.map_think {α : Type u} {β : Type v} (f : α → β) (s : Computation α) : Computation.map f s.think = (Computation.map f s).think

@[simp]

theorem Computation.destruct_map {α : Type u} {β : Type v} (f : α → β) (s : Computation α) : (Computation.map f s).destruct = Computation.lmap f (Computation.rmap (Computation.map f) s.destruct)

@[simp]

theorem Computation.map_id {α : Type u} (s : Computation α) : Computation.map id s = s

theorem Computation.map_comp {α : Type u} {β : Type v} {γ : Type w} (f : α → β) (g : β → γ) (s : Computation α) : Computation.map (g ∘ f) s = Computation.map g (Computation.map f s)

@[simp]

theorem Computation.ret_bind {α : Type u} {β : Type v} (a : α) (f : α → Computation β) : (Computation.pure a).bind f = f a

@[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_pure {α : Type u} {β : Type v} (f : α → β) (s : Computation α) : s.bind (Computation.pure ∘ f) = Computation.map f s

@[simp]

theorem Computation.bind_pure' {α : Type u} (s : Computation α) : s.bind Computation.pure = s

@[simp]

theorem Computation.bind_assoc {α : Type u} {β : Type v} {γ : Type w} (s : Computation α) (f : α → Computation β) (g : β → Computation γ) : (s.bind f).bind g = s.bind fun (x : α) => (f x).bind g

theorem Computation.results_bind {α : Type u} {β : Type v} {s : Computation α} {f : α → Computation β} {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 : α → Computation β} {a : α} {b : β} (h1 : a ∈ s) (h2 : b ∈ f a) : b ∈ s.bind f

instance Computation.terminates_bind {α : Type u} {β : Type v} (s : Computation α) (f : α → Computation β) [s.Terminates] [(f s.get).Terminates] : (s.bind f).Terminates

Equations

• ⋯ = ⋯

@[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 : β} (h : b ∈ s.bind f) : ∃ (a : α), a ∈ s ∧ b ∈ f a

theorem Computation.bind_promises {α : Type u} {β : Type v} {s : Computation α} {f : α → Computation β} {a : α} {b : β} (h1 : s.Promises a) (h2 : (f a).Promises b) : (s.bind f).Promises b

instance Computation.monad : Monad Computation

Equations

• Computation.monad = Monad.mk

instance Computation.instLawfulMonad : LawfulMonad Computation

Equations

• Computation.instLawfulMonad = ⋯

theorem Computation.has_map_eq_map {α β : Type u} (f : α → β) (c : Computation α) : f <$> c = Computation.map f c

@[simp]

theorem Computation.pure_def {α : Type u} (a : α) : pure a = Computation.pure a

@[simp]

theorem Computation.map_pure' {α β : Type u_1} (f : α → β) (a : α) : f <$> Computation.pure a = Computation.pure (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 ∈ Computation.map f 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

instance Computation.terminates_map {α : Type u} {β : Type v} (f : α → β) (s : Computation α) [s.Terminates] : (Computation.map f s).Terminates

Equations

• ⋯ = ⋯

theorem Computation.terminates_map_iff {α : Type u} {β : Type v} (f : α → β) (s : Computation α) : (Computation.map f s).Terminates ↔ s.Terminates

def Computation.orElse {α : Type u} (c₁ : Computation α) (c₂ : Unit → Computation α) : Computation α

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.

instance Computation.instAlternativeComputation : Alternative Computation

Equations

• Computation.instAlternativeComputation = Alternative.mk Computation.empty @Computation.orElse

@[simp]

theorem Computation.ret_orElse {α : Type u} (a : α) (c₂ : Computation α) : (Computation.pure a <|> c₂) = Computation.pure a

@[simp]

theorem Computation.orElse_pure {α : Type u} (c₁ : Computation α) (a : α) : (c₁.think <|> Computation.pure a) = Computation.pure 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 α) : (Computation.empty α <|> c) = c

@[simp]

theorem Computation.orElse_empty {α : Type u} (c : Computation α) : (c <|> Computation.empty α) = 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

• c₁.Equiv c₂ = ∀ (a : α), a ∈ c₁ ↔ a ∈ c₂

def Computation.«term_~_» : Lean.TrailingParserDescr

equivalence relation for computations

Equations

• Computation.«term_~_» = Lean.ParserDescr.trailingNode `Computation.«term_~_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ~ ") (Lean.ParserDescr.cat `term 51))

theorem Computation.Equiv.refl {α : Type u} (s : Computation α) : s.Equiv s

theorem Computation.Equiv.symm {α : Type u} {s t : Computation α} : s.Equiv t → t.Equiv s

theorem Computation.Equiv.trans {α : Type u} {s t u : Computation α} : s.Equiv t → t.Equiv u → s.Equiv u

theorem Computation.Equiv.equivalence {α : Type u} : Equivalence Computation.Equiv

theorem Computation.equiv_of_mem {α : Type u} {s t : Computation α} {a : α} (h1 : a ∈ s) (h2 : a ∈ t) : s.Equiv t

theorem Computation.terminates_congr {α : Type u} {c₁ c₂ : Computation α} (h : c₁.Equiv c₂) : c₁.Terminates ↔ c₂.Terminates

theorem Computation.promises_congr {α : Type u} {c₁ c₂ : Computation α} (h : c₁.Equiv c₂) (a : α) : c₁.Promises a ↔ c₂.Promises a

theorem Computation.get_equiv {α : Type u} {c₁ c₂ : Computation α} (h : c₁.Equiv c₂) [c₁.Terminates] [c₂.Terminates] : c₁.get = c₂.get

theorem Computation.think_equiv {α : Type u} (s : Computation α) : s.think.Equiv s

theorem Computation.thinkN_equiv {α : Type u} (s : Computation α) (n : ℕ) : (s.thinkN n).Equiv s

theorem Computation.bind_congr {α : Type u} {β : Type v} {s1 s2 : Computation α} {f1 f2 : α → Computation β} (h1 : s1.Equiv s2) (h2 : ∀ (a : α), (f1 a).Equiv (f2 a)) : (s1.bind f1).Equiv (s2.bind f2)

theorem Computation.equiv_pure_of_mem {α : Type u} {s : Computation α} {a : α} (h : a ∈ s) : s.Equiv (Computation.pure a)

def Computation.LiftRel {α : Type u} {β : Type v} (R : α → β → Prop) (ca : Computation α) (cb : Computation β) : Prop

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

• Computation.LiftRel R ca cb = ((∀ {a : α}, a ∈ ca → ∃ (b : β), b ∈ cb ∧ R a b) ∧ ∀ {b : β}, b ∈ cb → ∃ (a : α), a ∈ ca ∧ R a b)

theorem Computation.LiftRel.swap {α : Type u} {β : Type v} (R : α → β → Prop) (ca : Computation α) (cb : Computation β) : Computation.LiftRel (Function.swap R) cb ca ↔ Computation.LiftRel R ca cb

theorem Computation.lift_eq_iff_equiv {α : Type u} (c₁ c₂ : Computation α) : Computation.LiftRel (fun (x1 x2 : α) => x1 = x2) c₁ c₂ ↔ c₁.Equiv c₂

theorem Computation.LiftRel.refl {α : Type u} (R : α → α → Prop) (H : Reflexive R) : Reflexive (Computation.LiftRel R)

theorem Computation.LiftRel.symm {α : Type u} (R : α → α → Prop) (H : Symmetric R) : Symmetric (Computation.LiftRel R)

theorem Computation.LiftRel.trans {α : Type u} (R : α → α → Prop) (H : Transitive R) : Transitive (Computation.LiftRel R)

theorem Computation.LiftRel.equiv {α : Type u} (R : α → α → Prop) : Equivalence R → Equivalence (Computation.LiftRel R)

theorem Computation.LiftRel.imp {α : Type u} {β : Type v} {R S : α → β → Prop} (H : ∀ {a : α} {b : β}, R a b → S a b) (s : Computation α) (t : Computation β) : Computation.LiftRel R s t → Computation.LiftRel S s t

theorem Computation.terminates_of_liftRel {α : Type u} {β : Type v} {R : α → β → Prop} {s : Computation α} {t : Computation β} : Computation.LiftRel R s t → (s.Terminates ↔ t.Terminates)

theorem Computation.rel_of_liftRel {α : Type u} {β : Type v} {R : α → β → Prop} {ca : Computation α} {cb : Computation β} : Computation.LiftRel R ca cb → ∀ {a : α} {b : β}, a ∈ ca → b ∈ cb → R 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) : Computation.LiftRel R ca cb

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 ↔ (ca.Terminates ↔ cb.Terminates) ∧ ∀ {a : α} {b : β}, a ∈ ca → b ∈ cb → R 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 b → Computation.LiftRel S (f1 a) (f2 b)) : Computation.LiftRel S (s1.bind f1) (s2.bind f2)

@[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 : β) : Computation.LiftRel R (Computation.pure a) (Computation.pure b) ↔ R a b

@[simp]

theorem Computation.liftRel_think_left {α : Type u} {β : Type v} (R : α → β → Prop) (ca : Computation α) (cb : Computation β) : Computation.LiftRel R ca.think cb ↔ Computation.LiftRel R ca cb

@[simp]

theorem Computation.liftRel_think_right {α : Type u} {β : Type v} (R : α → β → Prop) (ca : Computation α) (cb : Computation β) : Computation.LiftRel R ca cb.think ↔ Computation.LiftRel R ca cb

theorem Computation.liftRel_mem_cases {α : Type u} {β : Type v} {R : α → β → Prop} {ca : Computation α} {cb : Computation β} (Ha : ∀ (a : α), a ∈ ca → Computation.LiftRel R ca cb) (Hb : ∀ (b : β), b ∈ cb → Computation.LiftRel R ca cb) : Computation.LiftRel R ca cb

theorem Computation.liftRel_congr {α : Type u} {β : Type v} {R : α → β → Prop} {ca ca' : Computation α} {cb cb' : Computation β} (ha : ca.Equiv ca') (hb : cb.Equiv cb') : Computation.LiftRel R ca cb ↔ Computation.LiftRel R ca' 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 b → S (f1 a) (f2 b)) : Computation.LiftRel S (Computation.map f1 s1) (Computation.map f2 s2)

theorem Computation.map_congr {α : Type u} {β : Type v} {s1 s2 : Computation α} {f : α → β} (h1 : s1.Equiv s2) : (Computation.map f s1).Equiv (Computation.map f s2)

def Computation.LiftRelAux {α : Type u} {β : Type v} (R : α → β → Prop) (C : Computation α → Computation β → Prop) : α ⊕ Computation α → β ⊕ Computation β → Prop

Alternate definition of LiftRel over relations between Computations

Equations

• Computation.LiftRelAux R C (Sum.inl a) (Sum.inl b) = R a b
• Computation.LiftRelAux R C (Sum.inl a) (Sum.inr cb) = ∃ (b : β), b ∈ cb ∧ R a b
• Computation.LiftRelAux R C (Sum.inr ca) (Sum.inl b) = ∃ (a : α), a ∈ ca ∧ R a b
• Computation.LiftRelAux R C (Sum.inr ca) (Sum.inr cb) = C ca cb

@[simp]

theorem Computation.liftRelAux_inl_inl {α : Type u} {β : Type v} {R : α → β → Prop} {C : Computation α → Computation β → Prop} {a : α} {b : β} : Computation.LiftRelAux R C (Sum.inl a) (Sum.inl b) = R a b

@[simp]

theorem Computation.liftRelAux_inl_inr {α : Type u} {β : Type v} {R : α → β → Prop} {C : Computation α → Computation β → Prop} {a : α} {cb : Computation β} : Computation.LiftRelAux R C (Sum.inl a) (Sum.inr cb) = ∃ (b : β), b ∈ cb ∧ R a b

@[simp]

theorem Computation.liftRelAux_inr_inl {α : Type u} {β : Type v} {R : α → β → Prop} {C : Computation α → Computation β → Prop} {b : β} {ca : Computation α} : Computation.LiftRelAux R C (Sum.inr ca) (Sum.inl b) = ∃ (a : α), a ∈ ca ∧ R a b

@[simp]

theorem Computation.liftRelAux_inr_inr {α : Type u} {β : Type v} {R : α → β → Prop} {C : Computation α → Computation β → Prop} {ca : Computation α} {cb : Computation β} : 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 β) : Computation.LiftRelAux R C (Sum.inl a) cb.destruct ↔ ∃ (b : β), b ∈ cb ∧ R a b

theorem Computation.LiftRelAux.swap {α : Type u} {β : Type v} (R : α → β → Prop) (C : Computation α → Computation β → Prop) (a : α ⊕ Computation α) (b : β ⊕ Computation β) : Computation.LiftRelAux (Function.swap R) (Function.swap C) b a = Computation.LiftRelAux R C a b

@[simp]

theorem Computation.LiftRelAux.ret_right {α : Type u} {β : Type v} (R : α → β → Prop) (C : Computation α → Computation β → Prop) (b : β) (ca : Computation α) : Computation.LiftRelAux R C ca.destruct (Sum.inl b) ↔ ∃ (a : α), a ∈ ca ∧ R a b

theorem Computation.LiftRelRec.lem {α : Type u} {β : Type v} {R : α → β → Prop} (C : Computation α → Computation β → Prop) (H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → Computation.LiftRelAux R C ca.destruct cb.destruct) (ca : Computation α) (cb : Computation β) (Hc : C ca cb) (a : α) (ha : a ∈ ca) : Computation.LiftRel R ca cb

theorem Computation.liftRel_rec {α : Type u} {β : Type v} {R : α → β → Prop} (C : Computation α → Computation β → Prop) (H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → Computation.LiftRelAux R C ca.destruct cb.destruct) (ca : Computation α) (cb : Computation β) (Hc : C ca cb) : Computation.LiftRel R ca cb