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.
/-
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
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
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⟩
/- ./././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
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
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
Computation.destruct
/-- `run c` is an unsound meta function that runs `c` to completion, possibly
resulting in an infinite loop in the VM. -/
unsafedef
α: Type u β: Type v γ: Type w s': Computationα x✝: Optionα f: Stream' (Optionα) al: ∀ ⦃n : ℕ⦄ ⦃a : α⦄, fn=somea → f (n+1)=somea f0✝: ↑{ val := f, property := al }0=x✝ f0: ↑{ val := f, property := al }0=none h': tail{ val := f, property := al }=s'
none.mk
{ val := f, property := al }=think (tail{ val := f, property := al })
α: Type u β: Type v γ: Type w s': Computationα x✝: Optionα f: Stream' (Optionα) al: ∀ ⦃n : ℕ⦄ ⦃a : α⦄, fn=somea → f (n+1)=somea f0✝: ↑{ val := f, property := al }0=x✝ f0: ↑{ val := f, property := al }0=none h': tail{ val := f, property := al }=s'
none.mk.a
↑{ val := f, property := al }=↑(think (tail{ val := f, property := al }))
α: Type u β: Type v γ: Type w s': Computationα x✝: Optionα f: Stream' (Optionα) al: ∀ ⦃n : ℕ⦄ ⦃a : α⦄, fn=somea → f (n+1)=somea f0✝: ↑{ val := f, property := al }0=x✝ f0: ↑{ val := f, property := al }0=none h': tail{ val := f, property := al }=s'
α: Type u β: Type v γ: Type w s': Computationα x✝: Optionα f: Stream' (Optionα) al: ∀ ⦃n : ℕ⦄ ⦃a : α⦄, fn=somea → f (n+1)=somea f0✝: ↑{ val := f, property := al }0=x✝ f0: ↑{ val := f, property := al }0=none h': tail{ val := f, property := al }=s'
α: Type u β: Type v γ: Type w s': Computationα x✝: Optionα f: Stream' (Optionα) al: ∀ ⦃n : ℕ⦄ ⦃a : α⦄, fn=somea → f (n+1)=somea f0✝: ↑{ val := f, property := al }0=x✝ f0: ↑{ val := f, property := al }0=none h': tail{ val := f, property := al }=s'
α: Type u β: Type v γ: Type w s': Computationα x✝: Optionα f: Stream' (Optionα) al: ∀ ⦃n : ℕ⦄ ⦃a : α⦄, fn=somea → f (n+1)=somea f0✝: ↑{ val := f, property := al }0=x✝ f0: ↑{ val := f, property := al }0=none h': tail{ val := f, property := al }=s'
b)
set_option linter.uppercaseLean3 falsein#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
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.rmapattribute [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