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 = { val := Stream'.const (some a), property := ⋯ }

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

Equations

• Computation.instCoeTCComputation = { 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

• Computation.think c = { val := Stream'.cons none ↑c, property := ⋯ }

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

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

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

• Computation.head c = Stream'.head ↑c

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

• Computation.tail c = { val := Stream'.tail ↑c, property := ⋯ }

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

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

Equations

• Computation.empty α = { val := Stream'.const none, property := ⋯ }

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

Equations

• Computation.instInhabitedComputation = { 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

• Computation.destruct c = match ↑c 0 with | none => Sum.inr (Computation.tail c) | 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.

Equations

• Computation.run x = let c := x; match Computation.destruct c with | Sum.inl a => a | Sum.inr ca => Computation.run ca

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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 = { val := Stream'.corec' (Computation.Corec.f f) (Sum.inr b), property := ⋯ }

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

left map of ⊕

Equations

• Computation.lmap f x = match x with | Sum.inl a => Sum.inl (f a) | Sum.inr b => Sum.inr b

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

right map of ⊕

Equations

• Computation.rmap f x = match x with | Sum.inl a => Sum.inl a | Sum.inr b => Sum.inr (f b)

@[simp]

theorem Computation.corec_eq {α : Type u} {β : Type v} (f : β → α ⊕ β) (b : β) : Computation.destruct (Computation.corec f b) = 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 x✝ x = match x✝, x with | Sum.inl a, Sum.inl a' => a = a' | Sum.inr s, Sum.inr s' => R s s' | x, x_1 => 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 (Computation.destruct s₁) (Computation.destruct s₂)

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

Assertion that a Computation limits to a given value

Equations

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

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

Equations

• Computation.instMembershipComputation = { 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 (x : α) (x_1 : Computation α) => x ∈ x_1

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 α) : Computation.Terminates s ↔ ∃ (a : α), a ∈ s

theorem Computation.terminates_of_mem {α : Type u} {s : Computation α} {a : α} (h : a ∈ s) : Computation.Terminates s

theorem Computation.terminates_def {α : Type u} (s : Computation α) : Computation.Terminates s ↔ ∃ (n : ℕ), Option.isSome (↑s n) = 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.Terminates (Computation.pure a)

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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

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

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

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

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

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

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

Equations

• ⋯ = ⋯

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

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

• Computation.Promises s 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

• One or more equations did not get rendered due to their size.

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

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

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

length s gets the number of steps of a terminating computation

Equations

• Computation.length s = Nat.find ⋯

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

get s returns the result of a terminating computation

Equations

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

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

theorem Computation.get_eq_of_mem {α : Type u} (s : Computation α) [h : Computation.Terminates s] {a : α} : a ∈ s → Computation.get s = a

theorem Computation.mem_of_get_eq {α : Type u} (s : Computation α) [h : Computation.Terminates s] {a : α} : Computation.get s = a → a ∈ s

@[simp]

theorem Computation.get_think {α : Type u} (s : Computation α) [h : Computation.Terminates s] : Computation.get (Computation.think s) = Computation.get s

@[simp]

theorem Computation.get_thinkN {α : Type u} (s : Computation α) [h : Computation.Terminates s] (n : ℕ) : Computation.get (Computation.thinkN s n) = Computation.get s

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

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

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

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

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

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

theorem Computation.Results.mem {α : Type u} {s : Computation α} {a : α} {n : ℕ} : Computation.Results s a n → a ∈ s

theorem Computation.Results.terminates {α : Type u} {s : Computation α} {a : α} {n : ℕ} (h : Computation.Results s a n) : Computation.Terminates s

theorem Computation.Results.length {α : Type u} {s : Computation α} {a : α} {n : ℕ} [_T : Computation.Terminates s] : Computation.Results s a n → Computation.length s = n

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

@[simp]

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

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

@[simp]

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

theorem Computation.results_think {α : Type u} {s : Computation α} {a : α} {n : ℕ} (h : Computation.Results s a n) : Computation.Results (Computation.think s) a (n + 1)

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

@[simp]

theorem Computation.results_think_iff {α : Type u} {s : Computation α} {a : α} {n : ℕ} : Computation.Results (Computation.think s) a (n + 1) ↔ Computation.Results s a n

theorem Computation.results_thinkN {α : Type u} {s : Computation α} {a : α} {m : ℕ} (n : ℕ) : Computation.Results s a m → Computation.Results (Computation.thinkN s n) a (m + n)

theorem Computation.results_thinkN_pure {α : Type u} (a : α) (n : ℕ) : Computation.Results (Computation.thinkN (Computation.pure a) n) a n

@[simp]

theorem Computation.length_thinkN {α : Type u} (s : Computation α) [_h : Computation.Terminates s] (n : ℕ) : Computation.length (Computation.thinkN s n) = Computation.length s + n

theorem Computation.eq_thinkN {α : Type u} {s : Computation α} {a : α} {n : ℕ} (h : Computation.Results s a n) : s = Computation.thinkN (Computation.pure a) n

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

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 (Computation.think s)) : C s

Recursor based on membership

Equations

• One or more equations did not get rendered due to their size.

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

Recursor based on assertion of Terminates

Equations

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

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

Map a function on the result of a computation.

Equations

• Computation.map f x = match x with | { val := s, property := al } => { val := Stream'.map (fun (o : Option α) => Option.casesOn o none (some ∘ f)) s, property := ⋯ }

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

bind over a Sum of Computation

Equations

• Computation.Bind.g x = match x with | Sum.inl b => Sum.inl b | Sum.inr cb' => Sum.inr (Sum.inr cb')

def Computation.Bind.f {α : Type u} {β : Type v} (f : α → Computation β) : Computation α ⊕ Computation β → β ⊕ Computation α ⊕ 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 β) : Computation β

Compose two computations into a monadic bind operation.

Equations

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

instance Computation.instBindComputation : Bind Computation

Equations

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

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

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

Flatten a computation of computations into a single computation.

Equations

• Computation.join c = 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 (Computation.think s) = Computation.think (Computation.map f s)

@[simp]

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

@[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.bind (Computation.pure a) f = f a

@[simp]

theorem Computation.think_bind {α : Type u} {β : Type v} (c : Computation α) (f : α → Computation β) : Computation.bind (Computation.think c) f = Computation.think (Computation.bind c f)

@[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 γ) : Computation.bind (Computation.bind s f) g = Computation.bind s fun (x : α) => Computation.bind (f x) g

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) : Computation.Results (Computation.bind s f) 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 ∈ Computation.bind s f

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

Equations

• ⋯ = ⋯

@[simp]

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

@[simp]

theorem Computation.length_bind {α : Type u} {β : Type v} (s : Computation α) (f : α → Computation β) [_T1 : Computation.Terminates s] [_T2 : Computation.Terminates (f (Computation.get s))] : Computation.length (Computation.bind s f) = Computation.length (f (Computation.get s)) + Computation.length s

theorem Computation.of_results_bind {α : Type u} {β : Type v} {s : Computation α} {f : α → Computation β} {b : β} {k : ℕ} : Computation.Results (Computation.bind s f) b k → ∃ (a : α), ∃ (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) : Computation.Promises (Computation.bind s f) b

instance Computation.monad : Monad Computation

Equations

• Computation.monad = Monad.mk

instance Computation.instLawfulMonadComputationMonad : LawfulMonad Computation

Equations

• Computation.instLawfulMonadComputationMonad = ⋯

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

@[simp]

theorem Computation.map_think' {α : Type u_1} {β : Type u_1} (f : α → β) (s : Computation α) : f <$> Computation.think s = Computation.think (f <$> s)

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 α) [Computation.Terminates s] : Computation.Terminates (Computation.map f s)

Equations

• ⋯ = ⋯

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

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 = let __src := Computation.monad; Alternative.mk Computation.empty @Computation.orElse

@[simp]

theorem Computation.ret_orElse {α : Type u} (a : α) (c₂ : Computation α) : (HOrElse.hOrElse (Computation.pure a) fun (x : Unit) => c₂) = Computation.pure a

@[simp]

theorem Computation.orElse_pure {α : Type u} (c₁ : Computation α) (a : α) : (HOrElse.hOrElse (Computation.think c₁) fun (x : Unit) => Computation.pure a) = Computation.pure a

@[simp]

theorem Computation.orElse_think {α : Type u} (c₁ : Computation α) (c₂ : Computation α) : (HOrElse.hOrElse (Computation.think c₁) fun (x : Unit) => Computation.think c₂) = Computation.think (HOrElse.hOrElse c₁ fun (x : Unit) => c₂)

@[simp]

theorem Computation.empty_orElse {α : Type u} (c : Computation α) : (HOrElse.hOrElse (Computation.empty α) fun (x : Unit) => c) = c

@[simp]

theorem Computation.orElse_empty {α : Type u} (c : Computation α) : (HOrElse.hOrElse c fun (x : Unit) => Computation.empty α) = c

def Computation.Equiv {α : Type u} (c₁ : Computation α) (c₂ : Computation α) : Prop

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

Equations

• Computation.Equiv c₁ 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 α) : Computation.Equiv s s

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

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

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) : Computation.Equiv s t

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

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

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

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

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

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)) : Computation.Equiv (Computation.bind s1 f1) (Computation.bind s2 f2)

theorem Computation.equiv_pure_of_mem {α : Type u} {s : Computation α} {a : α} (h : a ∈ s) : Computation.Equiv s (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₁ : 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) : 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 : α → β → Prop} {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 → (Computation.Terminates s ↔ Computation.Terminates t)

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 ↔ (Computation.Terminates ca ↔ Computation.Terminates cb) ∧ ∀ {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 (Computation.bind s1 f1) (Computation.bind s2 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 (Computation.think ca) 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 (Computation.think cb) ↔ 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 : Computation α} {ca' : Computation α} {cb : Computation β} {cb' : Computation β} (ha : Computation.Equiv ca ca') (hb : Computation.Equiv cb 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 : Computation α} {s2 : Computation α} {f : α → β} (h1 : Computation.Equiv s1 s2) : Computation.Equiv (Computation.map f s1) (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

• 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 : α → α_1 → Prop} {C : Computation α → Computation α_1 → Prop} {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 : α → α_1 → Prop} {C : Computation α → Computation α_1 → Prop} {a : α} {cb : Computation α_1}, Computation.LiftRelAux R C (Sum.inl a) (Sum.inr cb) = ∃ (b : α_1), b ∈ cb ∧ R a b

@[simp]

theorem Computation.liftRelAux_inr_inl : ∀ {α : Type u_1} {α_1 : Type u_2} {R : α → α_1 → Prop} {C : Computation α → Computation α_1 → Prop} {b : α_1} {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_1} {α_1 : Type u_2} {R : α → α_1 → Prop} {C : Computation α → Computation α_1 → Prop} {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 β) : Computation.LiftRelAux R C (Sum.inl a) (Computation.destruct cb) ↔ ∃ (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 (Computation.destruct ca) (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 (Computation.destruct ca) (Computation.destruct cb)) (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 (Computation.destruct ca) (Computation.destruct cb)) (ca : Computation α) (cb : Computation β) (Hc : C ca cb) : Computation.LiftRel R ca cb