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.

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

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

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

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

think c is the computation that delays for one "tick" and then performs computation 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

• 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'.

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

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

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

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

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.

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

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

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

Corecursor constructor for corec

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').

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

left map of ⊕

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

right map of ⊕

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

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

Attribute expressing bisimilarity over two Computations

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

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

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 => x ∈ x_1

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

• term : ∃ a, a ∈ s✝

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

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

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)

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)

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)

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.

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.

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

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

get s returns the result of a terminating computation

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.

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

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

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

Map a function on the result of a computation.

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

bind over a Sum of Computation

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

bind over a function mapping α to a Computation

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

Compose two computations into a monadic bind operation.

instance Computation.instBindComputation : Bind Computation

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.

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

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

instance Computation.instLawfulMonadComputationMonad : LawfulMonad Computation

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)

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.

instance Computation.instAlternativeComputation : Alternative Computation

@[simp]

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

@[simp]

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

@[simp]

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

@[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 α) : (HOrElse.hOrElse c fun x => 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.

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

equivalence relation for computations

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.

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

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