Changeset 1949 for src/common/IOMonad.ma


Ignore:
Timestamp:
May 15, 2012, 5:51:25 PM (8 years ago)
Author:
tranquil
Message:
  • lemma trace rel to eq flatten trace
  • some more properties of generic monad relations and predicates
  • removed 'iff notation from extralib as already there
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/IOMonad.ma

    r1930 r1949  
    4646
    4747include "hints_declaration.ma".
    48 
     48alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
    4949unification hint 0 ≔ O, I, T;
    5050  N ≟ IOMonad O I, M ≟ max_def N
     
    5353.
    5454
     55let rec rel_io O I A B (Perr : relation errmsg) (P : A → B → Prop) (v1 : IO O I A)
     56  (v2 : IO O I B) on v1 : Prop ≝
     57  match v1 with
     58  [ Value x ⇒
     59    match v2 with
     60    [ Value y ⇒
     61      P x y
     62    | _ ⇒ False
     63    ]
     64  | Wrong e1 ⇒
     65    match v2 with
     66    [ Wrong e2 ⇒ Perr e1 e2
     67    | _ ⇒ False
     68    ]
     69  | Interact o1 f1 ⇒
     70    match v2 with
     71    [ Interact o2 f2 ⇒
     72      ∃prf:o1 = o2.∀i.rel_io … Perr P (f1 i) (f2 ?)
     73    | _ ⇒ False
     74    ]
     75  ]. <prf @i qed.
     76
     77definition IORel ≝ λO,I,Perr.
     78  mk_MonadRel (IOMonad O I) (IOMonad O I)
     79    (λA,B.rel_io O I A B Perr)
     80    ???.
     81[//
     82|#X #Y #Z #W #relin #relout #m elim m
     83  [ #o #f #IH * [#o' #f' | #v | #e] * #EQ destruct(EQ) #G
     84    #f1 #f2 #G' whd %{(refl …)} #i
     85    @(IH … (G i) f1 f2 G')
     86  | #v * [#o #f * | #v' | #e *]
     87    #Pvv' #f #g #H normalize @H @Pvv'
     88  | #e1 * [#o #f * | #v' *| #e2] //
     89  ]
     90| #X #Y #P #Q #H #m elim m [#o #f #IH | #v | #e] *
     91  [1,4,7: #o' #f' [2,3: *]
     92    normalize * #prf destruct(prf) normalize #G
     93    % [%] normalize #i @IH @G
     94  |2,5,8: #v' [1,3: *]
     95    @H
     96  |*: #e' [1,2: *] //
     97  ]
     98]
     99qed.
     100
     101lemma IORel_refl : ∀O,I,Perr.reflexive ? Perr → ∀X,rel.reflexive X rel →
     102  reflexive ? (m_rel ?? (IORel O I Perr) ?? rel).
     103#O #I #Perr #G #X #rel #H #m elim m
     104[ #o #f #IH whd %[%] #i normalize @IH
     105| #v @H
     106| #e @G
     107]
     108qed.
     109
     110lemma IORel_transitive : ∀O,I,Perr1,Perr2,Perr3.
     111  (∀e1,e2,e3.Perr1 e1 e2 → Perr2 e2 e3 → Perr3 e1 e3) →
     112  ∀X,Y,Z,rel1,rel2,rel3.
     113  (∀x : X.∀y : Y.∀z : Z.rel1 x y → rel2 y z → rel3 x z) →
     114  ∀m,n,o.
     115  m_rel ?? (IORel O I Perr1) … rel1 m n →
     116  m_rel ?? (IORel O I Perr2) … rel2 n o →
     117  m_rel ?? (IORel O I Perr3) … rel3 m o.
     118#O #I #Perr1 #Perr2 #Perr3 #Herr #X #Y #Z #rel1 #rel2 #rel3 #H #m elim m
     119[ #o #f #IH * [#o' #f' * [#o'' #f'' | #v #_ * | #e #_ * ] | #v #x * | #e #x * ]
     120  normalize * #EQ #H1 * #EQ' #H2 destruct %[%] normalize #i @(IH ? (f' i)) //
     121| #v * [#o #f #x * | #v' * [#o #f #_ * | #v'' |#e #_ *] | #e #x *]
     122  @H
     123| #e * [#o #f #x * | #v #x * | #e' * [#o #f #_ * | #v #_ * | #e'']] @Herr
     124]
     125qed.
     126
     127
     128lemma rel_io_eq : ∀O,I,A.∀m,n:IO O I A.m = n → m_rel ?? (IORel O I (eq ?)) … (eq ?) m n.
     129#O#I#A#m#n#EQ >EQ @IORel_refl //
     130qed.
     131
     132lemma eq_rel_io : ∀O,I,A.∀m,n:IO O I A.m_rel ?? (IORel O I (eq ?)) … (eq ?) m n → m = n.
     133#O#I#A#m elim m
     134[ #o #f #IH * [#o' #f' | #v * | #e * ]
     135  normalize * #EQ #H destruct @interact_proper #i @IH @H
     136| #v * [#o #f * | #v' | #e *]
     137| #e * [#o #f * | #v * | #e']
     138] #EQ >EQ %
     139qed.
     140
     141coercion rel_io_to_eq nocomposites : ∀O,I,A,m,n.∀prf : m = n.
     142m_rel ?? (IORel O I (eq ?)) A A (eq ?) m n ≝ rel_io_eq on
     143  _prf : eq (IO ???) ?? to m_rel ?? (IORel ?? (eq ?)) ?? (eq ?) ??.
     144
     145coercion eq_to_rel_io nocomposites : ∀O,I,A,m,n.∀prf :
     146m_rel ?? (IORel O I (eq ?)) A A (eq ?) m n.m = n ≝ eq_rel_io on
     147  _prf : m_rel ?? (IORel ?? (eq ?)) ?? (eq ?) ?? to eq (IO ???) ??.
     148
     149
     150let rec pred_io O I A (Perr : predicate errmsg) (P : A → Prop) (v : IO O I A) on v : Prop ≝
     151  match v with
     152  [ Value x ⇒ P x
     153  | Wrong e ⇒ Perr e
     154  | Interact o f ⇒ ∀i.pred_io … Perr P (f i)
     155  ].
     156
     157let rec pred_io_inject O I A Perr P (a : IO O I A)
     158  on a : pred_io O I A Perr P a → IO O I (Σx.P x) ≝
     159  match a return λx.pred_io O I A Perr P x → IO O I (Σx.P x) with
     160  [ Interact o f ⇒ λprf.
     161    Interact … o (λx.pred_io_inject … Perr P (f x) (prf x))
     162  | Value x ⇒ λprf.return «x, prf»
     163  | Wrong e ⇒ λ_.Wrong … e
     164  ].
     165
     166definition IOPred ≝ λO,I,Perr.
     167  mk_MonadPred (IOMonad O I)
     168    (λA.pred_io O I A Perr)
     169    (λA,P,a_sig.match a_sig with [ mk_Sig a prf ⇒ pred_io_inject O I A Perr P a prf ])
     170    ????.
     171[//
     172|#X #Y #relin #relout #m elim m
     173  [ #o #f #IH whd in ⊢ (%→?); #H
     174    #f #G whd #i
     175    @(IH … (H i) f G)
     176  | #v #Pv #f #H normalize @H @Pv
     177  | #e //
     178  ]
     179| #X #P #Q #H #m elim m
     180  [#o #f #IH #H #i @IH @H
     181  | #v @H
     182  | #e //
     183  ]
     184|#X #P * #m elim m
     185  [ #o #f #IH whd in ⊢ (%→?); #H
     186    change with (Interact ?????) in ⊢ (???%);
     187    @interact_proper #i
     188    @(IH i (H i))
     189  |*: //
     190]
     191qed.
     192
     193unification hint 0 ≔ O, I, Perr, A, P, v;
     194M ≟ IOMonad O I, Pr ≟ IOPred O I Perr
     195⊢ pred_io O I A Perr P v ≡ m_pred M Pr A P v.
    55196
    56197definition err_to_io : ∀O,I,T. res T → IO O I T ≝
     
    58199
    59200coercion err_to_io : ∀O,I,A.∀c:res A.IO O I A ≝ err_to_io on _c:res ? to IO ???.
     201
     202lemma res_io_pred : ∀O,I,A,Perr,P.∀m : res A.pred_res … Perr P m → pred_io O I ? Perr P m.
     203#O #I #A #Perr #P * /2/ qed.
     204
     205lemma io_res_pred : ∀O,I,A,Perr,P.∀m : res A.pred_io O I ? Perr P m → pred_res ? Perr P m.
     206#O #I #A #Perr #P * /2/ qed.
    60207
    61208definition err_to_io_sig : ∀O,I,T.∀P:T → Prop. res (Sig T P) → IO O I (Sig T P) ≝
Note: See TracChangeset for help on using the changeset viewer.