Ignore:
Timestamp:
Nov 29, 2012, 3:32:50 PM (7 years ago)
Author:
mckinna
Message:

tidied up, with new auxiliary defns, some refactoring, some code motion, to support a cleaned-up compiler.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StructuredTraces.ma

    r2423 r2503  
    3131
    3232(* temporary alias for backward compatibility *)
    33 definition final_abstract_status ≝ abstract_status.
     33(* definition final_abstract_status ≝ abstract_status. *)
    3434
    3535definition as_costed : ∀a_s : abstract_status.a_s → Prop ≝
    3636  λa_s,st.as_label ? st ≠ None ?.
    37 
    38 lemma as_costed_exc : ∀S:abstract_status. ∀s:S. (as_costed S s) ∨ (¬as_costed S s).
    39 #S #s whd in match (as_costed S s);
    40 cases (as_label S s) [ %2 % * /2/ | #c %1 % #E destruct ]
    41 qed.
    4237
    4338definition as_label_safe : ∀a_s : abstract_status.
    4439  (Σs : a_s.as_costed ? s) → costlabel ≝
    4540  λa_s,st_sig.opt_safe … (pi2 … st_sig).
     41
     42lemma as_costed_exc : ∀S:abstract_status. ∀s:S. (as_costed S s) + (¬as_costed S s).
     43#S #s whd in match (as_costed S s);
     44cases (as_label S s) [ %2 % * /2/ | #c %1 % #E destruct ]
     45qed.
     46
     47lemma not_costed_no_label : ∀S,st.
     48  ¬as_costed S st →
     49  as_label S st = None ?.
     50#S #st * normalize cases (as_label_of_pc S ?)
     51[ // | #l #H cases (H ?) % #E destruct ]
     52qed.
     53
     54(* cost maps generalities *)
     55
     56definition as_cost_labelled ≝
     57  λS : abstract_status. λl.∃pc.as_label_of_pc S pc = Some ? l.
     58
     59definition as_cost_label ≝
     60  λS : abstract_status. Σl.as_cost_labelled S l.
     61
     62definition as_cost_labels ≝
     63  λS : abstract_status. list (as_cost_label S).
     64
     65definition as_cost_get_label ≝
     66  λS : abstract_status. λl_sig: as_cost_label S. pi1 … l_sig.
     67
     68definition as_cost_get_labels ≝
     69  λS : abstract_status. map … (as_cost_get_label S).
     70
     71definition as_cost_map ≝
     72  (* λS : abstract_status. (Σl.∃pc.as_label_of_pc S pc = Some ? l) → ℕ. *)
     73  λS : abstract_status. (as_cost_label S) → ℕ.
     74 
     75definition lift_sigma_map_id :
     76  ∀A,B : Type[0].∀P_in,P_out : A → Prop.B →
     77    (∀a.P_out a + ¬ P_out a) →
     78  ((Σa.P_out a) → B) → (Σa.P_in a) → B ≝ λA,B,P_in,P_out,dflt,dec,m,a_sig.
     79   match dec a_sig with
     80   [ inl prf ⇒ m «a_sig, prf»
     81   | inr _ ⇒ dflt (* labels not present in out code get 0 *)
     82   ].
     83
     84lemma lift_sigma_map_id_eq :
     85  ∀A,B,P_in,P_out,dflt,dec,m,a_in,a_out.
     86  pi1 ?? a_in = pi1 ?? a_out →
     87  lift_sigma_map_id A B P_in P_out dflt dec m a_in = m a_out.
     88#A#B#P_in#P_out#dflt#dec#m#a_in#a_out#EQ
     89whd in match lift_sigma_map_id; normalize nodelta
     90cases (dec a_in) normalize nodelta >EQ cases a_out
     91#a #H #G [ % | @⊥ /2 by absurd/ ]
     92qed.
     93
     94notation > "Σ_{ ident i ∈ l } f"
     95  with precedence 20
     96  for @{'fold plus 0 (λ${ident i}.true) (λ${ident i}. $f) $l}.
     97notation < "Σ_{ ident i ∈ l } f"
     98  with precedence 20
     99for @{'fold plus 0 (λ${ident i}:$X.true) (λ${ident i}:$Y. $f) $l}.
     100
     101definition lift_cost_map_id :
     102  ∀S_in,S_out : abstract_status.? →
     103  as_cost_map S_out → as_cost_map S_in
     104  ≝
     105 λS_in,S_out : abstract_status.
     106  lift_sigma_map_id costlabel ℕ
     107    (*λl.∃pc.as_label_of_pc S_in pc = Some ? l*) (as_cost_labelled S_in)
     108    (*λl.∃pc.as_label_of_pc S_out pc = Some ? l*) (as_cost_labelled S_out)
     109    0.
     110
     111lemma lift_cost_map_same_cost :
     112  ∀S_in, S_out, dec, m_out, trace_in, trace_out.
     113  map … (pi1 ??) trace_in = map … (pi1 ??) trace_out →
     114  (Σ_{ l_sig ∈ trace_in } (lift_cost_map_id S_in S_out dec m_out l_sig)) =
     115  (Σ_{ l_sig ∈ trace_out } (m_out l_sig)).
     116#S_in #S_out #dec #m_out #trace_in elim trace_in
     117[2: #hd_in #tl_in #IH] * [2,4: #hd_out #tl_out]
     118normalize in ⊢ (%→?);
     119[2,3: #ABS destruct(ABS)
     120|4: #_ %
     121|1:
     122  #EQ destruct
     123  whd in ⊢(??%%);
     124  whd in match lift_cost_map_id; normalize nodelta
     125  >(lift_sigma_map_id_eq ????????? e0)
     126  >e0 in e1; normalize in ⊢(%→?); #EQ
     127  >(IH … EQ) %
     128]
     129qed.
     130
     131
     132(* structured traces: down to business *)
    46133
    47134inductive trace_ends_with_ret: Type[0] ≝
     
    189276qed.
    190277
    191 lemma not_costed_no_label : ∀S,st.
    192   ¬as_costed S st →
    193   as_label_of_pc S (as_pc_of S st) = None ?.
    194 #S #st * normalize cases (as_label_of_pc S ?)
    195 [ // | #l #H cases (H ?) % #E destruct ]
    196 qed.
    197 
    198278lemma tal_pc_list_start : ∀S,fl,s1,s2. ∀tal: trace_any_label S fl s1 s2.
    199279  ∃tl. tal_pc_list … tal = (as_pc_of S s1)::tl.
     
    209289let rec tal_tail_not_costed S fl st1 st2 tal
    210290  (H:Not (as_costed S st1)) on tal :
    211   All ? (λl. as_label_of_pc S l = None ?) (tal_pc_list S fl st1 st2 tal) ≝ ?.
     291  All ? (λpc. as_label_of_pc S pc = None ?) (tal_pc_list S fl st1 st2 tal) ≝ ?.
    212292cases tal in H ⊢ %;
    213293[ #start #final #EX #CL #CS #CS' % // @(not_costed_no_label ?? CS')
     
    624704    (start_status: S) (final_status: S)
    625705      (the_trace: trace_label_label S trace_ends_flag start_status final_status)
    626         on the_trace: list (Σl: costlabel. ∃pc. as_label_of_pc S pc = Some … l) ≝
     706        on the_trace: list (as_cost_label S) (*Σl: costlabel. ∃pc. as_label_of_pc S pc = Some … l*) ≝
    627707  match the_trace with
    628708  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
    629709      let label ≝
    630         match as_label … initial return λx: option costlabel. x ≠ None costlabel → ? with
     710        match as_label … initial return λx: option costlabel. x ≠ None ? → ? with
    631711        [ None ⇒ λabs. ⊥
    632712        | Some l ⇒ λ_. l
     
    639719    (start_status: S) (final_status: S)
    640720      (the_trace: trace_any_label S trace_ends_flag start_status final_status)
    641         on the_trace: list (Σl: costlabel.  ∃pc. as_label_of_pc S pc = Some … l) ≝
     721        on the_trace: list (as_cost_label S) (*Σl: costlabel. ∃pc. as_label_of_pc S pc = Some … l*) ≝
    642722  match the_trace with
    643723  [ tal_base_not_return the_status _ _ _ _ ⇒ [ ]
     
    657737    (start_status: S) (final_status: S)
    658738      (the_trace: trace_label_return S start_status final_status)
    659         on the_trace: list (Σl: costlabel.  ∃pc. as_label_of_pc S pc = Some … l) ≝
     739        on the_trace: list (as_cost_label S) (*Σl: costlabel. ∃pc. as_label_of_pc S pc = Some … l*) ≝
    660740  match the_trace with
    661741  [ tlr_base before after trace_to_lift ⇒
     
    681761qed.
    682762
     763(* JHM: base case now passes the termination checker *)
    683764let rec taa_append_tal_same_flatten
    684765  S st1 fl st2 st3 (taa : trace_any_any S st1 st2) on taa :
     
    687768      flatten_trace_any_label … tal ≝ ?.
    688769cases taa -st1 -st2
    689 [ //
     770[ #st #tal normalize in ⊢ (??%?); //
    690771| #st_pre #st_init #st2 #H #G #K #taa' #tal
    691772  whd in match (? @ ?);
     
    797878qed.
    798879
    799 definition as_cost_map ≝
    800   λS : abstract_status. (Σl.∃pc.as_label_of_pc S pc = Some ? l) → ℕ.
    801 
    802 definition lift_sigma_map_id :
    803   ∀A,B : Type[0].∀P_in,P_out : A → Prop.B →
    804     (∀a.P_out a + ¬ P_out a) →
    805   ((Σa.P_out a) → B) → (Σa.P_in a) → B ≝ λA,B,P_in,P_out,dflt,dec,m,a_sig.
    806    match dec a_sig with
    807    [ inl prf ⇒ m «a_sig, prf»
    808    | inr _ ⇒ dflt (* labels not present in out code get 0 *)
    809    ].
    810 
    811 lemma lift_sigma_map_id_eq :
    812   ∀A,B,P_in,P_out,dflt,dec,m,a_in,a_out.
    813   pi1 ?? a_in = pi1 ?? a_out →
    814   lift_sigma_map_id A B P_in P_out dflt dec m a_in = m a_out.
    815 #A#B#P_in#P_out#dflt#dec#m#a_in#a_out#EQ
    816 whd in match lift_sigma_map_id; normalize nodelta
    817 cases (dec a_in) normalize nodelta >EQ cases a_out
    818 #a #H #G [ % | @⊥ /2 by absurd/ ]
    819 qed.
    820 
    821 notation > "Σ_{ ident i ∈ l } f"
    822   with precedence 20
    823   for @{'fold plus 0 (λ${ident i}.true) (λ${ident i}. $f) $l}.
    824 notation < "Σ_{ ident i ∈ l } f"
    825   with precedence 20
    826 for @{'fold plus 0 (λ${ident i}:$X.true) (λ${ident i}:$Y. $f) $l}.
    827 
    828 definition lift_cost_map_id :
    829   ∀S_in,S_out : abstract_status.? →
    830   as_cost_map S_out → as_cost_map S_in
    831   ≝
    832  λS_in,S_out : abstract_status.
    833   lift_sigma_map_id costlabel ℕ
    834     (λl.∃pc.as_label_of_pc S_in pc = Some ? l)
    835     (λl.∃pc.as_label_of_pc S_out pc = Some ? l)
    836     0.
    837 
    838 lemma lift_cost_map_same_cost :
    839   ∀S_in, S_out, dec, m_out, trace_in, trace_out.
    840   map … (pi1 ??) trace_in = map … (pi1 ??) trace_out →
    841   (Σ_{ l_sig ∈ trace_in } (lift_cost_map_id S_in S_out dec m_out l_sig)) =
    842   (Σ_{ l_sig ∈ trace_out } (m_out l_sig)).
    843 #S_in #S_out #dec #m_out #trace_in elim trace_in
    844 [2: #hd_in #tl_in #IH] * [2,4: #hd_out #tl_out]
    845 normalize in ⊢ (%→?);
    846 [2,3: #ABS destruct(ABS)
    847 |4: #_ %
    848 |1:
    849   #EQ destruct
    850   whd in ⊢(??%%);
    851   whd in match lift_cost_map_id; normalize nodelta
    852   >(lift_sigma_map_id_eq ????????? e0)
    853   >e0 in e1; normalize in ⊢(%→?); #EQ
    854   >(IH … EQ) %
    855 ]
    856 qed.
     880(* cost maps specifics: summing over flattened traces *)
    857881
    858882lemma lift_cost_map_same_cost_tal :
Note: See TracChangeset for help on using the changeset viewer.