Changeset 3487 for LTS/Traces.ma


Ignore:
Timestamp:
Sep 24, 2014, 3:23:24 PM (5 years ago)
Author:
sacerdot
Message:

No more i_act.

Note: we do not ask anywhere that no transitions to an initial
state are allowed, nor that no transitions from the final state
are allowed. Are those conditions really vacuous? Do they make
the final statement on measurable traces more accurate?

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Traces.ma

    r3478 r3487  
    3333 | a_call : CallCostLabel → CostLabel
    3434 | a_return_post : ReturnPostCostLabel → CostLabel
    35  | a_non_functional_label : NonFunctionalLabel → CostLabel
    36  | i_act : CostLabel.
     35 | a_non_functional_label : NonFunctionalLabel → CostLabel.
    3736
    3837coercion a_call.
     
    150149  | a_non_functional_label x1 ⇒
    151150     λc2.match c2 with [a_non_functional_label y1 ⇒ x1 == y1 | _ ⇒ false ]
    152   | i_act ⇒ λc2.match c2 with [i_act ⇒ true | _ ⇒ false ]
    153151  ].
    154152
    155153lemma eq_costlabel_elim : ∀P : bool → Prop.∀c1,c2.(c1 = c2 → P true) →
    156154(c1 ≠ c2 → P false) → P (eq_costlabel c1 c2).
    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 ??);
     155#P * #c1 * #c2 #H1 #H2 whd in match (eq_costlabel ??);
    159156try (@H2 % #EQ destruct)
    160157[ change with (eq_call_cost_lab ??) in ⊢ (?%); @eq_call_cost_lab_elim
     
    165162| change with (eq_nf_label ??) in ⊢ (?%); @eq_fn_label_elim
    166163  [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H % ]
    167 | @H1 %
    168164]
    169165qed.
Note: See TracChangeset for help on using the changeset viewer.