Changeset 1638 for src/RTLabs/Traces.ma


Ignore:
Timestamp:
Jan 10, 2012, 4:31:27 PM (8 years ago)
Author:
campbell
Message:

Tidy up RTLabs structured traces code a little.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1637 r1638  
    229229.
    230230
     231(* The way we will use [will_return] won't satisfy Matita's guardedness check,
     232   so we will measure the length of these termination proofs and use an upper
     233   bound to show termination of the finite structured trace construction
     234   functions. *)
     235
    231236let rec will_return_length ge d s tr (T:will_return ge d s tr) on T : nat ≝
    232237match T with
     
    236241| wr_base _ _ _ _ _ _ ⇒ S O
    237242].
     243
    238244include alias "arithmetics/nat.ma".
    239245
     246(* Specialised to the particular situation it is used in. *)
    240247lemma wrl_nonzero : ∀ge,d,s,tr,T. O ≥ 3 * (will_return_length ge d s tr T) → False.
    241248#ge #d #s #tr * #s1 #tr1 #s2 [ 1,2,3: #d ] #EX #tr' #CL [1,2,3:#IH]
     
    246253normalize #E destruct
    247254qed.
    248 (*
    249 lemma wrl_nonzero : ∀ge,d,s,tr,T. ∀P:nat → Prop. (∀x. P (S x)) → P (will_return_length ge d s tr T).
    250 #ge #d #s #tr * #s1 #tr1 #s2 [ 1,2,3: #d ] #EX #tr' #CL [1,2,3:#IH] #P #H @H
    251 qed.
    252 *)
    253 discriminator nat.
    254 
    255 lemma will_return_call : ∀ge,depth,s,trace.
    256   will_return ge depth s trace →
    257   will_return ge (pred depth) s trace.
    258 #ge #depth #s #trace #H elim H
    259 [ #s1 #tr #s2 #d #EX #trc #CL #H1 #H2 %1 //
    260 | #s1 #tr #s2 #d #EX #trc #CL #H1 #H2 %2 //
    261   cases d in H1 H2 ⊢ %; //
    262 | #s1 #tr #s2 #d #EX #trc #CL #H1 #H2
    263   cases d in H1 H2 ⊢ %; [ #H1 #H2 %4 // | /2/ ]
    264 | #s1 #tr #s2 #EX #trc #CL %4 //
    265 ] qed.
    266 
    267 lemma will_return_call' : ∀ge,d,s,tr,s',EX,trace.
     255
     256(* Inversion lemmas on [will_return] that also note the effect on the length
     257   of the proof. *)
     258lemma will_return_call : ∀ge,d,s,tr,s',EX,trace.
    268259  RTLabs_classify s = cl_call →
    269260  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
     
    451442
    452443(* A bit of mucking around with the depth to avoid proving termination after
    453   termination. *)
     444   termination.  Note that we keep a proof that our upper bound on the length
     445   of the termination proof is respected. *)
    454446record trace_result (ge:genv) (depth:nat) (T:state → Type[0]) (limit:nat) : Type[0] ≝ {
    455447  new_state : state;
     
    463455}.
    464456
     457(* The same with a flag indicating whether the function returned, as opposed to
     458   encountering a label. *)
    465459record sub_trace_result (ge:genv) (depth:nat) (T:trace_ends_with_ret → state → Type[0]) (limit:nat) : Type[0] ≝ {
    466460  ends : trace_ends_with_ret;
    467461  trace_res :> trace_result ge (match ends with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth]) (T ends) limit
    468462}.
     463
     464(* We often return the result from a recursive call with an addition to the
     465   structured trace, so we define a couple of functions to help.  The bound on
     466   the size of the termination proof might need to be relaxed, too. *)
    469467
    470468definition replace_trace : ∀ge,d,T1,T2,l1,l2. l2 ≥ l1 →
     
    488486    (replace_trace … lGE … r trace).
    489487
     488(* Small syntax hack to avoid ambiguous input problems. *)
    490489definition myge : nat → nat → Prop ≝ ge.
    491490
     
    498497  (TIME: nat)
    499498  (TERMINATES_IN_TIME: myge TIME (plus 2 (times 3 (will_return_length … TERMINATES))))
    500   on TIME : trace_result ge depth (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝
     499  on TIME : trace_result ge depth
     500              (trace_label_return (RTLabs_status ge) s)
     501              (will_return_length … TERMINATES) ≝
     502             
    501503match TIME return λTIME. TIME ≥ ? → ? with
    502504[ O ⇒ λTERMINATES_IN_TIME. ⊥
    503505| S TIME ⇒ λTERMINATES_IN_TIME.
    504   let r ≝ make_label_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES TIME ? in
     506
     507  let r ≝ make_label_label ge depth s
     508            trace
     509            ENV_COSTLABELLED
     510            STATE_COSTLABELLED
     511            STATEMENT_COSTLABEL
     512            TERMINATES
     513            TIME ? in
    505514  match ends … r return λx. trace_result ge (match x with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth]) (trace_label_label (RTLabs_status ge) x s) ? → trace_result ge depth (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) with
    506515  [ ends_with_ret ⇒ λr.
     
    508517  | doesnt_end_with_ret ⇒ λr.
    509518      let r' ≝ make_label_return ge depth (new_state … r)
    510                  (remainder … r) ENV_COSTLABELLED (cost_labelled … r) ? (pi1 … (terminates … r)) TIME ? in
     519                 (remainder … r)
     520                 ENV_COSTLABELLED
     521                 (cost_labelled … r) ?
     522                 (pi1 … (terminates … r)) TIME ? in
    511523        replace_trace … r'
    512           (tlr_step (RTLabs_status ge) s (new_state … r) (new_state … r') (new_trace … r) (new_trace … r'))
     524          (tlr_step (RTLabs_status ge) s (new_state … r)
     525            (new_state … r') (new_trace … r) (new_trace … r'))
    513526  ] (trace_res … r)
     527
    514528] TERMINATES_IN_TIME
     529
    515530
    516531and make_label_label ge depth s
     
    522537  (TIME: nat)
    523538  (TERMINATES_IN_TIME:  myge TIME (plus 1 (times 3 (will_return_length … TERMINATES))))
    524   on TIME : sub_trace_result ge depth (λends. trace_label_label (RTLabs_status ge) ends s) (will_return_length … TERMINATES) ≝
     539  on TIME : sub_trace_result ge depth
     540              (λends. trace_label_label (RTLabs_status ge) ends s)
     541              (will_return_length … TERMINATES) ≝
     542             
    525543match TIME return λTIME. TIME ≥ ? → ? with
    526544[ O ⇒ λTERMINATES_IN_TIME. ⊥
    527545| S TIME ⇒ λTERMINATES_IN_TIME.
     546
    528547let r ≝ make_any_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES TIME ? in
    529548  replace_sub_trace … r
    530549    (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) STATEMENT_COSTLABEL)
     550
    531551] TERMINATES_IN_TIME
     552
    532553
    533554and make_any_label ge depth s
     
    538559  (TIME: nat)
    539560  (TERMINATES_IN_TIME: myge TIME (times 3 (will_return_length … TERMINATES)))
    540   on TIME : sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TERMINATES) ≝
     561  on TIME : sub_trace_result ge depth
     562              (λends. trace_any_label (RTLabs_status ge) ends s)
     563              (will_return_length … TERMINATES) ≝
    541564
    542565match TIME return λTIME. TIME ≥ ? → ? with
    543566[ O ⇒ λTERMINATES_IN_TIME. ⊥
    544567| S TIME ⇒ λTERMINATES_IN_TIME.
     568
    545569  match trace return λs,trace. well_cost_labelled_state s → ∀TM:will_return ??? trace. myge ? (times 3 (will_return_length ??? trace TM)) → sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TM) with
    546   [ ft_stop st FINAL ⇒ λSTATE_COSTLABELLED,TERMINATES. ?
     570  [ ft_stop st FINAL ⇒
     571      λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ?
     572
    547573  | ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME.
    548574    match RTLabs_classify start return λx. RTLabs_classify start = x → sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
    549575    [ cl_other ⇒ λCL.
    550576        match RTLabs_cost next return λx. RTLabs_cost next = x → sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
     577        (* We're about to run into a label. *)
    551578        [ true ⇒ λCS.
    552579            mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start) ?
    553580              doesnt_end_with_ret
    554               (mk_trace_result ge ??? next trace' ? (tal_base_not_return (RTLabs_status ge) start next ???) ?)
     581              (mk_trace_result ge ??? next trace' ?
     582                (tal_base_not_return (RTLabs_status ge) start next ???) ?)
     583        (* An ordinary step, keep going. *)
    555584        | false ⇒ λCS.
    556             let r ≝ make_any_label ge depth next trace' ENV_COSTLABELLED ?? TIME ? in
     585            let r ≝ make_any_label ge depth next trace' ENV_COSTLABELLED ? (will_return_notfn … TERMINATES) TIME ? in
    557586                replace_sub_trace … r
    558                   (tal_step_default (RTLabs_status ge) (ends … r) start next (new_state … r) ? (new_trace … r) ??)
     587                  (tal_step_default (RTLabs_status ge) (ends … r)
     588                     start next (new_state … r) ? (new_trace … r) ??)
    559589        ] (refl ??)
     590       
    560591    | cl_jump ⇒ λCL.
    561592        mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start) ?
    562593          doesnt_end_with_ret
    563           (mk_trace_result ge ??? next trace' ? (tal_base_not_return (RTLabs_status ge) start next ???) ?)
     594          (mk_trace_result ge ??? next trace' ?
     595            (tal_base_not_return (RTLabs_status ge) start next ???) ?)
     596           
    564597    | cl_call ⇒ λCL.
    565         let r ≝ make_label_return ge (S depth) next trace' ENV_COSTLABELLED ??? TIME ? in
    566         let r' ≝ make_any_label ge depth (new_state … r) (remainder … r) ENV_COSTLABELLED ? (pi1 … (terminates … r)) TIME ? in
     598        let r ≝ make_label_return ge (S depth) next trace' ENV_COSTLABELLED ?? (will_return_call … TERMINATES) TIME ? in
     599        let r' ≝ make_any_label ge depth
     600                   (new_state … r) (remainder … r) ENV_COSTLABELLED ?
     601                   (pi1 … (terminates … r)) TIME ? in
    567602        replace_sub_trace … r'
    568           (tal_step_call (RTLabs_status ge) (ends … r') start next (new_state … r) (new_state … r') ? CL ? (new_trace … r) (new_trace … r'))
     603          (tal_step_call (RTLabs_status ge) (ends … r')
     604            start next (new_state … r) (new_state … r') ? CL ?
     605            (new_trace … r) (new_trace … r'))
     606
    569607    | cl_return ⇒ λCL.
    570608        mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start) ?
     
    577615            ?)
    578616    ] (refl ? (RTLabs_classify start))
     617   
    579618  | ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥
     619 
    580620  ] STATE_COSTLABELLED TERMINATES TERMINATES_IN_TIME
    581621] TERMINATES_IN_TIME.
     
    597637| @le_S_S_to_le @TERMINATES_IN_TIME
    598638| @(wrl_nonzero … TERMINATES_IN_TIME)
    599 |
     639| (* Bad - we've reached the end of the trace; need to fix semantics so that
     640     this can't happen *)
    600641| @(will_return_return … CL TERMINATES)
    601642| %{tr} @EV
     
    606647| @(well_cost_labelled_jump … EV) //
    607648| @(well_cost_labelled_state_step  … EV) //
    608 | 27: @(will_return_call' … CL TERMINATES)
    609649| cases r #H1 #H2 #H3 #H4 * #H5
    610   cases (will_return_call' … CL TERMINATES)
     650  cases (will_return_call … CL TERMINATES)
    611651  #TM #X #Y @le_S_to_le @(transitive_lt … Y X)
    612 | (* oh dear *)
     652| (* TODO oh dear *)
    613653| %{tr} @EV
    614654| @(cost_labelled … r)
    615655| cases r #H72 #H73 #H74 #H75 * #H76 #H78
    616656  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
    617   cases (will_return_call' … TERMINATES) in H78;
     657  cases (will_return_call … TERMINATES) in H78;
    618658  #X #Y #Z
    619659  @(transitive_le … (monotonic_lt_times_r 3 … Y))
     
    623663| @(well_cost_labelled_state_step  … EV) //
    624664| @(well_cost_labelled_call … EV) //
    625 | cases (will_return_call' … TERMINATES)
     665| skip
     666| cases (will_return_call … TERMINATES)
    626667  #TM #GT @le_S_S_to_le
    627668  >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times
     
    633674| @CS
    634675| @(well_cost_labelled_state_step  … EV) //
    635 | 39: @(will_return_notfn … TERMINATES) %1 @CL
    636676| cases (will_return_notfn … TERMINATES) #TM @le_S_to_le
    637677| % whd in ⊢ (% → ?); >CS #E destruct
     
    639679| %{tr} @EV
    640680| @(well_cost_labelled_state_step  … EV) //
     681| %1 @CL
    641682| cases (will_return_notfn … TERMINATES) #TM #GT
    642683  @le_S_S_to_le
     
    651692] cases daemon qed.
    652693
     694(* We can initialise TIME with a suitably large value based on the length of the
     695   termination proof. *)
    653696let rec make_label_return' ge depth s
    654697  (trace: flat_trace io_out io_in ge s)
Note: See TracChangeset for help on using the changeset viewer.