Changeset 1637 for src/RTLabs


Ignore:
Timestamp:
Jan 10, 2012, 11:26:48 AM (8 years ago)
Author:
campbell
Message:

RTLabs structured traces: Add a termination measure to satisfy guardedness check.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1617 r1637  
    208208   performs the call/return counting necessary for handling deeper function
    209209   calls.  It should be zero at the top level. *)
    210 inductive will_return (ge:genv) : nat → ∀s. flat_trace io_out io_in ge s → Prop
     210inductive will_return (ge:genv) : nat → ∀s. flat_trace io_out io_in ge s → Type[0]
    211211| wr_step : ∀s,tr,s',depth,EX,trace.
    212212    RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump →
     
    229229.
    230230
     231let rec will_return_length ge d s tr (T:will_return ge d s tr) on T : nat ≝
     232match T with
     233[ wr_step _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
     234| wr_call _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
     235| wr_ret _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
     236| wr_base _ _ _ _ _ _ ⇒ S O
     237].
     238include alias "arithmetics/nat.ma".
     239
     240lemma wrl_nonzero : ∀ge,d,s,tr,T. O ≥ 3 * (will_return_length ge d s tr T) → False.
     241#ge #d #s #tr * #s1 #tr1 #s2 [ 1,2,3: #d ] #EX #tr' #CL [1,2,3:#IH]
     242whd in ⊢ (??(??%) → ?);
     243>commutative_times
     244#H lapply (le_plus_b … H)
     245#H lapply (le_to_leb_true … H)
     246normalize #E destruct
     247qed.
     248(*
     249lemma 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
     251qed.
     252*)
    231253discriminator nat.
    232254
     
    243265] qed.
    244266
     267lemma will_return_call' : ∀ge,d,s,tr,s',EX,trace.
     268  RTLabs_classify s = cl_call →
     269  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
     270  ΣTM':will_return ge (S d) s' trace. will_return_length … TM > will_return_length … TM'.
     271#ge #d #s #tr #s' #EX #trace #CL #TERM inversion TERM
     272[ #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 @⊥ destruct >CL in H25; * #E destruct
     273| #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 destruct % //
     274| #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 @⊥ destruct >CL in H53; #E destruct
     275| #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 @⊥ destruct >CL in H66; #E destruct
     276] qed.
     277
     278lemma will_return_return : ∀ge,d,s,tr,s',EX,trace.
     279  RTLabs_classify s = cl_return →
     280  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
     281  match d with
     282  [ O ⇒ True
     283  | S d' ⇒
     284      ΣTM':will_return ge d' s' trace. will_return_length … TM > will_return_length … TM'
     285  ].
     286#ge #d #s #tr #s' #EX #trace #CL #TERM inversion TERM
     287[ #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 @⊥ destruct >CL in H25; * #E destruct
     288| #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 @⊥  destruct >CL in H39; #E destruct
     289| #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 destruct % //
     290| #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct @I
     291] qed.
    245292
    246293lemma will_return_notfn : ∀ge,d,s,tr,s',EX,trace.
    247   RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump
    248   will_return ge d s (ft_step ?? ge s tr s' EX trace) →
    249   will_return ge d s' trace.
     294  (RTLabs_classify s = cl_other) ⊎ (RTLabs_classify s = cl_jump)
     295  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
     296  ΣTM':will_return ge d s' trace. will_return_length … TM > will_return_length … TM'.
    250297#ge #d #s #tr #s' #EX #trace * #CL #TERM inversion TERM
    251 [ #H290 #H291 #H292 #H293 #H294 #H295 #H296 #H297 #H298 #H299 #H300 #H301 #H302 destruct //
    252 | #H304 #H305 #H306 #H307 #H308 #H309 #H310 #H311 #H312 #H313 #H314 #H315 #H316 destruct >CL in H310; #E destruct
    253 | #H318 #H319 #H320 #H321 #H322 #H323 #H324 #H325 #H326 #H327 #H328 #H329 #H330 destruct >CL in H324; #E destruct
    254 | #H332 #H333 #H334 #H335 #H336 #H337 #H338 #H339 #H340 #H341 destruct >CL in H337; #E destruct
    255 | #H343 #H344 #H345 #H346 #H347 #H348 #H349 #H350 #H351 #H352 #H353 #H354 #H355 destruct //
    256 | #H357 #H358 #H359 #H360 #H361 #H362 #H363 #H364 #H365 #H366 #H367 #H368 #H369 destruct >CL in H363; #E destruct
    257 | #H371 #H372 #H373 #H374 #H375 #H376 #H377 #H378 #H379 #H380 #H381 #H382 #H383 destruct >CL in H377; #E destruct
    258 | #H385 #H386 #H387 #H388 #H389 #H390 #H391 #H392 #H393 #H394 destruct >CL in H390; #E destruct
     298[ #H290 #H291 #H292 #H293 #H294 #H295 #H296 #H297 #H298 #H299 #H300 #H301 #H302 destruct % //
     299| #H304 #H305 #H306 #H307 #H308 #H309 #H310 #H311 #H312 #H313 #H314 #H315 #H316 @⊥ destruct >CL in H310; #E destruct
     300| #H318 #H319 #H320 #H321 #H322 #H323 #H324 #H325 #H326 #H327 #H328 #H329 #H330 @⊥ destruct >CL in H324; #E destruct
     301| #H332 #H333 #H334 #H335 #H336 #H337 #H338 #H339 #H340 #H341 @⊥ destruct >CL in H337; #E destruct
     302| #H343 #H344 #H345 #H346 #H347 #H348 #H349 #H350 #H351 #H352 #H353 #H354 #H355 destruct % //
     303| #H357 #H358 #H359 #H360 #H361 #H362 #H363 #H364 #H365 #H366 #H367 #H368 #H369 @⊥ destruct >CL in H363; #E destruct
     304| #H371 #H372 #H373 #H374 #H375 #H376 #H377 #H378 #H379 #H380 #H381 #H382 #H383 @⊥ destruct >CL in H377; #E destruct
     305| #H385 #H386 #H387 #H388 #H389 #H390 #H391 #H392 #H393 #H394 @⊥ destruct >CL in H390; #E destruct
    259306] qed.
    260307
     
    405452(* A bit of mucking around with the depth to avoid proving termination after
    406453  termination. *)
    407 record trace_result (ge:genv) (depth:nat) (T:state → Type[0]) : Type[0] ≝ {
     454record trace_result (ge:genv) (depth:nat) (T:state → Type[0]) (limit:nat) : Type[0] ≝ {
    408455  new_state : state;
    409456  remainder : flat_trace io_out io_in ge new_state;
     
    412459  terminates : match depth with
    413460               [ O ⇒ True
    414                | S d ⇒ will_return ge d new_state remainder
     461               | S d ⇒ ΣTM:will_return ge d new_state remainder. limit > will_return_length … TM
    415462               ]
    416463}.
    417464
    418 record sub_trace_result (ge:genv) (depth:nat) (T:trace_ends_with_ret → state → Type[0]) : Type[0] ≝ {
     465record sub_trace_result (ge:genv) (depth:nat) (T:trace_ends_with_ret → state → Type[0]) (limit:nat) : Type[0] ≝ {
    419466  ends : trace_ends_with_ret;
    420   trace_res :> trace_result ge (match ends with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth]) (T ends)
     467  trace_res :> trace_result ge (match ends with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth]) (T ends) limit
    421468}.
    422469
    423 definition replace_sub_trace : ∀ge,trm,T1,T2.
    424   ∀r:sub_trace_result ge trm T1. T2 (ends … r) (new_state … r) → sub_trace_result ge trm T2 ≝
    425 λge,trm,T1,T2,r,trace.
    426   mk_sub_trace_result ge trm T2
    427     (ends … r)
    428     (mk_trace_result ge ? (T2 (ends … r))
    429       (new_state … r)
    430       (remainder … r)
    431       (cost_labelled … r)
    432       trace
    433       (terminates … r)
    434     )
    435 .
    436 
    437 definition replace_trace : ∀ge,trm,T1,T2.
    438   ∀r:trace_result ge trm T1. T2 (new_state … r) → trace_result ge trm T2 ≝
    439 λge,trm,T1,T2,r,trace.
    440   mk_trace_result ge trm T2
     470definition replace_trace : ∀ge,d,T1,T2,l1,l2. l2 ≥ l1 →
     471  ∀r:trace_result ge d T1 l1. T2 (new_state … r) → trace_result ge d T2 l2 ≝
     472λge,d,T1,T2,l1,l2,lGE,r,trace.
     473  mk_trace_result ge d T2 l2
    441474    (new_state … r)
    442475    (remainder … r)
    443476    (cost_labelled … r)
    444477    trace
    445     (terminates … r)
    446 .
     478    (match d return λd'.match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l1 > will_return_length ge d'' (new_state … r) (remainder … r) TM] →
     479                        match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l2 > will_return_length ge d'' (new_state … r) (remainder … r) TM] with
     480     [O ⇒ λ_. I | _ ⇒ λTM. «pi1 … TM, ?» ] (terminates ???? r))
     481. @(transitive_le … lGE) @(pi2 … TM) qed.
     482
     483definition replace_sub_trace : ∀ge,d,T1,T2,l1,l2. l2 ≥ l1 →
     484  ∀r:sub_trace_result ge d T1 l1. T2 (ends … r) (new_state … r) → sub_trace_result ge d T2 l2 ≝
     485λge,d,T1,T2,l1,l2,lGE,r,trace.
     486  mk_sub_trace_result ge d T2 l2
     487    (ends … r)
     488    (replace_trace … lGE … r trace).
     489
     490definition myge : nat → nat → Prop ≝ ge.
    447491
    448492let rec make_label_return ge depth s
     
    452496  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
    453497  (TERMINATES: will_return ge depth s trace)
    454   : trace_result ge depth (trace_label_return (RTLabs_status ge) s) ≝
    455 
    456   let r ≝ make_label_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES in
    457   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) → ? with
     498  (TIME: nat)
     499  (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) ≝
     501match TIME return λTIME. TIME ≥ ? → ? with
     502[ O ⇒ λTERMINATES_IN_TIME. ⊥
     503| S TIME ⇒ λTERMINATES_IN_TIME.
     504  let r ≝ make_label_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES TIME ? in
     505  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
    458506  [ ends_with_ret ⇒ λr.
    459507      replace_trace … r (tlr_base (RTLabs_status ge) s (new_state … r) (new_trace … r))
    460508  | doesnt_end_with_ret ⇒ λr.
    461509      let r' ≝ make_label_return ge depth (new_state … r)
    462                  (remainder … r) ENV_COSTLABELLED (cost_labelled … r) ? (terminates ??? r) in
     510                 (remainder … r) ENV_COSTLABELLED (cost_labelled … r) ? (pi1 … (terminates … r)) TIME ? in
    463511        replace_trace … r'
    464512          (tlr_step (RTLabs_status ge) s (new_state … r) (new_state … r') (new_trace … r) (new_trace … r'))
    465513  ] (trace_res … r)
     514] TERMINATES_IN_TIME
    466515
    467516and make_label_label ge depth s
     
    471520  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
    472521  (TERMINATES: will_return ge depth s trace)
    473   : sub_trace_result ge depth (λends. trace_label_label (RTLabs_status ge) ends s) ≝
    474 let r ≝ make_any_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES in
     522  (TIME: nat)
     523  (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) ≝
     525match TIME return λTIME. TIME ≥ ? → ? with
     526[ O ⇒ λTERMINATES_IN_TIME. ⊥
     527| S TIME ⇒ λTERMINATES_IN_TIME.
     528let r ≝ make_any_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES TIME ? in
    475529  replace_sub_trace … r
    476530    (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) STATEMENT_COSTLABEL)
     531] TERMINATES_IN_TIME
    477532
    478533and make_any_label ge depth s
     
    481536  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
    482537  (TERMINATES: will_return ge depth s trace)
    483   : sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends s) ≝
    484 match trace return λs,trace. well_cost_labelled_state s → will_return ??? trace → sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends s) with
    485 [ ft_stop st FINAL ⇒ λSTATE_COSTLABELLED,TERMINATES. ?
    486 | ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES.
    487     match RTLabs_classify start return λx. RTLabs_classify start = x → ? with
     538  (TIME: nat)
     539  (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) ≝
     541
     542match TIME return λTIME. TIME ≥ ? → ? with
     543[ O ⇒ λTERMINATES_IN_TIME. ⊥
     544| S TIME ⇒ λTERMINATES_IN_TIME.
     545  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. ?
     547  | ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME.
     548    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
    488549    [ cl_other ⇒ λCL.
    489         match RTLabs_cost next return λx. RTLabs_cost next = x → ? with
     550        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
    490551        [ true ⇒ λCS.
    491             mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start)
     552            mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start) ?
    492553              doesnt_end_with_ret
    493               (mk_trace_result ge ?? next trace' ? (tal_base_not_return (RTLabs_status ge) start next ???) ?)
     554              (mk_trace_result ge ??? next trace' ? (tal_base_not_return (RTLabs_status ge) start next ???) ?)
    494555        | false ⇒ λCS.
    495             let r ≝ make_any_label ge depth next trace' ENV_COSTLABELLED ?? in
     556            let r ≝ make_any_label ge depth next trace' ENV_COSTLABELLED ?? TIME ? in
    496557                replace_sub_trace … r
    497558                  (tal_step_default (RTLabs_status ge) (ends … r) start next (new_state … r) ? (new_trace … r) ??)
    498559        ] (refl ??)
    499560    | cl_jump ⇒ λCL.
    500         mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start)
     561        mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start) ?
    501562          doesnt_end_with_ret
    502           (mk_trace_result ge ?? next trace' ? (tal_base_not_return (RTLabs_status ge) start next ???) ?)
     563          (mk_trace_result ge ??? next trace' ? (tal_base_not_return (RTLabs_status ge) start next ???) ?)
    503564    | cl_call ⇒ λCL.
    504         let r ≝ make_label_return ge (S depth) next trace' ENV_COSTLABELLED ??? in
    505         let r' ≝ make_any_label ge depth (new_state … r) (remainder … r) ENV_COSTLABELLED ?? in
    506         replace_sub_trace ???? r'
     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
     567        replace_sub_trace r'
    507568          (tal_step_call (RTLabs_status ge) (ends … r') start next (new_state … r) (new_state … r') ? CL ? (new_trace … r) (new_trace … r'))
    508569    | cl_return ⇒ λCL.
    509         mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start)
     570        mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start) ?
    510571          ends_with_ret
    511           (mk_trace_result ge ??
     572          (mk_trace_result ge ???
    512573            next
    513574            trace'
     
    516577            ?)
    517578    ] (refl ? (RTLabs_classify start))
    518 | ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥
    519 ] STATE_COSTLABELLED TERMINATES.
    520 
    521 [ @(trace_label_label_label … (new_trace … r))
     579  | ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥
     580  ] STATE_COSTLABELLED TERMINATES TERMINATES_IN_TIME
     581] TERMINATES_IN_TIME.
     582
     583[ cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ]
     584| //
     585| cases r #H1 #H2 #H3 #H4 * #x @le_S_to_le
     586| @(trace_label_label_label … (new_trace … r))
     587| cases r #H1 #H2 #H3 #H4 * #H5 #H6
     588  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
     589  @(transitive_le …  (3*(will_return_length … TERMINATES)))
     590  [ >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times
     591    @(monotonic_le_times_r 3 … H6)
     592  | @le_S @le_S @le_n
     593  ]
     594| @le_S_S_to_le @TERMINATES_IN_TIME
     595| cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ]
     596| @le_n
     597| @le_S_S_to_le @TERMINATES_IN_TIME
     598| @(wrl_nonzero … TERMINATES_IN_TIME)
    522599|
    523 | inversion TERMINATES
    524   [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 -TERMINATES destruct >CL in H7; * #E destruct
    525   | #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 -TERMINATES destruct >CL in H21; #E destruct
    526   | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 -TERMINATES destruct @H36
    527   | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 whd @I
    528   ]
     600| @(will_return_return … CL TERMINATES)
    529601| %{tr} @EV
    530602| @(well_cost_labelled_state_step  … EV) //
     
    534606| @(well_cost_labelled_jump … EV) //
    535607| @(well_cost_labelled_state_step  … EV) //
     608| 27: @(will_return_call' … CL TERMINATES)
     609| cases r #H1 #H2 #H3 #H4 * #H5
     610  cases (will_return_call' … CL TERMINATES)
     611  #TM #X #Y @le_S_to_le @(transitive_lt … Y X)
    536612| (* oh dear *)
    537613| %{tr} @EV
    538614| @(cost_labelled … r)
    539 | @(terminates … r)
     615| cases r #H72 #H73 #H74 #H75 * #H76 #H78
     616  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
     617  cases (will_return_call' … TERMINATES) in H78;
     618  #X #Y #Z
     619  @(transitive_le … (monotonic_lt_times_r 3 … Y))
     620  [ @(transitive_le … (monotonic_lt_times_r 3 … Z)) //
     621  | //
     622  ]
    540623| @(well_cost_labelled_state_step  … EV) //
    541624| @(well_cost_labelled_call … EV) //
    542 | inversion TERMINATES
    543   [ #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 -TERMINATES destruct >CL in H60; * #E destruct
    544   | #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 -TERMINATES destruct @H75
    545   | #H82 #H83 #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 -TERMINATES destruct >CL in H88; #E destruct
    546   | #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 -TERMINATES destruct >CL in H101; #E destruct
    547   ]
     625| cases (will_return_call' … TERMINATES)
     626  #TM #GT @le_S_S_to_le
     627  >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times
     628  @(transitive_le … TERMINATES_IN_TIME)
     629  @(monotonic_le_times_r 3 … GT)
    548630| whd @(will_return_notfn … TERMINATES) %1 @CL
    549631| %{tr} @EV
     
    551633| @CS
    552634| @(well_cost_labelled_state_step  … EV) //
     635| 39: @(will_return_notfn … TERMINATES) %1 @CL
     636| cases (will_return_notfn … TERMINATES) #TM @le_S_to_le
    553637| % whd in ⊢ (% → ?); >CS #E destruct
    554638| @CL
    555639| %{tr} @EV
    556640| @(well_cost_labelled_state_step  … EV) //
    557 | @(will_return_notfn … TERMINATES) %1 @CL
     641| cases (will_return_notfn … TERMINATES) #TM #GT
     642  @le_S_S_to_le
     643  @(transitive_le … (monotonic_lt_times_r … GT) TERMINATES_IN_TIME)
     644  //
    558645| inversion TERMINATES
    559   [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 -TERMINATES destruct
    560   | #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 -TERMINATES destruct
    561   | #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 -TERMINATES destruct
    562   | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 -TERMINATES destruct
    563   ]
    564 |
    565 
    566 
     646  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 -TERMINATES -TERMINATES destruct
     647  | #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 -TERMINATES -TERMINATES destruct
     648  | #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 -TERMINATES -TERMINATES destruct
     649  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 -TERMINATES -TERMINATES destruct
     650  ]
     651] cases daemon qed.
     652
     653let rec make_label_return' ge depth s
     654  (trace: flat_trace io_out io_in ge s)
     655  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
     656  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
     657  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
     658  (TERMINATES: will_return ge depth s trace)
     659  : trace_result ge depth (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝
     660make_label_return ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES
     661  (2 + 3 * will_return_length … TERMINATES) ?.
     662@le_n
     663qed.
    567664 
    568665(* FIXME: there's trouble at the end of the program because we can't make a step
Note: See TracChangeset for help on using the changeset viewer.