Changeset 251 for C-semantics/IOMonad.ma


Ignore:
Timestamp:
Nov 22, 2010, 2:40:26 PM (9 years ago)
Author:
campbell
Message:

Separate out soundness of exec_expr from definition.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/IOMonad.ma

    r211 r251  
    2626ndefinition err_to_io : ∀I,O,T. res T → IO I O T ≝
    2727λI,O,T,v. match v with [ OK v' ⇒ Value I O T v' | Error ⇒ Wrong I O T ].
    28 (*ncoercion err_to_io : ∀I,O,A.∀c:res A.IO I O A ≝ err_to_io on _c:res ? to IO ???.*)
     28ncoercion err_to_io : ∀I,O,A.∀c:res A.IO I O A ≝ err_to_io on _c:res ? to IO ???.
    2929ndefinition err_to_io_sig : ∀I,O,T.∀P:T → Prop. res (sigma T P) → IO I O (sigma T P) ≝
    3030λI,O,T,P,v. match v with [ OK v' ⇒ Value I O (sigma T P) v' | Error ⇒ Wrong I O (sigma T P) ].
    31 ncoercion err_to_io_sig : ∀I,O,A.∀P:A → Prop.∀c:res (sigma A P).IO I O (sigma A P) ≝ err_to_io_sig on _c:res (sigma ??) to IO ?? (sigma ??).
     31(*ncoercion err_to_io_sig : ∀I,O,A.∀P:A → Prop.∀c:res (sigma A P).IO I O (sigma A P) ≝ err_to_io_sig on _c:res (sigma ??) to IO ?? (sigma ??).*)
    3232
    3333
     
    126126nqed.
    127127
     128nlemma res_bindIO_OK: ∀I,O,A,B. ∀P:B → Prop. ∀e:res A. ∀f: A → IO I O B.
     129  (∀v:A. e = OK A v → P_io I O ? P (f v)) →
     130  P_io I O ? P (bindIO I O A B e f).
     131#I O A B P e; nelim e; //; #v f H; napply H; //;
     132nqed.
     133
     134nlemma res_bindIO2_OK: ∀I,O,A,B,C. ∀P:C → Prop. ∀e:res (A×B). ∀f: A → B → IO I O C.
     135  (∀vA:A.∀vB:B. e = OK (A×B) 〈vA,vB〉 → P_io I O ? P (f vA vB)) →
     136  P_io I O ? P (bindIO2 I O A B C e f).
     137#I O A B C P e; nelim e; //; #v; ncases v; #vA vB f H; napply H; //;
     138nqed.
     139
    128140nlemma bindIO_OK: ∀I,O,A,B. ∀P:B → Prop. ∀e:IO I O A. ∀f: A → IO I O B.
    129141  (∀v:A. P_io I O ? P (f v)) →
Note: See TracChangeset for help on using the changeset viewer.