Changeset 411 for Deliverables/D3.1


Ignore:
Timestamp:
Dec 13, 2010, 5:11:00 PM (9 years ago)
Author:
campbell
Message:

Note associativity of IOMonad, subject to extensionality.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/IOMonad.ma

    r366 r411  
    177177
    178178
    179 (* TODO: is there a way to prove this without extensionality?
     179(* Is there a way to prove this without extensionality? *)
    180180
    181 nlemma bind_assoc_r: ∀A,B,C,e,f,g.
    182   bindIO B C (bindIO A B e f) g = bindIO A C e (λx.bindIO B C (f x) g).
    183 #A B C e f g; nelim e;
    184 ##[ #fn args k IH; nwhd in ⊢ (???%);
    185 nnormalize;
    186 *)
     181nlemma bind_assoc_r: ∀O,I,A,B,C,e,f,g.
     182  ∀ext:(∀T1,T2:Type.∀f,f':T1 → T2.(∀x.f x = f' x) → f = f').
     183  bindIO O I B C (bindIO O I A B e f) g = bindIO O I A C e (λx.bindIO O I B C (f x) g).
     184#O I A B C e f g ext; nelim e;
     185##[ #o k IH; nwhd in ⊢ (??%%); napply eq_f;
     186    napply ext; napply IH;
     187##| #v; napply refl;
     188##| napply refl;
     189##] nqed.
     190
    187191
    188192nlemma extract_subset_pair_io: ∀O,I,A,B,C,P. ∀e:{e:A×B | P e}. ∀Q:A→B→IO O I C. ∀R:C→Prop.
Note: See TracChangeset for help on using the changeset viewer.