Changeset 2503

Timestamp:

Nov 29, 2012, 3:32:50 PM (8 years ago)

Author:

mckinna

Message:

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

File:

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

src/common/StructuredTraces.ma

@@ -31 +31 @@
 
 (* temporary alias for backward compatibility *)
-definition final_abstract_status ≝ abstract_status.
+(* definition final_abstract_status ≝ abstract_status. *)
 
 definition as_costed : ∀a_s : abstract_status.a_s → Prop ≝
   λa_s,st.as_label ? st ≠ None ?.
-
-lemma as_costed_exc : ∀S:abstract_status. ∀s:S. (as_costed S s) ∨ (¬as_costed S s).
-#S #s whd in match (as_costed S s);
-cases (as_label S s) [ %2 % * /2/ | #c %1 % #E destruct ]
-qed.
 
 definition as_label_safe : ∀a_s : abstract_status.
   (Σs : a_s.as_costed ? s) → costlabel ≝
   λa_s,st_sig.opt_safe … (pi2 … st_sig).
+
+lemma as_costed_exc : ∀S:abstract_status. ∀s:S. (as_costed S s) + (¬as_costed S s).
+#S #s whd in match (as_costed S s);
+cases (as_label S s) [ %2 % * /2/ | #c %1 % #E destruct ]
+qed.
+
+lemma not_costed_no_label : ∀S,st.
+  ¬as_costed S st →
+  as_label S st = None ?.
+#S #st * normalize cases (as_label_of_pc S ?)
+[ // | #l #H cases (H ?) % #E destruct ]
+qed.
+
+(* cost maps generalities *)
+
+definition as_cost_labelled ≝
+  λS : abstract_status. λl.∃pc.as_label_of_pc S pc = Some ? l.
+
+definition as_cost_label ≝
+  λS : abstract_status. Σl.as_cost_labelled S l. 
+
+definition as_cost_labels ≝
+  λS : abstract_status. list (as_cost_label S). 
+
+definition as_cost_get_label ≝
+  λS : abstract_status. λl_sig: as_cost_label S. pi1 … l_sig. 
+
+definition as_cost_get_labels ≝
+  λS : abstract_status. map … (as_cost_get_label S). 
+
+definition as_cost_map ≝
+  (* λS : abstract_status. (Σl.∃pc.as_label_of_pc S pc = Some ? l) → ℕ. *)
+  λS : abstract_status. (as_cost_label S) → ℕ.
+  
+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_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.
+
+notation > "Σ_{ ident i ∈ l } f"
+  with precedence 20
+  for @{'fold plus 0 (λ${ident i}.true) (λ${ident i}. $f) $l}.
+notation < "Σ_{ ident i ∈ l } f"
+  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*) (as_cost_labelled S_in)
+    (*λl.∃pc.as_label_of_pc S_out pc = Some ? l*) (as_cost_labelled S_out)
+    0.
+
+lemma lift_cost_map_same_cost :
+  ∀S_in, S_out, dec, m_out, trace_in, trace_out.
+  map … (pi1 ??) trace_in = map … (pi1 ??) trace_out →
+  (Σ_{ l_sig ∈ trace_in } (lift_cost_map_id S_in S_out dec m_out l_sig)) =
+  (Σ_{ l_sig ∈ trace_out } (m_out l_sig)).
+#S_in #S_out #dec #m_out #trace_in elim trace_in
+[2: #hd_in #tl_in #IH] * [2,4: #hd_out #tl_out]
+normalize in ⊢ (%→?);
+[2,3: #ABS destruct(ABS)
+|4: #_ %
+|1:
+  #EQ destruct
+  whd in ⊢(??%%);
+  whd in match lift_cost_map_id; normalize nodelta
+  >(lift_sigma_map_id_eq ????????? e0)
+  >e0 in e1; normalize in ⊢(%→?); #EQ
+  >(IH … EQ) %
+]
+qed.
+
+
+(* structured traces: down to business *)
 
 inductive trace_ends_with_ret: Type[0] ≝
@@ -189 +276 @@
 qed.
 
-lemma not_costed_no_label : ∀S,st.
-  ¬as_costed S st →
-  as_label_of_pc S (as_pc_of S st) = None ?.
-#S #st * normalize cases (as_label_of_pc S ?)
-[ // | #l #H cases (H ?) % #E destruct ]
-qed.
-
 lemma tal_pc_list_start : ∀S,fl,s1,s2. ∀tal: trace_any_label S fl s1 s2.
   ∃tl. tal_pc_list … tal = (as_pc_of S s1)::tl.
@@ -209 +289 @@
 let rec tal_tail_not_costed S fl st1 st2 tal
   (H:Not (as_costed S st1)) on tal :
-  All ? (λl. as_label_of_pc S l = None ?) (tal_pc_list S fl st1 st2 tal) ≝ ?.
+  All ? (λpc. as_label_of_pc S pc = None ?) (tal_pc_list S fl st1 st2 tal) ≝ ?.
 cases tal in H ⊢ %;
 [ #start #final #EX #CL #CS #CS' % // @(not_costed_no_label ?? CS')
@@ -624 +704 @@
     (start_status: S) (final_status: S)
       (the_trace: trace_label_label S trace_ends_flag start_status final_status)
-        on the_trace: list (Σl: costlabel. ∃pc. as_label_of_pc S pc = Some … l) ≝
+        on the_trace: list (as_cost_label S) (*Σl: costlabel. ∃pc. as_label_of_pc S pc = Some … l*) ≝
   match the_trace with
   [ tll_base ends_flag initial final given_trace labelled_proof ⇒
       let label ≝
-        match as_label … initial return λx: option costlabel. x ≠ None costlabel → ? with
+        match as_label … initial return λx: option costlabel. x ≠ None ? → ? with
         [ None ⇒ λabs. ⊥
         | Some l ⇒ λ_. l
@@ -639 +719 @@
     (start_status: S) (final_status: S)
       (the_trace: trace_any_label S trace_ends_flag start_status final_status)
-        on the_trace: list (Σl: costlabel.  ∃pc. as_label_of_pc S pc = Some … l) ≝
+        on the_trace: list (as_cost_label S) (*Σl: costlabel. ∃pc. as_label_of_pc S pc = Some … l*) ≝
   match the_trace with
   [ tal_base_not_return the_status _ _ _ _ ⇒ [ ]
@@ -657 +737 @@
     (start_status: S) (final_status: S)
       (the_trace: trace_label_return S start_status final_status)
-        on the_trace: list (Σl: costlabel.  ∃pc. as_label_of_pc S pc = Some … l) ≝
+        on the_trace: list (as_cost_label S) (*Σl: costlabel. ∃pc. as_label_of_pc S pc = Some … l*) ≝
   match the_trace with
   [ tlr_base before after trace_to_lift ⇒
@@ -681 +761 @@
 qed.
 
+(* JHM: base case now passes the termination checker *)
 let rec taa_append_tal_same_flatten
   S st1 fl st2 st3 (taa : trace_any_any S st1 st2) on taa :
@@ -687 +768 @@
       flatten_trace_any_label … tal ≝ ?.
 cases taa -st1 -st2
-[ //
+[ #st #tal normalize in ⊢ (??%?); //
 | #st_pre #st_init #st2 #H #G #K #taa' #tal
   whd in match (? @ ?);
@@ -797 +878 @@
 qed.
 
-definition as_cost_map ≝
-  λS : abstract_status. (Σl.∃pc.as_label_of_pc S pc = Some ? l) → ℕ.
-
-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_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.
-
-notation > "Σ_{ ident i ∈ l } f"
-  with precedence 20
-  for @{'fold plus 0 (λ${ident i}.true) (λ${ident i}. $f) $l}.
-notation < "Σ_{ ident i ∈ l } f"
-  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 :
-  ∀S_in, S_out, dec, m_out, trace_in, trace_out.
-  map … (pi1 ??) trace_in = map … (pi1 ??) trace_out →
-  (Σ_{ l_sig ∈ trace_in } (lift_cost_map_id S_in S_out dec m_out l_sig)) =
-  (Σ_{ l_sig ∈ trace_out } (m_out l_sig)).
-#S_in #S_out #dec #m_out #trace_in elim trace_in
-[2: #hd_in #tl_in #IH] * [2,4: #hd_out #tl_out]
-normalize in ⊢ (%→?);
-[2,3: #ABS destruct(ABS)
-|4: #_ %
-|1:
-  #EQ destruct
-  whd in ⊢(??%%);
-  whd in match lift_cost_map_id; normalize nodelta
-  >(lift_sigma_map_id_eq ????????? e0)
-  >e0 in e1; normalize in ⊢(%→?); #EQ
-  >(IH … EQ) %
-]
-qed.
+(* cost maps specifics: summing over flattened traces *)
 
 lemma lift_cost_map_same_cost_tal :