case bisim
α : Type u
β : Type v
γ : Type w
f : α → β
s : Computation α
⊢ IsBisimulation fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = bind s (pure ∘ f) ∧ c₂ = map f s

case r
α : Type u
β : Type v
γ : Type w
f : α → β
s : Computation α
⊢ bind s (pure ∘ f) = map f s ∨ ∃ s_1, bind s (pure ∘ f) = bind s_1 (pure ∘ f) ∧ map f s = map f s_1
α : Type u
β : Type v
γ : Type w
f : α → β
s : Computation α
⊢ bind s (pure ∘ f) = map f s
apply eq_of_bisim fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = bind s (pure ∘ f) ∧ c₂ = map f s
case bisim
α : Type u
β : Type v
γ : Type w
f : α → β
s : Computation α
c₁ c₂ : Computation β
h : c₁ = c₂ ∨ ∃ s, c₁ = bind s (pure ∘ f) ∧ c₂ = map f s
⊢ BisimO (fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = bind s (pure ∘ f) ∧ c₂ = map f s) (destruct c₁) (destruct c₂)
case bisim
α : Type u
β : Type v
γ : Type w
f : α → β
s : Computation α
⊢ IsBisimulation fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = bind s (pure ∘ f) ∧ c₂ = map f s
intro c₁ c₂ h
no goals
case bisim
α : Type u
β : Type v
γ : Type w
f : α → β
s : Computation α
c₁ c₂ : Computation β
h : c₁ = c₂ ∨ ∃ s, c₁ = bind s (pure ∘ f) ∧ c₂ = map f s
⊢ BisimO (fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = bind s (pure ∘ f) ∧ c₂ = map f s) (destruct c₁) (destruct c₂)
exact
  match c₁, c₂, h with
  | _, c₂, Or.inl (Eq.refl _) => by cases' destruct c₂ with b cb <;> simp
  | _, _, Or.inr ⟨s, rfl, rfl⟩ => by
    apply recOn s <;> intro s <;> simp
    exact Or.inr ⟨s, rfl, rfl⟩
no goals
α : Type u
β : Type v
γ : Type w
f : α → β
s : Computation α
c₁ c₂✝ : Computation β
h : c₁ = c₂✝ ∨ ∃ s, c₁ = bind s (pure ∘ f) ∧ c₂✝ = map f s
c₂ : Computation β
⊢ BisimO (fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = bind s (pure ∘ f) ∧ c₂ = map f s) (destruct c₂) (destruct c₂)
cases' destruct c₂ with b cb <;> simp
case h2
α : Type u
β : Type v
γ : Type w
f : α → β
s✝¹ : Computation α
c₁ c₂ : Computation β
h : c₁ = c₂ ∨ ∃ s, c₁ = bind s (pure ∘ f) ∧ c₂ = map f s
s✝ s : Computation α
⊢ bind s (pure ∘ f) = map f s ∨ ∃ s_1, bind s (pure ∘ f) = bind s_1 (pure ∘ f) ∧ map f s = map f s_1
α : Type u
β : Type v
γ : Type w
f : α → β
s✝ : Computation α
c₁ c₂ : Computation β
h : c₁ = c₂ ∨ ∃ s, c₁ = bind s (pure ∘ f) ∧ c₂ = map f s
s : Computation α
⊢ BisimO (fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = bind s (pure ∘ f) ∧ c₂ = map f s) (destruct (bind s (pure ∘ f)))
    (destruct (map f s))
apply recOn s <;> intro s <;> simp
no goals
case h2
α : Type u
β : Type v
γ : Type w
f : α → β
s✝¹ : Computation α
c₁ c₂ : Computation β
h : c₁ = c₂ ∨ ∃ s, c₁ = bind s (pure ∘ f) ∧ c₂ = map f s
s✝ s : Computation α
⊢ bind s (pure ∘ f) = map f s ∨ ∃ s_1, bind s (pure ∘ f) = bind s_1 (pure ∘ f) ∧ map f s = map f s_1
exact Or.inr ⟨s, rfl, rfl⟩
no goals
case r
α : Type u
β : Type v
γ : Type w
f : α → β
s : Computation α
⊢ bind s (pure ∘ f) = map f s ∨ ∃ s_1, bind s (pure ∘ f) = bind s_1 (pure ∘ f) ∧ map f s = map f s_1
exact Or.inr ⟨s, rfl, rfl⟩