Theory itree

⊢ ∀itr f. ibind itr f = iflat (imap f itr)

⊢ ∀itr.
    iflat itr =
    itree_unfold
      (λx.
           case x of
             INL (ireturn (ireturn r0)) => Ret' r0
           | INL (ireturn Div) => Div'
           | INL (ireturn (Vis e f)) => Vis' e (λi. INR (f i))
           | INL Div => Div'
           | INL (Vis e f) => Vis' e (λi. INL (f i))
           | INR (ireturn r) => Ret' r
           | INR Div => Div'
           | INR (Vis e' f') => Vis' e' (λi. INR (f' i))) (INL itr)

⊢ ∀g itr.
    imap g itr =
    itree_unfold (λx. itree_CASE x (λr. Ret' (g r)) Div' (λe f. Vis' e f))
      itr

⊢ ∃rep. TYPE_DEFINITION itree_rep_ok rep

⊢ (∀a f f1 v. itree_el_CASE (Event a) f f1 v = f a) ∧
  (∀a f f1 v. itree_el_CASE (Return a) f f1 v = f1 a) ∧
  ∀f f1 v. itree_el_CASE Stuck f f1 v = v

⊢ (∀f f1 a. itree_el_size f f1 (Event a) = 1 + f a) ∧
  (∀f f1 a. itree_el_size f f1 (Return a) = 1 + f1 a) ∧
  ∀f f1. itree_el_size f f1 Stuck = 0

⊢ (∀a f v f1. itree_next_CASE (Ret' a) f v f1 = f a) ∧
  (∀f v f1. itree_next_CASE Div' f v f1 = v) ∧
  ∀a0 a1 f v f1. itree_next_CASE (Vis' a0 a1) f v f1 = f1 a0 a1

⊢ (∀f f1 f2 f3 a. itree_next_size f f1 f2 f3 (Ret' a) = 1 + f2 a) ∧
  (∀f f1 f2 f3. itree_next_size f f1 f2 f3 Div' = 0) ∧
  ∀f f1 f2 f3 a0 a1. itree_next_size f f1 f2 f3 (Vis' a0 a1) = 1 + f1 a0

⊢ ∀x y. ireturn x = ireturn y ⇔ x = y

⊢ ∀x f y g. Vis x f = Vis y g ⇔ x = y ∧ f = g

⊢ ∀a0 a1 a2.
    at_path a0 a1 a2 ⇔
    a0 = ireturn a2 ∧ a1 = [] ∨
    ∃f i ov p. a0 = Vis ov f ∧ a1 = (ov,i)::p ∧ at_path (f i) p a2

⊢ at_path itree p e ⇒ iset itree e

⊢ ∀at_path'.
    (∀e. at_path' (ireturn e) [] e) ∧
    (∀e f i ov p. at_path' (f i) p e ⇒ at_path' (Vis ov f) ((ov,i)::p) e) ⇒
    ∀a0 a1 a2. at_path a0 a1 a2 ⇒ at_path' a0 a1 a2

⊢ ∀e. at_path (ireturn e) [] e

⊢ (∀e. at_path (ireturn e) [] e) ∧
  ∀e f i ov p. at_path (f i) p e ⇒ at_path (Vis ov f) ((ov,i)::p) e

⊢ ∀at_path'.
    (∀e. at_path' (ireturn e) [] e) ∧
    (∀e f i ov p.
       at_path (f i) p e ∧ at_path' (f i) p e ⇒
       at_path' (Vis ov f) ((ov,i)::p) e) ⇒
    ∀a0 a1 a2. at_path a0 a1 a2 ⇒ at_path' a0 a1 a2

⊢ (at_path Div p e ⇔ F) ∧ (at_path (ireturn e) p a ⇔ p = [] ∧ a = e) ∧
  (at_path (Vis ov f) p e ⇔ ∃i l. p = (ov,i)::l ∧ at_path (f i) l e)

⊢ ∀e f i ov p. at_path (f i) p e ⇒ at_path (Vis ov f) ((ov,i)::p) e

⊢ DATATYPE (itree ireturn Div Vis)

⊢ DATATYPE (itree_el Event Return Stuck)

⊢ DATATYPE (itree_next Ret' Div' Vis')

⊢ ibind itr (λx. ibind (f x) g) = ibind (ibind itr f) g

⊢ ibind itr f = Div ⇔ itr = Div ∨ ∃x. itr = ireturn x ∧ f x = Div

⊢ ibind itr f = ireturn v ⇔ ∃v'. itr = ireturn v' ∧ f v' = ireturn v

⊢ ibind itr f = Vis rv g ⇔
  (∃h. itr = Vis rv h ∧ iflat ∘ imap f ∘ h = g) ∨
  ∃x. itr = ireturn x ∧ f x = Vis rv g

⊢ ibind (ireturn itr) f = f itr

⊢ ibind itr ireturn = itr

⊢ ∀P a0.
    ievery P a0 ⇔
    a0 = Div ∨ (∃e. a0 = ireturn e ∧ P e) ∨
    ∃f ov. a0 = Vis ov f ∧ ∀iv. ievery P (f iv)

⊢ ∀P ievery'.
    (∀a0.
       ievery' a0 ⇒
       a0 = Div ∨ (∃e. a0 = ireturn e ∧ P e) ∨
       ∃f ov. a0 = Vis ov f ∧ ∀iv. ievery' (f iv)) ⇒
    ∀a0. ievery' a0 ⇒ ievery P a0

⊢ ∀P. ievery P Div

⊢ ∀P e. P e ⇒ ievery P (ireturn e)

⊢ ∀P. ievery P Div ∧ (∀e. P e ⇒ ievery P (ireturn e)) ∧
      ∀f ov. (∀iv. ievery P (f iv)) ⇒ ievery P (Vis ov f)

⊢ ∀itr. ievery P itr ⇔ ∀rv. iset itr rv ⇒ P rv

⊢ (ievery P Div ⇔ T) ∧ (ievery P (ireturn e) ⇔ P e) ∧
  (ievery P (Vis ov f) ⇔ ∀iv. ievery P (f iv))

⊢ ∀P f ov. (∀iv. ievery P (f iv)) ⇒ ievery P (Vis ov f)

⊢ ∀P a0.
    iexists P a0 ⇔
    (∃e. a0 = ireturn e ∧ P e) ∨
    ∃f ov. a0 = Vis ov f ∧ ∃iv. iexists P (f iv)

⊢ ∀P iexists'.
    (∀e. P e ⇒ iexists' (ireturn e)) ∧
    (∀f ov. (∃iv. iexists' (f iv)) ⇒ iexists' (Vis ov f)) ⇒
    ∀a0. iexists P a0 ⇒ iexists' a0

⊢ ∀P e. P e ⇒ iexists P (ireturn e)

⊢ ∀P. (∀e. P e ⇒ iexists P (ireturn e)) ∧
      ∀f ov. (∃iv. iexists P (f iv)) ⇒ iexists P (Vis ov f)

⊢ iexists P itr ⇔ ∃x. iset itr x ∧ P x

⊢ ∀P iexists'.
    (∀e. P e ⇒ iexists' (ireturn e)) ∧
    (∀f ov. (∃iv. iexists P (f iv) ∧ iexists' (f iv)) ⇒ iexists' (Vis ov f)) ⇒
    ∀a0. iexists P a0 ⇒ iexists' a0

⊢ (iexists P Div ⇔ F) ∧ (iexists P (ireturn e) ⇔ P e) ∧
  (iexists P (Vis ov f) ⇔ ∃iv. iexists P (f iv))

⊢ ∀P f ov. (∃iv. iexists P (f iv)) ⇒ iexists P (Vis ov f)

⊢ ∀a0.
    ifinite a0 ⇔
    (∃e. a0 = ireturn e) ∨ a0 = Div ∨
    ∃f ov. a0 = Vis ov f ∧ ∀iv. ifinite (f iv)

⊢ ifinite Div

⊢ ∀ifinite'.
    (∀e. ifinite' (ireturn e)) ∧ ifinite' Div ∧
    (∀f ov. (∀iv. ifinite' (f iv)) ⇒ ifinite' (Vis ov f)) ⇒
    ∀a0. ifinite a0 ⇒ ifinite' a0

⊢ ∀e. ifinite (ireturn e)

⊢ (∀e. ifinite (ireturn e)) ∧ ifinite Div ∧
  ∀f ov. (∀iv. ifinite (f iv)) ⇒ ifinite (Vis ov f)

⊢ ∀ifinite'.
    (∀e. ifinite' (ireturn e)) ∧ ifinite' Div ∧
    (∀f ov. (∀iv. ifinite (f iv) ∧ ifinite' (f iv)) ⇒ ifinite' (Vis ov f)) ⇒
    ∀a0. ifinite a0 ⇒ ifinite' a0

⊢ ∀f ov. (∀iv. ifinite (f iv)) ⇒ ifinite (Vis ov f)

⊢ iflat Div = Div

⊢ iflat itr = Div ⇔ itr = Div ∨ itr = ireturn Div

⊢ (iflat itr = ireturn rv ⇔ itr = ireturn (ireturn rv)) ∧
  (ireturn rv = iflat itr ⇔ itr = ireturn (ireturn rv))

⊢ iflat itr = Vis ov f ⇔
  (∃g. itr = Vis ov g ∧ iflat ∘ g = f) ∨ itr = ireturn (Vis ov f)

⊢ iflat (ireturn r) = r

⊢ iflat (Vis ov f) = Vis ov (iflat ∘ f)

⊢ imap (f ∘ g) itr = imap f (imap g itr)

⊢ imap g Div = Div

⊢ (imap g itr = Div ⇔ itr = Div) ∧ (Div = imap g itr ⇔ itr = Div)

⊢ ireturn r = imap g itr ⇔ ∃x. itr = ireturn x ∧ g x = r

⊢ Vis rv f = imap g itr ⇔ ∃h. itr = Vis rv h ∧ imap g ∘ h = f

⊢ imap (λx. x) itr = itr

⊢ imap g (ireturn rv) = ireturn (g rv)

⊢ imap f (Vis ov g) = Vis ov (imap f ∘ g)

⊢ ∀a0 a1.
    iset a0 a1 ⇔ a0 = ireturn a1 ∨ ∃f i ov. a0 = Vis ov f ∧ iset (f i) a1

⊢ ∀itr e. iset (iflat itr) e ⇔ ∃t0. iset itr t0 ∧ iset t0 e

⊢ ∀itr e. iset (iflat itr) e ⇒ ∃t0. iset itr t0 ∧ iset t0 e

⊢ ∀itr t0 e. iset itr t0 ∧ iset t0 e ⇒ iset (iflat itr) e

⊢ iset itree e ⇔ ∃p. at_path itree p e

⊢ ∀iset'.
    (∀e. iset' (ireturn e) e) ∧
    (∀e f i ov. iset' (f i) e ⇒ iset' (Vis ov f) e) ⇒
    ∀a0 a1. iset a0 a1 ⇒ iset' a0 a1

⊢ iset (imap f itr) = IMAGE f (iset itr)

⊢ ∀itr x. iset (imap f itr) x ⇒ ∃y. x = f y ∧ iset itr y

⊢ ∀itr. iset itr y ⇒ iset (imap f itr) (f y)

⊢ ∀e. iset (ireturn e) e

⊢ (∀e. iset (ireturn e) e) ∧ ∀e f i ov. iset (f i) e ⇒ iset (Vis ov f) e

⊢ ∀iset'.
    (∀e. iset' (ireturn e) e) ∧
    (∀e f i ov. iset (f i) e ∧ iset' (f i) e ⇒ iset' (Vis ov f) e) ⇒
    ∀a0 a1. iset a0 a1 ⇒ iset' a0 a1

⊢ (iset (ireturn e) e' ⇔ e = e') ∧ (iset Div e ⇔ F) ∧
  (iset (Vis ov f) e ⇔ ∃i. iset (f i) e)

⊢ iset itr elem ⇒ ∃n. iset (itruncate n itr) elem

⊢ ∀e f i ov. iset (f i) e ⇒ iset (Vis ov f) e

⊢ (∀x y. ireturn x = ireturn y ⇔ x = y) ∧
  ∀x f y g. Vis x f = Vis y g ⇔ x = y ∧ f = g

⊢ itree_CASE (ireturn r) ret div vis = ret r ∧
  itree_CASE Div ret div vis = div ∧
  itree_CASE (Vis a g) ret div vis = vis a g

⊢ ∀M M' ret div vis ret' div' vis'.
    M = M' ∧ (∀x. M' = ireturn x ⇒ ret x = ret' x) ∧
    (M' = Div ⇒ div = div') ∧ (∀a g. M' = Vis a g ⇒ vis a g = vis' a g) ⇒
    itree_CASE M ret div vis = itree_CASE M' ret' div' vis'

⊢ ∀f. f (itree_CASE t ret div vis) ⇔
      (∃r. t = ireturn r ∧ f (ret r)) ∨ t = Div ∧ f div ∨
      ∃a g. t = Vis a g ∧ f (vis a g)

⊢ itree_CASE t ret div vis = v ⇔
  (∃r. t = ireturn r ∧ ret r = v) ∨ t = Div ∧ div = v ∨
  ∃a g. t = Vis a g ∧ vis a g = v

⊢ ∀t1 t2.
    t1 = t2 ⇔
    ∃R. R t1 t2 ∧ (∀x t. R (ireturn x) t ⇒ t = ireturn x) ∧
        (∀t. R Div t ⇒ t = Div) ∧
        ∀a f t. R (Vis a f) t ⇒ ∃b g. t = Vis a g ∧ ∀s. R (f s) (g s)

⊢ ∀t. (∃x. t = ireturn x) ∨ t = Div ∨ ∃a g. t = Vis a g

⊢ (∀x. ireturn x ≠ Div) ∧ (∀x g e. ireturn x ≠ Vis e g) ∧
  ∀g e. Div ≠ Vis e g

⊢ (∀a a'. Event a = Event a' ⇔ a = a') ∧
  ∀a a'. Return a = Return a' ⇔ a = a'

⊢ ∀f0 f1 f2. ∃fn.
    (∀a. fn (Event a) = f0 a) ∧ (∀a. fn (Return a) = f1 a) ∧ fn Stuck = f2

⊢ ∀M M' f f1 v.
    M = M' ∧ (∀a. M' = Event a ⇒ f a = f' a) ∧
    (∀a. M' = Return a ⇒ f1 a = f1' a) ∧ (M' = Stuck ⇒ v = v') ⇒
    itree_el_CASE M f f1 v = itree_el_CASE M' f' f1' v'

⊢ itree_el_CASE x f f1 v = v' ⇔
  (∃e. x = Event e ∧ f e = v') ∨ (∃r. x = Return r ∧ f1 r = v') ∨
  x = Stuck ∧ v = v'

⊢ itree_el (ireturn r) [] = Return r ∧ itree_el Div [] = Stuck ∧
  itree_el (Vis e g) [] = Event e ∧
  itree_el (ireturn r) (a::ns) = Return ARB ∧
  itree_el Div (a::ns) = Return ARB ∧
  itree_el (Vis e g) (a::ns) = itree_el (g a) ns

⊢ (∀a' a. Event a ≠ Return a') ∧ (∀a. Event a ≠ Stuck) ∧
  ∀a. Return a ≠ Stuck

⊢ ∀t1 t2. t1 = t2 ⇔ ∀path. itree_el t1 path = itree_el t2 path

⊢ ∀P. (∀e. P (Event e)) ∧ (∀r. P (Return r)) ∧ P Stuck ⇒ ∀i. P i

⊢ ∀ii. (∃e. ii = Event e) ∨ (∃r. ii = Return r) ∨ ii = Stuck

⊢ (∀a a'. Ret' a = Ret' a' ⇔ a = a') ∧
  ∀a0 a1 a0' a1'. Vis' a0 a1 = Vis' a0' a1' ⇔ a0 = a0' ∧ a1 = a1'

⊢ ∀f0 f1 f2. ∃fn.
    (∀a. fn (Ret' a) = f0 a) ∧ fn Div' = f1 ∧
    ∀a0 a1. fn (Vis' a0 a1) = f2 a0 a1

⊢ ∀M M' f v f1.
    M = M' ∧ (∀a. M' = Ret' a ⇒ f a = f' a) ∧ (M' = Div' ⇒ v = v') ∧
    (∀a0 a1. M' = Vis' a0 a1 ⇒ f1 a0 a1 = f1' a0 a1) ⇒
    itree_next_CASE M f v f1 = itree_next_CASE M' f' v' f1'

⊢ itree_next_CASE x f v f1 = v' ⇔
  (∃r. x = Ret' r ∧ f r = v') ∨ x = Div' ∧ v = v' ∨
  ∃e f'. x = Vis' e f' ∧ f1 e f' = v'

⊢ (∀a. Ret' a ≠ Div') ∧ (∀a1 a0 a. Ret' a ≠ Vis' a0 a1) ∧
  ∀a1 a0. Div' ≠ Vis' a0 a1

⊢ ∀P. (∀r. P (Ret' r)) ∧ P Div' ∧ (∀e f. P (Vis' e f)) ⇒ ∀i. P i

⊢ ∀ii. (∃r. ii = Ret' r) ∨ ii = Div' ∨ ∃e f. ii = Vis' e f

⊢ itree_unfold f seed =
  case f seed of
    Ret' r => ireturn r
  | Div' => Div
  | Vis' e g => Vis e (itree_unfold f ∘ g)

⊢ itree_unfold_err f (rel,err_f,err) seed =
  case f seed of
    Ret' r => ireturn r
  | Div' => Div
  | Vis' e g =>
    Vis e
      (λa.
           case a of
             INL x => ireturn (err_f e x)
           | INR y =>
             if rel e y then itree_unfold_err f (rel,err_f,err) (g y)
             else ireturn (err e))

⊢ (∀itr. itruncate 0 itr = Div) ∧
  (∀v2. itruncate (NUMERAL (BIT1 v2)) Div = Div) ∧
  (∀v2. itruncate (NUMERAL (BIT2 v2)) Div = Div) ∧
  (∀v3 rv. itruncate (NUMERAL (BIT1 v3)) (ireturn rv) = ireturn rv) ∧
  (∀v3 rv. itruncate (NUMERAL (BIT2 v3)) (ireturn rv) = ireturn rv) ∧
  (∀v4 ov f.
     itruncate (NUMERAL (BIT1 v4)) (Vis ov f) =
     Vis ov (λx. itruncate (NUMERAL (BIT1 v4) − 1) (f x))) ∧
  ∀v4 ov f.
    itruncate (NUMERAL (BIT2 v4)) (Vis ov f) =
    Vis ov (λx. itruncate (NUMERAL (BIT2 v4) − 1) (f x))

⊢ (∀itr. itruncate 0 itr = Div) ∧ (∀v2. itruncate (SUC v2) Div = Div) ∧
  (∀v3 rv. itruncate (SUC v3) (ireturn rv) = ireturn rv) ∧
  ∀v4 ov f.
    itruncate (SUC v4) (Vis ov f) =
    Vis ov (λx. itruncate (SUC v4 − 1) (f x))

⊢ ∀itr. itruncate n itr = itr ⇒ ifinite itr

⊢ ∀P. (∀itr. P 0 itr) ∧ (∀v2. P (SUC v2) Div) ∧
      (∀v3 rv. P (SUC v3) (ireturn rv)) ∧
      (∀v4 ov f. (∀x. P (SUC v4 − 1) (f x)) ⇒ P (SUC v4) (Vis ov f)) ⇒
      ∀v v1. P v v1

⊢ ∀n. itruncate n itr = ireturn r ⇔ itr = ireturn r ∧ n ≠ 0

⊢ ¬ievery P itr ⇔ iexists (λx. ¬P x) itr