mathlib docs: data.seq.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 // ∀ {n : ℕ} {a : α}, f n = option.some a → f (n + 1) = option.some a}

source

def computation.return {α : Type u} :

α → computation α

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

Equations

computation.return a = ⟨stream.const (option.some a), _⟩

source

@[instance]

def computation.has_coe_t {α : Type u} :

has_coe_t α (computation α)

Equations

computation.has_coe_t = {coe := computation.return α}

source

def computation.think {α : Type u} :

computation α → computation α

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

Equations

c.think = ⟨option.none :: c.val, _⟩

source

def computation.thinkN {α : Type u} :

computation α → ℕ → computation α

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

Equations

c.thinkN (n + 1) = (c.thinkN n).think
c.thinkN 0 = c

source

def computation.head {α : Type u} :

computation α → option α

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

Equations

c.head = c.val.head

source

def computation.tail {α : Type u} :

computation α → computation α

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

Equations

c.tail = ⟨c.val.tail, _⟩

source

def computation.empty (α : Type u_1) :

computation α

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

Equations

computation.empty α = ⟨stream.const option.none, _⟩

source

@[instance]

def computation.inhabited {α : Type u} :

inhabited (computation α)

Equations

computation.inhabited = {default := computation.empty α}

source

def computation.run_for {α : Type u} :

computation α → ℕ → option α

run_for c n evaluates c for n steps and returns the result, or none if it did not terminate after n steps.

Equations

computation.run_for = subtype.val

source

def computation.destruct {α : Type u} :

computation α → α ⊕ computation α

destruct c is the destructor for computation α as a coinductive type. It returns inl a if c = return a and inr c' if c = think c'.

Equations

c.destruct = computation.destruct._match_1 c (c.val 0)
computation.destruct._match_1 c (option.some a) = sum.inl a
computation.destruct._match_1 c option.none = sum.inr c.tail

source

meta def computation.run {α : Type u} :

computation α → α

run c is an unsound meta function that runs c to completion, possibly resulting in an infinite loop in the VM.

source

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

s.destruct = sum.inl a → s = computation.return a

source

theorem computation.destruct_eq_think {α : Type u} {s s' : computation α} :

s.destruct = sum.inr s' → s = s'.think

source

@[simp]

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

(computation.return a).destruct = sum.inl a

source

@[simp]

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

s.think.destruct = sum.inr s

source

@[simp]

theorem computation.destruct_empty {α : Type u} :

(computation.empty α).destruct = sum.inr (computation.empty α)

source

@[simp]

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

(computation.return a).head = option.some a

source

@[simp]

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

s.think.head = option.none

source

@[simp]

theorem computation.head_empty {α : Type u} :

(computation.empty α).head = option.none

source

@[simp]

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

(computation.return a).tail = computation.return a

source

@[simp]

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

s.think.tail = s

source

@[simp]

theorem computation.tail_empty {α : Type u} :

(computation.empty α).tail = computation.empty α

source

theorem computation.think_empty {α : Type u} :

computation.empty α = (computation.empty α).think

source

def computation.cases_on {α : Type u} {C : computation α → Sort v} (s : computation α) :

(Π (a : α), C (computation.return a)) → (Π (s : computation α), C s.think) → C s

Equations

s.cases_on h1 h2 = (λ (_x : α ⊕ computation α) (H : s.destruct = _x), sum.rec (λ (v : α) (H : s.destruct = sum.inl v), _.mpr (h1 v)) (λ (v : computation α) (H : s.destruct = sum.inr v), subtype.cases_on v (λ (a : stream (option α)) (s' : ∀ {n : ℕ} {a_1 : α}, a n = option.some a_1 → a (n + 1) = option.some a_1) (H : s.destruct = sum.inr ⟨a, s'⟩), _.mpr (h2 ⟨a, s'⟩)) H) _x H) s.destruct _

source

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

(β → α ⊕ β) → α ⊕ β → option α × (α ⊕ β)

Equations

computation.corec.F f (sum.inr b) = (computation.corec.F._match_1 (f b), f b)
computation.corec.F f (sum.inl a) = (option.some a, sum.inl a)
computation.corec.F._match_1 (sum.inr b') = option.none
computation.corec.F._match_1 (sum.inl a) = option.some a

source

def computation.corec {α : Type u} {β : Type v} :

(β → α ⊕ β) → β → computation α

corec f b is the corecursor for computation α as a coinductive type. If f b = inl a then corec f b = return a, and if f b = inl b' then corec f b = think (corec f b').

Equations

computation.corec f b = ⟨stream.corec' (computation.corec.F f) (sum.inr b), _⟩

source

@[simp]

def computation.lmap {α : Type u} {β : Type v} {γ : Type w} :

(α → β) → α ⊕ γ → β ⊕ γ

left map of ⊕

Equations

computation.lmap f (sum.inr b) = sum.inr b
computation.lmap f (sum.inl a) = sum.inl (f a)

source

@[simp]

def computation.rmap {α : Type u} {β : Type v} {γ : Type w} :

(β → γ) → α ⊕ β → α ⊕ γ

right map of ⊕

Equations

computation.rmap f (sum.inr b) = sum.inr (f b)
computation.rmap f (sum.inl a) = sum.inl a

source

@[simp]

theorem computation.corec_eq {α : Type u} {β : Type v} (f : β → α ⊕ β) (b : β) :

(computation.corec f b).destruct = computation.rmap (computation.corec f) (f b)

source

@[simp]

def computation.bisim_o {α : Type u} :

(computation α → computation α → Prop) → α ⊕ computation α → α ⊕ computation α → Prop

Equations

computation.bisim_o R (sum.inr s) (sum.inr s') = R s s'
computation.bisim_o R (sum.inr val) (sum.inl val_1) = false
computation.bisim_o R (sum.inl val) (sum.inr val_1) = false
computation.bisim_o R (sum.inl a) (sum.inl a') = (a = a')

source

def computation.is_bisimulation {α : Type u} :

(computation α → computation α → Prop) → Prop

Equations

computation.is_bisimulation R = ∀ ⦃s₁ s₂ : computation α⦄, R s₁ s₂ → computation.bisim_o R s₁.destruct s₂.destruct

source

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

R s₁ s₂ → s₁ = s₂

source

def computation.mem {α : Type u} :

α → computation α → Prop

Equations

computation.mem a s = (option.some a ∈ s.val)

source

@[instance]

def computation.has_mem {α : Type u} :

has_mem α (computation α)

Equations

computation.has_mem = {mem := computation.mem α}

source

theorem computation.le_stable {α : Type u} (s : computation α) {a : α} {m n : ℕ} :

m ≤ n → s.val m = option.some a → s.val n = option.some a

source

theorem computation.mem_unique {α : Type u} :

relator.left_unique has_mem.mem

source

@[class]

def computation.terminates {α : Type u} :

computation α → Prop

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

Equations

s.terminates = ∃ (a : α), a ∈ s

Instances

source

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

a ∈ s → s.terminates

source

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

s.terminates ↔ ∃ (n : ℕ), ↥((s.val n).is_some)

source

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

a ∈ computation.return a

source

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

a' ∈ computation.return a → a' = a

source

@[instance]

def computation.ret_terminates {α : Type u} (a : α) :

(computation.return a).terminates

Equations

_ = _

source

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

a ∈ s → a ∈ s.think

source

@[instance]

def computation.think_terminates {α : Type u} (s : computation α) [s.terminates] :

s.think.terminates

Equations

_ = _

source

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

a ∈ s.think → a ∈ s

source

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

s.think.terminates → s.terminates

source

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

a ∉ computation.empty α

source

theorem computation.not_terminates_empty {α : Type u} :

¬(computation.empty α).terminates

source

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

¬s.terminates → s = computation.empty α

source

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

a ∈ s.thinkN n ↔ a ∈ s

source

@[instance]

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

(s.thinkN n).terminates

Equations

_ = _

source

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

(s.thinkN n).terminates → s.terminates

source

def computation.promises {α : Type u} :

computation α → α → Prop

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

Equations

s ~> a = ∀ ⦃a' : α⦄, a' ∈ s → a = a'

source

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

a ∈ s → s ~> a

source

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

computation.empty α ~> a

source

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 _

source

def computation.get {α : Type u} (s : computation α) [h : s.terminates] :

α

get s returns the result of a terminating computation

Equations

s.get = option.get _

source

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

s.get ∈ s

source

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

a ∈ s → s.get = a

source

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

s.get = a → a ∈ s

source

@[simp]

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

s.think.get = s.get

source

@[simp]

theorem computation.get_thinkN {α : Type u} (s : computation α) [h : s.terminates] (n : ℕ) :

(s.thinkN n).get = s.get

source

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

s ~> s.get

source

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

s ~> a → a ∈ s

source

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

s ~> a → s.get = a

source

def computation.results {α : Type u} :

computation α → α → ℕ → Prop

results s a n completely characterizes a terminating computation: it asserts that s terminates after exactly n steps, with result a.

Equations

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

source

theorem computation.results_of_terminates {α : Type u} (s : computation α) [T : s.terminates] :

s.results s.get s.length

source

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

a ∈ s → s.results a s.length

source

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

s.results a n → a ∈ s

source

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

s.results a n → s.terminates

source

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

s.results a n → s.length = n

source

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

s.results a m → s.results b n → a = b

source

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

s.results a m → s.results b n → m = n

source

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

a ∈ s → (∃ (n : ℕ), s.results a n)

source

@[simp]

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

(computation.return a).get = a

source

@[simp]

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

(computation.return a).length = 0

source

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

(computation.return a).results a 0

source

@[simp]

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

s.think.length = s.length + 1

source

theorem computation.results_think {α : Type u} {s : computation α} {a : α} {n : ℕ} :

s.results a n → s.think.results a (n + 1)

source

theorem computation.of_results_think {α : Type u} {s : computation α} {a : α} {n : ℕ} :

s.think.results a n → (∃ (m : ℕ), s.results a m ∧ n = m + 1)

source

@[simp]

theorem computation.results_think_iff {α : Type u} {s : computation α} {a : α} {n : ℕ} :

s.think.results a (n + 1) ↔ s.results a n

source

theorem computation.results_thinkN {α : Type u} {s : computation α} {a : α} {m : ℕ} (n : ℕ) :

s.results a m → (s.thinkN n).results a (m + n)

source

theorem computation.results_thinkN_ret {α : Type u} (a : α) (n : ℕ) :

((computation.return a).thinkN n).results a n

source

@[simp]

theorem computation.length_thinkN {α : Type u} (s : computation α) [h : s.terminates] (n : ℕ) :

(s.thinkN n).length = s.length + n

source

theorem computation.eq_thinkN {α : Type u} {s : computation α} {a : α} {n : ℕ} :

s.results a n → s = (computation.return a).thinkN n

source

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

s = (computation.return s.get).thinkN s.length

source

def computation.mem_rec_on {α : Type u} {C : computation α → Sort v} {a : α} {s : computation α} :

a ∈ s → C (computation.return a) → (Π (s : computation α), C s → C s.think) → C s

Equations

computation.mem_rec_on M h1 h2 = _.mpr (_.mpr (nat.rec h1 (λ (n : ℕ) (IH : C ((computation.return a).thinkN n)), h2 ((computation.return a).thinkN n) IH) s.length))

source

def computation.terminates_rec_on {α : Type u} {C : computation α → Sort v} (s : computation α) [s.terminates] :

(Π (a : α), C (computation.return a)) → (Π (s : computation α), C s → C s.think) → C s

Equations

s.terminates_rec_on h1 h2 = computation.mem_rec_on _ (h1 s.get) h2

source

def computation.map {α : Type u} {β : Type v} :

(α → β) → computation α → computation β

Map a function on the result of a computation.

Equations

computation.map f ⟨s, al⟩ = ⟨stream.map (λ (o : option α), o.cases_on option.none (option.some ∘ f)) s, _⟩

source

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

β ⊕ computation β → β ⊕ computation α ⊕ computation β

Equations

computation.bind.G (sum.inr cb') = sum.inr (sum.inr cb')
computation.bind.G (sum.inl b) = sum.inl b

source

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

(α → computation β) → computation α ⊕ computation β → β ⊕ computation α ⊕ computation β

Equations

computation.bind.F f (sum.inr cb) = computation.bind.G cb.destruct
computation.bind.F f (sum.inl ca) = computation.bind.F._match_1 f ca.destruct
computation.bind.F._match_1 f (sum.inr ca') = sum.inr (sum.inl ca')
computation.bind.F._match_1 f (sum.inl a) = computation.bind.G (f a).destruct

source

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

computation α → (α → computation β) → computation β

Compose two computations into a monadic bind operation.

Equations

c.bind f = computation.corec (computation.bind.F f) (sum.inl c)

source

@[instance]

def computation.has_bind :

has_bind computation

Equations

computation.has_bind = {bind := computation.bind}

source

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

c >>= f = c.bind f

source

def computation.join {α : Type u} :

computation (computation α) → computation α

Flatten a computation of computations into a single computation.

Equations

c.join = c >>= id

source

@[simp]

theorem computation.map_ret {α : Type u} {β : Type v} (f : α → β) (a : α) :

computation.map f (computation.return a) = computation.return (f a)

source

@[simp]

theorem computation.map_think {α : Type u} {β : Type v} (f : α → β) (s : computation α) :

computation.map f s.think = (computation.map f s).think

source

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

source

@[simp]

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

computation.map id s = s

source

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)

source

@[simp]

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

(computation.return a).bind f = f a

source

@[simp]

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

c.think.bind f = (c.bind f).think

source

@[simp]

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

s.bind (computation.return ∘ f) = computation.map f s

source

@[simp]

theorem computation.bind_ret' {α : Type u} (s : computation α) :

s.bind computation.return = s

source

@[simp]

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

(s.bind f).bind g = s.bind (λ (x : α), (f x).bind g)

source

theorem computation.results_bind {α : Type u} {β : Type v} {s : computation α} {f : α → computation β} {a : α} {b : β} {m n : ℕ} :

s.results a m → (f a).results b n → (s.bind f).results b (n + m)

source

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

a ∈ s → b ∈ f a → b ∈ s.bind f

source

@[instance]

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

(s.bind f).terminates

Equations

_ = _

source

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

source

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

source

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)

source

theorem computation.exists_of_mem_bind {α : Type u} {β : Type v} {s : computation α} {f : α → computation β} {b : β} :

b ∈ s.bind f → (∃ (a : α) (H : a ∈ s), b ∈ f a)

source

theorem computation.bind_promises {α : Type u} {β : Type v} {s : computation α} {f : α → computation β} {a : α} {b : β} :

s ~> a → f a ~> b → s.bind f ~> b

source

@[instance]

def computation.monad :

monad computation

Equations

computation.monad = monad.mk

source

@[instance]

def computation.is_lawful_monad :

is_lawful_monad computation

Equations

computation.is_lawful_monad = _

source

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

f <$> c = computation.map f c

source

@[simp]

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

return a = computation.return a

source

@[simp]

theorem computation.map_ret' {α β : Type u_1} (f : α → β) (a : α) :

f <$> computation.return a = computation.return (f a)

source

@[simp]

theorem computation.map_think' {α β : Type u_1} (f : α → β) (s : computation α) :

f <$> s.think = (f <$> s).think

source

theorem computation.mem_map {α : Type u} {β : Type v} (f : α → β) {a : α} {s : computation α} :

a ∈ s → f a ∈ computation.map f s

source

theorem computation.exists_of_mem_map {α : Type u} {β : Type v} {f : α → β} {b : β} {s : computation α} :

b ∈ computation.map f s → (∃ (a : α), a ∈ s ∧ f a = b)

source

@[instance]

def computation.terminates_map {α : Type u} {β : Type v} (f : α → β) (s : computation α) [s.terminates] :

(computation.map f s).terminates

Equations

_ = _

source

theorem computation.terminates_map_iff {α : Type u} {β : Type v} (f : α → β) (s : computation α) :

(computation.map f s).terminates ↔ s.terminates

source

def computation.orelse {α : Type u} :

computation α → computation α → computation α

c₁ <|> c₂ calculates c₁ and c₂ simultaneously, returning the first one that gives a result.

Equations

c₁.orelse c₂ = computation.corec (λ (_x : computation α × computation α), computation.orelse._match_3 _x) (c₁, c₂)
computation.orelse._match_3 (c₁, c₂) = computation.orelse._match_1 c₂ c₁.destruct
computation.orelse._match_1 c₂ (sum.inr c₁') = computation.orelse._match_2 c₁' c₂.destruct
computation.orelse._match_1 c₂ (sum.inl a) = sum.inl a
computation.orelse._match_2 c₁' (sum.inr c₂') = sum.inr (c₁', c₂')
computation.orelse._match_2 c₁' (sum.inl a) = sum.inl a

source

@[instance]

def computation.alternative :

alternative computation

Equations

computation.alternative = {to_applicative := monad.to_applicative computation.monad, to_has_orelse := {orelse := computation.orelse}, failure := computation.empty}

source

@[simp]

theorem computation.ret_orelse {α : Type u} (a : α) (c₂ : computation α) :

(computation.return a <|> c₂) = computation.return a

source

@[simp]

theorem computation.orelse_ret {α : Type u} (c₁ : computation α) (a : α) :

(c₁.think <|> computation.return a) = computation.return a

source

@[simp]

theorem computation.orelse_think {α : Type u} (c₁ c₂ : computation α) :

(c₁.think <|> c₂.think) = (c₁ <|> c₂).think

source

@[simp]

theorem computation.empty_orelse {α : Type u} (c : computation α) :

(computation.empty α <|> c) = c

source

@[simp]

theorem computation.orelse_empty {α : Type u} (c : computation α) :

(c <|> computation.empty α) = c

source

def computation.equiv {α : Type u} :

computation α → computation α → Prop

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

Equations

c₁ ~ c₂ = ∀ (a : α), a ∈ c₁ ↔ a ∈ c₂

source

theorem computation.equiv.refl {α : Type u} (s : computation α) :

s ~ s

source

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

s ~ t → t ~ s

source

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

s ~ t → t ~ u → s ~ u

source

theorem computation.equiv.equivalence {α : Type u} :

equivalence computation.equiv

source

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

a ∈ s → a ∈ t → s ~ t

source

theorem computation.terminates_congr {α : Type u} {c₁ c₂ : computation α} :

c₁ ~ c₂ → (c₁.terminates ↔ c₂.terminates)

source

theorem computation.promises_congr {α : Type u} {c₁ c₂ : computation α} (h : c₁ ~ c₂) (a : α) :

c₁ ~> a ↔ c₂ ~> a

source

theorem computation.get_equiv {α : Type u} {c₁ c₂ : computation α} (h : c₁ ~ c₂) [c₁.terminates] [c₂.terminates] :

c₁.get = c₂.get

source

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

s.think ~ s

source

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

s.thinkN n ~ s

source

theorem computation.bind_congr {α : Type u} {β : Type v} {s1 s2 : computation α} {f1 f2 : α → computation β} :

s1 ~ s2 → (∀ (a : α), f1 a ~ f2 a) → s1.bind f1 ~ s2.bind f2

source

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

a ∈ s → s ~ computation.return a

source

def computation.lift_rel {α : Type u} {β : Type v} :

(α → β → Prop) → computation α → computation β → Prop

lift_rel R ca cb is a generalization of equiv to relations other than equality. It asserts that if ca terminates with a, then cb terminates with some b such that R a b, and if cb terminates with b then ca terminates with some a such that R a b.

Equations

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

source

theorem computation.lift_rel.swap {α : Type u} {β : Type v} (R : α → β → Prop) (ca : computation α) (cb : computation β) :

computation.lift_rel (function.swap R) cb ca ↔ computation.lift_rel R ca cb

source

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

computation.lift_rel eq c₁ c₂ ↔ c₁ ~ c₂

source

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

reflexive R → reflexive (computation.lift_rel R)

source

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

symmetric R → symmetric (computation.lift_rel R)

source

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

transitive R → transitive (computation.lift_rel R)

source

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

equivalence R → equivalence (computation.lift_rel R)

source

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

computation.lift_rel R s t → computation.lift_rel S s t

source

theorem computation.terminates_of_lift_rel {α : Type u} {β : Type v} {R : α → β → Prop} {s : computation α} {t : computation β} :

computation.lift_rel R s t → (s.terminates ↔ t.terminates)

source

theorem computation.rel_of_lift_rel {α : Type u} {β : Type v} {R : α → β → Prop} {ca : computation α} {cb : computation β} (a : computation.lift_rel R ca cb) {a_1 : α} {b : β} :

a_1 ∈ ca → b ∈ cb → R a_1 b

source

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

a ∈ ca → b ∈ cb → R a b → computation.lift_rel R ca cb

source

theorem computation.exists_of_lift_rel_left {α : Type u} {β : Type v} {R : α → β → Prop} {ca : computation α} {cb : computation β} (H : computation.lift_rel R ca cb) {a : α} :

a ∈ ca → (∃ {b : β}, b ∈ cb ∧ R a b)

source

theorem computation.exists_of_lift_rel_right {α : Type u} {β : Type v} {R : α → β → Prop} {ca : computation α} {cb : computation β} (H : computation.lift_rel R ca cb) {b : β} :

b ∈ cb → (∃ {a : α}, a ∈ ca ∧ R a b)

source

theorem computation.lift_rel_def {α : Type u} {β : Type v} {R : α → β → Prop} {ca : computation α} {cb : computation β} :

computation.lift_rel R ca cb ↔ (ca.terminates ↔ cb.terminates) ∧ ∀ {a : α} {b : β}, a ∈ ca → b ∈ cb → R a b

source

theorem computation.lift_rel_bind {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} (R : α → β → Prop) (S : γ → δ → Prop) {s1 : computation α} {s2 : computation β} {f1 : α → computation γ} {f2 : β → computation δ} :

computation.lift_rel R s1 s2 → (∀ {a : α} {b : β}, R a b → computation.lift_rel S (f1 a) (f2 b)) → computation.lift_rel S (s1.bind f1) (s2.bind f2)

source

@[simp]

theorem computation.lift_rel_return_left {α : Type u} {β : Type v} (R : α → β → Prop) (a : α) (cb : computation β) :

computation.lift_rel R (computation.return a) cb ↔ ∃ {b : β}, b ∈ cb ∧ R a b

source

@[simp]

theorem computation.lift_rel_return_right {α : Type u} {β : Type v} (R : α → β → Prop) (ca : computation α) (b : β) :

computation.lift_rel R ca (computation.return b) ↔ ∃ {a : α}, a ∈ ca ∧ R a b

source

@[simp]

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

computation.lift_rel R (computation.return a) (computation.return b) ↔ R a b

source

@[simp]

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

computation.lift_rel R ca.think cb ↔ computation.lift_rel R ca cb

source

@[simp]

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

computation.lift_rel R ca cb.think ↔ computation.lift_rel R ca cb

source

theorem computation.lift_rel_mem_cases {α : Type u} {β : Type v} {R : α → β → Prop} {ca : computation α} {cb : computation β} :

(∀ (a : α), a ∈ ca → computation.lift_rel R ca cb) → (∀ (b : β), b ∈ cb → computation.lift_rel R ca cb) → computation.lift_rel R ca cb

source

theorem computation.lift_rel_congr {α : Type u} {β : Type v} {R : α → β → Prop} {ca ca' : computation α} {cb cb' : computation β} :

ca ~ ca' → cb ~ cb' → (computation.lift_rel R ca cb ↔ computation.lift_rel R ca' cb')

source

theorem computation.lift_rel_map {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} (R : α → β → Prop) (S : γ → δ → Prop) {s1 : computation α} {s2 : computation β} {f1 : α → γ} {f2 : β → δ} :

computation.lift_rel R s1 s2 → (∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)) → computation.lift_rel S (computation.map f1 s1) (computation.map f2 s2)

source

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

s1 ~ s2 → computation.map f s1 ~ computation.map f s2

source

@[simp]

def computation.lift_rel_aux {α : Type u} {β : Type v} :

(α → β → Prop) → (computation α → computation β → Prop) → α ⊕ computation α → β ⊕ computation β → Prop

Equations

computation.lift_rel_aux R C (sum.inr ca) (sum.inr cb) = C ca cb
computation.lift_rel_aux R C (sum.inr ca) (sum.inl b) = ∃ {a : α}, a ∈ ca ∧ R a b
computation.lift_rel_aux R C (sum.inl a) (sum.inr cb) = ∃ {b : β}, b ∈ cb ∧ R a b
computation.lift_rel_aux R C (sum.inl a) (sum.inl b) = R a b

source

@[simp]

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

computation.lift_rel_aux R C (sum.inl a) cb.destruct ↔ ∃ {b : β}, b ∈ cb ∧ R a b

source

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

computation.lift_rel_aux (function.swap R) (function.swap C) b a = computation.lift_rel_aux R C a b

source

@[simp]

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

computation.lift_rel_aux R C ca.destruct (sum.inl b) ↔ ∃ {a : α}, a ∈ ca ∧ R a b

source

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

a ∈ ca → computation.lift_rel R ca cb

source

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

C ca cb → computation.lift_rel R ca cb

mathlib documentation

data.seq.computation

General documentation

Additional documentation

Library

mathlib documentation

data.​seq.​computation

General documentation

Additional documentation

Library

data.seq.computation