include "utilities/monad.ma". inductive bind_new (B : Type[0]) (E : Type[0]) : Type[0] ≝ | bret : E → bind_new B E | bnew : (B → bind_new B E) → bind_new B E. interpretation "new bind_new" 'new f = (bnew ?? f). notation > "ν list1 (ident x opt ( : ty)) sep , 'in' f" with precedence 48 for @{ \${ fold right @{\$f} rec acc @{ \${default @{'new (λ\${ident x} : \$ty.\$acc)} @{'new (λ\${ident x}.\$acc)} }} }}. notation < "hvbox(mstyle color #0000ff (ν) ident i : ty \nbsp 'in' \nbsp break p)" with precedence 48 for @{'new (λ\${ident i} : \$ty. \$p) }. let rec bnews B E n (f : list B → bind_new B E) on n : bind_new B E ≝ match n with [ O ⇒ f [ ] | S x ⇒ νy in bnews … x (λl. f (y :: l)) ]. let rec bnews_strong B E n (f : ∀l:list B.|l| = n → bind_new B E) on n : bind_new B E ≝ match n return λx.x = n → bind_new B E with [ O ⇒ λprf.f [ ] ? | S n' ⇒ λprf.νx in bnews_strong … n' (λl',prf'. f (x :: l') ?) ] (refl …). normalize // qed. interpretation "iterated new" 'unews n f = (bnews ?? n f). interpretation "iterated new strong" 'sunews n f = (bnews_strong ?? n f). notation > "νν n 'as' ident l opt('with' ident EQ) 'in' f" with precedence 47 for \${default @{ 'sunews \$n (λ\${ident l}.λ\${ident EQ}.\$f) } @{ 'unews \$n (λ\${ident l}.\$f)} }. notation > "νν n 'as' ident l : ty opt('with' ident EQ) 'in' f" with precedence 47 for \${default @{ 'sunews \$n (λ\${ident l}:\$ty.λ\${ident EQ}.\$f) } @{ 'unews \$n (λ\${ident l}:\$ty.\$f)} }. notation < "hvbox(νν n \nbsp 'as' ident l \nbsp 'with' \nbsp ident EQ : tyeq \nbsp 'in' \nbsp break f)" with precedence 47 for @{ 'sunews \$n (λ\${ident l} : \$ty.λ\${ident EQ} : \$tyeq.\$f) }. notation < "hvbox(νν n \nbsp 'as' ident l \nbsp 'in' \nbsp break f)" with precedence 47 for @{ 'unews \$n (λ\${ident l} : \$ty.\$f) }. axiom bnew_proper : ∀B,E,f,g. (∀x. f x = g x) → bnew B E f = bnew B E g. let rec bbind A B C (l : bind_new A B) (f : B → bind_new A C) on l : bind_new A C ≝ match l with [ bret x ⇒ f x | bnew n ⇒ bnew … (λx. bbind … (n x) f) ]. definition BindNew ≝ λB.MakeMonadProps (* the monad *) (bind_new B) (* return *) (λX,x.bret … x) (* bind *) (bbind B) ????. [ (* ret_bind *) // |(* bind_ret *) #X#m elim m normalize [//] #l' #Hi @bnew_proper // |(* bind_bind *) #X#Y#Z#m#f#g elim m normalize [// |(* case bnew *) #l #Hi @bnew_proper // ] | #X#Y #m #f #g #H elim m normalize [ /2/ ] #k #IH @bnew_proper #x >IH % ] qed. unification hint 0 ≔ B, X; N ≟ BindNew B, M ≟ max_def N (*--------------------------------------------*) ⊢ bind_new B X ≡ monad M X. include "utilities/state.ma". let rec bcompile U R E (fresh : state_monad U R) (b : bind_new R E) on b : state_monad U E ≝ match b with [ bret x ⇒ return x | bnew f ⇒ ! r ← fresh ; bcompile … fresh (f r) ]. theorem bcompile_bbind : ∀U,R,E,F.∀fresh : state_monad U R.∀ b : bind_new R E.∀f : E → bind_new R F. bcompile … fresh (! x ← b ; f x) ≅ ! x ← bcompile … fresh b ; bcompile … fresh (f x). #U#R#E#F#fresh#b#f elim b normalize [ // | #bf #Hi #u0 @pair_elim normalize #u #r >(Hi r) -Hi // ] qed.