Changeset 1949 for src/common


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
Location:
src/common
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/common/Errors.ma

    r1882 r1949  
    66include "utilities/monad.ma".
    77include "utilities/option.ma".
    8 
    9 (* first, generic exception monad *)
    10 
    11 inductive except (E : Type[0]) (X : Type[0]) : Type[0] ≝
    12   | raise : E → except E X
    13   | success : X → except E X.
    14 
    15 definition Except ≝ λE.MakeMonadProps
    16   (except E)
    17   (success E)
    18   (λX,Y,m,f.match m with [raise e ⇒ raise … e | success x ⇒ f x])
    19   ????.
    20 //
    21 [ #X * #x %
    22 | #X#Y#Z * #x#f#g %
    23 | #X#Y normalize * #x #f #g #H // normalize @H
    24 ]
    25 qed.
    26 
    27 unification hint 0 ≔ E,X;
    28 O ≟ Except E, N ≟ max_def O
    29 (*--------------------------------------*) ⊢
    30 except E X ≡ monad N X.
    31 
    32 definition try_catch : ∀E,X.except E X → (E → X) → X ≝
    33   λE,X,m,f.match m with
    34   [ success x ⇒ x
    35   | raise e ⇒ f e
    36   ].
    37 
    38 interpretation "exception try catch" 'trycatch e f = (try_catch ?? e f).
    39 
    40 definition except_elim : ∀E,X.∀m : except E X.∀P : ? → Prop.
    41   (∀x.m = success ?? x → P (success ?? x)) →
    42   (∀e.m = raise ?? e → P (raise ?? e)) →
    43   P m.
    44 #E #X * /2/
    45 qed.
    46 
    47 definition except_success ≝ λE,X.λm : except E X.
    48   match m with [success _ ⇒ True | _ ⇒ False].
    49 
    50 definition except_safe ≝
    51   λE,X.λm : except E X.
    52     match m return λx.except_success ?? x → X with
    53     [ success y ⇒ λ_.y
    54     | _ ⇒ λprf.match prf in False with []
    55     ].
    56 
    57 definition Except_P ≝ λE.λP_e : E → Prop.mk_MonadPred (Except E)
    58   (λX,P,m. Try ! x ← m ; return P x catch e ⇒ P_e e) ???.
    59 [ //
    60 | #X#Y #P1 #P2 * #x normalize /2/
    61 | #X #P #Q #H * #y normalize /2/
    62 ]
    63 qed.
    64 
    65 definition except_P ≝ λE,P_e.m_pred … (Except_P E P_e).
    66 
    67 definition except_All : ∀E,X.(X → Prop) → except E X → Prop ≝
    68   λE : Type[0].except_P E (λe.True).
    69 
    70 definition except_Exists : ∀E,X.(X → Prop) → except E X → Prop ≝
    71   λE : Type[0].except_P E (λe.False).
    72 
    73 definition except_rel ≝ λE,F.λrel_e : E → F → Prop.mk_MonadRel (Except E) (Except F)
    74   (λX,Y,rel,m,n.
    75     match m with
    76     [ success x ⇒ match n with [success y ⇒ rel x y | _ ⇒ False]
    77     | raise e ⇒ match n with [raise f ⇒ rel_e e f | _ ⇒ False]
    78     ]) ???.
    79 [ //
    80 |*: #X#Y[#Z#W] #rel1 #rel2 [2: #H] * #x * #y normalize /2/ *
    81 ]
    82 qed.
    838
    849(* * Error reporting and the error monad. *)
     
    13156
    13257include "hints_declaration.ma".
     58alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
    13359unification hint 0 ≔ X;
    13460N ≟ max_def Res
  • 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) ≝
  • src/common/Identifiers.ma

    r1928 r1949  
    8080@(eqb_elim x y P) [ /2 by / | * #H @F % #E destruct /2 by / ]
    8181qed.
    82    
     82
     83include "basics/deqsets.ma".
     84definition Deq_identifier : String → DeqSet ≝ λtag.
     85  mk_DeqSet (identifier tag) (eq_identifier tag) ?.
     86#x#y @eq_identifier_elim /2 by conj/ * #H % [#ABS destruct(ABS) | #G elim (H G)]
     87qed.
     88
     89unification hint 0 ≔ tag; D ≟ Deq_identifier tag
     90(*-----------------------------------------------------*)⊢
     91identifier tag ≡ carr D.
     92
    8393definition word_of_identifier ≝
    8494  λt.
  • src/common/StructuredTraces.ma

    r1944 r1949  
    412412  match tal1 with
    413413  [ tal_base_not_return st1 st1' _ _ _ ⇒
     414    fl2 = doesnt_end_with_ret ∧
    414415    ∃st2mid,taa,H,G,K.
    415416    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
    416417      (tal_base_not_return ? st2mid st2' H G K)
    417418  | tal_base_return st1 st1' _ _ ⇒
     419    fl2 = ends_with_ret ∧
    418420    ∃st2mid,taa,H,G.
    419421    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
    420422      (tal_base_return ? st2mid st2' H G)
    421423  | tal_base_call st1 st1' st1'' _ _ _ tlr1 _ ⇒
     424    fl2 = doesnt_end_with_ret ∧
    422425    ∃st2mid,taa,st2mid',H,G,K,tlr2,L.
    423426    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
     
    433436  ].
    434437
    435 let rec as_compute_cost_trace_label_label
     438let rec flatten_trace_label_label
    436439  (S: abstract_status) (trace_ends_flag: trace_ends_with_ret)
    437440    (start_status: S) (final_status: S)
    438      
    439441      (the_trace: trace_label_label S trace_ends_flag start_status final_status)
    440442        on the_trace: list (Σl: costlabel. ∃s. as_label S s = Some … l) ≝
     
    447449        ] labelled_proof
    448450      in
    449         (mk_Sig … label ?)::as_compute_cost_trace_any_label S ends_flag initial final given_trace
    450   ]
    451 and as_compute_cost_trace_any_label
     451        (mk_Sig … label ?)::flatten_trace_any_label S ends_flag initial final given_trace
     452  ]
     453and flatten_trace_any_label
    452454  (S: abstract_status) (trace_ends_flag: trace_ends_with_ret)
    453455    (start_status: S) (final_status: S)
     
    457459  [ tal_base_not_return the_status _ _ _ _ ⇒ [ ]
    458460  | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒
    459       as_compute_cost_trace_label_return … call_trace
     461      flatten_trace_label_return … call_trace
    460462  | tal_base_return the_status _ _ _ ⇒ [ ]
    461463  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
    462464    _ _ _ call_trace _ final_trace ⇒
    463     let call_cost_trace ≝ as_compute_cost_trace_label_return … call_trace in
    464     let final_cost_trace ≝ as_compute_cost_trace_any_label … end_flag … final_trace in
     465    let call_cost_trace ≝ flatten_trace_label_return … call_trace in
     466    let final_cost_trace ≝ flatten_trace_any_label … end_flag … final_trace in
    465467        call_cost_trace @ final_cost_trace
    466468  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
    467       as_compute_cost_trace_any_label … tail_trace
    468   ]
    469 and as_compute_cost_trace_label_return
     469      flatten_trace_any_label … tail_trace
     470  ]
     471and flatten_trace_label_return
    470472  (S: abstract_status)
    471473    (start_status: S) (final_status: S)
     
    474476  match the_trace with
    475477  [ tlr_base before after trace_to_lift ⇒
    476       as_compute_cost_trace_label_label … trace_to_lift
     478      flatten_trace_label_label … trace_to_lift
    477479  | tlr_step initial labelled final labelled_trace ret_trace ⇒
    478     let labelled_cost ≝ as_compute_cost_trace_label_label … doesnt_end_with_ret … labelled_trace in
    479     let return_cost ≝ as_compute_cost_trace_label_return … ret_trace in
     480    let labelled_cost ≝ flatten_trace_label_label … doesnt_end_with_ret … labelled_trace in
     481    let return_cost ≝ flatten_trace_label_return … ret_trace in
    480482        labelled_cost @ return_cost
    481483  ].
     
    494496qed.
    495497
    496 (* XXX: dependent type madness *)
    497 (*
    498 let rec tll_rel_to_traces_same_cost
     498let rec taa_append_tal_same_flatten
     499  S st1 fl st2 st3 (taa : trace_any_any S st1 st2) on taa :
     500  ∀tal : trace_any_label S fl st2 st3.
     501    flatten_trace_any_label … (taa_append_tal … taa tal) =
     502      flatten_trace_any_label … tal ≝ ?.
     503cases taa -st1 -st2
     504[ #st1 #tal %
     505| #st_pre #st_init #st2 #H #taa #G #K #tal
     506  whd in match (taa_append_tal ???????);
     507  whd in ⊢ (??%?); //
     508]
     509qed. 
     510
     511
     512let rec tll_rel_to_traces_same_flatten
    499513  (S: abstract_status) (S': abstract_status)
    500514    (trace_ends_flag_l: trace_ends_with_ret) (trace_ends_flag_r: trace_ends_with_ret)
     
    504518          on the_trace_l:
    505519            tll_rel … the_trace_l the_trace_r →
    506               as_compute_cost_trace_label_label … the_trace_l =
    507                 as_compute_cost_trace_label_label S' trace_ends_flag_r ? ? the_trace_r ≝ ?.
    508 and tal_rel_to_traces_same_cost
     520              map … (pi1 …) (flatten_trace_label_label … the_trace_l) =
     521                map … (pi1 …) (flatten_trace_label_label … the_trace_r) ≝
     522  match the_trace_l with
     523  [ tll_base fl1 st1 st1' tal1 H ⇒
     524    match the_trace_r with
     525    [ tll_base fl2 st2 st2 tal2 G ⇒ ?
     526    ]
     527  ]
     528and tal_rel_to_traces_same_flatten
    509529  (S: abstract_status) (S': abstract_status) (trace_ends_flag_l: trace_ends_with_ret)
    510530    (trace_ends_flag_r: trace_ends_with_ret)
     
    514534          on the_trace_l:
    515535            tal_rel … the_trace_l the_trace_r →
    516               as_compute_cost_trace_any_label … the_trace_l =
    517                 as_compute_cost_trace_any_label … the_trace_r ≝ ?
    518 and tlr_rel_to_traces_same_cost
     536              map … (pi1 …) (flatten_trace_any_label … the_trace_l) =
     537                map … (pi1 …) (flatten_trace_any_label … the_trace_r) ≝
     538  match the_trace_l with
     539  [ tal_base_not_return st1 st1' H G K ⇒ ?
     540  | tal_base_return st1 st1' H G ⇒ ?
     541  | tal_base_call st1 st1' st1'' H G K tlr1 L ⇒ ?
     542  | tal_step_call fl1 st1 st1' st1'' st1''' H G K tlr1 L tl1 ⇒ ?
     543  | tal_step_default fl1 st1 st1' st1'' H tl1 G K ⇒ ?
     544  ]
     545and tlr_rel_to_traces_same_flatten
    519546  (S: abstract_status) (S': abstract_status) (start_status_l: S) (final_status_l: S)
    520547    (start_status_r: S') (final_status_r: S')
     
    523550        on the_trace_l:
    524551          tlr_rel … the_trace_l the_trace_r →
    525             as_compute_cost_trace_label_return … the_trace_l =
    526               as_compute_cost_trace_label_return … the_trace_r ≝ ?.
    527   cases daemon
     552            map … (pi1 …) (flatten_trace_label_return … the_trace_l) =
     553              map … (pi1 …) (flatten_trace_label_return … the_trace_r) ≝
     554  match the_trace_l with
     555  [ tlr_base before after tll_l ⇒ ?
     556  | tlr_step initial labelled final tll_l tlr_l ⇒ ?
     557  ]. 
     558[ * whd in match as_label_safe; normalize nodelta
     559  @opt_safe_elim #l1 #EQ1
     560  @opt_safe_elim #l2 #EQ2
     561  #EQ destruct(EQ) #H_tal
     562  change with (? :: ? = ? :: ?) lapply H -H lapply G -G
     563  whd in match as_costed; normalize nodelta
     564  >EQ1 >EQ2 normalize nodelta #_ #_
     565  >(tal_rel_to_traces_same_flatten … H_tal) @refl
     566|2,3,4,5,6:
     567  [1,2,3: * #EQ destruct(EQ)]
     568  [1,2,3,4: * #st_mid * #taa
     569    [ *#H' *#G' *#K' #EQ
     570    | *#H' *#G' #EQ
     571    | *#st_mid' *#H' *#G' *#K' *#tlr2 *#L' * #EQ #H_tlr
     572    | *#st_fun *#st_after *#H' *#G' *#K' *#tlr2 *#L' *#tl2 ** #EQ #H_tlr #H_tal
     573    ] >EQ >taa_append_tal_same_flatten
     574  | whd in ⊢ (%→??(????%)?);
     575    @tal_rel_to_traces_same_flatten
     576  ]
     577  [1,2: %
     578  | @(tlr_rel_to_traces_same_flatten … H_tlr)
     579  | <map_append
     580    >(tlr_rel_to_traces_same_flatten … H_tlr)
     581    >(tal_rel_to_traces_same_flatten … H_tal)
     582    @map_append
     583  ]
     584|*: cases the_trace_r
     585  [1,3: #st_before_r #st_after_r #tll_r
     586    [ @tll_rel_to_traces_same_flatten | * ]
     587  |*: #st_init_r #st_labld_r #st_fin_r #tll_r #tlr_r *
     588    #H_tll #H_tlr
     589    <map_append
     590    >(tll_rel_to_traces_same_flatten … H_tll)
     591    >(tlr_rel_to_traces_same_flatten … H_tlr)
     592    @map_append
     593  ]
     594]
    528595qed.
    529 *)
     596
Note: See TracChangeset for help on using the changeset viewer.