import Mt.Reservation

namespace Mt.TaskM.impl

inductive IterationResult: Spec → Type → Sort ?u.5
IterationResult (spec: Spec
spec : Spec: Type 1
Spec) (T: Type
T : Type: Type 1
Type)
| Done: {spec : Spec} → {T : Type} → spec.State → T → IterationResult spec T
Done : spec: Spec
spec.State: Spec → Type
State -> T: Type
T -> IterationResult: Spec → Type → Sort ?u.5
IterationResult spec: Spec
spec T: Type
T
| Panic: {spec : Spec} → {T : Type} → spec.State → String → IterationResult spec T
Panic : spec: Spec
spec.State: Spec → Type
State -> String: Type
String -> IterationResult: Spec → Type → Sort ?u.5
IterationResult spec: Spec
spec T: Type
T
| Running: {spec : Spec} →
  {T : Type} → spec.State → (spec.State → Bool) → (spec.State → IterationResult spec T) → IterationResult spec T
Running : spec: Spec
spec.State: Spec → Type
State -> (spec: Spec
spec.State: Spec → Type
State -> Bool: Type
Bool) ->
    (spec: Spec
spec.State: Spec → Type
State -> IterationResult: Spec → Type → Sort ?u.5
IterationResult spec: Spec
spec T: Type
T) ->
    IterationResult: Spec → Type → Sort ?u.5
IterationResult spec: Spec
spec T: Type
T

def TaskM: (spec : Spec) → (T : Type) → ?m.1237 spec T
TaskM (spec: Spec
spec : Spec: Type 1
Spec) (T: Type
T : Type: Type 1
Type) :=spec: Spec
spec.State: Spec → Type
State -> IterationResult: Spec → Type → Type
IterationResult spec: Spec
spec T: Type
T

namespace TaskM

variable {spec: Spec
spec : Spec: Type 1
Spec}

def atomic_read_modify_read: {spec : Spec} → {T : Type} → (spec.State → T × spec.State) → TaskM spec T
atomic_read_modify_read
  (f: spec.State → T × spec.State
f : spec: Spec
spec.State: Spec → Type
State -> T: ?m.1264
T × spec: Spec
spec.State: Spec → Type
State)
  : TaskM: Spec → Type → Type
TaskM spec: Spec
spec T: ?m.1264
T
| s: ?m.1282
s => match f: spec.State → T × spec.State
f s: ?m.1282
s with
  | ⟨t: T
t, s': spec.State
s'⟩ => IterationResult.Done: {spec : Spec} → {T : Type} → spec.State → T → IterationResult spec T
IterationResult.Done s': spec.State
s' t: T
t

def panic: {T : Type} → String → TaskM spec T
panic {T: Type
T : Type: Type 1
Type} (msg: String
msg : String: Type
String) : TaskM: Spec → Type → Type
TaskM spec: Spec
spec T: Type
T
| s: ?m.1496
s => IterationResult.Panic: {spec : Spec} → {T : Type} → spec.State → String → IterationResult spec T
IterationResult.Panic s: ?m.1496
s msg: String
msg

def atomic_assert: (spec.State → Bool) → TaskM spec Unit
atomic_assert
  (cond: spec.State → Bool
cond : spec: Spec
spec.State: Spec → Type
State -> Bool: Type
Bool)
  : TaskM: Spec → Type → Type
TaskM spec: Spec
spec Unit: Type
Unit
| s: ?m.1564
s => if cond: spec.State → Bool
cond s: ?m.1564
s then
    IterationResult.Done: {spec : Spec} → {T : Type} → spec.State → T → IterationResult spec T
IterationResult.Done s: ?m.1564
s ⟨⟩: PUnit
⟨⟩
  else
    IterationResult.Panic: {spec : Spec} → {T : Type} → spec.State → String → IterationResult spec T
IterationResult.Panic s: ?m.1564
s "Assertion failed": String
"Assertion failed"

def atomic_blocking_rmr: {spec : Spec} → {T : Type} → (spec.State → Bool) → (spec.State → T × spec.State) → TaskM spec T
atomic_blocking_rmr
  (block_until: spec.State → Bool
block_until : spec: Spec
spec.State: Spec → Type
State -> Bool: Type
Bool)
  (f: spec.State → T × spec.State
f : spec: Spec
spec.State: Spec → Type
State -> T: ?m.1745
T × spec: Spec
spec.State: Spec → Type
State) : TaskM: Spec → Type → Type
TaskM spec: Spec
spec T: ?m.1745
T
| s: ?m.1769
s => IterationResult.Running: {spec : Spec} →
  {T : Type} → spec.State → (spec.State → Bool) → (spec.State → IterationResult spec T) → IterationResult spec T
IterationResult.Running s: ?m.1769
s block_until: spec.State → Bool
block_until (atomic_read_modify_read: {spec : Spec} → {T : Type} → (spec.State → T × spec.State) → TaskM spec T
atomic_read_modify_read f: spec.State → T × spec.State
f)

inductive is_direct_cont: {T : Type} → TaskM spec T → TaskM spec T → Prop
is_direct_cont {T: Type
T : Type: Type 1
Type} : TaskM: Spec → Type → Type
TaskM spec: Spec
spec T: Type
T -> TaskM: Spec → Type → Type
TaskM spec: Spec
spec T: Type
T -> Prop: Type
Prop
| running: ∀ {spec : Spec} {T : Type} {p cont : TaskM spec T} {s s' : spec.State} {block_until : spec.State → Bool},
  p s = IterationResult.Running s' block_until cont → is_direct_cont cont p
running
    {p: TaskM spec T
p cont: TaskM spec T
cont : TaskM: Spec → Type → Type
TaskM spec: Spec
spec T: Type
T}
    {s: ?m.1878
s s': ?m.1881
s'}
    {block_until: spec.State → Bool
block_until : spec: Spec
spec.State: Spec → Type
State -> Bool: Type
Bool}
    (iteration: p s = IterationResult.Running s' block_until cont
iteration : p: TaskM spec T
p s: ?m.1878
s = IterationResult.Running: {spec : Spec} →
  {T : Type} → spec.State → (spec.State → Bool) → (spec.State → IterationResult spec T) → IterationResult spec T
IterationResult.Running s': ?m.1881
s' block_until: spec.State → Bool
block_until cont: TaskM spec T
cont)
    : is_direct_cont: {T : Type} → TaskM spec T → TaskM spec T → Prop
is_direct_cont cont: TaskM spec T
cont p: TaskM spec T
p

theorem is_direct_cont.wf: ∀ {spec : Spec} {T : Type}, WellFounded is_direct_cont
is_direct_cont.wf {T: Type
T : Type: Type 1
Type} : WellFounded: {α : Sort ?u.1952} → (α → α → Prop) → Prop
WellFounded (@is_direct_cont: {spec : Spec} → {T : Type} → TaskM spec T → TaskM spec T → Prop
is_direct_cont spec: Spec
spec T: Type
T) :=by
  spec: Spec

T: Type

WellFounded is_direct_contconstructorspec: Spec

T: Type

h∀ (a : TaskM spec T), Acc is_direct_cont a
  spec: Spec

T: Type

WellFounded is_direct_contintro p: ?α
pspec: Spec

T: Type

p: TaskM spec T

hAcc is_direct_cont p
  spec: Spec

T: Type

WellFounded is_direct_contconstructorspec: Spec

T: Type

p: TaskM spec T

h.h∀ (y : TaskM spec T), is_direct_cont y p → Acc is_direct_cont y
  spec: Spec

T: Type

WellFounded is_direct_contintro cont: ?α
cont is_cont: ?r cont ?x
is_contspec: Spec

T: Type

p, cont: TaskM spec T

is_cont: is_direct_cont cont p

h.hAcc is_direct_cont cont
  spec: Spec

T: Type

WellFounded is_direct_contcases is_cont: ?r cont ?x
is_contspec: Spec

T: Type

p, cont: TaskM spec T

s✝, s'✝: spec.State

block_until✝: spec.State → Bool

h.h.runningAcc is_direct_cont cont
  spec: Spec

T: Type

WellFounded is_direct_contrename_i s: ?m.2363.State
s s': ?m.2363.State
s' bu: ?m.2363.State → Bool
bu iteration: p s = IterationResult.Running s' bu cont
iterationspec: Spec

T: Type

p, cont: TaskM spec T

s, s': spec.State

bu: spec.State → Bool

iteration: p s = IterationResult.Running s' bu cont

h.h.runningAcc is_direct_cont cont
  spec: Spec

T: Type

WellFounded is_direct_contexact helper: ∀ (it : IterationResult spec T) (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  it = IterationResult.Running s block_until p → Acc is_direct_cont p
helper (p: ?α
p s: ?m.2363.State
s) cont: ?α
cont iteration: p s = IterationResult.Running s' bu cont
iteration
Goals accomplished! 🐙

where
  helper: ∀ (it : IterationResult spec T) (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  it = IterationResult.Running s block_until p → Acc is_direct_cont p
helper (it: IterationResult spec T
it : IterationResult: Spec → Type → Type
IterationResult spec: Spec
spec T: Type
T) (p: TaskM spec T
p : TaskM: Spec → Type → Type
TaskM spec: Spec
spec T: Type
T) {s: ?m.1965
s block_until: ?m.1968
block_until} :
    it: IterationResult spec T
it = IterationResult.Running: {spec : Spec} →
  {T : Type} → spec.State → (spec.State → Bool) → (spec.State → IterationResult spec T) → IterationResult spec T
IterationResult.Running s: ?m.1965
s block_until: ?m.1968
block_until p: TaskM spec T
p → Acc: {α : Sort ?u.1985} → (α → α → Prop) → α → Prop
Acc is_direct_cont: {spec : Spec} → {T : Type} → TaskM spec T → TaskM spec T → Prop
is_direct_cont p: TaskM spec T
p :=by
    spec: Spec

T: Type

it: IterationResult spec T

p: TaskM spec T

s: spec.State

block_until: spec.State → Bool

it = IterationResult.Running s block_until p → Acc is_direct_cont prevert p: TaskM spec T
p s: spec.State
s block_until: spec.State → Bool
block_untilspec: Spec

T: Type

it: IterationResult spec T

∀ (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  it = IterationResult.Running s block_until p → Acc is_direct_cont p
    spec: Spec

T: Type

it: IterationResult spec T

p: TaskM spec T

s: spec.State

block_until: spec.State → Bool

it = IterationResult.Running s block_until p → Acc is_direct_cont pinduction it: IterationResult spec T
itspec: Spec

T: Type

a✝¹: spec.State

a✝: T

Done∀ (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  IterationResult.Done a✝¹ a✝ = IterationResult.Running s block_until p → Acc is_direct_cont p
spec: Spec

T: Type

a✝¹: spec.State

a✝: String

Panic∀ (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  IterationResult.Panic a✝¹ a✝ = IterationResult.Running s block_until p → Acc is_direct_cont p
spec: Spec

T: Type

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → IterationResult spec T

Running∀ (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  IterationResult.Running a✝² a✝¹ a✝ = IterationResult.Running s block_until p → Acc is_direct_cont p
    spec: Spec

T: Type

it: IterationResult spec T

p: TaskM spec T

s: spec.State

block_until: spec.State → Bool

it = IterationResult.Running s block_until p → Acc is_direct_cont p.spec: Spec

T: Type

a✝¹: spec.State

a✝: T

Done∀ (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  IterationResult.Done a✝¹ a✝ = IterationResult.Running s block_until p → Acc is_direct_cont p spec: Spec

T: Type

a✝¹: spec.State

a✝: T

Done∀ (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  IterationResult.Done a✝¹ a✝ = IterationResult.Running s block_until p → Acc is_direct_cont p
spec: Spec

T: Type

a✝¹: spec.State

a✝: String

Panic∀ (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  IterationResult.Panic a✝¹ a✝ = IterationResult.Running s block_until p → Acc is_direct_cont p
spec: Spec

T: Type

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → IterationResult spec T

Running∀ (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  IterationResult.Running a✝² a✝¹ a✝ = IterationResult.Running s block_until p → Acc is_direct_cont pintrosspec: Spec

T: Type

a✝²: spec.State

a✝¹: T

p✝: TaskM spec T

s✝: spec.State

block_until✝: spec.State → Bool

DoneAcc is_direct_cont p✝ spec: Spec

T: Type

a✝¹: spec.State

a✝: T

Done∀ (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  IterationResult.Done a✝¹ a✝ = IterationResult.Running s block_until p → Acc is_direct_cont p
spec: Spec

T: Type

a✝¹: spec.State

a✝: String

Panic∀ (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  IterationResult.Panic a✝¹ a✝ = IterationResult.Running s block_until p → Acc is_direct_cont p
spec: Spec

T: Type

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → IterationResult spec T

Running∀ (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  IterationResult.Running a✝² a✝¹ a✝ = IterationResult.Running s block_until p → Acc is_direct_cont p;spec: Spec

T: Type

a✝²: spec.State

a✝¹: T

p✝: TaskM spec T

s✝: spec.State

block_until✝: spec.State → Bool

DoneAcc is_direct_cont p✝ spec: Spec

T: Type

a✝¹: spec.State

a✝: T

Done∀ (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  IterationResult.Done a✝¹ a✝ = IterationResult.Running s block_until p → Acc is_direct_cont p
spec: Spec

T: Type

a✝¹: spec.State

a✝: String

Panic∀ (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  IterationResult.Panic a✝¹ a✝ = IterationResult.Running s block_until p → Acc is_direct_cont p
spec: Spec

T: Type

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → IterationResult spec T

Running∀ (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  IterationResult.Running a✝² a✝¹ a✝ = IterationResult.Running s block_until p → Acc is_direct_cont pcontradiction
Goals accomplished! 🐙
    spec: Spec

T: Type

it: IterationResult spec T

p: TaskM spec T

s: spec.State

block_until: spec.State → Bool

it = IterationResult.Running s block_until p → Acc is_direct_cont p.spec: Spec

T: Type

a✝¹: spec.State

a✝: String

Panic∀ (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  IterationResult.Panic a✝¹ a✝ = IterationResult.Running s block_until p → Acc is_direct_cont p spec: Spec

T: Type

a✝¹: spec.State

a✝: String

Panic∀ (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  IterationResult.Panic a✝¹ a✝ = IterationResult.Running s block_until p → Acc is_direct_cont p
spec: Spec

T: Type

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → IterationResult spec T

Running∀ (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  IterationResult.Running a✝² a✝¹ a✝ = IterationResult.Running s block_until p → Acc is_direct_cont pintrosspec: Spec

T: Type

a✝²: spec.State

a✝¹: String

p✝: TaskM spec T

s✝: spec.State

block_until✝: spec.State → Bool

PanicAcc is_direct_cont p✝ spec: Spec

T: Type

a✝¹: spec.State

a✝: String

Panic∀ (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  IterationResult.Panic a✝¹ a✝ = IterationResult.Running s block_until p → Acc is_direct_cont p
spec: Spec

T: Type

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → IterationResult spec T

Running∀ (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  IterationResult.Running a✝² a✝¹ a✝ = IterationResult.Running s block_until p → Acc is_direct_cont p;spec: Spec

T: Type

a✝²: spec.State

a✝¹: String

p✝: TaskM spec T

s✝: spec.State

block_until✝: spec.State → Bool

PanicAcc is_direct_cont p✝ spec: Spec

T: Type

a✝¹: spec.State

a✝: String

Panic∀ (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  IterationResult.Panic a✝¹ a✝ = IterationResult.Running s block_until p → Acc is_direct_cont p
spec: Spec

T: Type

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → IterationResult spec T

Running∀ (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  IterationResult.Running a✝² a✝¹ a✝ = IterationResult.Running s block_until p → Acc is_direct_cont pcontradiction
Goals accomplished! 🐙
    spec: Spec

T: Type

it: IterationResult spec T

p: TaskM spec T

s: spec.State

block_until: spec.State → Bool

it = IterationResult.Running s block_until p → Acc is_direct_cont p.spec: Spec

T: Type

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → IterationResult spec T

Running∀ (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  IterationResult.Running a✝² a✝¹ a✝ = IterationResult.Running s block_until p → Acc is_direct_cont p spec: Spec

T: Type

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → IterationResult spec T

Running∀ (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  IterationResult.Running a✝² a✝¹ a✝ = IterationResult.Running s block_until p → Acc is_direct_cont pintro p: TaskM spec T
p s: spec.State
s bu: spec.State → Bool
bu h: IterationResult.Running a✝² a✝¹ a✝ = IterationResult.Running s bu p
hspec: Spec

T: Type

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → IterationResult spec T

p: TaskM spec T

s: spec.State

bu: spec.State → Bool

h: IterationResult.Running a✝² a✝¹ a✝ = IterationResult.Running s bu p

RunningAcc is_direct_cont p
      spec: Spec

T: Type

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → IterationResult spec T

Running∀ (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  IterationResult.Running a✝² a✝¹ a✝ = IterationResult.Running s block_until p → Acc is_direct_cont prename_i s': ?m.2036.State
s' bu': ?m.2036.State → Bool
bu' p': ?m.2036.State → IterationResult ?m.2036 ?m.2037
p' IH: ∀ (a : ?m.2036.State), ?m.2038 (p' a)
IHspec: Spec

T: Type

s': spec.State

bu': spec.State → Bool

p': spec.State → IterationResult spec T

IH: ∀ (a : spec.State) (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  p' a = IterationResult.Running s block_until p → Acc is_direct_cont p

p: TaskM spec T

s: spec.State

bu: spec.State → Bool

h: IterationResult.Running s' bu' p' = IterationResult.Running s bu p

RunningAcc is_direct_cont p
      spec: Spec

T: Type

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → IterationResult spec T

Running∀ (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  IterationResult.Running a✝² a✝¹ a✝ = IterationResult.Running s block_until p → Acc is_direct_cont pinjection h: IterationResult.Running s' bu' p' = IterationResult.Running s bu p
hspec: Spec

T: Type

s': spec.State

bu': spec.State → Bool

p': spec.State → IterationResult spec T

IH: ∀ (a : spec.State) (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  p' a = IterationResult.Running s block_until p → Acc is_direct_cont p

p: TaskM spec T

s: spec.State

bu: spec.State → Bool

RunningAcc is_direct_cont p spec: Spec

T: Type

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → IterationResult spec T

Running∀ (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  IterationResult.Running a✝² a✝¹ a✝ = IterationResult.Running s block_until p → Acc is_direct_cont p;spec: Spec

T: Type

s': spec.State

bu': spec.State → Bool

p': spec.State → IterationResult spec T

IH: ∀ (a : spec.State) (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  p' a = IterationResult.Running s block_until p → Acc is_direct_cont p

p: TaskM spec T

s: spec.State

bu: spec.State → Bool

RunningAcc is_direct_cont p spec: Spec

T: Type

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → IterationResult spec T

Running∀ (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  IterationResult.Running a✝² a✝¹ a✝ = IterationResult.Running s block_until p → Acc is_direct_cont prename_i h: p' = p
hspec: Spec

T: Type

s': spec.State

bu': spec.State → Bool

p': spec.State → IterationResult spec T

IH: ∀ (a : spec.State) (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  p' a = IterationResult.Running s block_until p → Acc is_direct_cont p

p: TaskM spec T

s: spec.State

bu: spec.State → Bool

h: p' = p

RunningAcc is_direct_cont p spec: Spec

T: Type

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → IterationResult spec T

Running∀ (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  IterationResult.Running a✝² a✝¹ a✝ = IterationResult.Running s block_until p → Acc is_direct_cont p;spec: Spec

T: Type

s': spec.State

bu': spec.State → Bool

p': spec.State → IterationResult spec T

IH: ∀ (a : spec.State) (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  p' a = IterationResult.Running s block_until p → Acc is_direct_cont p

p: TaskM spec T

s: spec.State

bu: spec.State → Bool

h: p' = p

RunningAcc is_direct_cont p spec: Spec

T: Type

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → IterationResult spec T

Running∀ (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  IterationResult.Running a✝² a✝¹ a✝ = IterationResult.Running s block_until p → Acc is_direct_cont prw [spec: Spec

T: Type

s': spec.State

bu': spec.State → Bool

p': spec.State → IterationResult spec T

IH: ∀ (a : spec.State) (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  p' a = IterationResult.Running s block_until p → Acc is_direct_cont p

p: TaskM spec T

s: spec.State

bu: spec.State → Bool

h: p' = p

RunningAcc is_direct_cont ph: p' = p
hspec: Spec

T: Type

s': spec.State

bu': spec.State → Bool

p': spec.State → IterationResult spec T

p: TaskM spec T

IH: ∀ (a : spec.State) (p_1 : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  p a = IterationResult.Running s block_until p_1 → Acc is_direct_cont p_1

s: spec.State

bu: spec.State → Bool

h: p' = p

RunningAcc is_direct_cont p]spec: Spec

T: Type

s': spec.State

bu': spec.State → Bool

p': spec.State → IterationResult spec T

p: TaskM spec T

IH: ∀ (a : spec.State) (p_1 : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  p a = IterationResult.Running s block_until p_1 → Acc is_direct_cont p_1

s: spec.State

bu: spec.State → Bool

h: p' = p

RunningAcc is_direct_cont p at IH: ∀ (a : ?m.2036.State), ?m.2038 (p' a)
IHspec: Spec

T: Type

s': spec.State

bu': spec.State → Bool

p': spec.State → IterationResult spec T

p: TaskM spec T

IH: ∀ (a : spec.State) (p_1 : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  p a = IterationResult.Running s block_until p_1 → Acc is_direct_cont p_1

s: spec.State

bu: spec.State → Bool

h: p' = p

RunningAcc is_direct_cont p
      spec: Spec

T: Type

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → IterationResult spec T

Running∀ (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  IterationResult.Running a✝² a✝¹ a✝ = IterationResult.Running s block_until p → Acc is_direct_cont pconstructorspec: Spec

T: Type

s': spec.State

bu': spec.State → Bool

p': spec.State → IterationResult spec T

p: TaskM spec T

IH: ∀ (a : spec.State) (p_1 : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  p a = IterationResult.Running s block_until p_1 → Acc is_direct_cont p_1

s: spec.State

bu: spec.State → Bool

h: p' = p

Running.h∀ (y : TaskM spec T), is_direct_cont y p → Acc is_direct_cont y
      spec: Spec

T: Type

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → IterationResult spec T

Running∀ (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  IterationResult.Running a✝² a✝¹ a✝ = IterationResult.Running s block_until p → Acc is_direct_cont pintro cont: ?α
cont is_cont: ?r cont ?x
is_contspec: Spec

T: Type

s': spec.State

bu': spec.State → Bool

p': spec.State → IterationResult spec T

p: TaskM spec T

IH: ∀ (a : spec.State) (p_1 : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  p a = IterationResult.Running s block_until p_1 → Acc is_direct_cont p_1

s: spec.State

bu: spec.State → Bool

h: p' = p

cont: TaskM spec T

is_cont: is_direct_cont cont p

Running.hAcc is_direct_cont cont spec: Spec

T: Type

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → IterationResult spec T

Running∀ (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  IterationResult.Running a✝² a✝¹ a✝ = IterationResult.Running s block_until p → Acc is_direct_cont p;spec: Spec

T: Type

s': spec.State

bu': spec.State → Bool

p': spec.State → IterationResult spec T

p: TaskM spec T

IH: ∀ (a : spec.State) (p_1 : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  p a = IterationResult.Running s block_until p_1 → Acc is_direct_cont p_1

s: spec.State

bu: spec.State → Bool

h: p' = p

cont: TaskM spec T

is_cont: is_direct_cont cont p

Running.hAcc is_direct_cont cont spec: Spec

T: Type

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → IterationResult spec T

Running∀ (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  IterationResult.Running a✝² a✝¹ a✝ = IterationResult.Running s block_until p → Acc is_direct_cont pcases is_cont: ?r cont ?x
is_contspec: Spec

T: Type

s': spec.State

bu': spec.State → Bool

p': spec.State → IterationResult spec T

p: TaskM spec T

IH: ∀ (a : spec.State) (p_1 : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  p a = IterationResult.Running s block_until p_1 → Acc is_direct_cont p_1

s: spec.State

bu: spec.State → Bool

h: p' = p

cont: TaskM spec T

s✝, s'✝: spec.State

block_until✝: spec.State → Bool

Running.h.runningAcc is_direct_cont cont spec: Spec

T: Type

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → IterationResult spec T

Running∀ (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  IterationResult.Running a✝² a✝¹ a✝ = IterationResult.Running s block_until p → Acc is_direct_cont p;spec: Spec

T: Type

s': spec.State

bu': spec.State → Bool

p': spec.State → IterationResult spec T

p: TaskM spec T

IH: ∀ (a : spec.State) (p_1 : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  p a = IterationResult.Running s block_until p_1 → Acc is_direct_cont p_1

s: spec.State

bu: spec.State → Bool

h: p' = p

cont: TaskM spec T

s✝, s'✝: spec.State

block_until✝: spec.State → Bool

Running.h.runningAcc is_direct_cont cont spec: Spec

T: Type

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → IterationResult spec T

Running∀ (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  IterationResult.Running a✝² a✝¹ a✝ = IterationResult.Running s block_until p → Acc is_direct_cont prename_i h: p s✝ = IterationResult.Running s'✝ block_until✝ cont
hspec: Spec

T: Type

s': spec.State

bu': spec.State → Bool

p': spec.State → IterationResult spec T

p: TaskM spec T

IH: ∀ (a : spec.State) (p_1 : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  p a = IterationResult.Running s block_until p_1 → Acc is_direct_cont p_1

s: spec.State

bu: spec.State → Bool

cont: TaskM spec T

s✝, s'✝: spec.State

block_until✝: spec.State → Bool

h: p s✝ = IterationResult.Running s'✝ block_until✝ cont

Running.h.runningAcc is_direct_cont cont
      spec: Spec

T: Type

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → IterationResult spec T

Running∀ (p : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  IterationResult.Running a✝² a✝¹ a✝ = IterationResult.Running s block_until p → Acc is_direct_cont pexact IH: ∀ (a : spec.State) (p_1 : TaskM spec T) {s : spec.State} {block_until : spec.State → Bool},
  p a = IterationResult.Running s block_until p_1 → Acc is_direct_cont p_1
IH _: spec.State
_ _: TaskM spec T
_ h: p s✝ = IterationResult.Running s'✝ block_until✝ cont
h
Goals accomplished! 🐙

instance instWf: {T : Type} → WellFoundedRelation (TaskM spec T)
instWf {T: Type
T : Type: Type 1
Type} : WellFoundedRelation: Sort ?u.2740 → Sort (max 1 ?u.2740)
WellFoundedRelation (TaskM: Spec → Type → Type
TaskM spec: Spec
spec T: Type
T) where
  rel :=is_direct_cont: {spec : Spec} → {T : Type} → TaskM spec T → TaskM spec T → Prop
is_direct_cont
  wf  :=is_direct_cont.wf: ∀ {spec : Spec} {T : Type}, WellFounded is_direct_cont
is_direct_cont.wf

def pure: {spec : Spec} → {T : Type} → T → TaskM spec T
pure {T: Type
T : Type: Type 1
Type} (t: T
t : T: Type
T) : TaskM: Spec → Type → Type
TaskM spec: Spec
spec T: Type
T :=
  λ s: ?m.2825
s => IterationResult.Done: {spec : Spec} → {T : Type} → spec.State → T → IterationResult spec T
IterationResult.Done s: ?m.2825
s t: T
t

def bind: {spec : Spec} → {U V : Type} → (_ : TaskM spec U) ×' (_ : U → TaskM spec V) ×' spec.State → IterationResult spec V
bind {U: Type
U V: Type
V : Type: Type 1
Type} (mu: TaskM spec U
mu : TaskM: Spec → Type → Type
TaskM spec: Spec
spec U: Type
U) (f: U → TaskM spec V
f : U: Type
U -> TaskM: Spec → Type → Type
TaskM spec: Spec
spec V: Type
V) : TaskM: Spec → Type → Type
TaskM spec: Spec
spec V: Type
V :=
  λ s: ?m.2891
s => match h: mu s = IterationResult.Done s' u
h : mu: TaskM spec U
mu s: ?m.2891
s with
    | IterationResult.Done: {spec : Spec} → {T : Type} → spec.State → T → IterationResult spec T
IterationResult.Done s': spec.State
s' u: U
u => IterationResult.Running: {spec : Spec} →
  {T : Type} → spec.State → (spec.State → Bool) → (spec.State → IterationResult spec T) → IterationResult spec T
IterationResult.Running s': spec.State
s' (λ _: ?m.2922
_ => true: Bool
true) (f: U → TaskM spec V
f u: U
u)
    | IterationResult.Panic: {spec : Spec} → {T : Type} → spec.State → String → IterationResult spec T
IterationResult.Panic s': spec.State
s' msg: String
msg => IterationResult.Panic: {spec : Spec} → {T : Type} → spec.State → String → IterationResult spec T
IterationResult.Panic s': spec.State
s' msg: String
msg
    | IterationResult.Running: {spec : Spec} →
  {T : Type} → spec.State → (spec.State → Bool) → (spec.State → IterationResult spec T) → IterationResult spec T
IterationResult.Running s': spec.State
s' block_until: spec.State → Bool
block_until cont: spec.State → IterationResult spec U
cont =>
        have : is_direct_cont: {spec : Spec} → {T : Type} → TaskM spec T → TaskM spec T → Prop
is_direct_cont cont: spec.State → IterationResult spec U
cont mu: TaskM spec U
mu :=⟨h: mu s = IterationResult.Running s' block_until cont
h⟩
        IterationResult.Running: {spec : Spec} →
  {T : Type} → spec.State → (spec.State → Bool) → (spec.State → IterationResult spec T) → IterationResult spec T
IterationResult.Running s': spec.State
s' block_until: spec.State → Bool
block_until (bind: {U V : Type} → TaskM spec U → (U → TaskM spec V) → TaskM spec V
bind cont: spec.State → IterationResult spec U
cont f: U → TaskM spec V
f)
termination_by bind => mu: TaskM spec U
mu

theorem bind_def: ∀ {U V : Type} {spec : Spec} {mu : TaskM spec U} {f : U → TaskM spec V} {s : spec.State},
  bind mu f s =     let _discr := mu s;
    match mu s with
    | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
    | IterationResult.Panic s' msg => IterationResult.Panic s' msg
    | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont f)
bind_def {U: ?m.4332
U V: Type
V spec: ?m.4338
spec}
  {mu: TaskM spec U
mu : TaskM: Spec → Type → Type
TaskM spec: ?m.4338
spec U: ?m.4332
U} {f: U → TaskM spec V
f : U: ?m.4332
U -> TaskM: Spec → Type → Type
TaskM spec: ?m.4338
spec V: ?m.4335
V}
  {s: spec.State
s}
  : (bind: {spec : Spec} → {U V : Type} → TaskM spec U → (U → TaskM spec V) → TaskM spec V
bind mu: TaskM spec U
mu f: U → TaskM spec V
f) s: ?m.4348
s = match mu: TaskM spec U
mu s: ?m.4348
s with
    | IterationResult.Done: {spec : Spec} → {T : Type} → spec.State → T → IterationResult spec T
IterationResult.Done s': spec.State
s' u: U
u => IterationResult.Running: {spec : Spec} →
  {T : Type} → spec.State → (spec.State → Bool) → (spec.State → IterationResult spec T) → IterationResult spec T
IterationResult.Running s': spec.State
s' (λ _: ?m.4400
_ => true: Bool
true) (f: U → TaskM spec V
f u: U
u)
    | IterationResult.Panic: {spec : Spec} → {T : Type} → spec.State → String → IterationResult spec T
IterationResult.Panic s': spec.State
s' msg: String
msg => IterationResult.Panic: {spec : Spec} → {T : Type} → spec.State → String → IterationResult spec T
IterationResult.Panic s': spec.State
s' msg: String
msg
    | IterationResult.Running: {spec : Spec} →
  {T : Type} → spec.State → (spec.State → Bool) → (spec.State → IterationResult spec T) → IterationResult spec T
IterationResult.Running s': spec.State
s' block_until: spec.State → Bool
block_until cont: spec.State → IterationResult spec U
cont =>
        IterationResult.Running: {spec : Spec} →
  {T : Type} → spec.State → (spec.State → Bool) → (spec.State → IterationResult spec T) → IterationResult spec T
IterationResult.Running s': spec.State
s' block_until: spec.State → Bool
block_until (bind: {spec : Spec} → {U V : Type} → TaskM spec U → (U → TaskM spec V) → TaskM spec V
bind cont: spec.State → IterationResult spec U
cont f: U → TaskM spec V
f) :=by
  spec✝: Spec

U, V: Type

spec: Spec

mu: TaskM spec U

f: U → TaskM spec V

s: spec.State

bind mu f s =   let _discr := mu s;
  match mu s with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont f)simp only [bind: {spec : Spec} → {U V : Type} → TaskM spec U → (U → TaskM spec V) → TaskM spec V
bind]spec✝: Spec

U, V: Type

spec: Spec

mu: TaskM spec U

f: U → TaskM spec V

s: spec.State

(match h : mu s with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont f)) =   match mu s with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont f)
  spec✝: Spec

U, V: Type

spec: Spec

mu: TaskM spec U

f: U → TaskM spec V

s: spec.State

bind mu f s =   let _discr := mu s;
  match mu s with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont f)cases mu: TaskM spec U
mu s: spec.State
sspec✝: Spec

U, V: Type

spec: Spec

mu: TaskM spec U

f: U → TaskM spec V

s, a✝¹: spec.State

a✝: U

Done(match h : IterationResult.Done a✝¹ a✝ with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont f)) =   match IterationResult.Done a✝¹ a✝ with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont f)
spec✝: Spec

U, V: Type

spec: Spec

mu: TaskM spec U

f: U → TaskM spec V

s, a✝¹: spec.State

a✝: String

Panic(match h : IterationResult.Panic a✝¹ a✝ with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont f)) =   match IterationResult.Panic a✝¹ a✝ with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont f)
spec✝: Spec

U, V: Type

spec: Spec

mu: TaskM spec U

f: U → TaskM spec V

s, a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → IterationResult spec U

Running(match h : IterationResult.Running a✝² a✝¹ a✝ with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont f)) =   match IterationResult.Running a✝² a✝¹ a✝ with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont f) spec✝: Spec

U, V: Type

spec: Spec

mu: TaskM spec U

f: U → TaskM spec V

s: spec.State

(match h : mu s with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont f)) =   match mu s with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont f)<;>spec✝: Spec

U, V: Type

spec: Spec

mu: TaskM spec U

f: U → TaskM spec V

s, a✝¹: spec.State

a✝: U

Done(match h : IterationResult.Done a✝¹ a✝ with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont f)) =   match IterationResult.Done a✝¹ a✝ with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont f)
spec✝: Spec

U, V: Type

spec: Spec

mu: TaskM spec U

f: U → TaskM spec V

s, a✝¹: spec.State

a✝: String

Panic(match h : IterationResult.Panic a✝¹ a✝ with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont f)) =   match IterationResult.Panic a✝¹ a✝ with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont f)
spec✝: Spec

U, V: Type

spec: Spec

mu: TaskM spec U

f: U → TaskM spec V

s, a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → IterationResult spec U

Running(match h : IterationResult.Running a✝² a✝¹ a✝ with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont f)) =   match IterationResult.Running a✝² a✝¹ a✝ with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont f) spec✝: Spec

U, V: Type

spec: Spec

mu: TaskM spec U

f: U → TaskM spec V

s: spec.State

(match h : mu s with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont f)) =   match mu s with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont f)rfl
Goals accomplished! 🐙

theorem bind_assoc: ∀ {spec : Spec} {U V W : Type} (mu : TaskM spec U) (f : U → TaskM spec V) (g : V → TaskM spec W),
  (bind mu fun u => bind (f u) g) = bind (bind mu f) g
bind_assoc {U: Type
U V: Type
V W: Type
W : Type: Type 1
Type}
  (mu: TaskM spec U
mu : TaskM: Spec → Type → Type
TaskM spec: Spec
spec U: Type
U)
  (f: U → TaskM spec V
f : U: Type
U -> TaskM: Spec → Type → Type
TaskM spec: Spec
spec V: Type
V)
  (g: V → TaskM spec W
g : V: Type
V -> TaskM: Spec → Type → Type
TaskM spec: Spec
spec W: Type
W) :
  mu: TaskM spec U
mu.bind: {spec : Spec} → {U V : Type} → TaskM spec U → (U → TaskM spec V) → TaskM spec V
bind (fun u: ?m.6763
u => (f: U → TaskM spec V
f u: ?m.6763
u).bind: {spec : Spec} → {U V : Type} → TaskM spec U → (U → TaskM spec V) → TaskM spec V
bind g: V → TaskM spec W
g) = (mu: TaskM spec U
mu.bind: {spec : Spec} → {U V : Type} → TaskM spec U → (U → TaskM spec V) → TaskM spec V
bind f: U → TaskM spec V
f).bind: {spec : Spec} → {U V : Type} → TaskM spec U → (U → TaskM spec V) → TaskM spec V
bind g: V → TaskM spec W
g :=by
  spec: Spec

U, V, W: Type

mu: TaskM spec U

f: U → TaskM spec V

g: V → TaskM spec W

(bind mu fun u => bind (f u) g) = bind (bind mu f) gapply funext: ∀ {α : Sort ?u.6829} {β : α → Sort ?u.6828} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funextspec: Spec

U, V, W: Type

mu: TaskM spec U

f: U → TaskM spec V

g: V → TaskM spec W

h∀ (x : spec.State), bind mu (fun u => bind (f u) g) x = bind (bind mu f) g x spec: Spec

U, V, W: Type

mu: TaskM spec U

f: U → TaskM spec V

g: V → TaskM spec W

(bind mu fun u => bind (f u) g) = bind (bind mu f) g;spec: Spec

U, V, W: Type

mu: TaskM spec U

f: U → TaskM spec V

g: V → TaskM spec W

h∀ (x : spec.State), bind mu (fun u => bind (f u) g) x = bind (bind mu f) g x spec: Spec

U, V, W: Type

mu: TaskM spec U

f: U → TaskM spec V

g: V → TaskM spec W

(bind mu fun u => bind (f u) g) = bind (bind mu f) gintro s0: ?α
s0spec: Spec

U, V, W: Type

mu: TaskM spec U

f: U → TaskM spec V

g: V → TaskM spec W

s0: spec.State

hbind mu (fun u => bind (f u) g) s0 = bind (bind mu f) g s0
  spec: Spec

U, V, W: Type

mu: TaskM spec U

f: U → TaskM spec V

g: V → TaskM spec W

(bind mu fun u => bind (f u) g) = bind (bind mu f) gsimp only [bind_def: ∀ {U V : Type} {spec : Spec} {mu : TaskM spec U} {f : U → TaskM spec V} {s : spec.State},
  bind mu f s =     let _discr := mu s;
    match mu s with
    | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
    | IterationResult.Panic s' msg => IterationResult.Panic s' msg
    | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont f)
bind_def]spec: Spec

U, V, W: Type

mu: TaskM spec U

f: U → TaskM spec V

g: V → TaskM spec W

s0: spec.State

h(match mu s0 with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (bind (f u) g)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont =>
    IterationResult.Running s' block_until (bind cont fun u => bind (f u) g)) =   match
    match mu s0 with
    | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
    | IterationResult.Panic s' msg => IterationResult.Panic s' msg
    | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont f) with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (g u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont g)
  spec: Spec

U, V, W: Type

mu: TaskM spec U

f: U → TaskM spec V

g: V → TaskM spec W

(bind mu fun u => bind (f u) g) = bind (bind mu f) ginduction mu: TaskM spec U
mu s0: ?α
s0spec: Spec

U, V, W: Type

mu: TaskM spec U

f: U → TaskM spec V

g: V → TaskM spec W

s0, a✝¹: spec.State

a✝: U

h.Done(match IterationResult.Done a✝¹ a✝ with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (bind (f u) g)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont =>
    IterationResult.Running s' block_until (bind cont fun u => bind (f u) g)) =   match
    match IterationResult.Done a✝¹ a✝ with
    | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
    | IterationResult.Panic s' msg => IterationResult.Panic s' msg
    | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont f) with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (g u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont g)
spec: Spec

U, V, W: Type

mu: TaskM spec U

f: U → TaskM spec V

g: V → TaskM spec W

s0, a✝¹: spec.State

a✝: String

h.Panic(match IterationResult.Panic a✝¹ a✝ with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (bind (f u) g)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont =>
    IterationResult.Running s' block_until (bind cont fun u => bind (f u) g)) =   match
    match IterationResult.Panic a✝¹ a✝ with
    | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
    | IterationResult.Panic s' msg => IterationResult.Panic s' msg
    | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont f) with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (g u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont g)
spec: Spec

U, V, W: Type

mu: TaskM spec U

f: U → TaskM spec V

g: V → TaskM spec W

s0, a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → IterationResult spec U

h.Running(match IterationResult.Running a✝² a✝¹ a✝ with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (bind (f u) g)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont =>
    IterationResult.Running s' block_until (bind cont fun u => bind (f u) g)) =   match
    match IterationResult.Running a✝² a✝¹ a✝ with
    | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
    | IterationResult.Panic s' msg => IterationResult.Panic s' msg
    | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont f) with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (g u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont g) spec: Spec

U, V, W: Type

mu: TaskM spec U

f: U → TaskM spec V

g: V → TaskM spec W

s0: spec.State

h(match mu s0 with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (bind (f u) g)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont =>
    IterationResult.Running s' block_until (bind cont fun u => bind (f u) g)) =   match
    match mu s0 with
    | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
    | IterationResult.Panic s' msg => IterationResult.Panic s' msg
    | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont f) with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (g u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont g)<;>spec: Spec

U, V, W: Type

mu: TaskM spec U

f: U → TaskM spec V

g: V → TaskM spec W

s0, a✝¹: spec.State

a✝: U

h.Done(match IterationResult.Done a✝¹ a✝ with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (bind (f u) g)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont =>
    IterationResult.Running s' block_until (bind cont fun u => bind (f u) g)) =   match
    match IterationResult.Done a✝¹ a✝ with
    | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
    | IterationResult.Panic s' msg => IterationResult.Panic s' msg
    | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont f) with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (g u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont g)
spec: Spec

U, V, W: Type

mu: TaskM spec U

f: U → TaskM spec V

g: V → TaskM spec W

s0, a✝¹: spec.State

a✝: String

h.Panic(match IterationResult.Panic a✝¹ a✝ with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (bind (f u) g)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont =>
    IterationResult.Running s' block_until (bind cont fun u => bind (f u) g)) =   match
    match IterationResult.Panic a✝¹ a✝ with
    | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
    | IterationResult.Panic s' msg => IterationResult.Panic s' msg
    | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont f) with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (g u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont g)
spec: Spec

U, V, W: Type

mu: TaskM spec U

f: U → TaskM spec V

g: V → TaskM spec W

s0, a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → IterationResult spec U

h.Running(match IterationResult.Running a✝² a✝¹ a✝ with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (bind (f u) g)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont =>
    IterationResult.Running s' block_until (bind cont fun u => bind (f u) g)) =   match
    match IterationResult.Running a✝² a✝¹ a✝ with
    | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
    | IterationResult.Panic s' msg => IterationResult.Panic s' msg
    | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont f) with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (g u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont g) spec: Spec

U, V, W: Type

mu: TaskM spec U

f: U → TaskM spec V

g: V → TaskM spec W

s0: spec.State

h(match mu s0 with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (bind (f u) g)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont =>
    IterationResult.Running s' block_until (bind cont fun u => bind (f u) g)) =   match
    match mu s0 with
    | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
    | IterationResult.Panic s' msg => IterationResult.Panic s' msg
    | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont f) with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (g u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont g)try spec: Spec

U, V, W: Type

mu: TaskM spec U

f: U → TaskM spec V

g: V → TaskM spec W

s0, a✝¹: spec.State

a✝: U

h.Done(match IterationResult.Done a✝¹ a✝ with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (bind (f u) g)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont =>
    IterationResult.Running s' block_until (bind cont fun u => bind (f u) g)) =   match
    match IterationResult.Done a✝¹ a✝ with
    | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
    | IterationResult.Panic s' msg => IterationResult.Panic s' msg
    | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont f) with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (g u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont g)rfl
Goals accomplished! 🐙
  spec: Spec

U, V, W: Type

mu: TaskM spec U

f: U → TaskM spec V

g: V → TaskM spec W

(bind mu fun u => bind (f u) g) = bind (bind mu f) grename_i s': ?m.8227.State
s' block_until: ?m.8227.State → Bool
block_until cont: ?m.8227.State → IterationResult ?m.8227 ?m.8228
cont IH: ∀ (a : ?m.8227.State), ?m.8229 (cont a)
IHspec: Spec

U, V, W: Type

mu: TaskM spec U

f: U → TaskM spec V

g: V → TaskM spec W

s0, s': spec.State

block_until: spec.State → Bool

cont: spec.State → IterationResult spec U

IH: ∀ (a : spec.State),
  (match cont a with
    | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (bind (f u) g)
    | IterationResult.Panic s' msg => IterationResult.Panic s' msg
    | IterationResult.Running s' block_until cont =>
      IterationResult.Running s' block_until (bind cont fun u => bind (f u) g)) =     match
      match cont a with
      | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
      | IterationResult.Panic s' msg => IterationResult.Panic s' msg
      | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont f) with
    | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (g u)
    | IterationResult.Panic s' msg => IterationResult.Panic s' msg
    | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont g)

h.Running(match IterationResult.Running s' block_until cont with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (bind (f u) g)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont =>
    IterationResult.Running s' block_until (bind cont fun u => bind (f u) g)) =   match
    match IterationResult.Running s' block_until cont with
    | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
    | IterationResult.Panic s' msg => IterationResult.Panic s' msg
    | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont f) with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (g u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont g)
  spec: Spec

U, V, W: Type

mu: TaskM spec U

f: U → TaskM spec V

g: V → TaskM spec W

(bind mu fun u => bind (f u) g) = bind (bind mu f) gsimp only []spec: Spec

U, V, W: Type

mu: TaskM spec U

f: U → TaskM spec V

g: V → TaskM spec W

s0, s': spec.State

block_until: spec.State → Bool

cont: spec.State → IterationResult spec U

IH: ∀ (a : spec.State),
  (match cont a with
    | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (bind (f u) g)
    | IterationResult.Panic s' msg => IterationResult.Panic s' msg
    | IterationResult.Running s' block_until cont =>
      IterationResult.Running s' block_until (bind cont fun u => bind (f u) g)) =     match
      match cont a with
      | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
      | IterationResult.Panic s' msg => IterationResult.Panic s' msg
      | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont f) with
    | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (g u)
    | IterationResult.Panic s' msg => IterationResult.Panic s' msg
    | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont g)

h.RunningIterationResult.Running s' block_until (bind cont fun u => bind (f u) g) =   IterationResult.Running s' block_until (bind (bind cont f) g)
  spec: Spec

U, V, W: Type

mu: TaskM spec U

f: U → TaskM spec V

g: V → TaskM spec W

(bind mu fun u => bind (f u) g) = bind (bind mu f) gsimp only [<- bind_def: ∀ {U V : Type} {spec : Spec} {mu : TaskM spec U} {f : U → TaskM spec V} {s : spec.State},
  bind mu f s =     let _discr := mu s;
    match mu s with
    | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
    | IterationResult.Panic s' msg => IterationResult.Panic s' msg
    | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (bind cont f)
bind_def] at IH: ∀ (a : ?m.8227.State), ?m.8229 (cont a)
IHspec: Spec

U, V, W: Type

mu: TaskM spec U

f: U → TaskM spec V

g: V → TaskM spec W

s0, s': spec.State

block_until: spec.State → Bool

cont: spec.State → IterationResult spec U

IH: ∀ (a : spec.State), bind cont (fun u => bind (f u) g) a = bind (bind cont fun u => f u) (fun u => g u) a

h.RunningIterationResult.Running s' block_until (bind cont fun u => bind (f u) g) =   IterationResult.Running s' block_until (bind (bind cont f) g)
  spec: Spec

U, V, W: Type

mu: TaskM spec U

f: U → TaskM spec V

g: V → TaskM spec W

(bind mu fun u => bind (f u) g) = bind (bind mu f) gapply congrArg: ∀ {α : Sort ?u.8918} {β : Sort ?u.8917} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
congrArg (IterationResult.Running: {spec : Spec} →
  {T : Type} → spec.State → (spec.State → Bool) → (spec.State → IterationResult spec T) → IterationResult spec T
IterationResult.Running _: ?m.8923.State
_ _: ?m.8923.State → Bool
_)spec: Spec

U, V, W: Type

mu: TaskM spec U

f: U → TaskM spec V

g: V → TaskM spec W

s0, s': spec.State

block_until: spec.State → Bool

cont: spec.State → IterationResult spec U

IH: ∀ (a : spec.State), bind cont (fun u => bind (f u) g) a = bind (bind cont fun u => f u) (fun u => g u) a

h.Running(bind cont fun u => bind (f u) g) = bind (bind cont f) g
  spec: Spec

U, V, W: Type

mu: TaskM spec U

f: U → TaskM spec V

g: V → TaskM spec W

(bind mu fun u => bind (f u) g) = bind (bind mu f) gapply funext: ∀ {α : Sort ?u.8938} {β : α → Sort ?u.8937} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funextspec: Spec

U, V, W: Type

mu: TaskM spec U

f: U → TaskM spec V

g: V → TaskM spec W

s0, s': spec.State

block_until: spec.State → Bool

cont: spec.State → IterationResult spec U

IH: ∀ (a : spec.State), bind cont (fun u => bind (f u) g) a = bind (bind cont fun u => f u) (fun u => g u) a

h.Running.h∀ (x : spec.State), bind cont (fun u => bind (f u) g) x = bind (bind cont f) g x spec: Spec

U, V, W: Type

mu: TaskM spec U

f: U → TaskM spec V

g: V → TaskM spec W

(bind mu fun u => bind (f u) g) = bind (bind mu f) g;spec: Spec

U, V, W: Type

mu: TaskM spec U

f: U → TaskM spec V

g: V → TaskM spec W

s0, s': spec.State

block_until: spec.State → Bool

cont: spec.State → IterationResult spec U

IH: ∀ (a : spec.State), bind cont (fun u => bind (f u) g) a = bind (bind cont fun u => f u) (fun u => g u) a

h.Running.h∀ (x : spec.State), bind cont (fun u => bind (f u) g) x = bind (bind cont f) g x spec: Spec

U, V, W: Type

mu: TaskM spec U

f: U → TaskM spec V

g: V → TaskM spec W

(bind mu fun u => bind (f u) g) = bind (bind mu f) gintro s: ?α
sspec: Spec

U, V, W: Type

mu: TaskM spec U

f: U → TaskM spec V

g: V → TaskM spec W

s0, s': spec.State

block_until: spec.State → Bool

cont: spec.State → IterationResult spec U

IH: ∀ (a : spec.State), bind cont (fun u => bind (f u) g) a = bind (bind cont fun u => f u) (fun u => g u) a

s: spec.State

h.Running.hbind cont (fun u => bind (f u) g) s = bind (bind cont f) g s
  spec: Spec

U, V, W: Type

mu: TaskM spec U

f: U → TaskM spec V

g: V → TaskM spec W

(bind mu fun u => bind (f u) g) = bind (bind mu f) gexact IH: ∀ (a : spec.State), bind cont (fun u => bind (f u) g) a = bind (bind cont fun u => f u) (fun u => g u) a
IH ..
Goals accomplished! 🐙

end TaskM

end Mt.TaskM.impl