import Mt.Reservation
import Mt.Task.Basic

namespace Mt.TaskM

variable {spec: Spec
spec : Spec: Type 1
Spec}
local instance: {spec : Spec} → IsReservation spec.Reservation
instance : IsReservation: Type → Type
IsReservation spec: Spec
spec.Reservation: Spec → Type
Reservation :=spec: Spec
spec.is_reservation: (self : Spec) → IsReservation self.Reservation
is_reservation

/-- Validation primitive for reasoning for composable tasks.

  Validation may assume `assuming` and must ensure the following:
  * The task has to behave conform to the specification at all times
  * The task never panics
  * Finally, `motive` holds after the task completes

  ### Proving `valid`
  The definition is rather cumbersome to work with. You should use
  helper theorems like `valid_pure`, `valid_bind`, `valid_rmr`, ...

  They are designed to be used with the `apply` tactic.

  ### Blocking predicate: `assuming`
  When validating our task, we can assume `assuming state = true`. However,
  in most cases we have `assuming = λ _ => true`, i.e. our hypothesis does
  not provide anything useful.

  There is one important exception: Blocking threads. If a thread
  waits for a certain condition before it continues its task, we can
  safely assume that this condition holds when the task is excuting.

  ### Final goal: `motive`
  A valid thread must drop its reservations in the end. Therefore, the
  final goal on those tasks is `λ _ r => r = IsReservation.empty`.
  However, intermediate tasks (i.e. single operations) do not need to
  share this goal.
  
  In fact, they usally do not. If one operation
  prepares the next operation, it usually creates some reservation to
  ensure that no other thread undos this preparation. In this example,
  the motive should encode that the preparation has been made.

  `motive` is the only way to pass facts from one iteration to the next.
  See `valid_bind` for more information.
-/
def valid: {spec : Spec} →
  {T : Type} →
    (_ : TaskM spec T) ×' (_ : spec.Reservation) ×' (_ : spec.State → Bool) ×' (T → spec.Reservation → Prop) → Prop
valid {T: Type
T : Type: Type 1
Type} (p: TaskM spec T
p : TaskM: Spec → Type → Type
TaskM spec: Spec
spec T: Type
T) (r: spec.Reservation
r : spec: Spec
spec.Reservation: Spec → Type
Reservation)
  (assuming: spec.State → Bool
assuming : spec: Spec
spec.State: Spec → Type
State -> Bool: Type
Bool)
  (motive: T → spec.Reservation → Prop
motive : T: Type
T -> spec: Spec
spec.Reservation: Spec → Type
Reservation -> Prop: Type
Prop)
  : Prop: Type
Prop :=∀ env_r: ?m.51
env_r s: ?m.54
s,
    assuming: spec.State → Bool
assuming s: ?m.54
s →
    spec: Spec
spec.validate: (self : Spec) → self.Reservation → self.State → Prop
validate (env_r: ?m.51
env_r + r: spec.Reservation
r) s: ?m.54
s → ∃ r': spec.Reservation
r' : spec: Spec
spec.Reservation: Spec → Type
Reservation,
    match h: iterate p s = IterationResult.Panic a✝¹ a✝
h : p: TaskM spec T
p.iterate: {spec : Spec} → {T : Type} → TaskM spec T → spec.State → IterationResult spec T
iterate s: ?m.54
s with
    | IterationResult.Done: {spec : Spec} → {T : Type} → spec.State → T → IterationResult spec T
IterationResult.Done s': spec.State
s' t: T
t => spec: Spec
spec.validate: (self : Spec) → self.Reservation → self.State → Prop
validate (env_r: ?m.51
env_r + r': spec.Reservation
r') s': spec.State
s' ∧ motive: T → spec.Reservation → Prop
motive t: T
t r': spec.Reservation
r'
    | IterationResult.Panic: {spec : Spec} → {T : Type} → spec.State → String → IterationResult spec T
IterationResult.Panic .. => False: Prop
False
    | IterationResult.Running: {spec : Spec} → {T : Type} → spec.State → (spec.State → Bool) → TaskM spec T → IterationResult spec T
IterationResult.Running s': spec.State
s' block_until: spec.State → Bool
block_until cont: TaskM spec T
cont =>
        spec: Spec
spec.validate: (self : Spec) → self.Reservation → self.State → Prop
validate (env_r: ?m.51
env_r + r': spec.Reservation
r') s': spec.State
s' ∧
        cont: TaskM spec T
cont.valid: {T : Type} → TaskM spec T → spec.Reservation → (spec.State → Bool) → (T → spec.Reservation → Prop) → Prop
valid r': spec.Reservation
r' block_until: spec.State → Bool
block_until motive: T → spec.Reservation → Prop
motive
termination_by valid => p: TaskM spec T
p
decreasing_by simp_wfspec: Spec

T: Type

p: TaskM spec T

r: spec.Reservation

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

env_r: spec.Reservation

s: spec.State

r': spec.Reservation

s': spec.State

block_until: spec.State → Bool

cont: TaskM spec T

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

is_direct_cont cont p spec: Spec

T: Type

p: TaskM spec T

r: spec.Reservation

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

env_r: spec.Reservation

s: spec.State

r': spec.Reservation

s': spec.State

block_until: spec.State → Bool

cont: TaskM spec T

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

(invImage
      (fun a => PSigma.casesOn a fun p snd => PSigma.casesOn snd fun r snd => PSigma.casesOn snd fun assuming snd => p)
      instWf).1
  { fst := cont, snd := { fst := r', snd := { fst := block_until, snd := motive } } }
  { fst := p, snd := { fst := r, snd := { fst := assuming, snd := motive } } };spec: Spec

T: Type

p: TaskM spec T

r: spec.Reservation

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

env_r: spec.Reservation

s: spec.State

r': spec.Reservation

s': spec.State

block_until: spec.State → Bool

cont: TaskM spec T

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

is_direct_cont cont p spec: Spec

T: Type

p: TaskM spec T

r: spec.Reservation

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

env_r: spec.Reservation

s: spec.State

r': spec.Reservation

s': spec.State

block_until: spec.State → Bool

cont: TaskM spec T

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

(invImage
      (fun a => PSigma.casesOn a fun p snd => PSigma.casesOn snd fun r snd => PSigma.casesOn snd fun assuming snd => p)
      instWf).1
  { fst := cont, snd := { fst := r', snd := { fst := block_until, snd := motive } } }
  { fst := p, snd := { fst := r, snd := { fst := assuming, snd := motive } } }exact is_direct_cont.running: ∀ {spec : Spec} {T : Type} {p cont : TaskM spec T} {s s' : spec.State} {block_until : spec.State → Bool},
  iterate p s = IterationResult.Running s' block_until cont → is_direct_cont cont p
is_direct_cont.running h: iterate p s = IterationResult.Running s' block_until cont
h
Goals accomplished! 🐙

/-- To prove that `pure t` is valid you need to prove that the `motive` holds -/
theorem valid_pure: ∀ {T : Type} {t : T} {r : spec.Reservation} {assuming : spec.State → Bool} {motive : T → spec.Reservation → Prop},
  motive t r → valid (pure t) r assuming motive
valid_pure {T: Type
T : Type: Type 1
Type} {t: T
t : T: Type
T} {r: ?m.1199
r assuming: ?m.1202
assuming motive: ?m.1205
motive}
  (is_valid: ?m.1208
is_valid : motive: ?m.1205
motive t: T
t r: ?m.1199
r)
  : valid: {spec : Spec} →
  {T : Type} → TaskM spec T → spec.Reservation → (spec.State → Bool) → (T → spec.Reservation → Prop) → Prop
valid (spec :=spec: Spec
spec) (pure: {f : Type ?u.1213 → Type ?u.1212} → [self : Pure f] → {α : Type ?u.1213} → α → f α
pure t: T
t) r: ?m.1199
r assuming: ?m.1202
assuming motive: ?m.1205
motive :=by
  spec: Spec

T: Type

t: T

r: spec.Reservation

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

is_valid: motive t r

valid (pure t) r assuming motiverw [spec: Spec

T: Type

t: T

r: spec.Reservation

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

is_valid: motive t r

valid (pure t) r assuming motivevalid: {spec : Spec} →
  {T : Type} → TaskM spec T → spec.Reservation → (spec.State → Bool) → (T → spec.Reservation → Prop) → Prop
validspec: Spec

T: Type

t: T

r: spec.Reservation

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

is_valid: motive t r

∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        match h : iterate (pure t) s with
        | IterationResult.Done s' t_1 => Spec.validate spec (env_r + r') s' ∧ motive t_1 r'
        | IterationResult.Panic a a_1 => False
        | IterationResult.Running s' block_until cont =>
          Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive]spec: Spec

T: Type

t: T

r: spec.Reservation

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

is_valid: motive t r

∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        match h : iterate (pure t) s with
        | IterationResult.Done s' t_1 => Spec.validate spec (env_r + r') s' ∧ motive t_1 r'
        | IterationResult.Panic a a_1 => False
        | IterationResult.Running s' block_until cont =>
          Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive
  spec: Spec

T: Type

t: T

r: spec.Reservation

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

is_valid: motive t r

valid (pure t) r assuming motiveintro env_r: spec.Reservation
env_r s: spec.State
s _: assuming s = true
_ initial_valid: Spec.validate spec (env_r + r) s
initial_validspec: Spec

T: Type

t: T

r: spec.Reservation

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

is_valid: motive t r

env_r: spec.Reservation

s: spec.State

initial_valid: Spec.validate spec (env_r + r) s

∃ r',
  match h : iterate (pure t) s with
  | IterationResult.Done s' t_1 => Spec.validate spec (env_r + r') s' ∧ motive t_1 r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont => Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive
  spec: Spec

T: Type

t: T

r: spec.Reservation

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

is_valid: motive t r

valid (pure t) r assuming motiveexists r: spec.Reservation
r
Goals accomplished! 🐙

/-- To prove that `a >>= f` is valid you need to prove that both `a` and `f u`
  for all results `u` are valid.

  In many cases, `a` does something to prepare `f u`. Since only `f u` needs
  to fulfil the final motive, we can choose an arbitrary motive to validate `a`
  as "intermediate goal".

  To validate `f u` with the original `motive`, we can use the fact that the
  intermediate goal `motive_u` has been ensured by `a`. Motives use only results
  and reservations, which cannot be changed by other threads. Therefore, they
  stay valid even if other threads become active between `a` and `f u`. 
-/
theorem valid_bind: ∀ {spec : Spec} {U V : Type}
  (_x :
    (mu : TaskM spec U) ×'
      (f : U → TaskM spec V) ×'
        (r : spec.Reservation) ×'
          (assuming : spec.State → Bool) ×'
            (motive : V → spec.Reservation → Prop) ×'
              (motive_u : U → spec.Reservation → Prop) ×'
                (_ : valid mu r assuming motive_u) ×'
                  ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive),
  valid (_x.1 >>= _x.2.1) _x.2.2.1 _x.2.2.2.1 _x.2.2.2.2.1
valid_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}
  {r: spec.Reservation
r assuming: ?m.1562
assuming motive: V → spec.Reservation → Prop
motive}
  (motive_u: U → spec.Reservation → Prop
motive_u : U: Type
U -> spec: Spec
spec.Reservation: Spec → Type
Reservation -> Prop: Type
Prop)
  (mu_valid: valid mu r assuming motive_u
mu_valid : mu: TaskM spec U
mu.valid: {spec : Spec} →
  {T : Type} → TaskM spec T → spec.Reservation → (spec.State → Bool) → (T → spec.Reservation → Prop) → Prop
valid r: ?m.1559
r assuming: ?m.1562
assuming motive_u: U → spec.Reservation → Prop
motive_u)
  (f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive
f_valid : ∀ r': ?m.1595
r' u: ?m.1598
u,
    motive_u: U → spec.Reservation → Prop
motive_u u: ?m.1598
u r': ?m.1595
r' →
    (f: U → TaskM spec V
f u: ?m.1598
u).valid: {spec : Spec} →
  {T : Type} → TaskM spec T → spec.Reservation → (spec.State → Bool) → (T → spec.Reservation → Prop) → Prop
valid r': ?m.1595
r' (λ _: ?m.1613
_ => true: Bool
true) motive: ?m.1565
motive)
  : valid: {spec : Spec} →
  {T : Type} → TaskM spec T → spec.Reservation → (spec.State → Bool) → (T → spec.Reservation → Prop) → Prop
valid (mu: TaskM spec U
mu >>= f: U → TaskM spec V
f) r: ?m.1559
r assuming: ?m.1562
assuming motive: ?m.1565
motive :=by
  spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

mu_valid: valid mu r assuming motive_u

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

valid (mu >>= f) r assuming motiverw [spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

mu_valid: valid mu r assuming motive_u

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

valid (mu >>= f) r assuming motivevalid: {spec : Spec} →
  {T : Type} → TaskM spec T → spec.Reservation → (spec.State → Bool) → (T → spec.Reservation → Prop) → Prop
validspec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

mu_valid: valid mu r assuming motive_u

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        match h : iterate (mu >>= f) s with
        | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
        | IterationResult.Panic a a_1 => False
        | IterationResult.Running s' block_until cont =>
          Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive]spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

mu_valid: valid mu r assuming motive_u

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        match h : iterate (mu >>= f) s with
        | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
        | IterationResult.Panic a a_1 => False
        | IterationResult.Running s' block_until cont =>
          Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive
  spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

mu_valid: valid mu r assuming motive_u

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

valid (mu >>= f) r assuming motiveintro env_r: spec.Reservation
env_r s: spec.State
s assuming_true: assuming s = true
assuming_true initial_valid: Spec.validate spec (env_r + r) s
initial_validspec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

mu_valid: valid mu r assuming motive_u

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

∃ r',
  match h : iterate (mu >>= f) s with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont => Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive
  spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

mu_valid: valid mu r assuming motive_u

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

valid (mu >>= f) r assuming motiverw [spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

mu_valid: valid mu r assuming motive_u

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

∃ r',
  match h : iterate (mu >>= f) s with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont => Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motiveiterate_bind: ∀ {spec : Spec} {U V : Type} (mu : TaskM spec U) (f : U → TaskM spec V) (s : spec.State),
  iterate (mu >>= f) s =     let _discr := iterate mu s;
    match iterate 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 (cont >>= f)
iterate_bindspec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

mu_valid: valid mu r assuming motive_u

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

∃ r',
  match h :
    let _discr := iterate mu s;
    match iterate 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 (cont >>= f) with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont => Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive]spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

mu_valid: valid mu r assuming motive_u

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

∃ r',
  match h :
    let _discr := iterate mu s;
    match iterate 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 (cont >>= f) with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont => Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive
  spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

mu_valid: valid mu r assuming motive_u

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

valid (mu >>= f) r assuming motiverw [spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

mu_valid: valid mu r assuming motive_u

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

∃ r',
  match h :
    let _discr := iterate mu s;
    match iterate 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 (cont >>= f) with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont => Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motivevalid: {spec : Spec} →
  {T : Type} → TaskM spec T → spec.Reservation → (spec.State → Bool) → (T → spec.Reservation → Prop) → Prop
validspec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

mu_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        match h : iterate mu s with
        | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive_u t r'
        | IterationResult.Panic a a_1 => False
        | IterationResult.Running s' block_until cont =>
          Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive_u

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

∃ r',
  match h :
    let _discr := iterate mu s;
    match iterate 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 (cont >>= f) with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont => Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive]spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

mu_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        match h : iterate mu s with
        | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive_u t r'
        | IterationResult.Panic a a_1 => False
        | IterationResult.Running s' block_until cont =>
          Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive_u

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

∃ r',
  match h :
    let _discr := iterate mu s;
    match iterate 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 (cont >>= f) with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont => Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive at mu_valid: valid mu r assuming motive_u
mu_validspec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

mu_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        match h : iterate mu s with
        | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive_u t r'
        | IterationResult.Panic a a_1 => False
        | IterationResult.Running s' block_until cont =>
          Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive_u

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

∃ r',
  match h :
    let _discr := iterate mu s;
    match iterate 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 (cont >>= f) with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont => Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive
  spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

mu_valid: valid mu r assuming motive_u

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

valid (mu >>= f) r assuming motivecases iteration : iterate: {spec : Spec} → {T : Type} → TaskM spec T → spec.State → IterationResult spec T
iterate mu: TaskM spec U
mu s: spec.State
sspec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

mu_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        match h : iterate mu s with
        | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive_u t r'
        | IterationResult.Panic a a_1 => False
        | IterationResult.Running s' block_until cont =>
          Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive_u

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝¹: spec.State

a✝: U

iteration: iterate mu s = IterationResult.Done a✝¹ a✝

Done∃ r',
  match h :
    let _discr := IterationResult.Done a✝¹ a✝;
    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 (cont >>= f) with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont => Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive
spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

mu_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        match h : iterate mu s with
        | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive_u t r'
        | IterationResult.Panic a a_1 => False
        | IterationResult.Running s' block_until cont =>
          Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive_u

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝¹: spec.State

a✝: String

iteration: iterate mu s = IterationResult.Panic a✝¹ a✝

Panic∃ r',
  match h :
    let _discr := IterationResult.Panic a✝¹ a✝;
    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 (cont >>= f) with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont => Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive
spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

mu_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        match h : iterate mu s with
        | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive_u t r'
        | IterationResult.Panic a a_1 => False
        | IterationResult.Running s' block_until cont =>
          Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive_u

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: TaskM spec U

iteration: iterate mu s = IterationResult.Running a✝² a✝¹ a✝

Running∃ r',
  match h :
    let _discr := IterationResult.Running a✝² a✝¹ a✝;
    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 (cont >>= f) with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont => Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive
  spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

mu_valid: valid mu r assuming motive_u

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

valid (mu >>= f) r assuming motiveall_goals spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

mu_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        match h : iterate mu s with
        | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive_u t r'
        | IterationResult.Panic a a_1 => False
        | IterationResult.Running s' block_until cont =>
          Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive_u

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝¹: spec.State

a✝: U

iteration: iterate mu s = IterationResult.Done a✝¹ a✝

Done∃ r',
  match h :
    let _discr := IterationResult.Done a✝¹ a✝;
    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 (cont >>= f) with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont => Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive
spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

mu_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        match h : iterate mu s with
        | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive_u t r'
        | IterationResult.Panic a a_1 => False
        | IterationResult.Running s' block_until cont =>
          Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive_u

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝¹: spec.State

a✝: String

iteration: iterate mu s = IterationResult.Panic a✝¹ a✝

Panic∃ r',
  match h :
    let _discr := IterationResult.Panic a✝¹ a✝;
    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 (cont >>= f) with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont => Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive
spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

mu_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        match h : iterate mu s with
        | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive_u t r'
        | IterationResult.Panic a a_1 => False
        | IterationResult.Running s' block_until cont =>
          Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive_u

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: TaskM spec U

iteration: iterate mu s = IterationResult.Running a✝² a✝¹ a✝

Running∃ r',
  match h :
    let _discr := IterationResult.Running a✝² a✝¹ a✝;
    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 (cont >>= f) with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont => Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive(
    spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

mu_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        match h : iterate mu s with
        | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive_u t r'
        | IterationResult.Panic a a_1 => False
        | IterationResult.Running s' block_until cont =>
          Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive_u

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝¹: spec.State

a✝: U

iteration: iterate mu s = IterationResult.Done a✝¹ a✝

Done∃ r',
  match h :
    let _discr := IterationResult.Done a✝¹ a✝;
    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 (cont >>= f) with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont => Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motivesimp only []spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

mu_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        match h : iterate mu s with
        | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive_u t r'
        | IterationResult.Panic a a_1 => False
        | IterationResult.Running s' block_until cont =>
          Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive_u

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: TaskM spec U

iteration: iterate mu s = IterationResult.Running a✝² a✝¹ a✝

Running∃ r', Spec.validate spec (env_r + r') a✝² ∧ valid (a✝ >>= f) r' a✝¹ motive
    spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

mu_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        match h : iterate mu s with
        | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive_u t r'
        | IterationResult.Panic a a_1 => False
        | IterationResult.Running s' block_until cont =>
          Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive_u

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝¹: spec.State

a✝: String

iteration: iterate mu s = IterationResult.Panic a✝¹ a✝

Panic∃ r',
  match h :
    let _discr := IterationResult.Panic a✝¹ a✝;
    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 (cont >>= f) with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont => Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motivehave mu_valid: ?m.2547
mu_valid :=mu_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        match h : iterate mu s with
        | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive_u t r'
        | IterationResult.Panic a a_1 => False
        | IterationResult.Running s' block_until cont =>
          Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive_u
mu_valid env_r: spec.Reservation
env_r s: spec.State
s assuming_true: assuming s = true
assuming_true initial_valid: Spec.validate spec (env_r + r) s
initial_validspec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: TaskM spec U

iteration: iterate mu s = IterationResult.Running a✝² a✝¹ a✝

mu_valid: ∃ r',
  match h : iterate mu s with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive_u t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont =>
    Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive_u

Running∃ r', Spec.validate spec (env_r + r') a✝² ∧ valid (a✝ >>= f) r' a✝¹ motive
    spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

mu_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        match h : iterate mu s with
        | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive_u t r'
        | IterationResult.Panic a a_1 => False
        | IterationResult.Running s' block_until cont =>
          Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive_u

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝¹: spec.State

a✝: String

iteration: iterate mu s = IterationResult.Panic a✝¹ a✝

Panic∃ r',
  match h :
    let _discr := IterationResult.Panic a✝¹ a✝;
    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 (cont >>= f) with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont => Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motiverw [spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: TaskM spec U

iteration: iterate mu s = IterationResult.Running a✝² a✝¹ a✝

mu_valid: ∃ r',
  match h : iterate mu s with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive_u t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont =>
    Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive_u

Running∃ r', Spec.validate spec (env_r + r') a✝² ∧ valid (a✝ >>= f) r' a✝¹ motiveiteration: iterate mu s = IterationResult.Done a✝¹ a✝
iterationspec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝¹: spec.State

a✝: String

iteration: iterate mu s = IterationResult.Panic a✝¹ a✝

mu_valid: ∃ r',
  match h : IterationResult.Panic a✝¹ a✝ with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive_u t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont =>
    Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive_u

Panic∃ r', False]spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: TaskM spec U

iteration: iterate mu s = IterationResult.Running a✝² a✝¹ a✝

mu_valid: ∃ r',
  match h : IterationResult.Running a✝² a✝¹ a✝ with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive_u t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont =>
    Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive_u

Running∃ r', Spec.validate spec (env_r + r') a✝² ∧ valid (a✝ >>= f) r' a✝¹ motive at mu_valid: ?m.2119
mu_validspec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: TaskM spec U

iteration: iterate mu s = IterationResult.Running a✝² a✝¹ a✝

mu_valid: ∃ r',
  match h : IterationResult.Running a✝² a✝¹ a✝ with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive_u t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont =>
    Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive_u

Running∃ r', Spec.validate spec (env_r + r') a✝² ∧ valid (a✝ >>= f) r' a✝¹ motive
    spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

mu_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        match h : iterate mu s with
        | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive_u t r'
        | IterationResult.Panic a a_1 => False
        | IterationResult.Running s' block_until cont =>
          Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive_u

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝¹: spec.State

a✝: String

iteration: iterate mu s = IterationResult.Panic a✝¹ a✝

Panic∃ r',
  match h :
    let _discr := IterationResult.Panic a✝¹ a✝;
    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 (cont >>= f) with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont => Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motivesimp only [] at mu_valid: ∃ r',
  match h : IterationResult.Done a✝¹ a✝ with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive_u t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont =>
    Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive_u
mu_validspec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝¹: spec.State

a✝: U

iteration: iterate mu s = IterationResult.Done a✝¹ a✝

mu_valid: ∃ r', Spec.validate spec (env_r + r') a✝¹ ∧ motive_u a✝ r'

Done∃ r', Spec.validate spec (env_r + r') a✝¹ ∧ valid (f a✝) r' (fun x => true) motive
    spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

mu_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        match h : iterate mu s with
        | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive_u t r'
        | IterationResult.Panic a a_1 => False
        | IterationResult.Running s' block_until cont =>
          Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive_u

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝¹: spec.State

a✝: String

iteration: iterate mu s = IterationResult.Panic a✝¹ a✝

Panic∃ r',
  match h :
    let _discr := IterationResult.Panic a✝¹ a✝;
    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 (cont >>= f) with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont => Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motivecases mu_valid: ∃ r', False
mu_validspec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

mu_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        match h : iterate mu s with
        | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive_u t r'
        | IterationResult.Panic a a_1 => False
        | IterationResult.Running s' block_until cont =>
          Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive_u

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝¹: spec.State

a✝: String

iteration: iterate mu s = IterationResult.Panic a✝¹ a✝

w✝: spec.Reservation

Panic.intro∃ r', False spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

mu_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        match h : iterate mu s with
        | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive_u t r'
        | IterationResult.Panic a a_1 => False
        | IterationResult.Running s' block_until cont =>
          Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive_u

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝¹: spec.State

a✝: String

iteration: iterate mu s = IterationResult.Panic a✝¹ a✝

Panic∃ r',
  match h :
    let _discr := IterationResult.Panic a✝¹ a✝;
    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 (cont >>= f) with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont => Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive;spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

mu_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        match h : iterate mu s with
        | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive_u t r'
        | IterationResult.Panic a a_1 => False
        | IterationResult.Running s' block_until cont =>
          Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive_u

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: TaskM spec U

iteration: iterate mu s = IterationResult.Running a✝² a✝¹ a✝

w✝: spec.Reservation

Running.intro∃ r', Spec.validate spec (env_r + r') a✝² ∧ valid (a✝ >>= f) r' a✝¹ motive spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

mu_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        match h : iterate mu s with
        | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive_u t r'
        | IterationResult.Panic a a_1 => False
        | IterationResult.Running s' block_until cont =>
          Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive_u

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝¹: spec.State

a✝: String

iteration: iterate mu s = IterationResult.Panic a✝¹ a✝

Panic∃ r',
  match h :
    let _discr := IterationResult.Panic a✝¹ a✝;
    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 (cont >>= f) with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont => Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motiverename_i r': ?m.2222
r' mu_valid: ?m.2437 r'
mu_validspec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝¹: spec.State

a✝: String

iteration: iterate mu s = IterationResult.Panic a✝¹ a✝

r': spec.Reservation

mu_valid: False

Panic.intro∃ r', False
    spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

mu_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        match h : iterate mu s with
        | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive_u t r'
        | IterationResult.Panic a a_1 => False
        | IterationResult.Running s' block_until cont =>
          Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive_u

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝¹: spec.State

a✝: String

iteration: iterate mu s = IterationResult.Panic a✝¹ a✝

Panic∃ r',
  match h :
    let _discr := IterationResult.Panic a✝¹ a✝;
    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 (cont >>= f) with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont => Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motiveexists r': ?m.2222
r'spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝¹: spec.State

a✝: U

iteration: iterate mu s = IterationResult.Done a✝¹ a✝

r': spec.Reservation

mu_valid: Spec.validate spec (env_r + r') a✝¹ ∧ motive_u a✝ r'

Done.introSpec.validate spec (env_r + r') a✝¹ ∧ valid (f a✝) r' (fun x => true) motive
  )spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝¹: spec.State

a✝: U

iteration: iterate mu s = IterationResult.Done a✝¹ a✝

r': spec.Reservation

mu_valid: Spec.validate spec (env_r + r') a✝¹ ∧ motive_u a✝ r'

Done.introSpec.validate spec (env_r + r') a✝¹ ∧ valid (f a✝) r' (fun x => true) motive
  spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

mu_valid: valid mu r assuming motive_u

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

valid (mu >>= f) r assuming motive.spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝¹: spec.State

a✝: U

iteration: iterate mu s = IterationResult.Done a✝¹ a✝

r': spec.Reservation

mu_valid: Spec.validate spec (env_r + r') a✝¹ ∧ motive_u a✝ r'

Done.introSpec.validate spec (env_r + r') a✝¹ ∧ valid (f a✝) r' (fun x => true) motive spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝¹: spec.State

a✝: U

iteration: iterate mu s = IterationResult.Done a✝¹ a✝

r': spec.Reservation

mu_valid: Spec.validate spec (env_r + r') a✝¹ ∧ motive_u a✝ r'

Done.introSpec.validate spec (env_r + r') a✝¹ ∧ valid (f a✝) r' (fun x => true) motive
spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: TaskM spec U

iteration: iterate mu s = IterationResult.Running a✝² a✝¹ a✝

r': spec.Reservation

mu_valid: Spec.validate spec (env_r + r') a✝² ∧ valid a✝ r' a✝¹ motive_u

Running.introSpec.validate spec (env_r + r') a✝² ∧ valid (a✝ >>= f) r' a✝¹ motiveexact ⟨mu_valid: ?m.2223 r'
mu_valid.left: ∀ {a b : Prop}, a ∧ b → a
left, f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive
f_valid _: spec.Reservation
_ _: U
_ mu_valid: ?m.2223 r'
mu_valid.right: ∀ {a b : Prop}, a ∧ b → b
right⟩
Goals accomplished! 🐙
  spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

mu_valid: valid mu r assuming motive_u

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

valid (mu >>= f) r assuming motive.spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: TaskM spec U

iteration: iterate mu s = IterationResult.Running a✝² a✝¹ a✝

r': spec.Reservation

mu_valid: Spec.validate spec (env_r + r') a✝² ∧ valid a✝ r' a✝¹ motive_u

Running.introSpec.validate spec (env_r + r') a✝² ∧ valid (a✝ >>= f) r' a✝¹ motive spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: TaskM spec U

iteration: iterate mu s = IterationResult.Running a✝² a✝¹ a✝

r': spec.Reservation

mu_valid: Spec.validate spec (env_r + r') a✝² ∧ valid a✝ r' a✝¹ motive_u

Running.introSpec.validate spec (env_r + r') a✝² ∧ valid (a✝ >>= f) r' a✝¹ motiveconstructorspec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: TaskM spec U

iteration: iterate mu s = IterationResult.Running a✝² a✝¹ a✝

r': spec.Reservation

mu_valid: Spec.validate spec (env_r + r') a✝² ∧ valid a✝ r' a✝¹ motive_u

Running.intro.leftSpec.validate spec (env_r + r') a✝²
spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: TaskM spec U

iteration: iterate mu s = IterationResult.Running a✝² a✝¹ a✝

r': spec.Reservation

mu_valid: Spec.validate spec (env_r + r') a✝² ∧ valid a✝ r' a✝¹ motive_u

Running.intro.rightvalid (a✝ >>= f) r' a✝¹ motive
    spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: TaskM spec U

iteration: iterate mu s = IterationResult.Running a✝² a✝¹ a✝

r': spec.Reservation

mu_valid: Spec.validate spec (env_r + r') a✝² ∧ valid a✝ r' a✝¹ motive_u

Running.introSpec.validate spec (env_r + r') a✝² ∧ valid (a✝ >>= f) r' a✝¹ motive.spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: TaskM spec U

iteration: iterate mu s = IterationResult.Running a✝² a✝¹ a✝

r': spec.Reservation

mu_valid: Spec.validate spec (env_r + r') a✝² ∧ valid a✝ r' a✝¹ motive_u

Running.intro.leftSpec.validate spec (env_r + r') a✝² spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: TaskM spec U

iteration: iterate mu s = IterationResult.Running a✝² a✝¹ a✝

r': spec.Reservation

mu_valid: Spec.validate spec (env_r + r') a✝² ∧ valid a✝ r' a✝¹ motive_u

Running.intro.leftSpec.validate spec (env_r + r') a✝²
spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: TaskM spec U

iteration: iterate mu s = IterationResult.Running a✝² a✝¹ a✝

r': spec.Reservation

mu_valid: Spec.validate spec (env_r + r') a✝² ∧ valid a✝ r' a✝¹ motive_u

Running.intro.rightvalid (a✝ >>= f) r' a✝¹ motiveexact mu_valid: ?m.2641 r'
mu_valid.left: ∀ {a b : Prop}, a ∧ b → a
left
Goals accomplished! 🐙
    spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: TaskM spec U

iteration: iterate mu s = IterationResult.Running a✝² a✝¹ a✝

r': spec.Reservation

mu_valid: Spec.validate spec (env_r + r') a✝² ∧ valid a✝ r' a✝¹ motive_u

Running.introSpec.validate spec (env_r + r') a✝² ∧ valid (a✝ >>= f) r' a✝¹ motive.spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: TaskM spec U

iteration: iterate mu s = IterationResult.Running a✝² a✝¹ a✝

r': spec.Reservation

mu_valid: Spec.validate spec (env_r + r') a✝² ∧ valid a✝ r' a✝¹ motive_u

Running.intro.rightvalid (a✝ >>= f) r' a✝¹ motive spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: TaskM spec U

iteration: iterate mu s = IterationResult.Running a✝² a✝¹ a✝

r': spec.Reservation

mu_valid: Spec.validate spec (env_r + r') a✝² ∧ valid a✝ r' a✝¹ motive_u

Running.intro.rightvalid (a✝ >>= f) r' a✝¹ motivehave :=is_direct_cont.running: ∀ {spec : Spec} {T : Type} {p cont : TaskM spec T} {s s' : spec.State} {block_until : spec.State → Bool},
  iterate p s = IterationResult.Running s' block_until cont → is_direct_cont cont p
is_direct_cont.running iteration: iterate mu s = IterationResult.Running a✝² a✝¹ a✝
iterationspec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: TaskM spec U

iteration: iterate mu s = IterationResult.Running a✝² a✝¹ a✝

r': spec.Reservation

mu_valid: Spec.validate spec (env_r + r') a✝² ∧ valid a✝ r' a✝¹ motive_u

this: is_direct_cont a✝ mu

Running.intro.rightvalid (a✝ >>= f) r' a✝¹ motive
      spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

r: spec.Reservation

assuming: spec.State → Bool

motive: V → spec.Reservation → Prop

motive_u: U → spec.Reservation → Prop

f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: TaskM spec U

iteration: iterate mu s = IterationResult.Running a✝² a✝¹ a✝

r': spec.Reservation

mu_valid: Spec.validate spec (env_r + r') a✝² ∧ valid a✝ r' a✝¹ motive_u

Running.intro.rightvalid (a✝ >>= f) r' a✝¹ motiveexact valid_bind: ∀ {U V : Type} {mu : TaskM spec U} {f : U → TaskM spec V} {r : spec.Reservation} {assuming : spec.State → Bool}
  {motive : V → spec.Reservation → Prop} (motive_u : U → spec.Reservation → Prop),
  valid mu r assuming motive_u →
    (∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive) →
      valid (mu >>= f) r assuming motive
valid_bind motive_u: U → spec.Reservation → Prop
motive_u mu_valid: ?m.2641 r'
mu_valid.right: ∀ {a b : Prop}, a ∧ b → b
right f_valid: ∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive
f_valid
Goals accomplished! 🐙
termination_by valid_bind => mu: TaskM spec U
mu

theorem valid_rmr: ∀ {T : Type} {f : spec.State → T × spec.State} {r : spec.Reservation} {assuming : spec.State → Bool}
  {motive : T → spec.Reservation → Prop},
  (∀ (env_r : spec.Reservation) (s : spec.State),
      assuming s = true →
        Spec.validate spec (env_r + r) s →
          ∃ r',
            let _discr := f s;
            match f s with
            | (t, s') => Spec.validate spec (env_r + r') s' ∧ motive t r') →
    valid (atomic_read_modify_read f) r assuming motive
valid_rmr {T: Type
T : Type: Type 1
Type}
  {f: spec.State → T × spec.State
f : spec: Spec
spec.State: Spec → Type
State -> T: Type
T × spec: Spec
spec.State: Spec → Type
State}
  {r: ?m.6607
r assuming: spec.State → Bool
assuming motive: T → spec.Reservation → Prop
motive}
  (f_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  ?m.6797 env_r s →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        let _discr := f s;
        match f s with
        | (t, s') => Spec.validate spec (env_r + r') s' ∧ ?m.6798 env_r s r' t s'
f_valid : ∀ env_r: ?m.6617
env_r s: ?m.6620
s,
    assuming: ?m.6610
assuming s: ?m.6620
s →
    spec: Spec
spec.validate: (self : Spec) → self.Reservation → self.State → Prop
validate (env_r: ?m.6617
env_r + r: ?m.6607
r) s: ?m.6620
s → ∃ r': spec.Reservation
r' : spec: Spec
spec.Reservation: Spec → Type
Reservation,
    match f: spec.State → T × spec.State
f s: ?m.6620
s with
    | ⟨t: T
t, s': spec.State
s'⟩ => spec: Spec
spec.validate: (self : Spec) → self.Reservation → self.State → Prop
validate (env_r: ?m.6617
env_r + r': spec.Reservation
r') s': spec.State
s' ∧ motive: ?m.6613
motive t: T
t r': spec.Reservation
r'
  )
  : (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).valid: {spec : Spec} →
  {T : Type} → TaskM spec T → spec.Reservation → (spec.State → Bool) → (T → spec.Reservation → Prop) → Prop
valid r: ?m.6607
r assuming: ?m.6610
assuming motive: ?m.6613
motive :=by
  spec: Spec

T: Type

f: spec.State → T × spec.State

r: spec.Reservation

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

f_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        let _discr := f s;
        match f s with
        | (t, s') => Spec.validate spec (env_r + r') s' ∧ motive t r'

valid (atomic_read_modify_read f) r assuming motiverw [spec: Spec

T: Type

f: spec.State → T × spec.State

r: spec.Reservation

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

f_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        let _discr := f s;
        match f s with
        | (t, s') => Spec.validate spec (env_r + r') s' ∧ motive t r'

valid (atomic_read_modify_read f) r assuming motivevalid: {spec : Spec} →
  {T : Type} → TaskM spec T → spec.Reservation → (spec.State → Bool) → (T → spec.Reservation → Prop) → Prop
validspec: Spec

T: Type

f: spec.State → T × spec.State

r: spec.Reservation

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

f_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        let _discr := f s;
        match f s with
        | (t, s') => Spec.validate spec (env_r + r') s' ∧ motive t r'

∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        match h : iterate (atomic_read_modify_read f) s with
        | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
        | IterationResult.Panic a a_1 => False
        | IterationResult.Running s' block_until cont =>
          Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive]spec: Spec

T: Type

f: spec.State → T × spec.State

r: spec.Reservation

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

f_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        let _discr := f s;
        match f s with
        | (t, s') => Spec.validate spec (env_r + r') s' ∧ motive t r'

∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        match h : iterate (atomic_read_modify_read f) s with
        | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
        | IterationResult.Panic a a_1 => False
        | IterationResult.Running s' block_until cont =>
          Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive
  spec: Spec

T: Type

f: spec.State → T × spec.State

r: spec.Reservation

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

f_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        let _discr := f s;
        match f s with
        | (t, s') => Spec.validate spec (env_r + r') s' ∧ motive t r'

valid (atomic_read_modify_read f) r assuming motiveintro env_r: spec.Reservation
env_r s: spec.State
s assuming_true: assuming s = true
assuming_true initial_valid: Spec.validate spec (env_r + r) s
initial_validspec: Spec

T: Type

f: spec.State → T × spec.State

r: spec.Reservation

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

f_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        let _discr := f s;
        match f s with
        | (t, s') => Spec.validate spec (env_r + r') s' ∧ motive t r'

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

∃ r',
  match h : iterate (atomic_read_modify_read f) s with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont => Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive
  spec: Spec

T: Type

f: spec.State → T × spec.State

r: spec.Reservation

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

f_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        let _discr := f s;
        match f s with
        | (t, s') => Spec.validate spec (env_r + r') s' ∧ motive t r'

valid (atomic_read_modify_read f) r assuming motiverw [spec: Spec

T: Type

f: spec.State → T × spec.State

r: spec.Reservation

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

f_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        let _discr := f s;
        match f s with
        | (t, s') => Spec.validate spec (env_r + r') s' ∧ motive t r'

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

∃ r',
  match h : iterate (atomic_read_modify_read f) s with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont => Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motiveiterate_rmr: ∀ {spec : Spec} {T : Type} (f : spec.State → T × spec.State) (s : spec.State),
  iterate (atomic_read_modify_read f) s =     let _discr := f s;
    match f s with
    | (t, s') => IterationResult.Done s' t
iterate_rmrspec: Spec

T: Type

f: spec.State → T × spec.State

r: spec.Reservation

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

f_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        let _discr := f s;
        match f s with
        | (t, s') => Spec.validate spec (env_r + r') s' ∧ motive t r'

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

∃ r',
  match h :
    let _discr := f s;
    match f s with
    | (t, s') => IterationResult.Done s' t with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont => Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive]spec: Spec

T: Type

f: spec.State → T × spec.State

r: spec.Reservation

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

f_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        let _discr := f s;
        match f s with
        | (t, s') => Spec.validate spec (env_r + r') s' ∧ motive t r'

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

∃ r',
  match h :
    let _discr := f s;
    match f s with
    | (t, s') => IterationResult.Done s' t with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont => Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive
  spec: Spec

T: Type

f: spec.State → T × spec.State

r: spec.Reservation

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

f_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        let _discr := f s;
        match f s with
        | (t, s') => Spec.validate spec (env_r + r') s' ∧ motive t r'

valid (atomic_read_modify_read f) r assuming motiveexact f_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        let _discr := f s;
        match f s with
        | (t, s') => Spec.validate spec (env_r + r') s' ∧ motive t r'
f_valid env_r: spec.Reservation
env_r s: spec.State
s assuming_true: assuming s = true
assuming_true initial_valid: Spec.validate spec (env_r + r) s
initial_valid
Goals accomplished! 🐙

theorem valid_rm: ∀ {f : spec.State → spec.State} {r : spec.Reservation} {assuming : spec.State → Bool}
  {motive : Unit → spec.Reservation → Prop},
  (∀ (env_r : spec.Reservation) (s : spec.State),
      assuming s = true →
        Spec.validate spec (env_r + r) s →
          ∃ r',
            let s' := f s;
            Spec.validate spec (env_r + r') s' ∧ motive PUnit.unit r') →
    valid (atomic_read_modify f) r assuming motive
valid_rm
  {f: spec.State → spec.State
f : spec: Spec
spec.State: Spec → Type
State -> spec: Spec
spec.State: Spec → Type
State}
  {r: spec.Reservation
r assuming: spec.State → Bool
assuming motive: Unit → spec.Reservation → Prop
motive}
  (f_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  ?m.7259 env_r s →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        let s' := f s;
        Spec.validate spec (env_r + r') s' ∧ ?m.7260 env_r s r' s'
f_valid : ∀ env_r: ?m.7167
env_r s: ?m.7170
s,
    assuming: ?m.7160
assuming s: ?m.7170
s →
    spec: Spec
spec.validate: (self : Spec) → self.Reservation → self.State → Prop
validate (env_r: ?m.7167
env_r + r: ?m.7157
r) s: ?m.7170
s → ∃ r': spec.Reservation
r' : spec: Spec
spec.Reservation: Spec → Type
Reservation,
    match f: spec.State → spec.State
f s: ?m.7170
s with
    | s': ?m.7226
s' => spec: Spec
spec.validate: (self : Spec) → self.Reservation → self.State → Prop
validate (env_r: ?m.7167
env_r + r': spec.Reservation
r') s': ?m.7226
s' ∧ motive: ?m.7163
motive ⟨⟩: PUnit
⟨⟩ r': spec.Reservation
r')
  : (atomic_read_modify: {spec : Spec} → (spec.State → spec.State) → TaskM spec Unit
atomic_read_modify f: spec.State → spec.State
f).valid: {spec : Spec} →
  {T : Type} → TaskM spec T → spec.Reservation → (spec.State → Bool) → (T → spec.Reservation → Prop) → Prop
valid r: ?m.7157
r assuming: ?m.7160
assuming motive: ?m.7163
motive :=valid_rmr: ∀ {spec : Spec} {T : Type} {f : spec.State → T × spec.State} {r : spec.Reservation} {assuming : spec.State → Bool}
  {motive : T → spec.Reservation → Prop},
  (∀ (env_r : spec.Reservation) (s : spec.State),
      assuming s = true →
        Spec.validate spec (env_r + r) s →
          ∃ r',
            let _discr := f s;
            match f s with
            | (t, s') => Spec.validate spec (env_r + r') s' ∧ motive t r') →
    valid (atomic_read_modify_read f) r assuming motive
valid_rmr f_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        let s' := f s;
        Spec.validate spec (env_r + r') s' ∧ motive PUnit.unit r'
f_valid

theorem valid_read: ∀ {T : Type} {f : spec.State → T} {r : spec.Reservation} {assuming : spec.State → Bool}
  {motive : T → spec.Reservation → Prop},
  (∀ (env_r : spec.Reservation) (s : spec.State),
      assuming s = true →
        Spec.validate spec (env_r + r) s →
          ∃ r',
            let t := f s;
            Spec.validate spec (env_r + r') s ∧ motive t r') →
    valid (atomic_read f) r assuming motive
valid_read
  {f: spec.State → T
f : spec: Spec
spec.State: Spec → Type
State -> T: ?m.7474
T}
  {r: ?m.7481
r assuming: spec.State → Bool
assuming motive: T → spec.Reservation → Prop
motive}
  (f_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        let t := f s;
        Spec.validate spec (env_r + r') s ∧ motive t r'
f_valid : ∀ env_r: ?m.7491
env_r s: ?m.7494
s,
    assuming: ?m.7484
assuming s: ?m.7494
s →
    spec: Spec
spec.validate: (self : Spec) → self.Reservation → self.State → Prop
validate (env_r: ?m.7491
env_r + r: ?m.7481
r) s: ?m.7494
s → ∃ r': spec.Reservation
r' : spec: Spec
spec.Reservation: Spec → Type
Reservation,
    match f: spec.State → T
f s: ?m.7494
s with
    | t: ?m.7550
t => spec: Spec
spec.validate: (self : Spec) → self.Reservation → self.State → Prop
validate (env_r: ?m.7491
env_r + r': spec.Reservation
r') s: ?m.7494
s ∧ motive: ?m.7487
motive t: ?m.7550
t r': spec.Reservation
r')
  : (atomic_read: {spec : Spec} → {T : Type} → (spec.State → T) → TaskM spec T
atomic_read f: spec.State → T
f).valid: {spec : Spec} →
  {T : Type} → TaskM spec T → spec.Reservation → (spec.State → Bool) → (T → spec.Reservation → Prop) → Prop
valid r: ?m.7481
r assuming: ?m.7484
assuming motive: ?m.7487
motive :=valid_rmr: ∀ {spec : Spec} {T : Type} {f : spec.State → T × spec.State} {r : spec.Reservation} {assuming : spec.State → Bool}
  {motive : T → spec.Reservation → Prop},
  (∀ (env_r : spec.Reservation) (s : spec.State),
      assuming s = true →
        Spec.validate spec (env_r + r) s →
          ∃ r',
            let _discr := f s;
            match f s with
            | (t, s') => Spec.validate spec (env_r + r') s' ∧ motive t r') →
    valid (atomic_read_modify_read f) r assuming motive
valid_rmr f_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        let t := f s;
        Spec.validate spec (env_r + r') s ∧ motive t r'
f_valid

theorem valid_assert: ∀ {cond : spec.State → Bool} {r : spec.Reservation} {assuming : spec.State → Bool}
  {motive : Unit → spec.Reservation → Prop},
  motive PUnit.unit r →
    (∀ (env_r : spec.Reservation) (s : spec.State),
        assuming s = true → Spec.validate spec (env_r + r) s → cond s = true) →
      valid (atomic_assert cond) r assuming motive
valid_assert
  {cond: spec.State → Bool
cond : spec: Spec
spec.State: Spec → Type
State -> Bool: Type
Bool}
  {r: ?m.7801
r assuming: spec.State → Bool
assuming motive: Unit → spec.Reservation → Prop
motive}
  (motive_holds: ?m.7810
motive_holds : motive: ?m.7807
motive ⟨⟩: PUnit
⟨⟩ r: ?m.7801
r)
  (assertion_succeeds: ∀ (env_r : spec.Reservation) (s : spec.State), assuming s = true → Spec.validate spec (env_r + r) s → cond s = true
assertion_succeeds : ∀ env_r: ?m.7814
env_r s: ?m.7817
s,
    assuming: ?m.7804
assuming s: ?m.7817
s →
    spec: Spec
spec.validate: (self : Spec) → self.Reservation → self.State → Prop
validate (env_r: ?m.7814
env_r + r: ?m.7801
r) s: ?m.7817
s →
    cond: spec.State → Bool
cond s: ?m.7817
s)
  : (atomic_assert: {spec : Spec} → (spec.State → Bool) → TaskM spec Unit
atomic_assert cond: spec.State → Bool
cond).valid: {spec : Spec} →
  {T : Type} → TaskM spec T → spec.Reservation → (spec.State → Bool) → (T → spec.Reservation → Prop) → Prop
valid r: ?m.7801
r assuming: ?m.7804
assuming motive: ?m.7807
motive :=by
  spec: Spec

cond: spec.State → Bool

r: spec.Reservation

assuming: spec.State → Bool

motive: Unit → spec.Reservation → Prop

motive_holds: motive PUnit.unit r

assertion_succeeds: ∀ (env_r : spec.Reservation) (s : spec.State), assuming s = true → Spec.validate spec (env_r + r) s → cond s = true

valid (atomic_assert cond) r assuming motiverw [spec: Spec

cond: spec.State → Bool

r: spec.Reservation

assuming: spec.State → Bool

motive: Unit → spec.Reservation → Prop

motive_holds: motive PUnit.unit r

assertion_succeeds: ∀ (env_r : spec.Reservation) (s : spec.State), assuming s = true → Spec.validate spec (env_r + r) s → cond s = true

valid (atomic_assert cond) r assuming motivevalid: {spec : Spec} →
  {T : Type} → TaskM spec T → spec.Reservation → (spec.State → Bool) → (T → spec.Reservation → Prop) → Prop
validspec: Spec

cond: spec.State → Bool

r: spec.Reservation

assuming: spec.State → Bool

motive: Unit → spec.Reservation → Prop

motive_holds: motive PUnit.unit r

assertion_succeeds: ∀ (env_r : spec.Reservation) (s : spec.State), assuming s = true → Spec.validate spec (env_r + r) s → cond s = true

∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        match h : iterate (atomic_assert cond) s with
        | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
        | IterationResult.Panic a a_1 => False
        | IterationResult.Running s' block_until cont =>
          Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive]spec: Spec

cond: spec.State → Bool

r: spec.Reservation

assuming: spec.State → Bool

motive: Unit → spec.Reservation → Prop

motive_holds: motive PUnit.unit r

assertion_succeeds: ∀ (env_r : spec.Reservation) (s : spec.State), assuming s = true → Spec.validate spec (env_r + r) s → cond s = true

∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        match h : iterate (atomic_assert cond) s with
        | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
        | IterationResult.Panic a a_1 => False
        | IterationResult.Running s' block_until cont =>
          Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive
  spec: Spec

cond: spec.State → Bool

r: spec.Reservation

assuming: spec.State → Bool

motive: Unit → spec.Reservation → Prop

motive_holds: motive PUnit.unit r

assertion_succeeds: ∀ (env_r : spec.Reservation) (s : spec.State), assuming s = true → Spec.validate spec (env_r + r) s → cond s = true

valid (atomic_assert cond) r assuming motiveintro env_r: spec.Reservation
env_r s: spec.State
s assuming_true: assuming s = true
assuming_true initial_valid: Spec.validate spec (env_r + r) s
initial_validspec: Spec

cond: spec.State → Bool

r: spec.Reservation

assuming: spec.State → Bool

motive: Unit → spec.Reservation → Prop

motive_holds: motive PUnit.unit r

assertion_succeeds: ∀ (env_r : spec.Reservation) (s : spec.State), assuming s = true → Spec.validate spec (env_r + r) s → cond s = true

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

∃ r',
  match h : iterate (atomic_assert cond) s with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont => Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive
  spec: Spec

cond: spec.State → Bool

r: spec.Reservation

assuming: spec.State → Bool

motive: Unit → spec.Reservation → Prop

motive_holds: motive PUnit.unit r

assertion_succeeds: ∀ (env_r : spec.Reservation) (s : spec.State), assuming s = true → Spec.validate spec (env_r + r) s → cond s = true

valid (atomic_assert cond) r assuming motiverw [spec: Spec

cond: spec.State → Bool

r: spec.Reservation

assuming: spec.State → Bool

motive: Unit → spec.Reservation → Prop

motive_holds: motive PUnit.unit r

assertion_succeeds: ∀ (env_r : spec.Reservation) (s : spec.State), assuming s = true → Spec.validate spec (env_r + r) s → cond s = true

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

∃ r',
  match h : iterate (atomic_assert cond) s with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont => Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motiveiterate_assert: ∀ {spec : Spec} (cond : spec.State → Bool) (s : spec.State),
  iterate (atomic_assert cond) s =     if cond s = true then IterationResult.Done s PUnit.unit else IterationResult.Panic s "Assertion failed"
iterate_assertspec: Spec

cond: spec.State → Bool

r: spec.Reservation

assuming: spec.State → Bool

motive: Unit → spec.Reservation → Prop

motive_holds: motive PUnit.unit r

assertion_succeeds: ∀ (env_r : spec.Reservation) (s : spec.State), assuming s = true → Spec.validate spec (env_r + r) s → cond s = true

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

∃ r',
  match h : if cond s = true then IterationResult.Done s PUnit.unit else IterationResult.Panic s "Assertion failed" with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont => Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive]spec: Spec

cond: spec.State → Bool

r: spec.Reservation

assuming: spec.State → Bool

motive: Unit → spec.Reservation → Prop

motive_holds: motive PUnit.unit r

assertion_succeeds: ∀ (env_r : spec.Reservation) (s : spec.State), assuming s = true → Spec.validate spec (env_r + r) s → cond s = true

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

∃ r',
  match h : if cond s = true then IterationResult.Done s PUnit.unit else IterationResult.Panic s "Assertion failed" with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont => Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive
  spec: Spec

cond: spec.State → Bool

r: spec.Reservation

assuming: spec.State → Bool

motive: Unit → spec.Reservation → Prop

motive_holds: motive PUnit.unit r

assertion_succeeds: ∀ (env_r : spec.Reservation) (s : spec.State), assuming s = true → Spec.validate spec (env_r + r) s → cond s = true

valid (atomic_assert cond) r assuming motivehave cond_true: ?m.8107
cond_true :=assertion_succeeds: ∀ (env_r : spec.Reservation) (s : spec.State), assuming s = true → Spec.validate spec (env_r + r) s → cond s = true
assertion_succeeds env_r: spec.Reservation
env_r s: spec.State
s assuming_true: assuming s = true
assuming_true initial_valid: Spec.validate spec (env_r + r) s
initial_validspec: Spec

cond: spec.State → Bool

r: spec.Reservation

assuming: spec.State → Bool

motive: Unit → spec.Reservation → Prop

motive_holds: motive PUnit.unit r

assertion_succeeds: ∀ (env_r : spec.Reservation) (s : spec.State), assuming s = true → Spec.validate spec (env_r + r) s → cond s = true

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

cond_true: cond s = true

∃ r',
  match h : if cond s = true then IterationResult.Done s PUnit.unit else IterationResult.Panic s "Assertion failed" with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont => Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive
  spec: Spec

cond: spec.State → Bool

r: spec.Reservation

assuming: spec.State → Bool

motive: Unit → spec.Reservation → Prop

motive_holds: motive PUnit.unit r

assertion_succeeds: ∀ (env_r : spec.Reservation) (s : spec.State), assuming s = true → Spec.validate spec (env_r + r) s → cond s = true

valid (atomic_assert cond) r assuming motiverw [spec: Spec

cond: spec.State → Bool

r: spec.Reservation

assuming: spec.State → Bool

motive: Unit → spec.Reservation → Prop

motive_holds: motive PUnit.unit r

assertion_succeeds: ∀ (env_r : spec.Reservation) (s : spec.State), assuming s = true → Spec.validate spec (env_r + r) s → cond s = true

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

cond_true: cond s = true

∃ r',
  match h : if cond s = true then IterationResult.Done s PUnit.unit else IterationResult.Panic s "Assertion failed" with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont => Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motivecond_true: ?m.8107
cond_truespec: Spec

cond: spec.State → Bool

r: spec.Reservation

assuming: spec.State → Bool

motive: Unit → spec.Reservation → Prop

motive_holds: motive PUnit.unit r

assertion_succeeds: ∀ (env_r : spec.Reservation) (s : spec.State), assuming s = true → Spec.validate spec (env_r + r) s → cond s = true

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

cond_true: cond s = true

∃ r',
  match h : if true = true then IterationResult.Done s PUnit.unit else IterationResult.Panic s "Assertion failed" with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont => Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive]spec: Spec

cond: spec.State → Bool

r: spec.Reservation

assuming: spec.State → Bool

motive: Unit → spec.Reservation → Prop

motive_holds: motive PUnit.unit r

assertion_succeeds: ∀ (env_r : spec.Reservation) (s : spec.State), assuming s = true → Spec.validate spec (env_r + r) s → cond s = true

env_r: spec.Reservation

s: spec.State

assuming_true: assuming s = true

initial_valid: Spec.validate spec (env_r + r) s

cond_true: cond s = true

∃ r',
  match h : if true = true then IterationResult.Done s PUnit.unit else IterationResult.Panic s "Assertion failed" with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until cont => Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until motive
  spec: Spec

cond: spec.State → Bool

r: spec.Reservation

assuming: spec.State → Bool

motive: Unit → spec.Reservation → Prop

motive_holds: motive PUnit.unit r

assertion_succeeds: ∀ (env_r : spec.Reservation) (s : spec.State), assuming s = true → Spec.validate spec (env_r + r) s → cond s = true

valid (atomic_assert cond) r assuming motiveexists r: spec.Reservation
r
Goals accomplished! 🐙

theorem valid_blocking_rmr: ∀ {spec : Spec} {T : Type} {block_until : spec.State → Bool} {f : spec.State → T × spec.State} {r : spec.Reservation}
  {assuming : spec.State → Bool} {motive : T → spec.Reservation → Prop},
  (∀ (env_r : spec.Reservation) (s : spec.State),
      block_until s = true →
        Spec.validate spec (env_r + r) s →
          ∃ r',
            let _discr := f s;
            match f s with
            | (t, s') => Spec.validate spec (env_r + r') s' ∧ motive t r') →
    valid (atomic_blocking_rmr block_until f) r assuming motive
valid_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.8336
T × spec: Spec
spec.State: Spec → Type
State}
  {r: ?m.8349
r assuming: spec.State → Bool
assuming motive: T → spec.Reservation → Prop
motive}
  (f_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  block_until s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        let _discr := f s;
        match f s with
        | (t, s') => Spec.validate spec (env_r + r') s' ∧ motive t r'
f_valid : ∀ env_r: ?m.8359
env_r s: ?m.8362
s,
    block_until: spec.State → Bool
block_until s: ?m.8362
s →
    spec: Spec
spec.validate: (self : Spec) → self.Reservation → self.State → Prop
validate (env_r: ?m.8359
env_r + r: ?m.8349
r) s: ?m.8362
s → ∃ r': spec.Reservation
r' : spec: Spec
spec.Reservation: Spec → Type
Reservation,
    match f: spec.State → T × spec.State
f s: ?m.8362
s with
    | ⟨t: T
t, s': spec.State
s'⟩ => spec: Spec
spec.validate: (self : Spec) → self.Reservation → self.State → Prop
validate (env_r: ?m.8359
env_r + r': spec.Reservation
r') s': spec.State
s' ∧ motive: ?m.8355
motive t: T
t r': spec.Reservation
r'
  )
  : (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 f: spec.State → T × spec.State
f).valid: {spec : Spec} →
  {T : Type} → TaskM spec T → spec.Reservation → (spec.State → Bool) → (T → spec.Reservation → Prop) → Prop
valid r: ?m.8349
r assuming: ?m.8352
assuming motive: ?m.8355
motive :=by
  spec: Spec

T: Type

block_until: spec.State → Bool

f: spec.State → T × spec.State

r: spec.Reservation

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

f_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  block_until s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        let _discr := f s;
        match f s with
        | (t, s') => Spec.validate spec (env_r + r') s' ∧ motive t r'

valid (atomic_blocking_rmr block_until f) r assuming motiverw [spec: Spec

T: Type

block_until: spec.State → Bool

f: spec.State → T × spec.State

r: spec.Reservation

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

f_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  block_until s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        let _discr := f s;
        match f s with
        | (t, s') => Spec.validate spec (env_r + r') s' ∧ motive t r'

valid (atomic_blocking_rmr block_until f) r assuming motivevalid: {spec : Spec} →
  {T : Type} → TaskM spec T → spec.Reservation → (spec.State → Bool) → (T → spec.Reservation → Prop) → Prop
validspec: Spec

T: Type

block_until: spec.State → Bool

f: spec.State → T × spec.State

r: spec.Reservation

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

f_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  block_until s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        let _discr := f s;
        match f s with
        | (t, s') => Spec.validate spec (env_r + r') s' ∧ motive t r'

∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        match h : iterate (atomic_blocking_rmr block_until f) s with
        | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
        | IterationResult.Panic a a_1 => False
        | IterationResult.Running s' block_until_1 cont =>
          Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until_1 motive]spec: Spec

T: Type

block_until: spec.State → Bool

f: spec.State → T × spec.State

r: spec.Reservation

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

f_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  block_until s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        let _discr := f s;
        match f s with
        | (t, s') => Spec.validate spec (env_r + r') s' ∧ motive t r'

∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        match h : iterate (atomic_blocking_rmr block_until f) s with
        | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
        | IterationResult.Panic a a_1 => False
        | IterationResult.Running s' block_until_1 cont =>
          Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until_1 motive
  spec: Spec

T: Type

block_until: spec.State → Bool

f: spec.State → T × spec.State

r: spec.Reservation

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

f_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  block_until s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        let _discr := f s;
        match f s with
        | (t, s') => Spec.validate spec (env_r + r') s' ∧ motive t r'

valid (atomic_blocking_rmr block_until f) r assuming motiveintro env_r: spec.Reservation
env_r s: spec.State
s _: assuming s = true
_ initial_valid: Spec.validate spec (env_r + r) s
initial_validspec: Spec

T: Type

block_until: spec.State → Bool

f: spec.State → T × spec.State

r: spec.Reservation

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

f_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  block_until s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        let _discr := f s;
        match f s with
        | (t, s') => Spec.validate spec (env_r + r') s' ∧ motive t r'

env_r: spec.Reservation

s: spec.State

initial_valid: Spec.validate spec (env_r + r) s

∃ r',
  match h : iterate (atomic_blocking_rmr block_until f) s with
  | IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ motive t r'
  | IterationResult.Panic a a_1 => False
  | IterationResult.Running s' block_until_1 cont =>
    Spec.validate spec (env_r + r') s' ∧ valid cont r' block_until_1 motive
  spec: Spec

T: Type

block_until: spec.State → Bool

f: spec.State → T × spec.State

r: spec.Reservation

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

f_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  block_until s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        let _discr := f s;
        match f s with
        | (t, s') => Spec.validate spec (env_r + r') s' ∧ motive t r'

valid (atomic_blocking_rmr block_until f) r assuming motivesimp only [iterate_blocking_rmr: ∀ {spec : Spec} {T : Type} (block_until : spec.State → Bool) (f : spec.State → T × spec.State) (s : spec.State),
  iterate (atomic_blocking_rmr block_until f) s = IterationResult.Running s block_until (atomic_read_modify_read f)
iterate_blocking_rmr, initial_valid: Spec.validate spec (env_r + r) s
initial_valid, true_and: ∀ (p : Prop), (True ∧ p) = p
true_and]spec: Spec

T: Type

block_until: spec.State → Bool

f: spec.State → T × spec.State

r: spec.Reservation

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

f_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  block_until s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        let _discr := f s;
        match f s with
        | (t, s') => Spec.validate spec (env_r + r') s' ∧ motive t r'

env_r: spec.Reservation

s: spec.State

initial_valid: Spec.validate spec (env_r + r) s

∃ r', Spec.validate spec (env_r + r') s ∧ valid (atomic_read_modify_read f) r' block_until motive
  
  spec: Spec

T: Type

block_until: spec.State → Bool

f: spec.State → T × spec.State

r: spec.Reservation

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

f_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  block_until s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        let _discr := f s;
        match f s with
        | (t, s') => Spec.validate spec (env_r + r') s' ∧ motive t r'

valid (atomic_blocking_rmr block_until f) r assuming motiveexists r: spec.Reservation
rspec: Spec

T: Type

block_until: spec.State → Bool

f: spec.State → T × spec.State

r: spec.Reservation

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

f_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  block_until s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        let _discr := f s;
        match f s with
        | (t, s') => Spec.validate spec (env_r + r') s' ∧ motive t r'

env_r: spec.Reservation

s: spec.State

initial_valid: Spec.validate spec (env_r + r) s

Spec.validate spec (env_r + r) s ∧ valid (atomic_read_modify_read f) r block_until motive
  spec: Spec

T: Type

block_until: spec.State → Bool

f: spec.State → T × spec.State

r: spec.Reservation

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

f_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  block_until s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        let _discr := f s;
        match f s with
        | (t, s') => Spec.validate spec (env_r + r') s' ∧ motive t r'

valid (atomic_blocking_rmr block_until f) r assuming motiveexact ⟨initial_valid: Spec.validate spec (env_r + r) s
initial_valid, valid_rmr: ∀ {spec : Spec} {T : Type} {f : spec.State → T × spec.State} {r : spec.Reservation} {assuming : spec.State → Bool}
  {motive : T → spec.Reservation → Prop},
  (∀ (env_r : spec.Reservation) (s : spec.State),
      assuming s = true →
        Spec.validate spec (env_r + r) s →
          ∃ r',
            let _discr := f s;
            match f s with
            | (t, s') => Spec.validate spec (env_r + r') s' ∧ motive t r') →
    valid (atomic_read_modify_read f) r assuming motive
valid_rmr f_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  block_until s = true →
    Spec.validate spec (env_r + r) s →
      ∃ r',
        let _discr := f s;
        match f s with
        | (t, s') => Spec.validate spec (env_r + r') s' ∧ motive t r'
f_valid⟩
Goals accomplished! 🐙

end Mt.TaskM