Changeset 1719 for src/RTLabs/Traces.ma


Ignore:
Timestamp:
Feb 22, 2012, 2:06:52 PM (8 years ago)
Author:
campbell
Message:

Show that non-termination survives a terminating function call.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1713 r1719  
    9393] qed.
    9494
    95 inductive flat_trace_prefix (o:Type[0]) (i:o → Type[0]) (ge:genv) : ∀s,s'. flat_trace o i ge s → flat_trace o i ge s' → Prop ≝
    96 | ftp_refl : ∀s,t. flat_trace_prefix o i ge s s t t
    97 | ftp_step : ∀s1,tr,s2,s3,t2,t3,EV.
    98     flat_trace_prefix o i ge s2 s3 t2 t3 →
    99     flat_trace_prefix o i ge s1 s3 (ft_step o i ge s1 tr s2 EV t2) t3
    100 .
    101 
    102 lemma concatenate_flat_trace_prefix : ∀o,i,ge,s1,s2,s3,t1,t2,t3.
    103   flat_trace_prefix o i ge s1 s2 t1 t2 →
    104   flat_trace_prefix o i ge s2 s3 t2 t3 →
    105   flat_trace_prefix o i ge s1 s3 t1 t3.
    106 #o #i #ge #s1 #s2 #s3 #t1 #t2 #t3 #p1 elim p1
    107 [ //
    108 | #s1' #tr #s2' #s3' #t2' #t3' #EV #p2 #IH #p3
    109   %2 /2/
    110 ] qed.
    111 
    11295let corec make_flat_trace ge s
    11396  (H:exec_no_io … (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s))) :
     
    291274normalize #E destruct
    292275qed.
     276   
     277let rec will_return_end ge d s tr (T:will_return ge d s tr) on T : 𝚺s'.flat_trace io_out io_in ge s' ≝
     278match T with
     279[ wr_step _ _ _ _ _ _ _ T' ⇒ will_return_end … T'
     280| wr_call _ _ _ _ _ _ _ T' ⇒ will_return_end … T'
     281| wr_ret _ _ _ _ _ _ _ T' ⇒ will_return_end … T'
     282| wr_base _ _ _ _ tr' _ ⇒ mk_DPair ? (λs.flat_trace io_out io_in ge s) ? tr'
     283].
    293284
    294285(* Inversion lemmas on [will_return] that also note the effect on the length
     
    297288  RTLabs_classify s = cl_call →
    298289  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
    299   ΣTM':will_return ge (S d) s' trace. will_return_length … TM > will_return_length … TM'.
     290  ΣTM':will_return ge (S d) s' trace. will_return_length … TM > will_return_length … TM' ∧ will_return_end … TM = will_return_end … TM'.
    300291#ge #d #s #tr #s' #EX #trace #CL #TERM inversion TERM
    301292[ #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 @⊥ destruct >CL in H25; * #E destruct
    302 | #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 destruct % //
     293| #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 destruct % /2/
    303294| #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 @⊥ destruct >CL in H53; #E destruct
    304295| #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 @⊥ destruct >CL in H66; #E destruct
     
    309300  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
    310301  match d with
    311   [ O ⇒ True
     302  [ O ⇒ will_return_end … TM = ❬s', trace❭
    312303  | S d' ⇒
    313       ΣTM':will_return ge d' s' trace. will_return_length … TM > will_return_length … TM'
     304      ΣTM':will_return ge d' s' trace. will_return_length … TM > will_return_length … TM' ∧ will_return_end … TM = will_return_end … TM'
    314305  ].
    315306#ge #d #s #tr #s' #EX #trace #CL #TERM inversion TERM
    316307[ #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 @⊥ destruct >CL in H25; * #E destruct
    317308| #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 @⊥  destruct >CL in H39; #E destruct
    318 | #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 destruct % //
    319 | #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct @I
     309| #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 destruct % /2/
     310| #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct @refl
    320311] qed.
    321312
     
    323314  (RTLabs_classify s = cl_other) ⊎ (RTLabs_classify s = cl_jump) →
    324315  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
    325   ΣTM':will_return ge d s' trace. will_return_length … TM > will_return_length … TM'.
     316  ΣTM':will_return ge d s' trace. will_return_length … TM > will_return_length … TM' ∧ will_return_end … TM = will_return_end … TM'.
    326317#ge #d #s #tr #s' #EX #trace * #CL #TERM inversion TERM
    327 [ #H290 #H291 #H292 #H293 #H294 #H295 #H296 #H297 #H298 #H299 #H300 #H301 #H302 destruct % //
     318[ #H290 #H291 #H292 #H293 #H294 #H295 #H296 #H297 #H298 #H299 #H300 #H301 #H302 destruct % /2/
    328319| #H304 #H305 #H306 #H307 #H308 #H309 #H310 #H311 #H312 #H313 #H314 #H315 #H316 @⊥ destruct >CL in H310; #E destruct
    329320| #H318 #H319 #H320 #H321 #H322 #H323 #H324 #H325 #H326 #H327 #H328 #H329 #H330 @⊥ destruct >CL in H324; #E destruct
    330321| #H332 #H333 #H334 #H335 #H336 #H337 #H338 #H339 #H340 #H341 @⊥ destruct >CL in H337; #E destruct
    331 | #H343 #H344 #H345 #H346 #H347 #H348 #H349 #H350 #H351 #H352 #H353 #H354 #H355 destruct % //
     322| #H343 #H344 #H345 #H346 #H347 #H348 #H349 #H350 #H351 #H352 #H353 #H354 #H355 destruct % /2/
    332323| #H357 #H358 #H359 #H360 #H361 #H362 #H363 #H364 #H365 #H366 #H367 #H368 #H369 @⊥ destruct >CL in H363; #E destruct
    333324| #H371 #H372 #H373 #H374 #H375 #H376 #H377 #H378 #H379 #H380 #H381 #H382 #H383 @⊥ destruct >CL in H377; #E destruct
    334325| #H385 #H386 #H387 #H388 #H389 #H390 #H391 #H392 #H393 #H394 @⊥ destruct >CL in H390; #E destruct
     326] qed.
     327
     328(* When it comes to building bits of nonterminating executions we'll need to be
     329   able to glue termination proofs together. *)
     330
     331lemma will_return_prepend : ∀ge,d1,s1,t1.
     332  ∀T1:will_return ge d1 s1 t1.
     333  ∀d2,s2,t2.
     334  will_return ge d2 s2 t2 →
     335  will_return_end … T1 = ❬s2, t2❭ →
     336  will_return ge (d1 + S d2) s1 t1.
     337#ge #d1 #s1 #tr1 #T1 elim T1
     338[ #s #tr #s' #depth #EX #t #CL #T #IH #d2 #s2 #t2 #T2 #E
     339  %1 // @(IH … T2) @E
     340| #s #tr #s' #depth #EX #t #CL #T #IH #d2 #s2 #t2 #T2 #E %2 // @(IH … T2) @E
     341| #s #tr #s' #depth #EX #t #CL #T #IH #s2 #s2 #t2 #T2 #E %3 // @(IH … T2) @E
     342| #s #tr #s' #EX #t #CL #d2 #s2 #t2 #T2 #E normalize in E; destruct %3 //
     343] qed.
     344
     345discriminator nat.
     346
     347lemma will_return_remove_call : ∀ge,d1,s1,t1.
     348  ∀T1:will_return ge d1 s1 t1.
     349  ∀d2.
     350  will_return ge (d1 + S d2) s1 t1 →
     351  ∀s2,t2.
     352  will_return_end … T1 = ❬s2, t2❭ →
     353  will_return ge d2 s2 t2.
     354(* The key part of the proof is to show that the two termination proofs follow
     355   the same pattern. *)
     356#ge #d1x #s1x #t1x #T1 elim T1
     357[ #s #tr #s' #d1 #EX #t #CL #T #IH #d2 #T2 #s2 #t2 #E @IH
     358  [ inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 destruct //
     359                 | #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 @⊥ destruct
     360                   >H21 in CL; * #E destruct
     361                 | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 @⊥ destruct
     362                   >H35 in CL; * #E destruct
     363                 | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 @⊥ destruct
     364                   >H48 in CL; * #E destruct
     365                 ]
     366  | @E
     367  ]
     368| #s #tr #s' #d1 #EX #t #CL #T #IH #d2 #T2 #s2 #t2 #E @IH
     369  [ inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 @⊥ destruct
     370                   >CL in H7; * #E destruct
     371                 | #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 destruct //
     372                 | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 @⊥ destruct
     373                   >H35 in CL; #E destruct
     374                 | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 @⊥ destruct
     375                   >H48 in CL; #E destruct
     376                 ]
     377  | @E
     378  ]
     379| #s #tr #s' #d1 #EX #t #CL #T #IH #d2 #T2 #s2 #t2 #E @IH
     380  [ inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 @⊥ destruct
     381                   >CL in H7; * #E destruct
     382                 | #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 @⊥ destruct
     383                   >H21 in CL; #E destruct
     384                 | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41
     385                   whd in H38:(??%??); destruct //
     386                 | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52
     387                   whd in H49:(??%??); @⊥ destruct
     388                 ]
     389  | @E
     390  ]
     391| #s #tr #s' #EX #t #CL #d2 #T2 #s2 #t2 #E whd in E:(??%?); destruct
     392  inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 @⊥ destruct
     393                 >CL in H7; * #E destruct
     394               | #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 @⊥ destruct
     395                 >H21 in CL; #E destruct
     396               | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41
     397                 whd in H38:(??%??); destruct //
     398               | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52
     399                 whd in H49:(??%??); @⊥ destruct
     400               ]
    335401] qed.
    336402
     
    642708   termination.  Note that we keep a proof that our upper bound on the length
    643709   of the termination proof is respected. *)
    644 record trace_result (ge:genv) (depth:nat) (ends:trace_ends_with_ret) (start:state) (full:flat_trace io_out io_in ge start) (T:state → Type[0]) (limit:nat) : Type[0] ≝ {
     710record trace_result (ge:genv) (depth:nat) (ends:trace_ends_with_ret)
     711  (start:state) (full:flat_trace io_out io_in ge start)
     712  (original_terminates: will_return ge depth start full)
     713  (T:state → Type[0]) (limit:nat) : Type[0] ≝
     714{
    645715  new_state : state;
    646716  remainder : flat_trace io_out io_in ge new_state;
    647   is_remainder : flat_trace_prefix … full remainder;
    648717  cost_labelled : well_cost_labelled_state new_state;
    649718  new_trace : T new_state;
    650719  stack_ok : stack_preserved ends start new_state;
    651   terminates : match depth with
    652                [ O ⇒ True
    653                | S d ⇒ ΣTM:will_return ge d new_state remainder. limit > will_return_length … TM
     720  terminates : match (match ends with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth ]) with
     721               [ O ⇒ will_return_end … original_terminates = ❬new_state, remainder❭
     722               | S d ⇒ ΣTM:will_return ge d new_state remainder.
     723                         limit > will_return_length … TM ∧
     724                         will_return_end … original_terminates = will_return_end … TM
    654725               ]
    655726}.
     
    657728(* The same with a flag indicating whether the function returned, as opposed to
    658729   encountering a label. *)
    659 record sub_trace_result (ge:genv) (depth:nat) (start:state) (full:flat_trace io_out io_in ge start) (T:trace_ends_with_ret → state → Type[0]) (limit:nat) : Type[0] ≝ {
     730record sub_trace_result (ge:genv) (depth:nat)
     731  (start:state) (full:flat_trace io_out io_in ge start)
     732  (original_terminates: will_return ge depth start full)
     733  (T:trace_ends_with_ret → state → Type[0]) (limit:nat) : Type[0] ≝
     734{
    660735  ends : trace_ends_with_ret;
    661   trace_res :> trace_result ge (match ends with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth]) ends start full (T ends) limit
     736  trace_res :> trace_result ge depth ends start full original_terminates (T ends) limit
    662737}.
    663738
     
    666741   the size of the termination proof might need to be relaxed, too. *)
    667742
    668 definition replace_trace : ∀ge,d,e1,e2,s1,s2,t1,t2,T1,T2,l1,l2. l2 ≥ l1 →
    669   ∀r:trace_result ge d e1 s1 t1 T1 l1.
    670     (∀s,t. flat_trace_prefix … s1 s t1 t → flat_trace_prefix … s2 s t2 t)
     743definition replace_trace : ∀ge,d,e,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →
     744  ∀r:trace_result ge d e s1 t1 TM1 T1 l1.
     745    will_return_end … TM1 = will_return_end … TM2
    671746    T2 (new_state … r) →
    672     stack_preserved e2 s2 (new_state … r) →
    673     trace_result ge d e2 s2 t2 T2 l2 ≝
    674 λge,d,e1,e2,s1,s2,t1,t2,T1,T2,l1,l2,lGE,r,PRE,trace,SP.
    675   mk_trace_result ge d e2 s2 t2 T2 l2
     747    stack_preserved e s2 (new_state … r) →
     748    trace_result ge d e s2 t2 TM2 T2 l2 ≝
     749λge,d,e,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2,lGE,r,TME,trace,SP.
     750  mk_trace_result ge d e s2 t2 TM2 T2 l2
    676751    (new_state … r)
    677752    (remainder … r)
    678     (PRE ?? (is_remainder ??????? r))
    679753    (cost_labelled … r)
    680754    trace
    681755    SP
    682     (match d return λd'.match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l1 > will_return_length ge d'' (new_state … r) (remainder … r) TM] →
     756    ?
     757    (*(match d return λd'.match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l1 > will_return_length ge d'' (new_state … r) (remainder … r) TM] →
    683758                        match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l2 > will_return_length ge d'' (new_state … r) (remainder … r) TM] with
    684      [O ⇒ λ_. I | _ ⇒ λTM. «pi1 … TM, ?» ] (terminates ??????? r))
    685 .
    686 @(transitive_le … lGE) @(pi2 … TM) qed.
    687 
    688 definition replace_sub_trace : ∀ge,d,s1,s2,t1,t2,T1,T2,l1,l2. l2 ≥ l1 →
    689   ∀r:sub_trace_result ge d s1 t1 T1 l1.
    690     (∀s,t. flat_trace_prefix … s1 s t1 t → flat_trace_prefix … s2 s t2 t) →
     759     [O ⇒ λ_. I | _ ⇒ λTM. «pi1 … TM, ?» ] (terminates ???????? r))*)
     760.
     761cases e in r ⊢ %;
     762[ <TME -TME * cases d in TM1 TM2 ⊢ %;
     763  [ #TM1 #TM2 #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %); #TMS @TMS
     764  | #d' #TM1 #TM2 #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %); * #TMa * #L1 #TME
     765    %{TMa} % // @(transitive_le … lGE) @L1
     766  ]
     767| <TME -TME * #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %);
     768   * #TMa * #L1 #TME
     769    %{TMa} % // @(transitive_le … lGE) @L1
     770] qed.
     771
     772definition replace_sub_trace : ∀ge,d,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →
     773  ∀r:sub_trace_result ge d s1 t1 TM1 T1 l1.
     774    will_return_end … TM1 = will_return_end … TM2 →
    691775    T2 (ends … r) (new_state … r) →
    692776    stack_preserved (ends … r) s2 (new_state … r) →
    693     sub_trace_result ge d s2 t2 T2 l2 ≝
    694 λge,d,s1,s2,t1,t2,T1,T2,l1,l2,lGE,r,PRE,trace,SP.
    695   mk_sub_trace_result ge d s2 t2 T2 l2
     777    sub_trace_result ge d s2 t2 TM2 T2 l2 ≝
     778λge,d,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2,lGE,r,TME,trace,SP.
     779  mk_sub_trace_result ge d s2 t2 TM2 T2 l2
    696780    (ends … r)
    697     (replace_trace … lGE … r PRE trace SP).
     781    (replace_trace … lGE … r TME trace SP).
    698782
    699783(* Small syntax hack to avoid ambiguous input problems. *)
     
    708792  (TIME: nat)
    709793  (TERMINATES_IN_TIME: myge TIME (plus 2 (times 3 (will_return_length … TERMINATES))))
    710   on TIME : trace_result ge depth ends_with_ret s trace
     794  on TIME : trace_result ge depth ends_with_ret s trace TERMINATES
    711795              (trace_label_return (RTLabs_status ge) s)
    712796              (will_return_length … TERMINATES) ≝
     
    723807            TERMINATES
    724808            TIME ? in
    725   match ends … r return λx. trace_result ge (match x with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth]) x s trace (trace_label_label (RTLabs_status ge) x s) ? → trace_result ge depth ends_with_ret s trace (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) with
     809  match ends … r return λx. trace_result ge depth x s trace TERMINATES (trace_label_label (RTLabs_status ge) x s) ? →
     810                            trace_result ge depth ends_with_ret s trace TERMINATES (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) with
    726811  [ ends_with_ret ⇒ λr.
    727812      replace_trace … r ? (tlr_base (RTLabs_status ge) s (new_state … r) (new_trace … r)) (stack_ok … r)
     
    748833  (TIME: nat)
    749834  (TERMINATES_IN_TIME:  myge TIME (plus 1 (times 3 (will_return_length … TERMINATES))))
    750   on TIME : sub_trace_result ge depth s trace
     835  on TIME : sub_trace_result ge depth s trace TERMINATES
    751836              (λends. trace_label_label (RTLabs_status ge) ends s)
    752837              (will_return_length … TERMINATES) ≝
     
    770855  (TIME: nat)
    771856  (TERMINATES_IN_TIME: myge TIME (times 3 (will_return_length … TERMINATES)))
    772   on TIME : sub_trace_result ge depth s trace
     857  on TIME : sub_trace_result ge depth s trace TERMINATES
    773858              (λends. trace_any_label (RTLabs_status ge) ends s)
    774859              (will_return_length … TERMINATES) ≝
     
    778863| S TIME ⇒ λTERMINATES_IN_TIME.
    779864
    780   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 s trace (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TM) with
     865  match trace return λs,trace. well_cost_labelled_state s →
     866                               ∀TM:will_return ??? trace.
     867                               myge ? (times 3 (will_return_length ??? trace TM)) →
     868                               sub_trace_result ge depth s trace TM (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TM) with
    781869  [ ft_stop st FINAL ⇒
    782870      λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ⊥
    783871
    784872  | ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME.
    785     match RTLabs_classify start return λx. RTLabs_classify start = x → sub_trace_result ge depth start ? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
     873    match RTLabs_classify start return λx. RTLabs_classify start = x → sub_trace_result ge depth start ?? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
    786874    [ cl_other ⇒ λCL.
    787         match RTLabs_cost next return λx. RTLabs_cost next = x → sub_trace_result ge depth start ? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
     875        match RTLabs_cost next return λx. RTLabs_cost next = x → sub_trace_result ge depth start ?? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
    788876        (* We're about to run into a label. *)
    789877        [ true ⇒ λCS.
    790             mk_sub_trace_result ge depth start ? (λends. trace_any_label (RTLabs_status ge) ends start) ?
     878            mk_sub_trace_result ge depth start ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start) ?
    791879              doesnt_end_with_ret
    792               (mk_trace_result ge … next trace' ??
     880              (mk_trace_result ge … next trace' ?
    793881                (tal_base_not_return (RTLabs_status ge) start next ?? CS) ??)
    794882        (* An ordinary step, keep going. *)
     
    801889       
    802890    | cl_jump ⇒ λCL.
    803         mk_sub_trace_result ge depth start ? (λends. trace_any_label (RTLabs_status ge) ends start) ?
     891        mk_sub_trace_result ge depth start ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start) ?
    804892          doesnt_end_with_ret
    805           (mk_trace_result ge ?????? next trace' ??
     893          (mk_trace_result ge … next trace' ?
    806894            (tal_base_not_return (RTLabs_status ge) start next ???) ??)
    807895           
    808896    | cl_call ⇒ λCL.
    809         let r ≝ make_label_return ge (S depth) next trace' ENV_COSTLABELLED ?? (will_return_call … TERMINATES) TIME ? in
    810         match RTLabs_cost (new_state … r) return λx. RTLabs_cost (new_state … r) = x → sub_trace_result ge depth start ? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
     897        let r ≝ make_label_return ge (S depth) next trace' ENV_COSTLABELLED ?? (will_return_call … CL TERMINATES) TIME ? in
     898        match RTLabs_cost (new_state … r) return λx. RTLabs_cost (new_state … r) = x → sub_trace_result ge depth start ?? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
    811899        (* We're about to run into a label, use base case for call *)
    812900        [ true ⇒ λCS.
    813             mk_sub_trace_result ge depth start ? (λends. trace_any_label (RTLabs_status ge) ends start) ?
     901            mk_sub_trace_result ge depth start ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start) ?
    814902            doesnt_end_with_ret
    815             (replace_trace … r ?
     903            (mk_trace_result ge …
    816904              (tal_base_call (RTLabs_status ge) start next (new_state … r)
    817                 ? CL ? (new_trace … r) CS) ?)
     905                ? CL ? (new_trace … r) CS) ??)
    818906        (* otherwise use step case *)
    819907        | false ⇒ λCS.
     
    828916
    829917    | cl_return ⇒ λCL.
    830         mk_sub_trace_result ge depth start ? (λends. trace_any_label (RTLabs_status ge) ends start) ?
     918        mk_sub_trace_result ge depth start ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start) ?
    831919          ends_with_ret
    832           (mk_trace_result ge ??????
     920          (mk_trace_result ge
    833921            next
    834922            trace'
    835             ?
    836923            ?
    837924            (tal_base_return (RTLabs_status ge) start next ? CL)
     
    848935| //
    849936| //
    850 | cases r #H1 #H2 #H3 #H4 #H5 #H6 * #H7 @le_S_to_le
    851 | #s0 #t @concatenate_flat_trace_prefix @(is_remainder … r)
     937| cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #GT #_ @(le_S_to_le … GT)
     938| cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #_ #EEQ //
    852939| @(stack_preserved_join … (stack_ok … r)) //
    853940| @(trace_label_label_label … (new_trace … r))
    854 | cases r #H1 #H2 #H3 #H4 #H5 #H6 * #H7 #LT
     941| cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #LT #_
    855942  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
    856943  @(transitive_le …  (3*(will_return_length … TERMINATES)))
     
    877964| %{tr} @EV
    878965| @(well_cost_labelled_state_step  … EV) //
    879 | %2 %1
    880966| whd @(will_return_notfn … TERMINATES) %2 @CL
    881967| @stack_preserved_step /2/
     
    884970| @(well_cost_labelled_jump … EV) //
    885971| @(well_cost_labelled_state_step  … EV) //
    886 | %2 %1
     972| whd cases (terminates ???????? r) #TMr * #LTr #EQr %{TMr} %
     973  [ @(transitive_lt … LTr) cases (will_return_call … CL TERMINATES)
     974    #TMx * #LT' #_ @LT'
     975  | <EQr cases (will_return_call … CL TERMINATES)
     976    #TM' * #_ #EQ' @EQ'
     977  ]
    887978| @(stack_preserved_call … EV (stack_ok … r)) //
    888979| %{tr} @EV
    889980| @RTLabs_after_call //
    890 | #s0 #t #p %2 @p
    891 | cases (will_return_call … TERMINATES) #H @le_S_to_le
    892 | cases r #H1 #H2 #H3 #H4 #H5 #H6 * #H7
    893   cases (will_return_call … CL TERMINATES)
    894   #TM #X #Y @le_S_to_le @(transitive_lt … Y X)
    895 | #s0 #t #p1 %2 @(concatenate_flat_trace_prefix … p1) @(is_remainder … r)
     981| @(cost_labelled … r)
     982| skip
     983| cases r #ns #rm #WS #TLR #SP * #TM * #LT #_ @le_S_to_le
     984  @(transitive_lt … LT)
     985  cases (will_return_call … CL TERMINATES) #TM' * #LT' #_ @LT'
     986| cases r #ns #rm #WS #TLR #SP * #TM * #_ #EQ <EQ
     987  cases (will_return_call … CL TERMINATES) #TM' * #_ #EQ' //
    896988| @RTLabs_after_call //
    897989| %{tr} @EV
    898990| @(stack_preserved_join … (stack_ok … r')) @(stack_preserved_call … EV (stack_ok … r)) //
    899991| @(cost_labelled … r)
    900 | cases r #H72 #H73 #H74 #H75 #HX #HY * #H76 #H78
     992| cases r #H72 #H73 #H74 #H75 #HX * #HY * #GT #H78
    901993  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
    902   cases (will_return_call … TERMINATES) in H78;
    903   #X #Y #Z
     994  cases (will_return_call … TERMINATES) in GT;
     995  #X * #Y #_ #Z
    904996  @(transitive_le … (monotonic_lt_times_r 3 … Y))
    905997  [ @(transitive_le … (monotonic_lt_times_r 3 … Z)) //
     
    9081000| @(well_cost_labelled_state_step  … EV) //
    9091001| @(well_cost_labelled_call … EV) //
    910 | skip
    9111002| cases (will_return_call … TERMINATES)
    912   #TM #GT @le_S_S_to_le
     1003  #TM * #GT #_ @le_S_S_to_le
    9131004  >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times
    9141005  @(transitive_le … TERMINATES_IN_TIME)
     
    9191010| %2 whd @CL
    9201011| @(well_cost_labelled_state_step  … EV) //
    921 | %2 %1
    922 | cases (will_return_notfn … TERMINATES) #TM @le_S_to_le
    923 | #s0 #t #p %2 @p
     1012| cases (will_return_notfn … TERMINATES) #TM * #GT #_ @(le_S_to_le … GT)
     1013| cases (will_return_notfn … TERMINATES) #TM * #_ #EQ //
    9241014| @CL
    9251015| %{tr} @EV
     
    9271017| @(well_cost_labelled_state_step  … EV) //
    9281018| %1 @CL
    929 | cases (will_return_notfn … TERMINATES) #TM #GT
     1019| cases (will_return_notfn … TERMINATES) #TM * #GT #_
    9301020  @le_S_S_to_le
    9311021  @(transitive_le … (monotonic_lt_times_r … GT) TERMINATES_IN_TIME)
     
    9471037  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
    9481038  (TERMINATES: will_return ge depth s trace)
    949   : trace_result ge depth ends_with_ret s trace (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝
     1039  : trace_result ge depth ends_with_ret s trace TERMINATES (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝
    9501040make_label_return ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES
    9511041  (2 + 3 * will_return_length … TERMINATES) ?.
     
    10871177qed.
    10881178  *) 
    1089 discriminator nat.
     1179
    10901180(*
    10911181definition soundly_labelled_pc ≝ λg,l. ∃n. steps_to_label_bound g l n.
     
    13191409| /2/
    13201410| //
    1321 | (* FIXME: post-call non-termination *)
     1411| @(not_to_not … NO_TERMINATION) * #depth * #TM1 %{depth} %
     1412  @wr_call //
     1413  @(will_return_prepend … TERMINATES … TM1)
     1414  cases (terminates … tlr) //
    13221415| (* FIXME: post-call not-wrong *)
    13231416| (* FIXME: bound on steps after call *)
Note: See TracChangeset for help on using the changeset viewer.