Ignore:
Timestamp:
May 17, 2012, 12:06:34 PM (8 years ago)
Author:
tranquil
Message:

introduced as_label_of_cost and adapted accordingly. Equality of cost mapping sums

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StructuredTraces.ma

    r1949 r1964  
    2020  ; as_pc_of : as_status → as_pc
    2121  ; as_classifier : as_status → status_class → Prop
    22   ; as_label : as_status → option costlabel
     22  ; as_label_of_pc : as_pc → option costlabel
    2323  ; as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop
    2424  ; as_final: as_status → Prop
    2525}.
     26
     27definition as_label ≝ λS : abstract_status. λs : S. as_label_of_pc … (as_pc_of … s).
    2628
    2729(* temporary alias for backward compatibility *)
     
    435437    tal_rel … tl1 tal2 (* <- this makes it many to many *)
    436438  ].
     439 
     440interpretation "trace any label rel" 'napart t1 t2 = (tal_rel ???????? t1 t2).
     441interpretation "trace label label rel" 'napart t1 t2 = (tll_rel ???????? t1 t2).
     442interpretation "trace label return rel" 'napart t1 t2 = (tlr_rel ???????? t1 t2).
     443
    437444
    438445let rec flatten_trace_label_label
     
    440447    (start_status: S) (final_status: S)
    441448      (the_trace: trace_label_label S trace_ends_flag start_status final_status)
    442         on the_trace: list (Σl: costlabel. ∃s. as_label S s = Some … l) ≝
     449        on the_trace: list (Σl: costlabel. ∃pc. as_label_of_pc S pc = Some … l) ≝
    443450  match the_trace with
    444451  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
     
    455462    (start_status: S) (final_status: S)
    456463      (the_trace: trace_any_label S trace_ends_flag start_status final_status)
    457         on the_trace: list (Σl: costlabel. ∃s. as_label … s = Some … l) ≝
     464        on the_trace: list (Σl: costlabel.  ∃pc. as_label_of_pc S pc = Some … l) ≝
    458465  match the_trace with
    459466  [ tal_base_not_return the_status _ _ _ _ ⇒ [ ]
     
    473480    (start_status: S) (final_status: S)
    474481      (the_trace: trace_label_return S start_status final_status)
    475         on the_trace: list (Σl: costlabel. ∃s. as_label … s = Some … l) ≝
     482        on the_trace: list (Σl: costlabel.  ∃pc. as_label_of_pc S pc = Some … l) ≝
    476483  match the_trace with
    477484  [ tlr_base before after trace_to_lift ⇒
     
    485492    cases abs -abs #abs @abs %
    486493  |1:
    487     %{initial} whd in match label;
     494    %{(as_pc_of … initial)} whd in match label;
     495    change with (as_label ?? = ?)
    488496    generalize in match labelled_proof; whd in ⊢ (% → ?);
    489497    cases (as_label S initial)
     
    595603qed.
    596604
     605definition as_cost_map ≝
     606  λS : abstract_status. (Σl.∃pc.as_label_of_pc S pc = Some ? l) → ℕ.
     607
     608definition lift_cost_map_id :
     609  ∀S_in, S_out: abstract_status.
     610   (∀l. (∃pc.as_label_of_pc S_out pc = Some … l) +
     611       ¬(∃pc.as_label_of_pc S_out pc = Some … l)) →
     612  (as_cost_map S_out) → as_cost_map S_in ≝ λS_in,S_out,dec,m,l_sig.
     613   match dec l_sig with
     614   [ inl prf ⇒ m «l_sig, prf»
     615   | inr _ ⇒ 0 (* labels not present in out code get 0 *)
     616   ].
     617
     618lemma lift_cost_map_id_eq :
     619  ∀S_in, S_out, dec, m, l_in, l_out.
     620  pi1 ?? l_in = pi1 ?? l_out → lift_cost_map_id S_in S_out dec m l_in = m l_out.
     621#S_in #S_out #dec #m #l_in * #l_out #prf #EQ
     622whd in match lift_cost_map_id; normalize nodelta
     623cases (dec l_in) normalize nodelta >EQ
     624[2: #H @⊥] /2 by refl, absurd/
     625qed.
     626
     627notation > "Σ_{ ident i ∈ l } f"
     628  with precedence 20
     629  for @{'fold plus 0 (λ${ident i}.true) (λ${ident i}. $f) $l}.
     630notation < "Σ_{ ident i ∈ l } f"
     631  with precedence 20
     632for @{'fold plus 0 (λ${ident i}:$X.true) (λ${ident i}:$Y. $f) $l}.
     633
     634definition as_cost_of_trace_any_label :
     635  ∀S : abstract_status.
     636  ∀fl, start, end.
     637  as_cost_map S →
     638  trace_any_label S fl start end → ℕ ≝
     639  λS,fl,start,end,m,the_trace.
     640  Σ_{ l_sig ∈ flatten_trace_any_label … the_trace } (m l_sig).
     641
     642definition as_cost_of_trace_label_label :
     643  ∀S : abstract_status.
     644  ∀fl, start, end.
     645  as_cost_map S →
     646  trace_label_label S fl start end → ℕ ≝
     647  λS,fl,start,end,m,the_trace.
     648  Σ_{ l_sig ∈ flatten_trace_label_label … the_trace } (m l_sig).
     649
     650definition as_cost_of_trace_label_return :
     651  ∀S : abstract_status.
     652  ∀start, end.
     653  as_cost_map S →
     654  trace_label_return S start end → ℕ ≝
     655  λS,start,end,m,the_trace.
     656  Σ_{ l_sig ∈ flatten_trace_label_return … the_trace } (m l_sig).
     657
     658lemma lift_cost_map_same_cost :
     659  ∀S_in, S_out, dec, m_out, trace_in, trace_out.
     660  map … (pi1 ??) trace_in = map … (pi1 ??) trace_out →
     661  (Σ_{ l_sig ∈ trace_in } (lift_cost_map_id S_in S_out dec m_out l_sig)) =
     662  (Σ_{ l_sig ∈ trace_out } (m_out l_sig)).
     663#S_in #S_out #dec #m_out #trace_in elim trace_in
     664[2: #hd_in #tl_in #IH] * [2,4: #hd_out #tl_out]
     665normalize in ⊢ (%→?);
     666[2,3: #ABS destruct(ABS)
     667|4: #_ %
     668|1:
     669  #EQ destruct
     670  whd in ⊢(??%%);
     671  >(lift_cost_map_id_eq … e0)
     672  >e0 in e1; normalize in ⊢(%→?); #EQ
     673  >(IH … EQ) %
     674]
     675qed.
     676
     677lemma lift_cost_map_same_cost_tal :
     678  ∀S_in, S_out, dec, m_out, f_in, f_out, start_in, start_out, end_in, end_out.
     679  ∀the_trace_in : trace_any_label S_in f_in start_in end_in.
     680  ∀the_trace_out : trace_any_label S_out f_out start_out end_out.
     681  tal_rel … the_trace_in the_trace_out →
     682  as_cost_of_trace_any_label … (lift_cost_map_id S_in S_out dec m_out) the_trace_in =
     683    as_cost_of_trace_any_label … m_out the_trace_out.
     684#S_in #S_out #dec #m_out #f_in #f_out #start_in #start_out #end_in #end_out
     685#tal_in #tal_out #H_tal
     686@(lift_cost_map_same_cost … (tal_rel_to_traces_same_flatten … H_tal))
     687qed.
     688
     689lemma lift_cost_map_same_cost_tll :
     690  ∀S_in, S_out, dec, m_out, f_in, f_out, start_in, start_out, end_in, end_out.
     691  ∀the_trace_in : trace_label_label S_in f_in start_in end_in.
     692  ∀the_trace_out : trace_label_label S_out f_out start_out end_out.
     693  tll_rel … the_trace_in the_trace_out →
     694  as_cost_of_trace_label_label … (lift_cost_map_id S_in S_out dec m_out) the_trace_in =
     695    as_cost_of_trace_label_label … m_out the_trace_out.
     696#S_in #S_out #dec #m_out #f_in #f_out #start_in #start_out #end_in #end_out
     697#tll_in #tll_out #H_tll
     698@(lift_cost_map_same_cost … (tll_rel_to_traces_same_flatten … H_tll))
     699qed.
     700
     701lemma lift_cost_map_same_cost_tlr :
     702  ∀S_in, S_out, dec, m_out, start_in, start_out, end_in, end_out.
     703  ∀the_trace_in : trace_label_return S_in start_in end_in.
     704  ∀the_trace_out : trace_label_return S_out start_out end_out.
     705  tlr_rel … the_trace_in the_trace_out →
     706  as_cost_of_trace_label_return … (lift_cost_map_id S_in S_out dec m_out) the_trace_in =
     707    as_cost_of_trace_label_return … m_out the_trace_out.
     708#S_in #S_out #dec #m_out #start_in #start_out #end_in #end_out
     709#tlr_in #tlr_out #H_tlr
     710@(lift_cost_map_same_cost … (tlr_rel_to_traces_same_flatten … H_tlr))
     711qed.
Note: See TracChangeset for help on using the changeset viewer.