Changeset 2186 for src/common

Timestamp:

Jul 16, 2012, 4:59:09 PM (7 years ago)

Author:

tranquil

Message:

updated joint semantics

File:

• src/common/StructuredTraces.ma (modified) (7 diffs)

src/common/StructuredTraces.ma

@@ -334 +334 @@
 qed.
 
-(* an uncalling, unreturning and *unjumping*,
-  as well as unlabelled (but possibly for the first and last statuses) 
-  possibly empty trace segment *)
-inductive trace_any_any (S:abstract_status) : S → S → Type[0] ≝
-  | taa_base :
+(*
+(* an trace of unlabeled and cl_other states, possibly empty *)
+inductive trace_no_label_any (S:abstract_status) : S → S → Type[0] ≝
+  | tna_base :
       ∀start_status: S.
-        trace_any_any S start_status start_status
-  | taa_step :
+      ¬as_costed … start_status →
+      trace_no_label_any S start_status start_status
+  | tna_step :
       ∀status_pre: S.
       ∀status_init: S.
       ∀status_end: S.
         as_execute S status_pre status_init →
-        trace_any_any S status_init status_end →
         as_classifier S status_pre cl_other →
-        ¬as_costed … status_init →
-          trace_any_any S status_pre status_end.
-
-let rec taa_status_list S st1 st2 (taa : trace_any_any S st1 st2) on taa : list S ≝
+        ¬as_costed … status_pre →
+        trace_no_label_any S status_init status_end →
+          trace_no_label_any S status_pre status_end.
+
+let rec tna_append_tna S st1 st2 st3 (taa1 : trace_no_label_any S st1 st2)
+  on taa1 :
+    trace_no_label_any S st2 st3 →
+    trace_no_label_any S st1 st3 ≝
+  match taa1 with
+  [ tna_base st1' H ⇒ λtaa2.taa2
+  | tna_step st1' st2' st3' H G K tl ⇒
+    λtaa2.tna_step ???? H G K (tna_append_tna … tl taa2)
+  ].
+
+definition tna_non_empty ≝ λS,st1,st2.λtna : trace_no_label_any S st1 st2.
+  match tna with
+  [ tna_base _ _ ⇒ false
+  | tna_step _ _ _ _ _ _ _ ⇒ true
+  ].
+
+coercion tna_to_bool : ∀S,st1,st2.∀tna:trace_no_label_any S st1 st2.bool ≝
+ tna_non_empty on _tna : trace_no_label_any ??? to bool.
+
+lemma tna_unlabelled : ∀S,st1,st2.trace_no_label_any S st1 st2 → ¬as_costed … st1.
+#S #st1 #st2 * [#st #H @H | #st #st' #st'' #_ #_ #H #_ @H] qed.
+
+let rec tna_append_tal S st1 fl st2 st3 (tna : trace_no_label_any S st1 st2)
+  on tna :
+  trace_any_label S fl st2 st3 →
+  if tna then Not (as_costed … st2) else True →
+  trace_any_label S fl st1 st3 ≝
+  match tna return λst1,st2.λx : trace_no_label_any S st1 st2.
+    ∀fl,st3.
+    trace_any_label S fl st2 st3 →
+    if x then Not (as_costed … st2) else True →
+    trace_any_label S fl st1 st3
+  with
+  [ tna_base st1' H ⇒ λfl,st3,taa2,prf.taa2
+  | tna_step st1' st2' st3' H G K tl ⇒ λfl,st3,taa2,prf.
+    tal_step_default ????? H (tna_append_tal ????? tl taa2 ?) G (tna_unlabelled … tl)
+  ] fl st3.
+  cases (tna_non_empty … tl) [@prf|%]
+  qed.
+*)
+
+inductive trace_any_any (S : abstract_status) : S → S → Type[0] ≝
+  | taa_base : ∀st.trace_any_any S st st
+  | taa_step : ∀st1,st2,st3.
+    as_execute S st1 st2 →
+    as_classifier S st1 cl_other →
+    ¬as_costed S st2 →
+    trace_any_any S st2 st3 →
+    trace_any_any S st1 st3.
+
+definition taa_non_empty ≝ λS,st1,st2.λtaa : trace_any_any S st1 st2.
   match taa with
-  [ taa_base st1' ⇒ [st1']
-  | taa_step st1' st2' st3' _ tl _ _ ⇒ st1' :: taa_status_list … tl
+  [ taa_base _ ⇒ false
+  | taa_step _ _ _ _ _ _ _ ⇒ true
   ].
 
-let rec taa_append_taa S st1 st2 st3 (taa1 : trace_any_any S st1 st2)
-  on taa1 : trace_any_any S st2 st3 → trace_any_any S st1 st3 ≝
-  match taa1
-  return λst1,st2.λx : trace_any_any S st1 st2.
-    trace_any_any S st2 st3 → trace_any_any S st1 st3
-  with
-  [ taa_base _ ⇒ λtaa2.taa2
-  | taa_step st1' st2' st3' H tl G K ⇒ λtaa2.
-      taa_step … H (taa_append_taa … tl taa2) G K
-  ].
-
-let rec taa_append_tal S st1 fl st2 st3 (taa : trace_any_any S st1 st2)
-  on taa :
+coercion taa_to_bool : ∀S,st1,st2.∀taa:trace_any_any S st1 st2.bool ≝
+ taa_non_empty on _taa : trace_any_any ??? to bool.
+
+let rec taa_append_tal S st1 fl st2 st3
+  (taa : trace_any_any S st1 st2) on taa :
   trace_any_label S fl st2 st3 →
   trace_any_label S fl st1 st3 ≝
-  match taa
-  return λst1,st2.λx : trace_any_any S st1 st2.
-    trace_any_label S fl st2 st3 → trace_any_label S fl st1 st3
+  match taa return λst1,st2.λx : trace_any_any S st1 st2.
+    ∀fl,st3.
+    trace_any_label S fl st2 st3 →
+    trace_any_label S fl st1 st3
   with
-  [ taa_base _ ⇒ λtaa2.taa2
-  | taa_step st1' st2' st3' H tl G K ⇒ λtaa2.
-      tal_step_default … H (taa_append_tal … tl taa2) G K
-  ].
+  [ taa_base st1' ⇒ λfl,st3,tal2.tal2
+  | taa_step st1' st2' st3' H G K tl ⇒ λfl,st3,tal2.
+    tal_step_default ????? H (taa_append_tal ????? tl tal2) G K
+  ] fl st3.
+
+interpretation "trace any any label append" 'append taa tal = (taa_append_tal ????? taa tal).
 
 let rec tlr_rel S1 st1 st1' S2 st2 st2'
@@ -416 +461 @@
     fl2 = doesnt_end_with_ret ∧
     ∃st2mid,taa,H,G,K.
-    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
+    tal2 ≃ taa_append_tal ? st2 ??? taa
       (tal_base_not_return ? st2mid st2' H G K)
   | tal_base_return st1 st1' _ _ ⇒
@@ -437 +482 @@
     tal_rel … tl1 tal2 (* <- this makes it many to many *)
   ].
-  
+
 interpretation "trace any label rel" 'napart t1 t2 = (tal_rel ???????? t1 t2).
 interpretation "trace label label rel" 'napart t1 t2 = (tll_rel ???????? t1 t2).
-interpretation "trace label return rel" 'napart t1 t2 = (tlr_rel ???????? t1 t2).
-
+interpretation "trace label return rel" 'napart t1 t2 = (tlr_rel ?????? t1 t2).
+
+let rec taa_rel_inv S1 fl1 st1 st1mid st1' S2 fl2 st2 st2'
+  (taa1 : trace_any_any S1 st1 st1mid) on taa1 :
+  ∀tal1 : trace_any_label S1 fl1 st1mid st1'.
+  ∀tal2 : trace_any_label S2 fl2 st2 st2'.
+  tal_rel … (taa1 @ tal1) tal2 →
+  tal_rel … tal1 tal2 ≝ ?.
+cases taa1 -taa1
+[ -taa_rel_inv //
+| #st #st' #st'' #H #G #K #tl #tal1 #tal2 whd in ⊢ (%→?);
+  @(taa_rel_inv … tl)
+]
+qed.
+
+let rec tlr_rel_transitive S1 st1 st1' S2 st2 st2' S3 st3 st3'
+  (tlr1 : trace_label_return S1 st1 st1')
+  (tlr2 : trace_label_return S2 st2 st2')
+  (tlr3 : trace_label_return S3 st3 st3') on tlr1 :
+  tlr_rel … tlr1 tlr2 → tlr_rel … tlr2 tlr3 → tlr_rel … tlr1 tlr3 ≝
+match tlr1 with
+  [ tlr_base st1' st1'' tll1 ⇒ ?
+  | tlr_step st1' st1'' st1''' tll1 tl1 ⇒ ?
+  ]
+and tll_rel_transitive S1 fl1 st1 st1' S2 fl2 st2 st2' S3 fl3 st3 st3'
+  (tll1 : trace_label_label S1 fl1 st1 st1')
+  (tll2 : trace_label_label S2 fl2 st2 st2')
+  (tll3 : trace_label_label S3 fl3 st3 st3') on tll1 :
+  tll1 ≈ tll2 → tll2 ≈ tll3 → tll1 ≈ tll3 ≝
+  match tll1 with
+  [ tll_base fl1' st1' st1'' tal1 H ⇒ ?
+  ]
+and tal_rel_transitive S1 fl1 st1 st1' S2 fl2 st2 st2' S3 fl3 st3 st3'
+  (tal1 : trace_any_label S1 fl1 st1 st1')
+  (tal2 : trace_any_label S2 fl2 st2 st2')
+  (tal3 : trace_any_label S3 fl3 st3 st3') on tal1 :
+  tal1 ≈ tal2 → tal2 ≈ tal3 → tal1 ≈ tal3 ≝
+  match tal1 with
+  [ tal_base_not_return st1' st1'' H G K ⇒ ?
+  | tal_base_return st1' st1'' H G ⇒ ?
+  | tal_base_call st1' st1'' st1''' H G K tlr1 L ⇒ ?
+  | tal_step_call fl1' st1' st1'' st1''' st1'''' H G L tlr1 K tl1 ⇒ ?
+  | tal_step_default fl1' st1' st1'' st1''' H tl1 G K ⇒ ?
+  ].
+[1,2: cases tlr2 #st2' #st2'' [1,3: #tllhd2 |2,4: #st2''' #tllhd2 #tlrtl2]
+  [2,3: *] normalize in ⊢ (%→?); [ #Rhd12 | * #Rhd12 #Rtl12 ]
+  cases tlr3 #st3' #st3'' [1,3: #tllhd3 |2,4: #st3''' #tllhd3 #tlrtl3]
+  [2,3: *] normalize in ⊢ (%→?); [ #Rhd23 | * #Rhd23 #Rtl23 ] whd
+  [ @(tll_rel_transitive … Rhd12 Rhd23) |
+    %{(tll_rel_transitive … Rhd12 Rhd23)}
+    @(tlr_rel_transitive … Rtl12 Rtl23) 
+  ]
+|3:
+  cases tll2 #fl2' #st2' #st2'' #tal2 #H2 * #G2 #R12
+  cases tll3 #fl3' #st3' #st3'' #tal3 #H3 * #G3 #R23
+  %{(tal_rel_transitive … R12 R23)} //
+|*:
+  [1,2,3: * #EQ]
+  [5: whd in ⊢ (%→?→%); @tal_rel_transitive]
+  *#st2mid *#taa2
+  [ *#H2 *#G2 *#K2 #R12
+  | *#H2 *#G2 #R12
+  | *#st2' *#H2 *#G2 *#K2 *#tlr2 *#L2 *#R12 #R12'
+  | *#st2' *#st2'' *#H2 *#G2 *#K2 *#tlr2 *#L2 *#tl2 ** #R12 #R12' #R12''
+  ] destruct #R23 lapply (taa_rel_inv … R23) [1,2: // |3: *#EQ destruct]
+  *#st3mid *#taa3
+  [ *#st3' *#H3 *#G3 *#K3 *#tlr3 *#L3 *#R23 #R23'
+    %{(refl …)} %{st3mid} %{taa3} %{st3'} %{H3} %{G3} %{K3} %{tlr3} %{L3}
+    %{R23} @(tlr_rel_transitive … R12' R23')
+  | *#st3' *#st3'' *#H3 *#G3 *#K3 *#tlr3 *#L3 *#tl3 ** #R23 #R23' #R23''
+    %{st3mid} %{taa3} %{st3'} %{st3''} %{H3} %{G3} %{K3} %{tlr3} %{L3} %{tl3}
+    %{(tal_rel_transitive … R12'' R23'')}
+    %{R23} @(tlr_rel_transitive … R12' R23')
+  ]
+]
+qed.
 
 let rec flatten_trace_label_label
@@ -507 +626 @@
   S st1 fl st2 st3 (taa : trace_any_any S st1 st2) on taa :
   ∀tal : trace_any_label S fl st2 st3.
-    flatten_trace_any_label … (taa_append_tal … taa tal) =
+    flatten_trace_any_label … (taa @ tal) =
       flatten_trace_any_label … tal ≝ ?.
 cases taa -st1 -st2
-[ #st1 #tal %
-| #st_pre #st_init #st2 #H #taa #G #K #tal
-  whd in match (taa_append_tal ???????);
+[ //
+| #st_pre #st_init #st2 #H #G #K #taa' #tal
+  whd in match (? @ ?);
   whd in ⊢ (??%?); //
 ]
-qed.  
-
+qed.
 
 let rec tll_rel_to_traces_same_flatten
@@ -606 +724 @@
   λS : abstract_status. (Σl.∃pc.as_label_of_pc S pc = Some ? l) → ℕ.
 
-definition lift_cost_map_id :
-  ∀S_in, S_out: abstract_status.
-   (∀l. (∃pc.as_label_of_pc S_out pc = Some … l) +
-       ¬(∃pc.as_label_of_pc S_out pc = Some … l)) →
-  (as_cost_map S_out) → as_cost_map S_in ≝ λS_in,S_out,dec,m,l_sig.
-   match dec l_sig with
-   [ inl prf ⇒ m «l_sig, prf»
-   | inr _ ⇒ 0 (* labels not present in out code get 0 *)
+definition lift_sigma_map_id :
+  ∀A,B : Type[0].∀P_in,P_out : A → Prop.B →
+    (∀a.P_out a + ¬ P_out a) →
+  ((Σa.P_out a) → B) → (Σa.P_in a) → B ≝ λA,B,P_in,P_out,dflt,dec,m,a_sig.
+   match dec a_sig with
+   [ inl prf ⇒ m «a_sig, prf»
+   | inr _ ⇒ dflt (* labels not present in out code get 0 *)
    ].
 
-lemma lift_cost_map_id_eq :
-  ∀S_in, S_out, dec, m, l_in, l_out.
-  pi1 ?? l_in = pi1 ?? l_out → lift_cost_map_id S_in S_out dec m l_in = m l_out.
-#S_in #S_out #dec #m #l_in * #l_out #prf #EQ
-whd in match lift_cost_map_id; normalize nodelta
-cases (dec l_in) normalize nodelta >EQ
-[2: #H @⊥] /2 by refl, absurd/
+lemma lift_sigma_map_id_eq :
+  ∀A,B,P_in,P_out,dflt,dec,m,a_in,a_out.
+  pi1 ?? a_in = pi1 ?? a_out →
+  lift_sigma_map_id A B P_in P_out dflt dec m a_in = m a_out.
+#A#B#P_in#P_out#dflt#dec#m#a_in#a_out#EQ
+whd in match lift_sigma_map_id; normalize nodelta
+cases (dec a_in) normalize nodelta >EQ cases a_out
+#a #H #G [ % | @⊥ /2 by absurd/ ]
 qed.
 
@@ -631 +749 @@
   with precedence 20
 for @{'fold plus 0 (λ${ident i}:$X.true) (λ${ident i}:$Y. $f) $l}.
+
+definition lift_cost_map_id :
+  ∀S_in,S_out : abstract_status.? →
+  as_cost_map S_out → as_cost_map S_in
+  ≝
+ λS_in,S_out : abstract_status.
+  lift_sigma_map_id costlabel ℕ
+    (λl.∃pc.as_label_of_pc S_in pc = Some ? l)
+    (λl.∃pc.as_label_of_pc S_out pc = Some ? l)
+    0.
 
 lemma lift_cost_map_same_cost :
@@ -645 +773 @@
   #EQ destruct
   whd in ⊢(??%%);
-  >(lift_cost_map_id_eq … e0)
+  whd in match lift_cost_map_id; normalize nodelta
+  >(lift_sigma_map_id_eq ????????? e0)
   >e0 in e1; normalize in ⊢(%→?); #EQ
   >(IH … EQ) %