Changeset 252 for C-semantics/IOMonad.ma


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

Separate out soundness of exec_step from definition.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/IOMonad.ma

    r251 r252  
    147147##] nqed.
    148148
     149nlemma bindIO2_OK: ∀I,O,A,B,C. ∀P:C → Prop. ∀e:IO I O (A×B). ∀f: A → B → IO I O C.
     150  (∀v1:A.∀v2:B. P_io I O ? P (f v1 v2)) →
     151  P_io I O ? P (bindIO2 I O A B C e f).
     152#I O A B C P e; nelim e;
     153##[ #out k IH; #f H; nwhd; #res; napply IH; //;
     154##| #v; ncases v; #v1 v2 f H; napply H;
     155##| //;
     156##] nqed.
     157
     158nlemma P_bindIO_OK: ∀I,O,A,B. ∀P':A → Prop. ∀P:B → Prop. ∀e:IO I O A. ∀f: A → IO I O B.
     159  P_io … P' e →
     160  (∀v:A. P' v → P_io I O ? P (f v)) →
     161  P_io I O ? P (bindIO I O A B e f).
     162#I O A B P' P e; nelim e;
     163##[ #out k IH f He H; nwhd in He ⊢ %; #res; napply IH; /2/;
     164##| #v f He H; napply H; napply He;
     165##| //;
     166##] nqed.
     167
     168nlemma P_bindIO2_OK: ∀I,O,A,B,C. ∀P':A×B → Prop. ∀P:C → Prop. ∀e:IO I O (A×B). ∀f: A → B → IO I O C.
     169  P_io … P' e →
     170  (∀v1:A.∀v2:B. P' 〈v1,v2〉 → P_io I O ? P (f v1 v2)) →
     171  P_io I O ? P (bindIO2 I O A B C e f).
     172#I O A B C P' P e; nelim e;
     173##[ #out k IH f He H; nwhd in He ⊢ %; #res; napply IH; /2/;
     174##| #v; ncases v; #v1 v2 f He H; napply H; napply He;
     175##| //;
     176##] nqed.
     177
     178
    149179(* TODO: is there a way to prove this without extensionality?
    150180
Note: See TracChangeset for help on using the changeset viewer.