Coinductive formalization of unbounded computations. #

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

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 = some a → f (n + 1) = some a }

source

ink

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 := (_ : ∀ (x : ℕ) (x_1 : α), Stream'.const (some a) x = some x_1 → Stream'.const (some a) x = some x_1) }

source

ink

instance Computation.instCoeTCComputation {α : Type u} :

CoeTC α (Computation α)

Equations

Computation.instCoeTCComputation = { coe := Computation.pure }

source

ink

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 := (_ : ∀ (n : ℕ) (a : α), Stream'.cons none (↑c) n = some a → Stream'.cons none (↑c) (n + 1) = some a) }

source

ink

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)

source

ink

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

source

ink

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 := (_ : ∀ (x : ℕ) (x_1 : α), Stream'.tail (↑c) x = some x_1 → ↑c (x + 1 + 1) = some x_1) }

source

ink

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 := (_ : ∀ (x : ℕ) (x_1 : α), Stream'.const none x = some x_1 → Stream'.const none x = some x_1) }

source

ink

instance Computation.instInhabitedComputation {α : Type u} :

Inhabited (Computation α)

Equations

Computation.instInhabitedComputation = { default := Computation.empty α }

source

ink

def Computation.runFor {α : Type u} :

Computation α → ℕ → Option α

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

Equations

Computation.runFor = Subtype.val

source

ink

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

source

ink

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

source

ink

theorem Computation.destruct_eq_pure {α : Type u} {s : Computation α} {a : α} :

Computation.destruct s = Sum.inl a → s = Computation.pure a

source

ink

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

Computation.destruct s = Sum.inr s' → s = Computation.think s'

source

ink

@[simp]

theorem Computation.destruct_pure {α : Type u} (a : α) :

Computation.destruct (Computation.pure a) = Sum.inl a

source

ink

@[simp]

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

Computation.destruct (Computation.think s) = Sum.inr s

source

ink

@[simp]

theorem Computation.destruct_empty {α : Type u} :

Computation.destruct (Computation.empty α) = Sum.inr (Computation.empty α)

source

ink

@[simp]

theorem Computation.head_pure {α : Type u} (a : α) :

Computation.head (Computation.pure a) = some a

source

ink

@[simp]

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

Computation.head (Computation.think s) = none

source

ink

@[simp]

theorem Computation.head_empty {α : Type u} :

Computation.head (Computation.empty α) = none

source

ink

@[simp]

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

Computation.tail (Computation.pure a) = Computation.pure a

source

ink

@[simp]

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

Computation.tail (Computation.think s) = s

source

ink

@[simp]

theorem Computation.tail_empty {α : Type u} :

Computation.tail (Computation.empty α) = Computation.empty α

source

ink

theorem Computation.think_empty {α : Type u} :

Computation.empty α = Computation.think (Computation.empty α)

source

ink

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.

source

ink

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)

source

ink

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

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

source

ink

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

source

ink

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)

source

ink

@[simp]

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

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

source

ink

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

source

ink

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₂)

source

ink

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₂

source

ink

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)

source

ink

instance Computation.instMembershipComputation {α : Type u} :

Membership α (Computation α)

Equations

Computation.instMembershipComputation = { mem := Computation.Mem }

source

ink

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

↑s m = some a → ↑s n = some a

source

ink

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

a ∈ s → b ∈ s → a = b

source

ink

theorem Computation.Mem.left_unique {α : Type u} :

Relator.LeftUnique fun x x_1 => x ∈ x_1

source

ink

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

Prop

assertion that there is some term a such that the Computation terminates
term : ∃ a, a ∈ s

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

Instances

source

ink

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

Computation.Terminates s ↔ ∃ a, a ∈ s

source

ink

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

Computation.Terminates s

source

ink

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

Computation.Terminates s ↔ ∃ n, Option.isSome (↑s n) = true

source

ink

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

a ∈ Computation.pure a

source

ink

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

a' = a

source

ink

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

Computation.Terminates (Computation.pure a)

Equations

@Computation.ret_terminates = @Computation.ret_terminates.proof_1

source

ink

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

a ∈ s → a ∈ Computation.think s

source

ink

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

Computation.Terminates (Computation.think s)

Equations

@Computation.think_terminates = @Computation.think_terminates.proof_1

source

ink

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

a ∈ Computation.think s → a ∈ s

source

ink

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

Computation.Terminates (Computation.think s) → Computation.Terminates s

source

ink

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

¬a ∈ Computation.empty α

source

ink

theorem Computation.not_terminates_empty {α : Type u} :

¬Computation.Terminates (Computation.empty α)

source

ink

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

s = Computation.empty α

source

ink

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

a ∈ Computation.thinkN s n ↔ a ∈ s

source

ink

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

Computation.Terminates (Computation.thinkN s n)

Equations

@Computation.thinkN_terminates = @Computation.thinkN_terminates.proof_1

source

ink

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

Computation.Terminates (Computation.thinkN s n) → Computation.Terminates s

source

ink

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'

source

ink

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.

source

ink

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

a ∈ s → Computation.Promises s a

source

ink

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

Computation.Promises (Computation.empty α) a

source

ink

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 (_ : ∃ n, Option.isSome (↑s n) = true)

source

ink

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 (_ : ∃ n, Option.isSome (↑s n) = true))) (_ : Option.isSome (↑s (Nat.find (_ : ∃ n, Option.isSome (↑s n) = true))) = true)

source

ink

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

Computation.get s ∈ s

source

ink

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

a ∈ s → Computation.get s = a

source

ink

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

Computation.get s = a → a ∈ s

source

ink

@[simp]

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

Computation.get (Computation.think s) = Computation.get s

source

ink

@[simp]

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

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

source

ink

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

Computation.Promises s (Computation.get s)

source

ink

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

a ∈ s

source

ink

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

Computation.Promises s a → Computation.get s = a

source

ink

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, Computation.length s = n

source

ink

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

Computation.Results s (Computation.get s) (Computation.length s)

source

ink

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

Computation.Results s a (Computation.length s)

source

ink

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

Computation.Results s a n → a ∈ s

source

ink

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

Computation.Terminates s

source

ink

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

Computation.Results s a n → Computation.length s = n

source

ink

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

source

ink

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

source

ink

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

∃ n, Computation.Results s a n

source

ink

@[simp]

theorem Computation.get_pure {α : Type u} (a : α) :

Computation.get (Computation.pure a) = a

source

ink

@[simp]

theorem Computation.length_pure {α : Type u} (a : α) :

Computation.length (Computation.pure a) = 0

source

ink

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

Computation.Results (Computation.pure a) a 0

source

ink

@[simp]

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

Computation.length (Computation.think s) = Computation.length s + 1

source

ink

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

Computation.Results (Computation.think s) a (n + 1)

source

ink

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

source

ink

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

source

ink

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)

source

ink

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

Computation.Results (Computation.thinkN (Computation.pure a) n) a n

source

ink

@[simp]

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

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

source

ink

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

s = Computation.thinkN (Computation.pure a) n

source

ink

theorem Computation.eq_thinkN' {α : Type u} (s : Computation α) [_h : Computation.Terminates s] :

s = Computation.thinkN (Computation.pure (Computation.get s)) (Computation.length s)

source

ink

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 memberhip

Equations

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

source

ink

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

C s

Recursor based on assertion of Terminates

Equations

Computation.terminatesRecOn s h1 h2 = Computation.memRecOn (_ : Computation.get s ∈ s) (h1 (Computation.get s)) h2

source

ink

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

Computation α → Computation β

Map a function on the result of a computation.

Equations

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

source

ink

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

source

ink

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.

source

ink

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)

source

ink

instance Computation.instBindComputation :

Bind Computation

Equations

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

source

ink

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

c >>= f = Computation.bind c f

source

ink

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

Computation α

Flatten a computation of computations into a single computation.

Equations

Computation.join c = c >>= id

source

ink

@[simp]

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

Computation.map f (Computation.pure a) = Computation.pure (f a)

source

ink

@[simp]

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

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

source

ink

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

source

ink

@[simp]

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

Computation.map id s = s

source

ink

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

ink

@[simp]

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

Computation.bind (Computation.pure a) f = f a

source

ink

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

source

ink

@[simp]

theorem Computation.bind_pure {α : Type u} {β : Type v} (f : α → β) (s : Computation α) :

Computation.bind s (Computation.pure ∘ f) = Computation.map f s

source

ink

@[simp]

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

Computation.bind s Computation.pure = s

source

ink

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

source

ink

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)

source

ink

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

source

ink

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

Computation.Terminates (Computation.bind s f)

Equations

@Computation.terminates_bind = @Computation.terminates_bind.proof_1

source

ink

@[simp]

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

Computation.get (Computation.bind s f) = Computation.get (f (Computation.get s))

source

ink

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

source

ink

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

source

ink

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

source

ink

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

source

ink

instance Computation.monad :

Monad Computation

Equations

Computation.monad = Monad.mk

source

ink

instance Computation.instLawfulMonadComputationMonad :

LawfulMonad Computation

Equations

Computation.instLawfulMonadComputationMonad = Computation.instLawfulMonadComputationMonad.proof_1

source

ink

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

f <$> c = Computation.map f c

source

ink

@[simp]

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

pure a = Computation.pure a

source

ink

@[simp]

theorem Computation.map_pure' {α : Type u_1} {β : Type u_1} (f : α → β) (a : α) :

f <$> Computation.pure a = Computation.pure (f a)

source

ink

@[simp]

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

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

source

ink

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

f a ∈ Computation.map f s

source

ink

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

source

ink

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

Computation.Terminates (Computation.map f s)

Equations

@Computation.terminates_map = @Computation.terminates_map.proof_1

source

ink

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

Computation.Terminates (Computation.map f s) ↔ Computation.Terminates s

source

ink

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.

source

ink

instance Computation.instAlternativeComputation :

Alternative Computation

Equations

Computation.instAlternativeComputation = let src := Computation.monad; Alternative.mk Computation.empty @Computation.orElse

source

ink

@[simp]

theorem Computation.ret_orElse {α : Type u} (a : α) (c₂ : Computation α) :

(HOrElse.hOrElse (Computation.pure a) fun x => c₂) = Computation.pure a

source

ink

@[simp]

theorem Computation.orelse_pure {α : Type u} (c₁ : Computation α) (a : α) :

(HOrElse.hOrElse (Computation.think c₁) fun x => Computation.pure a) = Computation.pure a

source

ink

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

source

ink

@[simp]

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

(HOrElse.hOrElse (Computation.empty α) fun x => c) = c

source

ink

@[simp]

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

(HOrElse.hOrElse c fun x => Computation.empty α) = c

source

ink

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₂

source

ink

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

source

ink

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

Computation.Equiv s s

source

ink

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

Computation.Equiv s t → Computation.Equiv t s

source

ink

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

Computation.Equiv s t → Computation.Equiv t u → Computation.Equiv s u

source

ink

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

Equivalence Computation.Equiv

source

ink

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

Computation.Equiv s t

source

ink

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

Computation.Terminates c₁ ↔ Computation.Terminates c₂

source

ink

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

Computation.Promises c₁ a ↔ Computation.Promises c₂ a

source

ink

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

Computation.get c₁ = Computation.get c₂

source

ink

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

Computation.Equiv (Computation.think s) s

source

ink

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

Computation.Equiv (Computation.thinkN s n) s

source

ink

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)

source

ink

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

Computation.Equiv s (Computation.pure a)

source

ink

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)

source

ink

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

source

ink

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₂

source

ink

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

Reflexive (Computation.LiftRel R)

source

ink

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

Symmetric (Computation.LiftRel R)

source

ink

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

Transitive (Computation.LiftRel R)

source

ink

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

Equivalence R → Equivalence (Computation.LiftRel R)

source

ink

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

source

ink

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)

source

ink

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

source

ink

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

source

ink

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

source

ink

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

source

ink

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)

source

ink

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)

source

ink

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

source

ink

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

source

ink

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

source

ink

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

source

ink

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

source

ink

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

source

ink

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'

source

ink

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)

source

ink

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)

source

ink

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

α ⊕ Computation α → β ⊕ Computation β → Prop

Alternate defintion of LiftRel over relations between Computations

Equations

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

source

ink

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

source

ink

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

source

ink

@[simp]

theorem Computation.LiftRelAux_inr_inl :

∀ {α : Type u_1} {α_1 : Type u_2} {R : α → α_1 → Prop} {C : Computation α → Computation α_1 → Prop} {ca : Computation α} {b : α_1}, Computation.LiftRelAux R C (Sum.inr ca) (Sum.inl b) = ∃ a, a ∈ ca ∧ R a b

source

ink

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

source

ink

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

source

ink

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

source

ink

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

source

ink

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

source

ink

theorem Computation.lift_rel_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