Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro

Coinductive formalization of unbounded computations.

! This file was ported from Lean 3 source module data.seq.computation
! leanprover-community/mathlib commit 1f0096e6caa61e9c849ec2adbd227e960e9dff58
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Stream.Init
import Mathlib.Tactic.Common

/-!
# Coinductive formalization of unbounded computations.

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

open Function

universe u v w

/-
coinductive Computation (α : Type u) : Type u
| pure : α → Computation α
| think : Computation α → Xomputation α
-/
/-- `Computation α` is the type of unbounded computations returning `α`.
An element of `Computation α` is an infinite sequence of `Option α` such
that if `f n = some a` for some `n` then it is constantly `some a` after that. -/
def Computation: Type u → Type uComputation (α: Type uα : Type u: Type (u+1)Type u) : Type u: Type (u+1)Type u :=
{ f: Stream' (Option α)f : Stream': Type ?u.9 → Type ?u.9Stream' (Option: Type ?u.10 → Type ?u.10Option α: Type uα) // ∀ ⦃n: ?m.13n a: ?m.16a⦄, f: Stream' (Option α)f n: ?m.13n = some: {α : Type ?u.21} → α → Option αsome a: ?m.16a → f: Stream' (Option α)f (n: ?m.13n + 1: ?m.581) = some: {α : Type ?u.118} → α → Option αsome a: ?m.16a }
#align computation Computation: Type u → Type uComputation

namespace Computation

variable {α: Type uα : Type u: Type (u+1)Type u} {β: Type vβ : Type v: Type (v+1)Type v} {γ: Type wγ : Type w: Type (w+1)Type w}

-- constructors
/-- `pure a` is the computation that immediately terminates with result `a`. -/
-- porting notes: `return` is reserved, so changed to `pure`
def pure: α → Computation αpure (a: αa : α: Type uα) : Computation: Type ?u.155 → Type ?u.155Computation α: Type uα :=
⟨Stream'.const: {α : Type ?u.174} → α → Stream' αStream'.const (some: {α : Type ?u.178} → α → Option αsome a: αa), fun _: ?m.183_ _: ?m.186_ => id: ∀ {α : Sort ?u.188}, α → αid⟩
#align computation.return Computation.pure: {α : Type u} → α → Computation αComputation.pure

instance: {α : Type u} → CoeTC α (Computation α)instance : CoeTC: Sort ?u.301 → Sort ?u.300 → Sort (max(max1?u.301)?u.300)CoeTC α: Type uα (Computation: Type ?u.302 → Type ?u.302Computation α: Type uα) :=
⟨pure: {α : Type ?u.313} → α → Computation αpure⟩

/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
-- note [use has_coe_t]
/-- `think c` is the computation that delays for one "tick" and then performs
computation `c`. -/
def think: {α : Type u} → Computation α → Computation αthink (c: Computation αc : Computation: Type ?u.387 → Type ?u.387Computation α: Type uα) : Computation: Type ?u.390 → Type ?u.390Computation α: Type uα :=
⟨Stream'.cons: {α : Type ?u.409} → α → Stream' α → Stream' αStream'.cons none: {α : Type ?u.413} → Option αnone c: Computation αc.1: {α : Sort ?u.416} → {p : α → Prop} → Subtype p → α1, fun n: ?m.423n a: ?m.426a h: ?m.429h => byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wc: Computation αn: ℕa: αh: Stream'.cons none (↑c) n = some aStream'.cons none (↑c) (n + 1) = some acases' n: ℕn with n: ℕnα: Type uβ: Type vγ: Type wc: Computation αa: αh: Stream'.cons none (↑c) Nat.zero = some azeroStream'.cons none (↑c) (Nat.zero + 1) = some aα: Type uβ: Type vγ: Type wc: Computation αa: αn: ℕh: Stream'.cons none (↑c) (Nat.succ n) = some asuccStream'.cons none (↑c) (Nat.succ n + 1) = some a
α: Type uβ: Type vγ: Type wc: Computation αn: ℕa: αh: Stream'.cons none (↑c) n = some aStream'.cons none (↑c) (n + 1) = some a.α: Type uβ: Type vγ: Type wc: Computation αa: αh: Stream'.cons none (↑c) Nat.zero = some azeroStream'.cons none (↑c) (Nat.zero + 1) = some a α: Type uβ: Type vγ: Type wc: Computation αa: αh: Stream'.cons none (↑c) Nat.zero = some azeroStream'.cons none (↑c) (Nat.zero + 1) = some aα: Type uβ: Type vγ: Type wc: Computation αa: αn: ℕh: Stream'.cons none (↑c) (Nat.succ n) = some asuccStream'.cons none (↑c) (Nat.succ n + 1) = some acontradictionGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wc: Computation αn: ℕa: αh: Stream'.cons none (↑c) n = some aStream'.cons none (↑c) (n + 1) = some a.α: Type uβ: Type vγ: Type wc: Computation αa: αn: ℕh: Stream'.cons none (↑c) (Nat.succ n) = some asuccStream'.cons none (↑c) (Nat.succ n + 1) = some a α: Type uβ: Type vγ: Type wc: Computation αa: αn: ℕh: Stream'.cons none (↑c) (Nat.succ n) = some asuccStream'.cons none (↑c) (Nat.succ n + 1) = some aexact c: Computation αc.2: ∀ {α : Sort ?u.505} {p : α → Prop} (self : Subtype p), p ↑self2 h: Stream'.cons none (↑c) (Nat.succ n) = some ahGoals accomplished! 🐙⟩
#align computation.think Computation.think: {α : Type u} → Computation α → Computation αComputation.think

/-- `thinkN c n` is the computation that delays for `n` ticks and then performs
computation `c`. -/
def thinkN: {α : Type u} → Computation α → ℕ → Computation αthinkN (c: Computation αc : Computation: Type ?u.643 → Type ?u.643Computation α: Type uα) : ℕ: Typeℕ → Computation: Type ?u.648 → Type ?u.648Computation α: Type uα
| 0: ℕ0 => c: Computation αc
| n: ℕn + 1 => think: {α : Type ?u.749} → Computation α → Computation αthink (thinkN: Computation α → ℕ → Computation αthinkN c: Computation αc n: ℕn)
set_option linter.uppercaseLean3 false in
#align computation.thinkN Computation.thinkN: {α : Type u} → Computation α → ℕ → Computation αComputation.thinkN

-- check for immediate result
/-- `head c` is the first step of computation, either `some a` if `c = pure a`
or `none` if `c = think c'`. -/
def head: {α : Type u} → Computation α → Option αhead (c: Computation αc : Computation: Type ?u.1040 → Type ?u.1040Computation α: Type uα) : Option: Type ?u.1043 → Type ?u.1043Option α: Type uα :=
c: Computation αc.1: {α : Sort ?u.1046} → {p : α → Prop} → Subtype p → α1.head: {α : Type ?u.1058} → Stream' α → αhead
#align computation.head Computation.head: {α : Type u} → Computation α → Option αComputation.head

-- one step of computation
/-- `tail c` is the remainder of computation, either `c` if `c = pure a`
or `c'` if `c = think c'`. -/
def tail: {α : Type u} → Computation α → Computation αtail (c: Computation αc : Computation: Type ?u.1131 → Type ?u.1131Computation α: Type uα) : Computation: Type ?u.1134 → Type ?u.1134Computation α: Type uα :=
⟨c: Computation αc.1: {α : Sort ?u.1153} → {p : α → Prop} → Subtype p → α1.tail: {α : Type ?u.1158} → Stream' α → Stream' αtail, fun _: ?m.1166_ _: ?m.1169_ h: ?m.1172h => c: Computation αc.2: ∀ {α : Sort ?u.1174} {p : α → Prop} (self : Subtype p), p ↑self2 h: ?m.1172h⟩
#align computation.tail Computation.tail: {α : Type u} → Computation α → Computation αComputation.tail

/-- `empty α` is the computation that never returns, an infinite sequence of
`think`s. -/
def empty: (α : Type ?u.1308) → Computation αempty (α: ?m.1305α) : Computation: Type ?u.1308 → Type ?u.1308Computation α: ?m.1305α :=
⟨Stream'.const: {α : Type ?u.1327} → α → Stream' αStream'.const none: {α : Type ?u.1331} → Option αnone, fun _: ?m.1336_ _: ?m.1339_ => id: ∀ {α : Sort ?u.1341}, α → αid⟩
#align computation.empty Computation.empty: (α : Type u_1) → Computation αComputation.empty

instance: {α : Type u} → Inhabited (Computation α)instance : Inhabited: Sort ?u.1435 → Sort (max1?u.1435)Inhabited (Computation: Type ?u.1436 → Type ?u.1436Computation α: Type uα) :=
⟨empty: (α : Type ?u.1443) → Computation αempty _: Type ?u.1443_⟩

/-- `run_for c n` evaluates `c` for `n` steps and returns the result, or `none`
if it did not terminate after `n` steps. -/
def runFor: Computation α → ℕ → Option αrunFor : Computation: Type ?u.1505 → Type ?u.1505Computation α: Type uα → ℕ: Typeℕ → Option: Type ?u.1509 → Type ?u.1509Option α: Type uα :=
Subtype.val: {α : Sort ?u.1511} → {p : α → Prop} → Subtype p → αSubtype.val
#align computation.run_for Computation.runFor: {α : Type u} → Computation α → ℕ → Option αComputation.runFor

/-- `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'`. -/
def destruct: Computation α → α ⊕ Computation αdestruct (c: Computation αc : Computation: Type ?u.1596 → Type ?u.1596Computation α: Type uα) : Sum: Type ?u.1600 → Type ?u.1599 → Type (max?u.1600?u.1599)Sum α: Type uα (Computation: Type ?u.1601 → Type ?u.1601Computation α: Type uα) :=
match c: Computation αc.1: {α : Sort ?u.1604} → {p : α → Prop} → Subtype p → α1 0: ?m.16160 with
| none: {α : Type ?u.1628} → Option αnone => Sum.inr: {α : Type ?u.1638} → {β : Type ?u.1637} → β → α ⊕ βSum.inr (tail: {α : Type ?u.1643} → Computation α → Computation αtail c: Computation αc)
| some: {α : Type ?u.1646} → α → Option αsome a: αa => Sum.inl: {α : Type ?u.1661} → {β : Type ?u.1660} → α → α ⊕ βSum.inl a: αa
#align computation.destruct Computation.destruct: {α : Type u} → Computation α → α ⊕ Computation αComputation.destruct

/-- `run c` is an unsound meta function that runs `c` to completion, possibly
resulting in an infinite loop in the VM. -/
unsafe def run: {α : Type u} → Computation α → αrun : Computation: Type ?u.1904 → Type ?u.1904Computation α: Type uα → α: Type uα
| c: ?m.1911c =>
match destruct: {α : Type ?u.1913} → Computation α → α ⊕ Computation αdestruct c: ?m.1911c with
| Sum.inl: {α : Type ?u.1919} → {β : Type ?u.1918} → α → α ⊕ βSum.inl a: αa => a: αa
| Sum.inr: {α : Type ?u.1939} → {β : Type ?u.1938} → β → α ⊕ βSum.inr ca: Computation αca => run: Computation α → αrun ca: Computation αca
#align computation.run Computation.run: {α : Type u} → Computation α → αComputation.run

theorem destruct_eq_pure: ∀ {s : Computation α} {a : α}, destruct s = Sum.inl a → s = pure adestruct_eq_pure {s: Computation αs : Computation: Type ?u.2155 → Type ?u.2155Computation α: Type uα} {a: αa : α: Type uα} : destruct: {α : Type ?u.2162} → Computation α → α ⊕ Computation αdestruct s: Computation αs = Sum.inl: {α : Type ?u.2167} → {β : Type ?u.2166} → α → α ⊕ βSum.inl a: αa → s: Computation αs = pure: {α : Type ?u.2205} → α → Computation αpure a: αa := byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type ws: Computation αa: αdestruct s = Sum.inl a → s = pure adsimp [destruct: {α : Type ?u.2213} → Computation α → α ⊕ Computation αdestruct]α: Type uβ: Type vγ: Type ws: Computation αa: α(match ↑s 0 with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =     Sum.inl a →
s = pure a
α: Type uβ: Type vγ: Type ws: Computation αa: αdestruct s = Sum.inl a → s = pure ainduction' f0 : s: Computation αs.1: {α : Sort ?u.2245} → {p : α → Prop} → Subtype p → α1 0: ?m.22570 with _α: Type uβ: Type vγ: Type ws: Computation αa: αx✝: Option αf0✝: ↑s 0 = x✝f0: ↑s 0 = nonenone(match none with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =     Sum.inl a →
s = pure aα: Type uβ: Type vγ: Type ws: Computation αa: αx✝: Option αf0✝: ↑s 0 = x✝val✝: αf0: ↑s 0 = some val✝some(match some val✝ with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =     Sum.inl a →
s = pure a α: Type uβ: Type vγ: Type ws: Computation αa: α(match ↑s 0 with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =     Sum.inl a →
s = pure a<;>α: Type uβ: Type vγ: Type ws: Computation αa: αx✝: Option αf0✝: ↑s 0 = x✝f0: ↑s 0 = nonenone(match none with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =     Sum.inl a →
s = pure aα: Type uβ: Type vγ: Type ws: Computation αa: αx✝: Option αf0✝: ↑s 0 = x✝val✝: αf0: ↑s 0 = some val✝some(match some val✝ with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =     Sum.inl a →
s = pure a α: Type uβ: Type vγ: Type ws: Computation αa: α(match ↑s 0 with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =     Sum.inl a →
s = pure aintro h: (match none with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =   Sum.inl ahα: Type uβ: Type vγ: Type ws: Computation αa: αx✝: Option αf0✝: ↑s 0 = x✝f0: ↑s 0 = noneh: (match none with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =   Sum.inl anones = pure a
α: Type uβ: Type vγ: Type ws: Computation αa: αdestruct s = Sum.inl a → s = pure a·α: Type uβ: Type vγ: Type ws: Computation αa: αx✝: Option αf0✝: ↑s 0 = x✝f0: ↑s 0 = noneh: (match none with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =   Sum.inl anones = pure a α: Type uβ: Type vγ: Type ws: Computation αa: αx✝: Option αf0✝: ↑s 0 = x✝f0: ↑s 0 = noneh: (match none with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =   Sum.inl anones = pure aα: Type uβ: Type vγ: Type ws: Computation αa: αx✝: Option αf0✝: ↑s 0 = x✝val✝: αf0: ↑s 0 = some val✝h: (match some val✝ with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =   Sum.inl asomes = pure acontradictionGoals accomplished! 🐙
α: Type uβ: Type vγ: Type ws: Computation αa: αdestruct s = Sum.inl a → s = pure a·α: Type uβ: Type vγ: Type ws: Computation αa: αx✝: Option αf0✝: ↑s 0 = x✝val✝: αf0: ↑s 0 = some val✝h: (match some val✝ with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =   Sum.inl asomes = pure a α: Type uβ: Type vγ: Type ws: Computation αa: αx✝: Option αf0✝: ↑s 0 = x✝val✝: αf0: ↑s 0 = some val✝h: (match some val✝ with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =   Sum.inl asomes = pure aapply Subtype.eq: ∀ {α : Type ?u.2324} {p : α → Prop} {a1 a2 : { x // p x }}, ↑a1 = ↑a2 → a1 = a2Subtype.eqα: Type uβ: Type vγ: Type ws: Computation αa: αx✝: Option αf0✝: ↑s 0 = x✝val✝: αf0: ↑s 0 = some val✝h: (match some val✝ with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =   Sum.inl asome.a↑s = ↑(pure a)
α: Type uβ: Type vγ: Type ws: Computation αa: αx✝: Option αf0✝: ↑s 0 = x✝val✝: αf0: ↑s 0 = some val✝h: (match some val✝ with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =   Sum.inl asomes = pure afunext n: ?αnα: Type uβ: Type vγ: Type ws: Computation αa: αx✝: Option αf0✝: ↑s 0 = x✝val✝: αf0: ↑s 0 = some val✝h: (match some val✝ with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =   Sum.inl an: ℕsome.a.h↑s n = ↑(pure a) n
α: Type uβ: Type vγ: Type ws: Computation αa: αx✝: Option αf0✝: ↑s 0 = x✝val✝: αf0: ↑s 0 = some val✝h: (match some val✝ with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =   Sum.inl asomes = pure ainduction' n: ?αn with n: ℕn IH: ?m.2380 nIHα: Type uβ: Type vγ: Type ws: Computation αa: αx✝: Option αf0✝: ↑s 0 = x✝val✝: αf0: ↑s 0 = some val✝h: (match some val✝ with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =   Sum.inl asome.a.h.zero↑s Nat.zero = ↑(pure a) Nat.zeroα: Type uβ: Type vγ: Type ws: Computation αa: αx✝: Option αf0✝: ↑s 0 = x✝val✝: αf0: ↑s 0 = some val✝h: (match some val✝ with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =   Sum.inl an: ℕIH: ↑s n = ↑(pure a) nsome.a.h.succ↑s (Nat.succ n) = ↑(pure a) (Nat.succ n)
α: Type uβ: Type vγ: Type ws: Computation αa: αx✝: Option αf0✝: ↑s 0 = x✝val✝: αf0: ↑s 0 = some val✝h: (match some val✝ with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =   Sum.inl asomes = pure a·α: Type uβ: Type vγ: Type ws: Computation αa: αx✝: Option αf0✝: ↑s 0 = x✝val✝: αf0: ↑s 0 = some val✝h: (match some val✝ with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =   Sum.inl asome.a.h.zero↑s Nat.zero = ↑(pure a) Nat.zero α: Type uβ: Type vγ: Type ws: Computation αa: αx✝: Option αf0✝: ↑s 0 = x✝val✝: αf0: ↑s 0 = some val✝h: (match some val✝ with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =   Sum.inl asome.a.h.zero↑s Nat.zero = ↑(pure a) Nat.zeroα: Type uβ: Type vγ: Type ws: Computation αa: αx✝: Option αf0✝: ↑s 0 = x✝val✝: αf0: ↑s 0 = some val✝h: (match some val✝ with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =   Sum.inl an: ℕIH: ↑s n = ↑(pure a) nsome.a.h.succ↑s (Nat.succ n) = ↑(pure a) (Nat.succ n)injection h: (match some val✝ with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =   Sum.inl ah with h'α: Type uβ: Type vγ: Type ws: Computation αa: αx✝: Option αf0✝: ↑s 0 = x✝val✝: αf0: ↑s 0 = some val✝h': val✝ = asome.a.h.zero↑s Nat.zero = ↑(pure a) Nat.zero
α: Type uβ: Type vγ: Type ws: Computation αa: αx✝: Option αf0✝: ↑s 0 = x✝val✝: αf0: ↑s 0 = some val✝h: (match some val✝ with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =   Sum.inl asome.a.h.zero↑s Nat.zero = ↑(pure a) Nat.zerorwa [α: Type uβ: Type vγ: Type ws: Computation αa: αx✝: Option αf0✝: ↑s 0 = x✝val✝: αf0: ↑s 0 = some val✝h': val✝ = asome.a.h.zero↑s Nat.zero = ↑(pure a) Nat.zeroh': val✝ = ah'α: Type uβ: Type vγ: Type ws: Computation αa: αx✝: Option αf0✝: ↑s 0 = x✝val✝: αf0: ↑s 0 = some ah': val✝ = asome.a.h.zero↑s Nat.zero = ↑(pure a) Nat.zero]α: Type uβ: Type vγ: Type ws: Computation αa: αx✝: Option αf0✝: ↑s 0 = x✝val✝: αf0: ↑s 0 = some ah': val✝ = asome.a.h.zero↑s Nat.zero = ↑(pure a) Nat.zero at f0: ↑s 0 = some val✝f0Goals accomplished! 🐙
α: Type uβ: Type vγ: Type ws: Computation αa: αx✝: Option αf0✝: ↑s 0 = x✝val✝: αf0: ↑s 0 = some val✝h: (match some val✝ with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =   Sum.inl asomes = pure a·α: Type uβ: Type vγ: Type ws: Computation αa: αx✝: Option αf0✝: ↑s 0 = x✝val✝: αf0: ↑s 0 = some val✝h: (match some val✝ with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =   Sum.inl an: ℕIH: ↑s n = ↑(pure a) nsome.a.h.succ↑s (Nat.succ n) = ↑(pure a) (Nat.succ n) α: Type uβ: Type vγ: Type ws: Computation αa: αx✝: Option αf0✝: ↑s 0 = x✝val✝: αf0: ↑s 0 = some val✝h: (match some val✝ with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =   Sum.inl an: ℕIH: ↑s n = ↑(pure a) nsome.a.h.succ↑s (Nat.succ n) = ↑(pure a) (Nat.succ n)exact s: Computation αs.2: ∀ {α : Sort ?u.2444} {p : α → Prop} (self : Subtype p), p ↑self2 IH: ?m.2380 nIHGoals accomplished! 🐙
#align computation.destruct_eq_ret Computation.destruct_eq_pure: ∀ {α : Type u} {s : Computation α} {a : α}, destruct s = Sum.inl a → s = pure aComputation.destruct_eq_pure

theorem destruct_eq_think: ∀ {s s' : Computation α}, destruct s = Sum.inr s' → s = think s'destruct_eq_think {s: Computation αs : Computation: Type ?u.2491 → Type ?u.2491Computation α: Type uα} {s': ?m.2494s'} : destruct: {α : Type ?u.2499} → Computation α → α ⊕ Computation αdestruct s: Computation αs = Sum.inr: {α : Type ?u.2504} → {β : Type ?u.2503} → β → α ⊕ βSum.inr s': ?m.2494s' → s: Computation αs = think: {α : Type ?u.2542} → Computation α → Computation αthink s': ?m.2494s' := byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type ws, s': Computation αdestruct s = Sum.inr s' → s = think s'dsimp [destruct: {α : Type ?u.2551} → Computation α → α ⊕ Computation αdestruct]α: Type uβ: Type vγ: Type ws, s': Computation α(match ↑s 0 with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =     Sum.inr s' →
s = think s'
α: Type uβ: Type vγ: Type ws, s': Computation αdestruct s = Sum.inr s' → s = think s'induction' f0 : s: Computation αs.1: {α : Sort ?u.2583} → {p : α → Prop} → Subtype p → α1 0: ?m.25950 with a': ?m.2636a'α: Type uβ: Type vγ: Type ws, s': Computation αx✝: Option αf0✝: ↑s 0 = x✝f0: ↑s 0 = nonenone(match none with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =     Sum.inr s' →
s = think s'α: Type uβ: Type vγ: Type ws, s': Computation αx✝: Option αf0✝: ↑s 0 = x✝a': αf0: ↑s 0 = some a'some(match some a' with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =     Sum.inr s' →
s = think s' α: Type uβ: Type vγ: Type ws, s': Computation α(match ↑s 0 with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =     Sum.inr s' →
s = think s'<;>α: Type uβ: Type vγ: Type ws, s': Computation αx✝: Option αf0✝: ↑s 0 = x✝f0: ↑s 0 = nonenone(match none with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =     Sum.inr s' →
s = think s'α: Type uβ: Type vγ: Type ws, s': Computation αx✝: Option αf0✝: ↑s 0 = x✝a': αf0: ↑s 0 = some a'some(match some a' with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =     Sum.inr s' →
s = think s' α: Type uβ: Type vγ: Type ws, s': Computation α(match ↑s 0 with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =     Sum.inr s' →
s = think s'intro h: (match none with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =   Sum.inr s'hα: Type uβ: Type vγ: Type ws, s': Computation αx✝: Option αf0✝: ↑s 0 = x✝f0: ↑s 0 = noneh: (match none with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =   Sum.inr s'nones = think s'
α: Type uβ: Type vγ: Type ws, s': Computation αdestruct s = Sum.inr s' → s = think s'·α: Type uβ: Type vγ: Type ws, s': Computation αx✝: Option αf0✝: ↑s 0 = x✝f0: ↑s 0 = noneh: (match none with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =   Sum.inr s'nones = think s' α: Type uβ: Type vγ: Type ws, s': Computation αx✝: Option αf0✝: ↑s 0 = x✝f0: ↑s 0 = noneh: (match none with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =   Sum.inr s'nones = think s'α: Type uβ: Type vγ: Type ws, s': Computation αx✝: Option αf0✝: ↑s 0 = x✝a': αf0: ↑s 0 = some a'h: (match some a' with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =   Sum.inr s'somes = think s'injection h: (match none with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =   Sum.inr s'h with h'α: Type uβ: Type vγ: Type ws, s': Computation αx✝: Option αf0✝: ↑s 0 = x✝f0: ↑s 0 = noneh': tail s = s'nones = think s'
α: Type uβ: Type vγ: Type ws, s': Computation αx✝: Option αf0✝: ↑s 0 = x✝f0: ↑s 0 = noneh: (match none with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =   Sum.inr s'nones = think s'rw [α: Type uβ: Type vγ: Type ws, s': Computation αx✝: Option αf0✝: ↑s 0 = x✝f0: ↑s 0 = noneh': tail s = s'nones = think s'← h': tail s = s'h'α: Type uβ: Type vγ: Type ws, s': Computation αx✝: Option αf0✝: ↑s 0 = x✝f0: ↑s 0 = noneh': tail s = s'nones = think (tail s)]α: Type uβ: Type vγ: Type ws, s': Computation αx✝: Option αf0✝: ↑s 0 = x✝f0: ↑s 0 = noneh': tail s = s'nones = think (tail s)
α: Type uβ: Type vγ: Type ws, s': Computation αx✝: Option αf0✝: ↑s 0 = x✝f0: ↑s 0 = noneh: (match none with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =   Sum.inr s'nones = think s'cases' s: Computation αs with f: ?m.2721f al: ?m.2722 falα: Type uβ: Type vγ: Type ws': Computation αx✝: Option αf: Stream' (Option α)al: ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some af0✝: ↑{ val := f, property := al } 0 = x✝f0: ↑{ val := f, property := al } 0 = noneh': tail { val := f, property := al } = s'none.mk{ val := f, property := al } = think (tail { val := f, property := al })
α: Type uβ: Type vγ: Type ws, s': Computation αx✝: Option αf0✝: ↑s 0 = x✝f0: ↑s 0 = noneh: (match none with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =   Sum.inr s'nones = think s'apply Subtype.eq: ∀ {α : Type ?u.2759} {p : α → Prop} {a1 a2 : { x // p x }}, ↑a1 = ↑a2 → a1 = a2Subtype.eqα: Type uβ: Type vγ: Type ws': Computation αx✝: Option αf: Stream' (Option α)al: ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some af0✝: ↑{ val := f, property := al } 0 = x✝f0: ↑{ val := f, property := al } 0 = noneh': tail { val := f, property := al } = s'none.mk.a↑{ val := f, property := al } = ↑(think (tail { val := f, property := al }))
α: Type uβ: Type vγ: Type ws, s': Computation αx✝: Option αf0✝: ↑s 0 = x✝f0: ↑s 0 = noneh: (match none with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =   Sum.inr s'nones = think s'dsimp [think: {α : Type ?u.2782} → Computation α → Computation αthink, tail: {α : Type ?u.2784} → Computation α → Computation αtail]α: Type uβ: Type vγ: Type ws': Computation αx✝: Option αf: Stream' (Option α)al: ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some af0✝: ↑{ val := f, property := al } 0 = x✝f0: ↑{ val := f, property := al } 0 = noneh': tail { val := f, property := al } = s'none.mk.af = Stream'.cons none (Stream'.tail f)
α: Type uβ: Type vγ: Type ws, s': Computation αx✝: Option αf0✝: ↑s 0 = x✝f0: ↑s 0 = noneh: (match none with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =   Sum.inr s'nones = think s'rw [α: Type uβ: Type vγ: Type ws': Computation αx✝: Option αf: Stream' (Option α)al: ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some af0✝: ↑{ val := f, property := al } 0 = x✝f0: ↑{ val := f, property := al } 0 = noneh': tail { val := f, property := al } = s'none.mk.af = Stream'.cons none (Stream'.tail f)← f0: ↑{ val := f, property := al } 0 = nonef0α: Type uβ: Type vγ: Type ws': Computation αx✝: Option αf: Stream' (Option α)al: ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some af0✝: ↑{ val := f, property := al } 0 = x✝f0: ↑{ val := f, property := al } 0 = noneh': tail { val := f, property := al } = s'none.mk.af = Stream'.cons (↑{ val := f, property := al } 0) (Stream'.tail f)]α: Type uβ: Type vγ: Type ws': Computation αx✝: Option αf: Stream' (Option α)al: ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some af0✝: ↑{ val := f, property := al } 0 = x✝f0: ↑{ val := f, property := al } 0 = noneh': tail { val := f, property := al } = s'none.mk.af = Stream'.cons (↑{ val := f, property := al } 0) (Stream'.tail f)
α: Type uβ: Type vγ: Type ws, s': Computation αx✝: Option αf0✝: ↑s 0 = x✝f0: ↑s 0 = noneh: (match none with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =   Sum.inr s'nones = think s'exact (Stream'.eta: ∀ {α : Type ?u.2822} (s : Stream' α), Stream'.cons (Stream'.head s) (Stream'.tail s) = sStream'.eta f: ?m.2721f).symm: ∀ {α : Sort ?u.2827} {a b : α}, a = b → b = asymmGoals accomplished! 🐙
α: Type uβ: Type vγ: Type ws, s': Computation αdestruct s = Sum.inr s' → s = think s'·α: Type uβ: Type vγ: Type ws, s': Computation αx✝: Option αf0✝: ↑s 0 = x✝a': αf0: ↑s 0 = some a'h: (match some a' with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =   Sum.inr s'somes = think s' α: Type uβ: Type vγ: Type ws, s': Computation αx✝: Option αf0✝: ↑s 0 = x✝a': αf0: ↑s 0 = some a'h: (match some a' with
| none => Sum.inr (tail s)
| some a => Sum.inl a) =   Sum.inr s'somes = think s'contradictionGoals accomplished! 🐙
#align computation.destruct_eq_think Computation.destruct_eq_think: ∀ {α : Type u} {s s' : Computation α}, destruct s = Sum.inr s' → s = think s'Computation.destruct_eq_think

@[simp]
theorem destruct_pure: ∀ {α : Type u} (a : α), destruct (pure a) = Sum.inl adestruct_pure (a: αa : α: Type uα) : destruct: {α : Type ?u.2892} → Computation α → α ⊕ Computation αdestruct (pure: {α : Type ?u.2894} → α → Computation αpure a: αa) = Sum.inl: {α : Type ?u.2899} → {β : Type ?u.2898} → α → α ⊕ βSum.inl a: αa :=
rfl: ∀ {α : Sort ?u.2937} {a : α}, a = arfl
#align computation.destruct_ret Computation.destruct_pure: ∀ {α : Type u} (a : α), destruct (pure a) = Sum.inl aComputation.destruct_pure

@[simp]
theorem destruct_think: ∀ {α : Type u} (s : Computation α), destruct (think s) = Sum.inr sdestruct_think : ∀ s: Computation αs : Computation: Type ?u.2970 → Type ?u.2970Computation α: Type uα, destruct: {α : Type ?u.2974} → Computation α → α ⊕ Computation αdestruct (think: {α : Type ?u.2976} → Computation α → Computation αthink s: Computation αs) = Sum.inr: {α : Type ?u.2982} → {β : Type ?u.2981} → β → α ⊕ βSum.inr s: Computation αs
| ⟨_, _⟩ => rfl: ∀ {α : Sort ?u.3078} {a : α}, a = arfl
#align computation.destruct_think Computation.destruct_think: ∀ {α : Type u} (s : Computation α), destruct (think s) = Sum.inr sComputation.destruct_think

@[simp]
theorem destruct_empty: destruct (empty α) = Sum.inr (empty α)destruct_empty : destruct: {α : Type ?u.3250} → Computation α → α ⊕ Computation αdestruct (empty: (α : Type ?u.3252) → Computation αempty α: Type uα) = Sum.inr: {α : Type ?u.3256} → {β : Type ?u.3255} → β → α ⊕ βSum.inr (empty: (α : Type ?u.3259) → Computation αempty α: Type uα) :=
rfl: ∀ {α : Sort ?u.3294} {a : α}, a = arfl
#align computation.destruct_empty Computation.destruct_empty: ∀ {α : Type u}, destruct (empty α) = Sum.inr (empty α)Computation.destruct_empty

@[simp]
theorem head_pure: ∀ (a : α), head (pure a) = some ahead_pure (a: αa : α: Type uα) : head: {α : Type ?u.3335} → Computation α → Option αhead (pure: {α : Type ?u.3337} → α → Computation αpure a: αa) = some: {α : Type ?u.3341} → α → Option αsome a: αa :=
rfl: ∀ {α : Sort ?u.3347} {a : α}, a = arfl
#align computation.head_ret Computation.head_pure: ∀ {α : Type u} (a : α), head (pure a) = some aComputation.head_pure

@[simp]
theorem head_think: ∀ (s : Computation α), head (think s) = nonehead_think (s: Computation αs : Computation: Type ?u.3370 → Type ?u.3370Computation α: Type uα) : head: {α : Type ?u.3374} → Computation α → Option αhead (think: {α : Type ?u.3376} → Computation α → Computation αthink s: Computation αs) = none: {α : Type ?u.3381} → Option αnone :=
rfl: ∀ {α : Sort ?u.3414} {a : α}, a = arfl
#align computation.head_think Computation.head_think: ∀ {α : Type u} (s : Computation α), head (think s) = noneComputation.head_think

@[simp]
theorem head_empty: ∀ {α : Type u}, head (empty α) = nonehead_empty : head: {α : Type ?u.3446} → Computation α → Option αhead (empty: (α : Type ?u.3448) → Computation αempty α: Type uα) = none: {α : Type ?u.3451} → Option αnone :=
rfl: ∀ {α : Sort ?u.3483} {a : α}, a = arfl

@[simp]
theorem tail_pure: ∀ (a : α), tail (pure a) = pure atail_pure (a: αa : α: Type uα) : tail: {α : Type ?u.3505} → Computation α → Computation αtail (pure: {α : Type ?u.3507} → α → Computation αpure a: αa) = pure: {α : Type ?u.3511} → α → Computation αpure a: αa :=
rfl: ∀ {α : Sort ?u.3516} {a : α}, a = arfl
#align computation.tail_ret Computation.tail_pure: ∀ {α : Type u} (a : α), tail (pure a) = pure aComputation.tail_pure

@[simp]
theorem tail_think: ∀ {α : Type u} (s : Computation α), tail (think s) = stail_think (s: Computation αs : Computation: Type ?u.3546 → Type ?u.3546Computation α: Type uα) : tail: {α : Type ?u.3550} → Computation α → Computation αtail (think: {α : Type ?u.3552} → Computation α → Computation αthink s: Computation αs) = s: Computation αs := byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type ws: Computation αtail (think s) = scases' s: Computation αs with f: ?m.3586f al: ?m.3587 falα: Type uβ: Type vγ: Type wf: Stream' (Option α)al: ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some amktail (think { val := f, property := al }) = { val := f, property := al } α: Type uβ: Type vγ: Type ws: Computation αtail (think s) = s;α: Type uβ: Type vγ: Type wf: Stream' (Option α)al: ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some amktail (think { val := f, property := al }) = { val := f, property := al } α: Type uβ: Type vγ: Type ws: Computation αtail (think s) = sapply Subtype.eq: ∀ {α : Type ?u.3619} {p : α → Prop} {a1 a2 : { x // p x }}, ↑a1 = ↑a2 → a1 = a2Subtype.eqα: Type uβ: Type vγ: Type wf: Stream' (Option α)al: ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some amk.a↑(tail (think { val := f, property := al })) = ↑{ val := f, property := al } α: Type uβ: Type vγ: Type ws: Computation αtail (think s) = s;α: Type uβ: Type vγ: Type wf: Stream' (Option α)al: ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some amk.a↑(tail (think { val := f, property := al })) = ↑{ val := f, property := al } α: Type uβ: Type vγ: Type ws: Computation αtail (think s) = sdsimp [tail: {α : Type ?u.3642} → Computation α → Computation αtail, think: {α : Type ?u.3644} → Computation α → Computation αthink]Goals accomplished! 🐙
#align computation.tail_think Computation.tail_think: ∀ {α : Type u} (s : Computation α), tail (think s) = sComputation.tail_think

@[simp]
theorem tail_empty: ∀ {α : Type u}, tail (empty α) = empty αtail_empty : tail: {α : Type ?u.3711} → Computation α → Computation αtail (empty: (α : Type ?u.3713) → Computation αempty α: Type uα) = empty: (α : Type ?u.3716) → Computation αempty α: Type uα :=
rfl: ∀ {α : Sort ?u.3719} {a : α}, a = arfl
#align computation.tail_empty Computation.tail_empty: ∀ {α : Type u}, tail (empty α) = empty αComputation.tail_empty

theorem think_empty: empty α = think (empty α)think_empty : empty: (α : Type ?u.3746) → Computation αempty α: Type uα = think: {α : Type ?u.3747} → Computation α → Computation αthink (empty: (α : Type ?u.3749) → Computation αempty α: Type uα) :=
destruct_eq_think: ∀ {α : Type ?u.3754} {s s' : Computation α}, destruct s = Sum.inr s' → s = think s'destruct_eq_think destruct_empty: ∀ {α : Type ?u.3764}, destruct (empty α) = Sum.inr (empty α)destruct_empty
#align computation.think_empty Computation.think_empty: ∀ {α : Type u}, empty α = think (empty α)Computation.think_empty

/-- Recursion principle for computations, compare with `List.recOn`. -/
def recOn: {α : Type u} →
{C : Computation α → Sort v} →
(s : Computation α) → ((a : α) → C (pure a)) → ((s : Computation α) → C (think s)) → C srecOn {C: Computation α → Sort vC : Computation: Type ?u.3783 → Type ?u.3783Computation α: Type uα → Sort v: Type vSortSort v: Type v v} (s: Computation αs : Computation: Type ?u.3787 → Type ?u.3787Computation α: Type uα) (h1: (a : α) → C (pure a)h1 : ∀ a: ?m.3791a, C: Computation α → Sort vC (pure: {α : Type ?u.3794} → α → Computation αpure a: ?m.3791a))
(h2: (s : Computation α) → C (think s)h2 : ∀ s: ?m.3800s, C: Computation α → Sort vC (think: {α : Type ?u.3803} → Computation α → Computation αthink s: ?m.3800s)) : C: Computation α → Sort vC s: Computation αs :=
match H: destruct s = Sum.inr vH: (destruct: {α : Type ?u.3812} → Computation α → α ⊕ Computation αdestruct s: Computation αs) with
| Sum.inl: {α : Type ?u.3817} → {β : Type ?u.3816} → α → α ⊕ βSum.inl v: αv => byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wC: Computation α → Sort vs: Computation αh1: (a : α) → C (pure a)h2: (s : Computation α) → C (think s)v: αH: destruct s = Sum.inl vC srw [α: Type uβ: Type vγ: Type wC: Computation α → Sort vs: Computation αh1: (a : α) → C (pure a)h2: (s : Computation α) → C (think s)v: αH: destruct s = Sum.inl vC sdestruct_eq_pure: ∀ {α : Type ?u.4143} {s : Computation α} {a : α}, destruct s = Sum.inl a → s = pure adestruct_eq_pure H: destruct s = Sum.inl vHα: Type uβ: Type vγ: Type wC: Computation α → Sort vs: Computation αh1: (a : α) → C (pure a)h2: (s : Computation α) → C (think s)v: αH: destruct s = Sum.inl vC (pure v)]α: Type uβ: Type vγ: Type wC: Computation α → Sort vs: Computation αh1: (a : α) → C (pure a)h2: (s : Computation α) → C (think s)v: αH: destruct s = Sum.inl vC (pure v)
α: Type uβ: Type vγ: Type wC: Computation α → Sort vs: Computation αh1: (a : α) → C (pure a)h2: (s : Computation α) → C (think s)v: αH: destruct s = Sum.inl vC sapply h1: (a : α) → C (pure a)h1Goals accomplished! 🐙
| Sum.inr: {α : Type ?u.3840} → {β : Type ?u.3839} → β → α ⊕ βSum.inr v: Computation αv => match v: Computation αv with
| ⟨a: Stream' (Option α)a, s': ∀ ⦃n : ℕ⦄ ⦃a_1 : α⦄, a n = some a_1 → a (n + 1) = some a_1s'⟩ => byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wC: Computation α → Sort vs: Computation αh1: (a : α) → C (pure a)h2: (s : Computation α) → C (think s)v: Computation αa: Stream' (Option α)s': ∀ ⦃n : ℕ⦄ ⦃a_1 : α⦄, a n = some a_1 → a (n + 1) = some a_1H: destruct s = Sum.inr { val := a, property := s' }C srw [α: Type uβ: Type vγ: Type wC: Computation α → Sort vs: Computation αh1: (a : α) → C (pure a)h2: (s : Computation α) → C (think s)v: Computation αa: Stream' (Option α)s': ∀ ⦃n : ℕ⦄ ⦃a_1 : α⦄, a n = some a_1 → a (n + 1) = some a_1H: destruct s = Sum.inr { val := a, property := s' }C sdestruct_eq_think: ∀ {α : Type ?u.4173} {s s' : Computation α}, destruct s = Sum.inr s' → s = think s'destruct_eq_think H: destruct s = Sum.inr { val := a, property := s' }Hα: Type uβ: Type vγ: Type wC: Computation α → Sort vs: Computation αh1: (a : α) → C (pure a)h2: (s : Computation α) → C (think s)v: Computation αa: Stream' (Option α)s': ∀ ⦃n : ℕ⦄ ⦃a_1 : α⦄, a n = some a_1 → a (n + 1) = some a_1H: destruct s = Sum.inr { val := a, property := s' }C (think { val := a, property := s' })]α: Type uβ: Type vγ: Type wC: Computation α → Sort vs: Computation αh1: (a : α) → C (pure a)h2: (s : Computation α) → C (think s)v: Computation αa: Stream' (Option α)s': ∀ ⦃n : ℕ⦄ ⦃a_1 : α⦄, a n = some a_1 → a (n + 1) = some a_1H: destruct s = Sum.inr { val := a, property := s' }C (think { val := a, property := s' })
α: Type uβ: Type vγ: Type wC: Computation α → Sort vs: Computation αh1: (a : α) → C (pure a)h2: (s : Computation α) → C (think s)v: Computation αa: Stream' (Option α)s': ∀ ⦃n : ℕ⦄ ⦃a_1 : α⦄, a n = some a_1 → a (n + 1) = some a_1H: destruct s = Sum.inr { val := a, property := s' }C sapply h2: (s : Computation α) → C (think s)h2Goals accomplished! 🐙
#align computation.rec_on Computation.recOn: {α : Type u} →
{C : Computation α → Sort v} →
(s : Computation α) → ((a : α) → C (pure a)) → ((s : Computation α) → C (think s)) → C sComputation.recOn

/-- Corecursor constructor for `corec`-/
def Corec.f: {α : Type u} → {β : Type v} → (β → α ⊕ β) → α ⊕ β → Option α × (α ⊕ β)Corec.f (f: β → α ⊕ βf : β: Type vβ → Sum: Type ?u.4622 → Type ?u.4621 → Type (max?u.4622?u.4621)Sum α: Type uα β: Type vβ) : Sum: Type ?u.4627 → Type ?u.4626 → Type (max?u.4627?u.4626)Sum α: Type uα β: Type vβ → Option: Type ?u.4631 → Type ?u.4631Option α: Type uα × Sum: Type ?u.4633 → Type ?u.4632 → Type (max?u.4633?u.4632)Sum α: Type uα β: Type vβ
| Sum.inl: {α : Type ?u.4640} → {β : Type ?u.4639} → α → α ⊕ βSum.inl a: αa => (some: {α : Type ?u.4665} → α → Option αsome a: αa, Sum.inl: {α : Type ?u.4669} → {β : Type ?u.4668} → α → α ⊕ βSum.inl a: αa)
| Sum.inr: {α : Type ?u.4675} → {β : Type ?u.4674} → β → α ⊕ βSum.inr b: βb =>
(match f: β → α ⊕ βf b: βb with
| Sum.inl: {α : Type ?u.4698} → {β : Type ?u.4697} → α → α ⊕ βSum.inl a: αa => some: {α : Type ?u.4715} → α → Option αsome a: αa
| Sum.inr: {α : Type ?u.4718} → {β : Type ?u.4717} → β → α ⊕ βSum.inr _ => none: {α : Type ?u.4736} → Option αnone,
f: β → α ⊕ βf b: βb)
set_option linter.uppercaseLean3 false in
#align computation.corec.F Computation.Corec.f: {α : Type u} → {β : Type v} → (β → α ⊕ β) → α ⊕ β → Option α × (α ⊕ β)Computation.Corec.f

/-- `corec f b` is the corecursor for `Computation α` as a coinductive type.
If `f b = inl a` then `corec f b = pure a`, and if `f b = inl b'` then
`corec f b = think (corec f b')`. -/
def corec: {α : Type u} → {β : Type v} → (β → α ⊕ β) → β → Computation αcorec (f: β → α ⊕ βf : β: Type vβ → Sum: Type ?u.5089 → Type ?u.5088 → Type (max?u.5089?u.5088)Sum α: Type uα β: Type vβ) (b: βb : β: Type vβ) : Computation: Type ?u.5094 → Type ?u.5094Computation α: Type uα := byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βComputation αrefine' ⟨Stream'.corec': {α : Type ?u.5118} → {β : Type ?u.5117} → (α → β × α) → α → Stream' βStream'.corec' (Corec.f: {α : Type ?u.5124} → {β : Type ?u.5123} → (β → α ⊕ β) → α ⊕ β → Option α × (α ⊕ β)Corec.f f: β → α ⊕ βf) (Sum.inr: {α : Type ?u.5143} → {β : Type ?u.5142} → β → α ⊕ βSum.inr b: βb), fun n: ?m.5148n a': ?m.5151a' h: ?m.5154h => _: Stream'.corec' (Corec.f f) (Sum.inr b) (n + 1) = some a'_⟩α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βn: ℕa': αh: Stream'.corec' (Corec.f f) (Sum.inr b) n = some a'Stream'.corec' (Corec.f f) (Sum.inr b) (n + 1) = some a'
α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βComputation αrw [α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βn: ℕa': αh: Stream'.corec' (Corec.f f) (Sum.inr b) n = some a'Stream'.corec' (Corec.f f) (Sum.inr b) (n + 1) = some a'Stream'.corec'_eq: ∀ {α : Type ?u.5168} {β : Type ?u.5167} (f : α → β × α) (a : α),
Stream'.corec' f a = Stream'.cons (f a).fst (Stream'.corec' f (f a).snd)Stream'.corec'_eqα: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βn: ℕa': αh: Stream'.corec' (Corec.f f) (Sum.inr b) n = some a'Stream'.cons (Corec.f f (Sum.inr b)).fst (Stream'.corec' (Corec.f f) (Corec.f f (Sum.inr b)).snd) (n + 1) = some a']α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βn: ℕa': αh: Stream'.corec' (Corec.f f) (Sum.inr b) n = some a'Stream'.cons (Corec.f f (Sum.inr b)).fst (Stream'.corec' (Corec.f f) (Corec.f f (Sum.inr b)).snd) (n + 1) = some a'
α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βComputation αchange Stream'.corec': {α : Type ?u.5203} → {β : Type ?u.5202} → (α → β × α) → α → Stream' βStream'.corec' (Corec.f: {α : Type ?u.5207} → {β : Type ?u.5206} → (β → α ⊕ β) → α ⊕ β → Option α × (α ⊕ β)Corec.f f: β → α ⊕ βf) (Corec.f: {α : Type ?u.5223} → {β : Type ?u.5222} → (β → α ⊕ β) → α ⊕ β → Option α × (α ⊕ β)Corec.f f: β → α ⊕ βf (Sum.inr: {α : Type ?u.5232} → {β : Type ?u.5231} → β → α ⊕ βSum.inr b: βb)).2: {α : Type ?u.5236} → {β : Type ?u.5235} → α × β → β2 n: ?m.5148n = some: {α : Type ?u.5239} → α → Option αsome a': ?m.5151a'α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βn: ℕa': αh: Stream'.corec' (Corec.f f) (Sum.inr b) n = some a'Stream'.corec' (Corec.f f) (Corec.f f (Sum.inr b)).snd n = some a'
α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βComputation αrevert h: ?m.5154hα: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βn: ℕa': αStream'.corec' (Corec.f f) (Sum.inr b) n = some a' → Stream'.corec' (Corec.f f) (Corec.f f (Sum.inr b)).snd n = some a';α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βn: ℕa': αStream'.corec' (Corec.f f) (Sum.inr b) n = some a' → Stream'.corec' (Corec.f f) (Corec.f f (Sum.inr b)).snd n = some a' α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βComputation αgeneralize Sum.inr: {α : Type ?u.5294} → {β : Type ?u.5293} → β → α ⊕ βSum.inr b: βb = oα: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βn: ℕa': αo: α ⊕ βStream'.corec' (Corec.f f) o n = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd n = some a';α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βn: ℕa': αo: α ⊕ βStream'.corec' (Corec.f f) o n = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd n = some a' α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βComputation αrevert o: ?m.5295 ⊕ βoα: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βn: ℕa': α∀ (o : α ⊕ β), Stream'.corec' (Corec.f f) o n = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd n = some a'
α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βComputation αinduction' n: ?m.5148n with n: ℕn IH: ?m.5323 nIHα: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βa': αzero∀ (o : α ⊕ β),
Stream'.corec' (Corec.f f) o Nat.zero = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd Nat.zero = some a'α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βa': αn: ℕIH: ∀ (o : α ⊕ β), Stream'.corec' (Corec.f f) o n = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd n = some a'succ∀ (o : α ⊕ β),
Stream'.corec' (Corec.f f) o (Nat.succ n) = some a' →
Stream'.corec' (Corec.f f) (Corec.f f o).snd (Nat.succ n) = some a' α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βn: ℕa': α∀ (o : α ⊕ β), Stream'.corec' (Corec.f f) o n = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd n = some a'<;>α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βa': αzero∀ (o : α ⊕ β),
Stream'.corec' (Corec.f f) o Nat.zero = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd Nat.zero = some a'α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βa': αn: ℕIH: ∀ (o : α ⊕ β), Stream'.corec' (Corec.f f) o n = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd n = some a'succ∀ (o : α ⊕ β),
Stream'.corec' (Corec.f f) o (Nat.succ n) = some a' →
Stream'.corec' (Corec.f f) (Corec.f f o).snd (Nat.succ n) = some a' α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βn: ℕa': α∀ (o : α ⊕ β), Stream'.corec' (Corec.f f) o n = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd n = some a'intro o: α ⊕ βoα: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βa': αo: α ⊕ βzeroStream'.corec' (Corec.f f) o Nat.zero = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd Nat.zero = some a'
α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βComputation α·α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βa': αo: α ⊕ βzeroStream'.corec' (Corec.f f) o Nat.zero = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd Nat.zero = some a' α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βa': αo: α ⊕ βzeroStream'.corec' (Corec.f f) o Nat.zero = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd Nat.zero = some a'α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βa': αn: ℕIH: ∀ (o : α ⊕ β), Stream'.corec' (Corec.f f) o n = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd n = some a'o: α ⊕ βsuccStream'.corec' (Corec.f f) o (Nat.succ n) = some a' →
Stream'.corec' (Corec.f f) (Corec.f f o).snd (Nat.succ n) = some a'change (Corec.f: {α : Type ?u.5346} → {β : Type ?u.5345} → (β → α ⊕ β) → α ⊕ β → Option α × (α ⊕ β)Corec.f f: β → α ⊕ βf o: α ⊕ βo).1: {α : Type ?u.5355} → {β : Type ?u.5354} → α × β → α1 = some: {α : Type ?u.5358} → α → Option αsome a': ?m.5151a' → (Corec.f: {α : Type ?u.5364} → {β : Type ?u.5363} → (β → α ⊕ β) → α ⊕ β → Option α × (α ⊕ β)Corec.f f: β → α ⊕ βf (Corec.f: {α : Type ?u.5373} → {β : Type ?u.5372} → (β → α ⊕ β) → α ⊕ β → Option α × (α ⊕ β)Corec.f f: β → α ⊕ βf o: α ⊕ βo).2: {α : Type ?u.5382} → {β : Type ?u.5381} → α × β → β2).1: {α : Type ?u.5386} → {β : Type ?u.5385} → α × β → α1 = some: {α : Type ?u.5389} → α → Option αsome a': ?m.5151a'α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βa': αo: α ⊕ βzero(Corec.f f o).fst = some a' → (Corec.f f (Corec.f f o).snd).fst = some a'
α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βa': αo: α ⊕ βzeroStream'.corec' (Corec.f f) o Nat.zero = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd Nat.zero = some a'cases' o: α ⊕ βo with _ b: ?m.5521bα: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βa', val✝: αzero.inl(Corec.f f (Sum.inl val✝)).fst = some a' → (Corec.f f (Corec.f f (Sum.inl val✝)).snd).fst = some a'α: Type uβ: Type vγ: Type wf: β → α ⊕ βb✝: βa': αb: βzero.inr(Corec.f f (Sum.inr b)).fst = some a' → (Corec.f f (Corec.f f (Sum.inr b)).snd).fst = some a' α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βa': αo: α ⊕ βzero(Corec.f f o).fst = some a' → (Corec.f f (Corec.f f o).snd).fst = some a'<;>α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βa', val✝: αzero.inl(Corec.f f (Sum.inl val✝)).fst = some a' → (Corec.f f (Corec.f f (Sum.inl val✝)).snd).fst = some a'α: Type uβ: Type vγ: Type wf: β → α ⊕ βb✝: βa': αb: βzero.inr(Corec.f f (Sum.inr b)).fst = some a' → (Corec.f f (Corec.f f (Sum.inr b)).snd).fst = some a' α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βa': αo: α ⊕ βzero(Corec.f f o).fst = some a' → (Corec.f f (Corec.f f o).snd).fst = some a'intro h: (Corec.f f (Sum.inr b)).fst = some a'hα: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βa', val✝: αh: (Corec.f f (Sum.inl val✝)).fst = some a'zero.inl(Corec.f f (Corec.f f (Sum.inl val✝)).snd).fst = some a'
α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βa': αo: α ⊕ βzeroStream'.corec' (Corec.f f) o Nat.zero = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd Nat.zero = some a'·α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βa', val✝: αh: (Corec.f f (Sum.inl val✝)).fst = some a'zero.inl(Corec.f f (Corec.f f (Sum.inl val✝)).snd).fst = some a' α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βa', val✝: αh: (Corec.f f (Sum.inl val✝)).fst = some a'zero.inl(Corec.f f (Corec.f f (Sum.inl val✝)).snd).fst = some a'α: Type uβ: Type vγ: Type wf: β → α ⊕ βb✝: βa': αb: βh: (Corec.f f (Sum.inr b)).fst = some a'zero.inr(Corec.f f (Corec.f f (Sum.inr b)).snd).fst = some a'exact h: (Corec.f f (Sum.inl val✝)).fst = some a'hGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βa': αo: α ⊕ βzeroStream'.corec' (Corec.f f) o Nat.zero = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd Nat.zero = some a'unfold Corec.f: {α : Type u} → {β : Type v} → (β → α ⊕ β) → α ⊕ β → Option α × (α ⊕ β)Corec.f at *α: Type uβ: Type vγ: Type wf: β → α ⊕ βb✝: βa': αb: βh: (match Sum.inr b 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)).fst =   some a'zero.inr(match
(match Sum.inr b 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)).snd 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)).fst =   some a';α: Type uβ: Type vγ: Type wf: β → α ⊕ βb✝: βa': αb: βh: (match Sum.inr b 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)).fst =   some a'zero.inr(match
(match Sum.inr b 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)).snd 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)).fst =   some a' α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βa': αo: α ⊕ βzeroStream'.corec' (Corec.f f) o Nat.zero = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd Nat.zero = some a'splitα: Type uβ: Type vγ: Type wf: β → α ⊕ βb✝: βa': αb: βh: (match Sum.inr b 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)).fst =   some a'x✝: α ⊕ βa✝: αheq✝: (match Sum.inr b 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)).snd =   Sum.inl a✝zero.inr.h_1(some a✝, Sum.inl a✝).fst = some a'α: Type uβ: Type vγ: Type wf: β → α ⊕ βb✝: βa': αb: βh: (match Sum.inr b 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)).fst =   some a'x✝: α ⊕ βval✝: βheq✝: (match Sum.inr b 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)).snd =   Sum.inr val✝zero.inr.h_2(match f val✝ with
| Sum.inl a => some a
| Sum.inr val => none,
f val✝).fst =   some a' α: Type uβ: Type vγ: Type wf: β → α ⊕ βb✝: βa': αb: βh: (match Sum.inr b 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)).fst =   some a'zero.inr(match
(match Sum.inr b 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)).snd 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)).fst =   some a'<;>α: Type uβ: Type vγ: Type wf: β → α ⊕ βb✝: βa': αb: βh: (match Sum.inr b 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)).fst =   some a'x✝: α ⊕ βa✝: αheq✝: (match Sum.inr b 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)).snd =   Sum.inl a✝zero.inr.h_1(some a✝, Sum.inl a✝).fst = some a'α: Type uβ: Type vγ: Type wf: β → α ⊕ βb✝: βa': αb: βh: (match Sum.inr b 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)).fst =   some a'x✝: α ⊕ βval✝: βheq✝: (match Sum.inr b 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)).snd =   Sum.inr val✝zero.inr.h_2(match f val✝ with
| Sum.inl a => some a
| Sum.inr val => none,
f val✝).fst =   some a' α: Type uβ: Type vγ: Type wf: β → α ⊕ βb✝: βa': αb: βh: (match Sum.inr b 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)).fst =   some a'zero.inr(match
(match Sum.inr b 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)).snd 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)).fst =   some a'simp_allGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βComputation α·α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βa': αn: ℕIH: ∀ (o : α ⊕ β), Stream'.corec' (Corec.f f) o n = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd n = some a'o: α ⊕ βsuccStream'.corec' (Corec.f f) o (Nat.succ n) = some a' →
Stream'.corec' (Corec.f f) (Corec.f f o).snd (Nat.succ n) = some a' α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βa': αn: ℕIH: ∀ (o : α ⊕ β), Stream'.corec' (Corec.f f) o n = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd n = some a'o: α ⊕ βsuccStream'.corec' (Corec.f f) o (Nat.succ n) = some a' →
Stream'.corec' (Corec.f f) (Corec.f f o).snd (Nat.succ n) = some a'rw [α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βa': αn: ℕIH: ∀ (o : α ⊕ β), Stream'.corec' (Corec.f f) o n = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd n = some a'o: α ⊕ βsuccStream'.corec' (Corec.f f) o (Nat.succ n) = some a' →
Stream'.corec' (Corec.f f) (Corec.f f o).snd (Nat.succ n) = some a'Stream'.corec'_eq: ∀ {α : Type ?u.7579} {β : Type ?u.7578} (f : α → β × α) (a : α),
Stream'.corec' f a = Stream'.cons (f a).fst (Stream'.corec' f (f a).snd)Stream'.corec'_eq (Corec.f: {α : Type ?u.7583} → {β : Type ?u.7582} → (β → α ⊕ β) → α ⊕ β → Option α × (α ⊕ β)Corec.f f: β → α ⊕ βf) (Corec.f: {α : Type ?u.7603} → {β : Type ?u.7602} → (β → α ⊕ β) → α ⊕ β → Option α × (α ⊕ β)Corec.f f: β → α ⊕ βf o: α ⊕ βo).2: {α : Type ?u.7612} → {β : Type ?u.7611} → α × β → β2,α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βa': αn: ℕIH: ∀ (o : α ⊕ β), Stream'.corec' (Corec.f f) o n = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd n = some a'o: α ⊕ βsuccStream'.corec' (Corec.f f) o (Nat.succ n) = some a' →
Stream'.cons (Corec.f f (Corec.f f o).snd).fst (Stream'.corec' (Corec.f f) (Corec.f f (Corec.f f o).snd).snd)
(Nat.succ n) =     some a' α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βa': αn: ℕIH: ∀ (o : α ⊕ β), Stream'.corec' (Corec.f f) o n = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd n = some a'o: α ⊕ βsuccStream'.corec' (Corec.f f) o (Nat.succ n) = some a' →
Stream'.corec' (Corec.f f) (Corec.f f o).snd (Nat.succ n) = some a'Stream'.corec'_eq: ∀ {α : Type ?u.7628} {β : Type ?u.7627} (f : α → β × α) (a : α),
Stream'.corec' f a = Stream'.cons (f a).fst (Stream'.corec' f (f a).snd)Stream'.corec'_eq (Corec.f: {α : Type ?u.7632} → {β : Type ?u.7631} → (β → α ⊕ β) → α ⊕ β → Option α × (α ⊕ β)Corec.f f: β → α ⊕ βf) o: α ⊕ βoα: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βa': αn: ℕIH: ∀ (o : α ⊕ β), Stream'.corec' (Corec.f f) o n = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd n = some a'o: α ⊕ βsuccStream'.cons (Corec.f f o).fst (Stream'.corec' (Corec.f f) (Corec.f f o).snd) (Nat.succ n) = some a' →
Stream'.cons (Corec.f f (Corec.f f o).snd).fst (Stream'.corec' (Corec.f f) (Corec.f f (Corec.f f o).snd).snd)
(Nat.succ n) =     some a']α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βa': αn: ℕIH: ∀ (o : α ⊕ β), Stream'.corec' (Corec.f f) o n = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd n = some a'o: α ⊕ βsuccStream'.cons (Corec.f f o).fst (Stream'.corec' (Corec.f f) (Corec.f f o).snd) (Nat.succ n) = some a' →
Stream'.cons (Corec.f f (Corec.f f o).snd).fst (Stream'.corec' (Corec.f f) (Corec.f f (Corec.f f o).snd).snd)
(Nat.succ n) =     some a'
α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βa': αn: ℕIH: ∀ (o : α ⊕ β), Stream'.corec' (Corec.f f) o n = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd n = some a'o: α ⊕ βsuccStream'.corec' (Corec.f f) o (Nat.succ n) = some a' →
Stream'.corec' (Corec.f f) (Corec.f f o).snd (Nat.succ n) = some a'exact IH: ?m.5323 nIH (Corec.f: {α : Type ?u.7660} → {β : Type ?u.7659} → (β → α ⊕ β) → α ⊕ β → Option α × (α ⊕ β)Corec.f f: β → α ⊕ βf o: α ⊕ βo).2: {α : Type ?u.7669} → {β : Type ?u.7668} → α × β → β2Goals accomplished! 🐙
#align computation.corec Computation.corec: {α : Type u} → {β : Type v} → (β → α ⊕ β) → β → Computation αComputation.corec

/-- left map of `⊕` -/
def lmap: {α : Type u} → {β : Type v} → {γ : Type w} → (α → β) → α ⊕ γ → β ⊕ γlmap (f: α → βf : α: Type uα → β: Type vβ) : Sum: Type ?u.7866 → Type ?u.7865 → Type (max?u.7866?u.7865)Sum α: Type uα γ: Type wγ → Sum: Type ?u.7869 → Type ?u.7868 → Type (max?u.7869?u.7868)Sum β: Type vβ γ: Type wγ
| Sum.inl: {α : Type ?u.7876} → {β : Type ?u.7875} → α → α ⊕ βSum.inl a: αa => Sum.inl: {α : Type ?u.7896} → {β : Type ?u.7895} → α → α ⊕ βSum.inl (f: α → βf a: αa)
| Sum.inr: {α : Type ?u.7902} → {β : Type ?u.7901} → β → α ⊕ βSum.inr b: γb => Sum.inr: {α : Type ?u.7920} → {β : Type ?u.7919} → β → α ⊕ βSum.inr b: γb
#align computation.lmap Computation.lmap: {α : Type u} → {β : Type v} → {γ : Type w} → (α → β) → α ⊕ γ → β ⊕ γComputation.lmap

/-- right map of `⊕` -/
def rmap: (β → γ) → α ⊕ β → α ⊕ γrmap (f: β → γf : β: Type vβ → γ: Type wγ) : Sum: Type ?u.8106 → Type ?u.8105 → Type (max?u.8106?u.8105)Sum α: Type uα β: Type vβ → Sum: Type ?u.8109 → Type ?u.8108 → Type (max?u.8109?u.8108)Sum α: Type uα γ: Type wγ
| Sum.inl: {α : Type ?u.8116} → {β : Type ?u.8115} → α → α ⊕ βSum.inl a: αa => Sum.inl: {α : Type ?u.8136} → {β : Type ?u.8135} → α → α ⊕ βSum.inl a: αa
| Sum.inr: {α : Type ?u.8142} → {β : Type ?u.8141} → β → α ⊕ βSum.inr b: βb => Sum.inr: {α : Type ?u.8160} → {β : Type ?u.8159} → β → α ⊕ βSum.inr (f: β → γf b: βb)
#align computation.rmap Computation.rmap: {α : Type u} → {β : Type v} → {γ : Type w} → (β → γ) → α ⊕ β → α ⊕ γComputation.rmap

attribute [simp] lmap: {α : Type u} → {β : Type v} → {γ : Type w} → (α → β) → α ⊕ γ → β ⊕ γlmap rmap: {α : Type u} → {β : Type v} → {γ : Type w} → (β → γ) → α ⊕ β → α ⊕ γrmap

-- porting note: this was far less painful in mathlib3. There seem to be two issues;
-- firstly, in mathlib3 we have `corec.F._match_1` and it's the obvious map α ⊕ β → option α.
-- In mathlib4 we have `Corec.f.match_1` and it's something completely different.
-- Secondly, the proof that `Stream'.corec' (Corec.f f) (Sum.inr b) 0` is this function
-- evaluated at `f b`, used to be `rfl` and now is `cases, rfl`.
@[simp]
theorem corec_eq: ∀ {α : Type u} {β : Type v} (f : β → α ⊕ β) (b : β), destruct (corec f b) = rmap (corec f) (f b)corec_eq (f: β → α ⊕ βf : β: Type vβ → Sum: Type ?u.8343 → Type ?u.8342 → Type (max?u.8343?u.8342)Sum α: Type uα β: Type vβ) (b: βb : β: Type vβ) : destruct: {α : Type ?u.8349} → Computation α → α ⊕ Computation αdestruct (corec: {α : Type ?u.8352} → {β : Type ?u.8351} → (β → α ⊕ β) → β → Computation αcorec f: β → α ⊕ βf b: βb) = rmap: {α : Type ?u.8366} → {β : Type ?u.8365} → {γ : Type ?u.8364} → (β → γ) → α ⊕ β → α ⊕ γrmap (corec: {α : Type ?u.8371} → {β : Type ?u.8370} → (β → α ⊕ β) → β → Computation αcorec f: β → α ⊕ βf) (f: β → α ⊕ βf b: βb) := byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βdestruct (corec f b) = rmap (corec f) (f b)dsimp [corec: {α : Type ?u.8395} → {β : Type ?u.8394} → (β → α ⊕ β) → β → Computation αcorec, destruct: {α : Type ?u.8397} → Computation α → α ⊕ Computation αdestruct]α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: β(match Stream'.corec' (Corec.f f) (Sum.inr b) 0 with
| none =>
Sum.inr
(tail
{ val := Stream'.corec' (Corec.f f) (Sum.inr b),
property :=
(_ :
∀ (n : ℕ) (a' : α),
Stream'.corec' (Corec.f f) (Sum.inr b) n = some a' →
Stream'.corec' (Corec.f f) (Sum.inr b) (n + 1) = some a') })
| some a => Sum.inl a) =   match f b with
| Sum.inl a => Sum.inl a
| Sum.inr b =>
Sum.inr
{ val := Stream'.corec' (Corec.f f) (Sum.inr b),
property :=
(_ :
∀ (n : ℕ) (a' : α),
Stream'.corec' (Corec.f f) (Sum.inr b) n = some a' →
Stream'.corec' (Corec.f f) (Sum.inr b) (n + 1) = some a') }
α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βdestruct (corec f b) = rmap (corec f) (f b)rw [α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: β(match Stream'.corec' (Corec.f f) (Sum.inr b) 0 with
| none =>
Sum.inr
(tail
{ val := Stream'.corec' (Corec.f f) (Sum.inr b),
property :=
(_ :
∀ (n : ℕ) (a' : α),
Stream'.corec' (Corec.f f) (Sum.inr b) n = some a' →
Stream'.corec' (Corec.f f) (Sum.inr b) (n + 1) = some a') })
| some a => Sum.inl a) =   match f b with
| Sum.inl a => Sum.inl a
| Sum.inr b =>
Sum.inr
{ val := Stream'.corec' (Corec.f f) (Sum.inr b),
property :=
(_ :
∀ (n : ℕ) (a' : α),
Stream'.corec' (Corec.f f) (Sum.inr b) n = some a' →
Stream'.corec' (Corec.f f) (Sum.inr b) (n + 1) = some a') }show Stream'.corec': {α : Type ?u.8475} → {β : Type ?u.8474} → (α → β × α) → α → Stream' βStream'.corec' (Corec.f: {α : Type ?u.8479} → {β : Type ?u.8478} → (β → α ⊕ β) → α ⊕ β → Option α × (α ⊕ β)Corec.f f: β → α ⊕ βf) (Sum.inr: {α : Type ?u.8497} → {β : Type ?u.8496} → β → α ⊕ βSum.inr b: βb) 0: ?m.85010 =
Sum.rec: {α : Type ?u.8552} →
{β : Type ?u.8551} →
{motive : α ⊕ β → Sort ?u.8553} →
((val : α) → motive (Sum.inl val)) → ((val : β) → motive (Sum.inr val)) → (t : α ⊕ β) → motive tSum.rec Option.some: {α : Type ?u.8584} → α → Option αOption.some (λ _: ?m.8591_ => none: {α : Type ?u.8593} → Option αnone) (f: β → α ⊕ βf b: βb) by
α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: β(match Stream'.corec' (Corec.f f) (Sum.inr b) 0 with
| none =>
Sum.inr
(tail
{ val := Stream'.corec' (Corec.f f) (Sum.inr b),
property :=
(_ :
∀ (n : ℕ) (a' : α),
Stream'.corec' (Corec.f f) (Sum.inr b) n = some a' →
Stream'.corec' (Corec.f f) (Sum.inr b) (n + 1) = some a') })
| some a => Sum.inl a) =   match f b with
| Sum.inl a => Sum.inl a
| Sum.inr b =>
Sum.inr
{ val := Stream'.corec' (Corec.f f) (Sum.inr b),
property :=
(_ :
∀ (n : ℕ) (a' : α),
Stream'.corec' (Corec.f f) (Sum.inr b) n = some a' →
Stream'.corec' (Corec.f f) (Sum.inr b) (n + 1) = some a') }dsimp [Corec.f: {α : Type ?u.8624} → {β : Type ?u.8623} → (β → α ⊕ β) → α ⊕ β → Option α × (α ⊕ β)Corec.f, Stream'.corec': {α : Type ?u.8627} → {β : Type ?u.8626} → (α → β × α) → α → Stream' βStream'.corec', Stream'.corec: {α : Type ?u.8630} → {β : Type ?u.8629} → (α → β) → (α → α) → α → Stream' βStream'.corec, Stream'.map: {α : Type ?u.8633} → {β : Type ?u.8632} → (α → β) → Stream' α → Stream' βStream'.map, Stream'.nth: {α : Type ?u.8635} → Stream' α → ℕ → αStream'.nth, Stream'.iterate: {α : Type ?u.8640} → (α → α) → α → Stream' αStream'.iterate]α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: β(match f b with
| Sum.inl a => some a
| Sum.inr val => none) =   Sum.rec some (fun x => none) (f b)
α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βStream'.corec' (Corec.f f) (Sum.inr b) 0 = Sum.rec some (fun x => none) (f b)match (f: β → α ⊕ βf b: βb) with
α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: β(match f b with
| Sum.inl a => some a
| Sum.inr val => none) =   Sum.rec some (fun x => none) (f b)| Sum.inl: {α : Type ?u.8753} → {β : Type ?u.8752} → α → α ⊕ βSum.inl x: αx =>α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βx: α(match Sum.inl x with
| Sum.inl a => some a
| Sum.inr val => none) =   Sum.rec some (fun x => none) (Sum.inl x) α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: β(match f b with
| Sum.inl a => some a
| Sum.inr val => none) =   Sum.rec some (fun x => none) (f b)rflGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: β(match f b with
| Sum.inl a => some a
| Sum.inr val => none) =   Sum.rec some (fun x => none) (f b)| Sum.inr: {α : Type ?u.8784} → {β : Type ?u.8783} → β → α ⊕ βSum.inr x: βx =>α: Type uβ: Type vγ: Type wf: β → α ⊕ βb, x: β(match Sum.inr x with
| Sum.inl a => some a
| Sum.inr val => none) =   Sum.rec some (fun x => none) (Sum.inr x) α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: β(match f b with
| Sum.inl a => some a
| Sum.inr val => none) =   Sum.rec some (fun x => none) (f b)rflGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: β(match Stream'.corec' (Corec.f f) (Sum.inr b) 0 with
| none =>
Sum.inr
(tail
{ val := Stream'.corec' (Corec.f f) (Sum.inr b),
property :=
(_ :
∀ (n : ℕ) (a' : α),
Stream'.corec' (Corec.f f) (Sum.inr b) n = some a' →
Stream'.corec' (Corec.f f) (Sum.inr b) (n + 1) = some a') })
| some a => Sum.inl a) =   match f b with
| Sum.inl a => Sum.inl a
| Sum.inr b =>
Sum.inr
{ val := Stream'.corec' (Corec.f f) (Sum.inr b),
property :=
(_ :
∀ (n : ℕ) (a' : α),
Stream'.corec' (Corec.f f) (Sum.inr b) n = some a' →
Stream'.corec' (Corec.f f) (Sum.inr b) (n + 1) = some a') }]α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: β(match Sum.rec some (fun x => none) (f b) with
| none =>
Sum.inr
(tail
{ val := Stream'.corec' (Corec.f f) (Sum.inr b),
property :=
(_ :
∀ (n : ℕ) (a' : α),
Stream'.corec' (Corec.f f) (Sum.inr b) n = some a' →
Stream'.corec' (Corec.f f) (Sum.inr b) (n + 1) = some a') })
| some a => Sum.inl a) =   match f b with
| Sum.inl a => Sum.inl a
| Sum.inr b =>
Sum.inr
{ val := Stream'.corec' (Corec.f f) (Sum.inr b),
property :=
(_ :
∀ (n : ℕ) (a' : α),
Stream'.corec' (Corec.f f) (Sum.inr b) n = some a' →
Stream'.corec' (Corec.f f) (Sum.inr b) (n + 1) = some a') }
α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βdestruct (corec f b) = rmap (corec f) (f b)induction' h : f: β → α ⊕ βf b: βb with a: ?m.8983a b': ?m.8984b'α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βx✝: α ⊕ βh✝: f b = x✝a: αh: f b = Sum.inl ainl(match Sum.rec some (fun x => none) (Sum.inl a) with
| none =>
Sum.inr
(tail
{ val := Stream'.corec' (Corec.f f) (Sum.inr b),
property :=
(_ :
∀ (n : ℕ) (a' : α),
Stream'.corec' (Corec.f f) (Sum.inr b) n = some a' →
Stream'.corec' (Corec.f f) (Sum.inr b) (n + 1) = some a') })
| some a => Sum.inl a) =   match Sum.inl a with
| Sum.inl a => Sum.inl a
| Sum.inr b =>
Sum.inr
{ val := Stream'.corec' (Corec.f f) (Sum.inr b),
property :=
(_ :
∀ (n : ℕ) (a' : α),
Stream'.corec' (Corec.f f) (Sum.inr b) n = some a' →
Stream'.corec' (Corec.f f) (Sum.inr b) (n + 1) = some a') }α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βx✝: α ⊕ βh✝: f b = x✝b': βh: f b = Sum.inr b'inr(match Sum.rec some (fun x => none) (Sum.inr b') with
| none =>
Sum.inr
(tail
{ val := Stream'.corec' (Corec.f f) (Sum.inr b),
property :=
(_ :
∀ (n : ℕ) (a' : α),
Stream'.corec' (Corec.f f) (Sum.inr b) n = some a' →
Stream'.corec' (Corec.f f) (Sum.inr b) (n + 1) = some a') })
| some a => Sum.inl a) =   match Sum.inr b' with
| Sum.inl a => Sum.inl a
| Sum.inr b =>
Sum.inr
{ val := Stream'.corec' (Corec.f f) (Sum.inr b),
property :=
(_ :
∀ (n : ℕ) (a' : α),
Stream'.corec' (Corec.f f) (Sum.inr b) n = some a' →
Stream'.corec' (Corec.f f) (Sum.inr b) (n + 1) = some a') };α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βx✝: α ⊕ βh✝: f b = x✝a: αh: f b = Sum.inl ainl(match Sum.rec some (fun x => none) (Sum.inl a) with
| none =>
Sum.inr
(tail
{ val := Stream'.corec' (Corec.f f) (Sum.inr b),
property :=
(_ :
∀ (n : ℕ) (a' : α),
Stream'.corec' (Corec.f f) (Sum.inr b) n = some a' →
Stream'.corec' (Corec.f f) (Sum.inr b) (n + 1) = some a') })
| some a => Sum.inl a) =   match Sum.inl a with
| Sum.inl a => Sum.inl a
| Sum.inr b =>
Sum.inr
{ val := Stream'.corec' (Corec.f f) (Sum.inr b),
property :=
(_ :
∀ (n : ℕ) (a' : α),
Stream'.corec' (Corec.f f) (Sum.inr b) n = some a' →
Stream'.corec' (Corec.f f) (Sum.inr b) (n + 1) = some a') }α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βx✝: α ⊕ βh✝: f b = x✝b': βh: f b = Sum.inr b'inr(match Sum.rec some (fun x => none) (Sum.inr b') with
| none =>
Sum.inr
(tail
{ val := Stream'.corec' (Corec.f f) (Sum.inr b),
property :=
(_ :
∀ (n : ℕ) (a' : α),
Stream'.corec' (Corec.f f) (Sum.inr b) n = some a' →
Stream'.corec' (Corec.f f) (Sum.inr b) (n + 1) = some a') })
| some a => Sum.inl a) =   match Sum.inr b' with
| Sum.inl a => Sum.inl a
| Sum.inr b =>
Sum.inr
{ val := Stream'.corec' (Corec.f f) (Sum.inr b),
property :=
(_ :
∀ (n : ℕ) (a' : α),
Stream'.corec' (Corec.f f) (Sum.inr b) n = some a' →
Stream'.corec' (Corec.f f) (Sum.inr b) (n + 1) = some a') } α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βdestruct (corec f b) = rmap (corec f) (f b)·α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βx✝: α ⊕ βh✝: f b = x✝a: αh: f b = Sum.inl ainl(match Sum.rec some (fun x => none) (Sum.inl a) with
| none =>
Sum.inr
(tail
{ val := Stream'.corec' (Corec.f f) (Sum.inr b),
property :=
(_ :
∀ (n : ℕ) (a' : α),
Stream'.corec' (Corec.f f) (Sum.inr b) n = some a' →
Stream'.corec' (Corec.f f) (Sum.inr b) (n + 1) = some a') })
| some a => Sum.inl a) =   match Sum.inl a with
| Sum.inl a => Sum.inl a
| Sum.inr b =>
Sum.inr
{ val := Stream'.corec' (Corec.f f) (Sum.inr b),
property :=
(_ :
∀ (n : ℕ) (a' : α),
Stream'.corec' (Corec.f f) (Sum.inr b) n = some a' →
Stream'.corec' (Corec.f f) (Sum.inr b) (n + 1) = some a') } α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βx✝: α ⊕ βh✝: f b = x✝a: αh: f b = Sum.inl ainl(match Sum.rec some (fun x => none) (Sum.inl a) with
| none =>
Sum.inr
(tail
{ val := Stream'.corec' (Corec.f f) (Sum.inr b),
property :=
(_ :
∀ (n : ℕ) (a' : α),
Stream'.corec' (Corec.f f) (Sum.inr b) n = some a' →
Stream'.corec' (Corec.f f) (Sum.inr b) (n + 1) = some a') })
| some a => Sum.inl a) =   match Sum.inl a with
| Sum.inl a => Sum.inl a
| Sum.inr b =>
Sum.inr
{ val := Stream'.corec' (Corec.f f) (Sum.inr b),
property :=
(_ :
∀ (n : ℕ) (a' : α),
Stream'.corec' (Corec.f f) (Sum.inr b) n = some a' →
Stream'.corec' (Corec.f f) (Sum.inr b) (n + 1) = some a') }α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βx✝: α ⊕ βh✝: f b = x✝b': βh: f b = Sum.inr b'inr(match Sum.rec some (fun x => none) (Sum.inr b') with
| none =>
Sum.inr
(tail
{ val := Stream'.corec' (Corec.f f) (Sum.inr b),
property :=
(_ :
∀ (n : ℕ) (a' : α),
Stream'.corec' (Corec.f f) (Sum.inr b) n = some a' →
Stream'.corec' (Corec.f f) (Sum.inr b) (n + 1) = some a') })
| some a => Sum.inl a) =   match Sum.inr b' with
| Sum.inl a => Sum.inl a
| Sum.inr b =>
Sum.inr
{ val := Stream'.corec' (Corec.f f) (Sum.inr b),
property :=
(_ :
∀ (n : ℕ) (a' : α),
Stream'.corec' (Corec.f f) (Sum.inr b) n = some a' →
Stream'.corec' (Corec.f f) (Sum.inr b) (n + 1) = some a') }rflGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βdestruct (corec f b) = rmap (corec f) (f b)dsimp [Corec.f: {α : Type ?u.9014} → {β : Type ?u.9013} → (β → α ⊕ β) → α ⊕ β → Option α × (α ⊕ β)Corec.f, destruct: {α : Type ?u.9016} → Computation α → α ⊕ Computation αdestruct]α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βx✝: α ⊕ βh✝: f b = x✝b': βh: f b = Sum.inr b'inrSum.inr
(tail
{
val :=
Stream'.corec'
(fun 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))
(Sum.inr b),
property :=
(_ :
∀ (n : ℕ) (a' : α),
Stream'.corec' (Corec.f f) (Sum.inr b) n = some a' →
Stream'.corec' (Corec.f f) (Sum.inr b) (n + 1) = some a') }) =   Sum.inr
{
val :=
Stream'.corec'
(fun 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))
(Sum.inr b'),
property :=
(_ :
∀ (n : ℕ) (a' : α),
Stream'.corec' (Corec.f f) (Sum.inr b') n = some a' →
Stream'.corec' (Corec.f f) (Sum.inr b') (n + 1) = some a') }
α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βdestruct (corec f b) = rmap (corec f) (f b)apply congr_arg: ∀ {α : Sort ?u.9070} {β : Sort ?u.9069} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂congr_argα: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βx✝: α ⊕ βh✝: f b = x✝b': βh: f b = Sum.inr b'inr.htail
{
val :=
Stream'.corec'
(fun 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))
(Sum.inr b),
property :=
(_ :
∀ (n : ℕ) (a' : α),
Stream'.corec' (Corec.f f) (Sum.inr b) n = some a' →
Stream'.corec' (Corec.f f) (Sum.inr b) (n + 1) = some a') } =   {
val :=
Stream'.corec'
(fun 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))
(Sum.inr b'),
property :=
(_ :
∀ (n : ℕ) (a' : α),
Stream'.corec' (Corec.f f) (Sum.inr b') n = some a' →
Stream'.corec' (Corec.f f) (Sum.inr b') (n + 1) = some a') };α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βx✝: α ⊕ βh✝: f b = x✝b': βh: f b = Sum.inr b'inr.htail
{
val :=
Stream'.corec'
(fun 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))
(Sum.inr b),
property :=
(_ :
∀ (n : ℕ) (a' : α),
Stream'.corec' (Corec.f f) (Sum.inr b) n = some a' →
Stream'.corec' (Corec.f f) (Sum.inr b) (n + 1) = some a') } =   {
val :=
Stream'.corec'
(fun 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))
(Sum.inr b'),
property :=
(_ :
∀ (n : ℕ) (a' : α),
Stream'.corec' (Corec.f f) (Sum.inr b') n = some a' →
Stream'.corec' (Corec.f f) (Sum.inr b') (n + 1) = some a') } α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βdestruct (corec f b) = rmap (corec f) (f b)apply Subtype.eq: ∀ {α : Type ?u.9090} {p : α → Prop} {a1 a2 : { x // p x }}, ↑a1 = ↑a2 → a1 = a2Subtype.eqα: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βx✝: α ⊕ βh✝: f b = x✝b': βh: f b = Sum.inr b'inr.h.a↑(tail
{
val :=
Stream'.corec'
(fun 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))
(Sum.inr b),
property :=
(_ :
∀ (n : ℕ) (a' : α),
Stream'.corec' (Corec.f f) (Sum.inr b) n = some a' →
Stream'.corec' (Corec.f f) (Sum.inr b) (n + 1) = some a') }) =   ↑{
val :=
Stream'.corec'
(fun 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))
(Sum.inr b'),
property :=
(_ :
∀ (n : ℕ) (a' : α),
Stream'.corec' (Corec.f f) (Sum.inr b') n = some a' →
Stream'.corec' (Corec.f f) (Sum.inr b') (n + 1) = some a') }
α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βdestruct (corec f b) = rmap (corec f) (f b)dsimp [corec: {α : Type ?u.9114} → {β : Type ?u.9113} → (β → α ⊕ β) → β → Computation αcorec, tail: {α : Type ?u.9116} → Computation α → Computation αtail]α: Type uβ: Type vγ: Type wf: β → α ⊕ βb: βx✝: α ⊕ βh✝: f b = x✝b': βh: f b = Sum.inr b'```