Ignore:
Timestamp:
Mar 5, 2012, 12:38:26 PM (8 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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StructuredTraces.ma

    r1783 r1806  
    9595          trace_any_label S end_flag status_pre status_end.
    9696
    97 coinductive trace_label_diverges (S:abstract_status) : S → Type[0] ≝
    98   | tld_step:
    99       ∀status_initial: S.
    100       ∀status_labelled: S.
    101           trace_label_label S doesnt_end_with_ret status_initial status_labelled →
    102           trace_label_diverges S status_labelled →
    103             trace_label_diverges S status_initial
    104   | tld_base:
    105       ∀status_initial: S.
    106       ∀status_pre_fun_call: S.
    107       ∀status_start_fun_call: S.
    108         trace_label_call S status_initial status_pre_fun_call →
    109         as_execute S status_pre_fun_call status_start_fun_call →
    110         ∀H:as_classifier S status_pre_fun_call cl_call.
    111           trace_label_diverges S status_start_fun_call →
    112             trace_label_diverges S status_initial
    113              
    114 with trace_label_call: S → S → Type[0] ≝
    115   | tlc_base:
    116       ∀start_status: S.
    117       ∀end_status: S.
    118         trace_any_call S start_status end_status →
    119         as_costed S start_status →
    120         trace_label_call S start_status end_status
    121        
    122 with trace_any_call: S → S → Type[0] ≝
     97inductive trace_any_call (S:abstract_status) : S → S → Type[0] ≝
    12398  | tac_base:
    12499      ∀status: S.
     
    147122          trace_any_call S status_pre status_end.
    148123
     124
     125coinductive trace_label_diverges (S:abstract_status) : S → Type[0] ≝
     126  | tld_step:
     127      ∀status_initial: S.
     128      ∀status_labelled: S.
     129          trace_label_label S doesnt_end_with_ret status_initial status_labelled →
     130          trace_label_diverges S status_labelled →
     131            trace_label_diverges S status_initial
     132  | tld_base:
     133      ∀status_initial: S.
     134      ∀status_pre_fun_call: S.
     135      ∀status_start_fun_call: S.
     136        trace_label_call S status_initial status_pre_fun_call →
     137        as_execute S status_pre_fun_call status_start_fun_call →
     138        ∀H:as_classifier S status_pre_fun_call cl_call.
     139          trace_label_diverges S status_start_fun_call →
     140            trace_label_diverges S status_initial
     141             
     142with trace_label_call: S → S → Type[0] ≝
     143  | tlc_base:
     144      ∀start_status: S.
     145      ∀end_status: S.
     146        trace_any_call S start_status end_status →
     147        as_costed S start_status →
     148        trace_label_call S start_status end_status
     149.       
     150
    149151let rec trace_any_label_label S s s' f
    150152  (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 ] ≝
     
    164166qed.
    165167
     168lemma trace_any_call_call : ∀S,s,s'.
     169  trace_any_call S s s' → as_classifier S s' cl_call.
     170#S #s #s' #T elim T //
     171qed.
Note: See TracChangeset for help on using the changeset viewer.