Changeset 1806 for src/common/StructuredTraces.ma

Timestamp:

Mar 5, 2012, 12:38:26 PM (9 years ago)

Author:

campbell

Message:

Show that we could construct RTLabs non-terminating structured traces
if it weren't for Prop/Type?/coinduction issue.
Separate out the inductive part of the coinductive structured traces so
that we get an induction principle.

File:

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

src/common/StructuredTraces.ma

@@ -95 +95 @@
           trace_any_label S end_flag status_pre status_end.
 
-coinductive trace_label_diverges (S:abstract_status) : S → Type[0] ≝
-  | tld_step:
-      ∀status_initial: S.
-      ∀status_labelled: S.
-          trace_label_label S doesnt_end_with_ret status_initial status_labelled →
-          trace_label_diverges S status_labelled →
-            trace_label_diverges S status_initial
-  | tld_base:
-      ∀status_initial: S.
-      ∀status_pre_fun_call: S.
-      ∀status_start_fun_call: S.
-        trace_label_call S status_initial status_pre_fun_call →
-        as_execute S status_pre_fun_call status_start_fun_call →
-        ∀H:as_classifier S status_pre_fun_call cl_call.
-          trace_label_diverges S status_start_fun_call →
-            trace_label_diverges S status_initial
-              
-with trace_label_call: S → S → Type[0] ≝
-  | tlc_base:
-      ∀start_status: S.
-      ∀end_status: S.
-        trace_any_call S start_status end_status →
-        as_costed S start_status →
-        trace_label_call S start_status end_status
-        
-with trace_any_call: S → S → Type[0] ≝
+inductive trace_any_call (S:abstract_status) : S → S → Type[0] ≝
   | tac_base:
       ∀status: S.
@@ -147 +122 @@
           trace_any_call S status_pre status_end.
 
+
+coinductive trace_label_diverges (S:abstract_status) : S → Type[0] ≝
+  | tld_step:
+      ∀status_initial: S.
+      ∀status_labelled: S.
+          trace_label_label S doesnt_end_with_ret status_initial status_labelled →
+          trace_label_diverges S status_labelled →
+            trace_label_diverges S status_initial
+  | tld_base:
+      ∀status_initial: S.
+      ∀status_pre_fun_call: S.
+      ∀status_start_fun_call: S.
+        trace_label_call S status_initial status_pre_fun_call →
+        as_execute S status_pre_fun_call status_start_fun_call →
+        ∀H:as_classifier S status_pre_fun_call cl_call.
+          trace_label_diverges S status_start_fun_call →
+            trace_label_diverges S status_initial
+              
+with trace_label_call: S → S → Type[0] ≝
+  | tlc_base:
+      ∀start_status: S.
+      ∀end_status: S.
+        trace_any_call S start_status end_status →
+        as_costed S start_status →
+        trace_label_call S start_status end_status
+.        
+
 let rec trace_any_label_label S s s' f
   (tr:trace_any_label S f s s') on tr : match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ] ≝
@@ -164 +166 @@
 qed.
 
+lemma trace_any_call_call : ∀S,s,s'.
+  trace_any_call S s s' → as_classifier S s' cl_call.
+#S #s #s' #T elim T //
+qed.