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/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.