Changeset 211 for C-semantics/IOMonad.ma


Ignore:
Timestamp:
Nov 3, 2010, 12:41:40 PM (9 years ago)
Author:
campbell
Message:

Make io_inject definition more straightforward.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/IOMonad.ma

    r208 r211  
    6565
    6666nlet rec io_inject_0 (I,O,A:Type) (P:A → Prop) (a:IO I O A) (p:P_io I O A P a) on a : IO I O (sigma A P) ≝
    67 (match a return λa'.a=a' → ? with
     67(match a return λa'.P_io I O A P a' → ? with
    6868 [ Wrong ⇒ λ_. Wrong I O ?
    69  | Value c ⇒ λe2. Value ??? (sig_intro A P c ?)
    70  | Interact out k ⇒ λe2. Interact ??? out (λv. io_inject_0 I O A P (k v) ?)
    71  ]) (refl ? a).
    72 nrewrite > e2 in p; nwhd in ⊢ (% → ?); //;
    73 nqed.
     69 | Value c ⇒ λp'. Value ??? (sig_intro A P c p')
     70 | Interact out k ⇒ λp'. Interact ??? out (λv. io_inject_0 I O A P (k v) (p' v))
     71 ]) p.
    7472
    7573ndefinition io_inject : ∀I,O,A.∀P:A → Prop.∀a:option (IO I O A).∀p:P_to_P_option_io I O A P a.IO I O (sigma A P) ≝
    7674  λI,O,A.λP:A → Prop.λa:option (IO I O A).λp:P_to_P_option_io I O A P a.
    77   (match a return λa'.a=a' → IO I O (sigma A P) with
    78    [ None ⇒ λe1.?
    79    | Some b ⇒ λe1. io_inject_0 I O A P b ?
    80    ]) (refl ? a).
    81 ##[ nrewrite > e1 in p; nnormalize; *;
    82 ##| nrewrite > e1 in p; nnormalize; //
    83 ##] nqed.
     75  (match a return λa'.P_to_P_option_io I O A P a' → IO I O (sigma A P) with
     76   [ None ⇒ λp'.?
     77   | Some b ⇒ λp'. io_inject_0 I O A P b p'
     78   ]) p.
     79nelim p'; nqed.
    8480
    8581nlet rec io_eject (I,O,A:Type) (P: A → Prop) (a:IO I O (sigma A P)) on a : IO I O A ≝
Note: See TracChangeset for help on using the changeset viewer.