Changeset 3478 for LTS/Traces.ma


Ignore:
Timestamp:
Sep 22, 2014, 4:50:21 PM (5 years ago)
Author:
piccolo
Message:

fixed costlabels

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Traces.ma

    r3396 r3478  
    3333 | a_call : CallCostLabel → CostLabel
    3434 | a_return_post : ReturnPostCostLabel → CostLabel
    35  | a_non_functional_label : NonFunctionalLabel → CostLabel.
     35 | a_non_functional_label : NonFunctionalLabel → CostLabel
     36 | i_act : CostLabel.
    3637
    3738coercion a_call.
     
    149150  | a_non_functional_label x1 ⇒
    150151     λc2.match c2 with [a_non_functional_label y1 ⇒ x1 == y1 | _ ⇒ false ]
     152  | i_act ⇒ λc2.match c2 with [i_act ⇒ true | _ ⇒ false ]
    151153  ].
    152154
    153155lemma eq_costlabel_elim : ∀P : bool → Prop.∀c1,c2.(c1 = c2 → P true) →
    154156(c1 ≠ c2 → P false) → P (eq_costlabel c1 c2).
    155 #P * #c1 * #c2 #H1 #H2 whd in match (eq_costlabel ??);
     157#P * [1,2,3: #c1 |] * [1,2,3,5,6,7,9,10,11,13,14,15: #c2 |*:]
     158#H1 #H2 whd in match (eq_costlabel ??);
    156159try (@H2 % #EQ destruct)
    157160[ change with (eq_call_cost_lab ??) in ⊢ (?%); @eq_call_cost_lab_elim
     
    162165| change with (eq_nf_label ??) in ⊢ (?%); @eq_fn_label_elim
    163166  [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H % ]
     167| @H1 %
    164168]
    165169qed.
     
    187191 | call_act : FunctionName → CallCostLabel → ActionLabel
    188192 | ret_act : option(ReturnPostCostLabel) → ActionLabel
    189  | cost_act : option NonFunctionalLabel → ActionLabel
    190  | init_act : ActionLabel.
     193 | cost_act : option NonFunctionalLabel → ActionLabel.
    191194 
    192195definition is_cost_label : ActionLabel → Prop ≝
     
    263266                    | ret_act x ⇒ match x with [ Some _ ⇒ True | None ⇒ False ]
    264267                    | cost_act x ⇒ match x with [ Some _ ⇒ True | None ⇒ False ]
    265                     | init_act ⇒ False
    266268                    ].
    267269(*
Note: See TracChangeset for help on using the changeset viewer.