# Coinductive formalization of unbounded computations. #

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

def Computation (α : 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
Instances For
def Computation.pure {α : Type u} (a : α) :

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

Equations
• = ⟨,
Instances For
instance Computation.instCoeTC {α : Type u} :
CoeTC α ()
Equations
• Computation.instCoeTC = { coe := Computation.pure }
def Computation.think {α : Type u} (c : ) :

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

Equations
Instances For
def Computation.thinkN {α : Type u} (c : ) :

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

Equations
• c.thinkN 0 = c
• c.thinkN n.succ = (c.thinkN n).think
Instances For
def Computation.head {α : Type u} (c : ) :

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

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

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

Equations
• c.tail = (c).tail,
Instances For
def Computation.empty (α : Type u_1) :

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

Equations
Instances For
instance Computation.instInhabited {α : Type u} :
Equations
• Computation.instInhabited = { default := }
def Computation.runFor {α : Type u} :

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

Equations
• Computation.runFor = Subtype.val
Instances For
def Computation.destruct {α : Type u} (c : ) :
α

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

Equations
• c.destruct = match c 0 with | none => Sum.inr c.tail | some a =>
Instances For
unsafe def Computation.run {α : Type u} :
α

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

Equations
• x.run = let c := x; match c.destruct with | => a | Sum.inr ca => ca.run
Instances For
theorem Computation.destruct_eq_pure {α : Type u} {s : } {a : α} :
s.destruct =
theorem Computation.destruct_eq_think {α : Type u} {s : } {s' : } :
s.destruct = Sum.inr s's = s'.think
@[simp]
theorem Computation.destruct_pure {α : Type u} (a : α) :
().destruct =
@[simp]
theorem Computation.destruct_think {α : Type u} (s : ) :
s.think.destruct =
@[simp]
theorem Computation.destruct_empty {α : Type u} :
.destruct =
@[simp]
theorem Computation.head_pure {α : Type u} (a : α) :
@[simp]
theorem Computation.head_think {α : Type u} (s : ) :
@[simp]
theorem Computation.head_empty {α : Type u} :
@[simp]
theorem Computation.tail_pure {α : Type u} (a : α) :
().tail =
@[simp]
theorem Computation.tail_think {α : Type u} (s : ) :
s.think.tail = s
@[simp]
theorem Computation.tail_empty {α : Type u} :
.tail =
theorem Computation.think_empty {α : Type u} :
= .think
def Computation.recOn {α : Type u} {C : Sort v} (s : ) (h1 : (a : α) → C ()) (h2 : (s : ) → C s.think) :
C s

Recursion principle for computations, compare with List.recOn.

Equations
• s.recOn h1 h2 = match H : s.destruct with | => .mpr (h1 v) | => match v, H with | a, s', H => .mpr (h2 a, s')
Instances For
def Computation.Corec.f {α : Type u} {β : Type v} (f : βα β) :
α β × (α β)

Corecursor constructor for corec

Equations
• = match x with | => (some a, ) | => (match f b with | => some a | Sum.inr val => none, f b)
Instances For
def Computation.corec {α : Type u} {β : Type v} (f : βα β) (b : β) :

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
• = ⟨,
Instances For
def Computation.lmap {α : Type u} {β : Type v} {γ : Type w} (f : αβ) :
α γβ γ

left map of ⊕

Equations
• = match x with | => Sum.inl (f a) | =>
Instances For
def Computation.rmap {α : Type u} {β : Type v} {γ : Type w} (f : βγ) :
α βα γ

right map of ⊕

Equations
Instances For
@[simp]
theorem Computation.corec_eq {α : Type u} {β : Type v} (f : βα β) (b : β) :
().destruct = Computation.rmap (f b)
def Computation.BisimO {α : Type u} (R : ) :
α α Prop

Bisimilarity over a sum of Computations

Equations
Instances For
def Computation.IsBisimulation {α : Type u} (R : ) :

Attribute expressing bisimilarity over two Computations

Equations
Instances For
theorem Computation.eq_of_bisim {α : Type u} (R : ) (bisim : ) {s₁ : } {s₂ : } (r : R s₁ s₂) :
s₁ = s₂
def Computation.Mem {α : Type u} (a : α) (s : ) :

Assertion that a Computation limits to a given value

Equations
Instances For
instance Computation.instMembership {α : Type u} :
Equations
• Computation.instMembership = { mem := Computation.Mem }
theorem Computation.le_stable {α : Type u} (s : ) {a : α} {m : } {n : } (h : m n) :
s m = some as n = some a
theorem Computation.mem_unique {α : Type u} {s : } {a : α} {b : α} :
a sb sa = b
theorem Computation.Mem.left_unique {α : Type u} :
Relator.LeftUnique fun (x : α) (x_1 : ) => x x_1
class Computation.Terminates {α : Type u} (s : ) :

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

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

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

Instances
theorem Computation.Terminates.term {α : Type u} {s : } [self : s.Terminates] :
∃ (a : α), a s

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

theorem Computation.terminates_iff {α : Type u} (s : ) :
s.Terminates ∃ (a : α), a s
theorem Computation.terminates_of_mem {α : Type u} {s : } {a : α} (h : a s) :
s.Terminates
theorem Computation.terminates_def {α : Type u} (s : ) :
s.Terminates ∃ (n : ), (s n).isSome = true
theorem Computation.ret_mem {α : Type u} (a : α) :
theorem Computation.eq_of_pure_mem {α : Type u} {a : α} {a' : α} (h : ) :
a' = a
instance Computation.ret_terminates {α : Type u} (a : α) :
().Terminates
Equations
• =
theorem Computation.think_mem {α : Type u} {s : } {a : α} :
a sa s.think
instance Computation.think_terminates {α : Type u} (s : ) [s.Terminates] :
s.think.Terminates
Equations
• =
theorem Computation.of_think_mem {α : Type u} {s : } {a : α} :
a s.thinka s
theorem Computation.of_think_terminates {α : Type u} {s : } :
s.think.Terminatess.Terminates
theorem Computation.not_mem_empty {α : Type u} (a : α) :
theorem Computation.not_terminates_empty {α : Type u} :
¬.Terminates
theorem Computation.eq_empty_of_not_terminates {α : Type u} {s : } (H : ¬s.Terminates) :
theorem Computation.thinkN_mem {α : Type u} {s : } {a : α} (n : ) :
a s.thinkN n a s
instance Computation.thinkN_terminates {α : Type u} (s : ) [s.Terminates] (n : ) :
(s.thinkN n).Terminates
Equations
• =
theorem Computation.of_thinkN_terminates {α : Type u} (s : ) (n : ) :
(s.thinkN n).Terminatess.Terminates
def Computation.Promises {α : Type u} (s : ) (a : α) :

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

Equations
• s.Promises a = ∀ ⦃a' : α⦄, a' sa = a'
Instances For

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

Equations
Instances For
theorem Computation.mem_promises {α : Type u} {s : } {a : α} :
a ss.Promises a
theorem Computation.empty_promises {α : Type u} (a : α) :
.Promises a
def Computation.length {α : Type u} (s : ) [h : s.Terminates] :

length s gets the number of steps of a terminating computation

Equations
• s.length =
Instances For
def Computation.get {α : Type u} (s : ) [h : s.Terminates] :
α

get s returns the result of a terminating computation

Equations
• s.get = (s ()).get
Instances For
theorem Computation.get_mem {α : Type u} (s : ) [h : s.Terminates] :
s.get s
theorem Computation.get_eq_of_mem {α : Type u} (s : ) [h : s.Terminates] {a : α} :
a ss.get = a
theorem Computation.mem_of_get_eq {α : Type u} (s : ) [h : s.Terminates] {a : α} :
s.get = aa s
@[simp]
theorem Computation.get_think {α : Type u} (s : ) [h : s.Terminates] :
s.think.get = s.get
@[simp]
theorem Computation.get_thinkN {α : Type u} (s : ) [h : s.Terminates] (n : ) :
(s.thinkN n).get = s.get
theorem Computation.get_promises {α : Type u} (s : ) [h : s.Terminates] :
s.Promises s.get
theorem Computation.mem_of_promises {α : Type u} (s : ) [h : s.Terminates] {a : α} (p : s.Promises a) :
a s
theorem Computation.get_eq_of_promises {α : Type u} (s : ) [h : s.Terminates] {a : α} :
s.Promises as.get = a
def Computation.Results {α : Type u} (s : ) (a : α) (n : ) :

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
Instances For
theorem Computation.results_of_terminates {α : Type u} (s : ) [_T : s.Terminates] :
s.Results s.get s.length
theorem Computation.results_of_terminates' {α : Type u} (s : ) [T : s.Terminates] {a : α} (h : a s) :
s.Results a s.length
theorem Computation.Results.mem {α : Type u} {s : } {a : α} {n : } :
s.Results a na s
theorem Computation.Results.terminates {α : Type u} {s : } {a : α} {n : } (h : s.Results a n) :
s.Terminates
theorem Computation.Results.length {α : Type u} {s : } {a : α} {n : } [_T : s.Terminates] :
s.Results a ns.length = n
theorem Computation.Results.val_unique {α : Type u} {s : } {a : α} {b : α} {m : } {n : } (h1 : s.Results a m) (h2 : s.Results b n) :
a = b
theorem Computation.Results.len_unique {α : Type u} {s : } {a : α} {b : α} {m : } {n : } (h1 : s.Results a m) (h2 : s.Results b n) :
m = n
theorem Computation.exists_results_of_mem {α : Type u} {s : } {a : α} (h : a s) :
∃ (n : ), s.Results a n
@[simp]
theorem Computation.get_pure {α : Type u} (a : α) :
().get = a
@[simp]
theorem Computation.length_pure {α : Type u} (a : α) :
().length = 0
theorem Computation.results_pure {α : Type u} (a : α) :
().Results a 0
@[simp]
theorem Computation.length_think {α : Type u} (s : ) [h : s.Terminates] :
s.think.length = s.length + 1
theorem Computation.results_think {α : Type u} {s : } {a : α} {n : } (h : s.Results a n) :
s.think.Results a (n + 1)
theorem Computation.of_results_think {α : Type u} {s : } {a : α} {n : } (h : s.think.Results a n) :
∃ (m : ), s.Results a m n = m + 1
@[simp]
theorem Computation.results_think_iff {α : Type u} {s : } {a : α} {n : } :
s.think.Results a (n + 1) s.Results a n
theorem Computation.results_thinkN {α : Type u} {s : } {a : α} {m : } (n : ) :
s.Results a m(s.thinkN n).Results a (m + n)
theorem Computation.results_thinkN_pure {α : Type u} (a : α) (n : ) :
(().thinkN n).Results a n
@[simp]
theorem Computation.length_thinkN {α : Type u} (s : ) [_h : s.Terminates] (n : ) :
(s.thinkN n).length = s.length + n
theorem Computation.eq_thinkN {α : Type u} {s : } {a : α} {n : } (h : s.Results a n) :
s = ().thinkN n
theorem Computation.eq_thinkN' {α : Type u} (s : ) [_h : s.Terminates] :
s = (Computation.pure s.get).thinkN s.length
def Computation.memRecOn {α : Type u} {C : Sort v} {a : α} {s : } (M : a s) (h1 : C ()) (h2 : (s : ) → C sC s.think) :
C s

Recursor based on membership

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

Recursor based on assertion of Terminates

Equations
Instances For
def Computation.map {α : Type u} {β : Type v} (f : αβ) :

Map a function on the result of a computation.

Equations
Instances For
def Computation.Bind.g {α : Type u} {β : Type v} :
β β

bind over a Sum of Computation

Equations
Instances For
def Computation.Bind.f {α : Type u} {β : Type v} (f : α) :
β

bind over a function mapping α to a Computation

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Computation.bind {α : Type u} {β : Type v} (c : ) (f : α) :

Compose two computations into a monadic bind operation.

Equations
• c.bind f =
Instances For
theorem Computation.has_bind_eq_bind {α : Type u} {β : Type u} (c : ) (f : α) :
c >>= f = c.bind f
def Computation.join {α : Type u} (c : ) :

Flatten a computation of computations into a single computation.

Equations
Instances For
@[simp]
theorem Computation.map_pure {α : Type u} {β : Type v} (f : αβ) (a : α) :
@[simp]
theorem Computation.map_think {α : Type u} {β : Type v} (f : αβ) (s : ) :
Computation.map f s.think = ().think
@[simp]
theorem Computation.destruct_map {α : Type u} {β : Type v} (f : αβ) (s : ) :
().destruct = Computation.lmap f (Computation.rmap () s.destruct)
@[simp]
theorem Computation.map_id {α : Type u} (s : ) :
= s
theorem Computation.map_comp {α : Type u} {β : Type v} {γ : Type w} (f : αβ) (g : βγ) (s : ) :
@[simp]
theorem Computation.ret_bind {α : Type u} {β : Type v} (a : α) (f : α) :
().bind f = f a
@[simp]
theorem Computation.think_bind {α : Type u} {β : Type v} (c : ) (f : α) :
c.think.bind f = (c.bind f).think
@[simp]
theorem Computation.bind_pure {α : Type u} {β : Type v} (f : αβ) (s : ) :
s.bind (Computation.pure f) =
@[simp]
theorem Computation.bind_pure' {α : Type u} (s : ) :
s.bind Computation.pure = s
@[simp]
theorem Computation.bind_assoc {α : Type u} {β : Type v} {γ : Type w} (s : ) (f : α) (g : β) :
(s.bind f).bind g = s.bind fun (x : α) => (f x).bind g
theorem Computation.results_bind {α : Type u} {β : Type v} {s : } {f : α} {a : α} {b : β} {m : } {n : } (h1 : s.Results a m) (h2 : (f a).Results b n) :
(s.bind f).Results b (n + m)
theorem Computation.mem_bind {α : Type u} {β : Type v} {s : } {f : α} {a : α} {b : β} (h1 : a s) (h2 : b f a) :
b s.bind f
instance Computation.terminates_bind {α : Type u} {β : Type v} (s : ) (f : α) [s.Terminates] [(f s.get).Terminates] :
(s.bind f).Terminates
Equations
• =
@[simp]
theorem Computation.get_bind {α : Type u} {β : Type v} (s : ) (f : α) [s.Terminates] [(f s.get).Terminates] :
(s.bind f).get = (f s.get).get
@[simp]
theorem Computation.length_bind {α : Type u} {β : Type v} (s : ) (f : α) [_T1 : s.Terminates] [_T2 : (f s.get).Terminates] :
(s.bind f).length = (f s.get).length + s.length
theorem Computation.of_results_bind {α : Type u} {β : Type v} {s : } {f : α} {b : β} {k : } :
(s.bind f).Results b k∃ (a : α), ∃ (m : ), ∃ (n : ), s.Results a m (f a).Results b n k = n + m
theorem Computation.exists_of_mem_bind {α : Type u} {β : Type v} {s : } {f : α} {b : β} (h : b s.bind f) :
∃ (a : α), a s b f a
theorem Computation.bind_promises {α : Type u} {β : Type v} {s : } {f : α} {a : α} {b : β} (h1 : s.Promises a) (h2 : (f a).Promises b) :
(s.bind f).Promises b
Equations
Equations
theorem Computation.has_map_eq_map {α : Type u} {β : Type u} (f : αβ) (c : ) :
f <$> c = @[simp] theorem Computation.pure_def {α : Type u} (a : α) : @[simp] theorem Computation.map_pure' {α : Type u_1} {β : Type u_1} (f : αβ) (a : α) : @[simp] theorem Computation.map_think' {α : Type u_1} {β : Type u_1} (f : αβ) (s : ) : f <$> s.think = (f <\$> s).think
theorem Computation.mem_map {α : Type u} {β : Type v} (f : αβ) {a : α} {s : } (m : a s) :
f a
theorem Computation.exists_of_mem_map {α : Type u} {β : Type v} {f : αβ} {b : β} {s : } (h : b ) :
∃ (a : α), a s f a = b
instance Computation.terminates_map {α : Type u} {β : Type v} (f : αβ) (s : ) [s.Terminates] :
().Terminates
Equations
• =
theorem Computation.terminates_map_iff {α : Type u} {β : Type v} (f : αβ) (s : ) :
().Terminates s.Terminates
def Computation.orElse {α : Type u} (c₁ : ) (c₂ : ) :

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.
Instances For
Equations
@[simp]
theorem Computation.ret_orElse {α : Type u} (a : α) (c₂ : ) :
(HOrElse.hOrElse () fun (x : Unit) => c₂) =
@[simp]
theorem Computation.orElse_pure {α : Type u} (c₁ : ) (a : α) :
(HOrElse.hOrElse c₁.think fun (x : Unit) => ) =
@[simp]
theorem Computation.orElse_think {α : Type u} (c₁ : ) (c₂ : ) :
(HOrElse.hOrElse c₁.think fun (x : Unit) => c₂.think) = (HOrElse.hOrElse c₁ fun (x : Unit) => c₂).think
@[simp]
theorem Computation.empty_orElse {α : Type u} (c : ) :
(HOrElse.hOrElse fun (x : Unit) => c) = c
@[simp]
theorem Computation.orElse_empty {α : Type u} (c : ) :
(HOrElse.hOrElse c fun (x : Unit) => ) = c
def Computation.Equiv {α : Type u} (c₁ : ) (c₂ : ) :

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

Equations
• c₁.Equiv c₂ = ∀ (a : α), a c₁ a c₂
Instances For

equivalence relation for computations

Equations
Instances For
theorem Computation.Equiv.refl {α : Type u} (s : ) :
s.Equiv s
theorem Computation.Equiv.symm {α : Type u} {s : } {t : } :
s.Equiv tt.Equiv s
theorem Computation.Equiv.trans {α : Type u} {s : } {t : } {u : } :
s.Equiv tt.Equiv us.Equiv u
theorem Computation.Equiv.equivalence {α : Type u} :
Equivalence Computation.Equiv
theorem Computation.equiv_of_mem {α : Type u} {s : } {t : } {a : α} (h1 : a s) (h2 : a t) :
s.Equiv t
theorem Computation.terminates_congr {α : Type u} {c₁ : } {c₂ : } (h : c₁.Equiv c₂) :
c₁.Terminates c₂.Terminates
theorem Computation.promises_congr {α : Type u} {c₁ : } {c₂ : } (h : c₁.Equiv c₂) (a : α) :
c₁.Promises a c₂.Promises a
theorem Computation.get_equiv {α : Type u} {c₁ : } {c₂ : } (h : c₁.Equiv c₂) [c₁.Terminates] [c₂.Terminates] :
c₁.get = c₂.get
theorem Computation.think_equiv {α : Type u} (s : ) :
s.think.Equiv s
theorem Computation.thinkN_equiv {α : Type u} (s : ) (n : ) :
(s.thinkN n).Equiv s
theorem Computation.bind_congr {α : Type u} {β : Type v} {s1 : } {s2 : } {f1 : α} {f2 : α} (h1 : s1.Equiv s2) (h2 : ∀ (a : α), (f1 a).Equiv (f2 a)) :
(s1.bind f1).Equiv (s2.bind f2)
theorem Computation.equiv_pure_of_mem {α : Type u} {s : } {a : α} (h : a s) :
s.Equiv ()
def Computation.LiftRel {α : Type u} {β : Type v} (R : αβProp) (ca : ) (cb : ) :

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
Instances For
theorem Computation.LiftRel.swap {α : Type u} {β : Type v} (R : αβProp) (ca : ) (cb : ) :
theorem Computation.lift_eq_iff_equiv {α : Type u} (c₁ : ) (c₂ : ) :
Computation.LiftRel (fun (x x_1 : α) => x = x_1) c₁ c₂ c₁.Equiv c₂
theorem Computation.LiftRel.refl {α : Type u} (R : ααProp) (H : ) :
theorem Computation.LiftRel.symm {α : Type u} (R : ααProp) (H : ) :
theorem Computation.LiftRel.trans {α : Type u} (R : ααProp) (H : ) :
theorem Computation.LiftRel.equiv {α : Type u} (R : ααProp) :
theorem Computation.LiftRel.imp {α : Type u} {β : Type v} {R : αβProp} {S : αβProp} (H : ∀ {a : α} {b : β}, R a bS a b) (s : ) (t : ) :
theorem Computation.terminates_of_liftRel {α : Type u} {β : Type v} {R : αβProp} {s : } {t : } :
(s.Terminates t.Terminates)
theorem Computation.rel_of_liftRel {α : Type u} {β : Type v} {R : αβProp} {ca : } {cb : } :
Computation.LiftRel R ca cb∀ {a : α} {b : β}, a cab cbR a b
theorem Computation.liftRel_of_mem {α : Type u} {β : Type v} {R : αβProp} {a : α} {b : β} {ca : } {cb : } (ma : a ca) (mb : b cb) (ab : R a b) :
theorem Computation.exists_of_liftRel_left {α : Type u} {β : Type v} {R : αβProp} {ca : } {cb : } (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 : } {cb : } (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 : } {cb : } :
Computation.LiftRel R ca cb (ca.Terminates cb.Terminates) ∀ {a : α} {b : β}, a cab cbR a b
theorem Computation.liftRel_bind {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} (R : αβProp) (S : γδProp) {s1 : } {s2 : } {f1 : α} {f2 : β} (h1 : Computation.LiftRel R s1 s2) (h2 : ∀ {a : α} {b : β}, R a bComputation.LiftRel S (f1 a) (f2 b)) :
Computation.LiftRel S (s1.bind f1) (s2.bind f2)
@[simp]
theorem Computation.liftRel_pure_left {α : Type u} {β : Type v} (R : αβProp) (a : α) (cb : ) :
∃ (b : β), b cb R a b
@[simp]
theorem Computation.liftRel_pure_right {α : Type u} {β : Type v} (R : αβProp) (ca : ) (b : β) :
∃ (a : α), a ca R a b
@[simp]
theorem Computation.liftRel_pure {α : Type u} {β : Type v} (R : αβProp) (a : α) (b : β) :
R a b
@[simp]
theorem Computation.liftRel_think_left {α : Type u} {β : Type v} (R : αβProp) (ca : ) (cb : ) :
@[simp]
theorem Computation.liftRel_think_right {α : Type u} {β : Type v} (R : αβProp) (ca : ) (cb : ) :
theorem Computation.liftRel_mem_cases {α : Type u} {β : Type v} {R : αβProp} {ca : } {cb : } (Ha : ∀ (a : α), a caComputation.LiftRel R ca cb) (Hb : ∀ (b : β), b cbComputation.LiftRel R ca cb) :
theorem Computation.liftRel_congr {α : Type u} {β : Type v} {R : αβProp} {ca : } {ca' : } {cb : } {cb' : } (ha : ca.Equiv ca') (hb : cb.Equiv cb') :
theorem Computation.liftRel_map {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} (R : αβProp) (S : γδProp) {s1 : } {s2 : } {f1 : αγ} {f2 : βδ} (h1 : Computation.LiftRel R s1 s2) (h2 : ∀ {a : α} {b : β}, R a bS (f1 a) (f2 b)) :
theorem Computation.map_congr {α : Type u} {β : Type v} {s1 : } {s2 : } {f : αβ} (h1 : s1.Equiv s2) :
().Equiv ()
def Computation.LiftRelAux {α : Type u} {β : Type v} (R : αβProp) (C : ) :
α β Prop

Alternate definition of LiftRel over relations between Computations

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Computation.liftRelAux_inl_inl {α : Type u} {β : Type v} {R : αβProp} {C : } {a : α} {b : β} :
Computation.LiftRelAux R C () () = R a b
@[simp]
theorem Computation.liftRelAux_inl_inr {α : Type u} {β : Type v} {R : αβProp} {C : } {a : α} {cb : } :
Computation.LiftRelAux R C () (Sum.inr cb) = ∃ (b : β), b cb R a b
@[simp]
theorem Computation.liftRelAux_inr_inl {α : Type u} {β : Type v} {R : αβProp} {C : } {b : β} {ca : } :
Computation.LiftRelAux R C (Sum.inr ca) () = ∃ (a : α), a ca R a b
@[simp]
theorem Computation.liftRelAux_inr_inr {α : Type u} {β : Type v} {R : αβProp} {C : } {ca : } {cb : } :
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 : ) (a : α) (cb : ) :
Computation.LiftRelAux R C () cb.destruct ∃ (b : β), b cb R a b
theorem Computation.LiftRelAux.swap {α : Type u} {β : Type v} (R : αβProp) (C : ) (a : α ) (b : β ) :
=
@[simp]
theorem Computation.LiftRelAux.ret_right {α : Type u} {β : Type v} (R : αβProp) (C : ) (b : β) (ca : ) :
Computation.LiftRelAux R C ca.destruct () ∃ (a : α), a ca R a b
theorem Computation.LiftRelRec.lem {α : Type u} {β : Type v} {R : αβProp} (C : ) (H : ∀ {ca : } {cb : }, C ca cbComputation.LiftRelAux R C ca.destruct cb.destruct) (ca : ) (cb : ) (Hc : C ca cb) (a : α) (ha : a ca) :
theorem Computation.liftRel_rec {α : Type u} {β : Type v} {R : αβProp} (C : ) (H : ∀ {ca : } {cb : }, C ca cbComputation.LiftRelAux R C ca.destruct cb.destruct) (ca : ) (cb : ) (Hc : C ca cb) :