Ignore:
Timestamp:
Apr 3, 2013, 5:54:34 PM (7 years ago)
Author:
campbell
Message:

Tidy up recent work a little.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/SwitchAndLabel.ma

    r3047 r3081  
    22include "Clight/labelSimulation.ma".
    33
    4 
    5 lemma after_aux_result : ∀avs,n,s,tr,P.
    6   after_aux avs n s tr P →
    7   ∃tr',s'. P tr' s' ∧ after_aux avs n s tr (λtr'',s''. 〈tr'',s''〉 = 〈tr',s'〉).
    8 #avs #n elim n
    9 [ #s #tr #P #A whd in A; %{tr} %{s} % [ @A | % ]
    10 | #n' #IH #s #tr #P
    11   whd in ⊢ (% → ?);
    12   lapply (refl ? (is_final … s))
    13   cases (is_final … s) in ⊢ (???% → %);
    14   [ #F whd in ⊢ (% → ?);
    15     lapply (refl ? (step … s))
    16     cases (step … s) in ⊢ (???% → %);
    17     [ #o #k #_ *
    18     | * #tr1 #s1 #ST whd in ⊢ (% → ?);
    19       cases n' in IH ⊢ %;
    20       [ #_ whd in ⊢ (% → ?); #p % [2: % [2: %{p} whd >F whd >ST whd % | skip ] | skip ]
    21       | #n'' #IH lapply (refl ? (avs_inv avs s1)) cases (avs_inv avs s1) in ⊢ (???% → %);
    22         [ #INV #AF
    23           cases (IH … AF) #tr' * #s' * #p #AF'
    24          % [2: % [2: %{p} whd >F whd >ST whd >INV @AF' | skip ] | skip ]
    25         | #_ *
    26         ]
    27       ]
    28     | #m #_ *
    29     ]
    30   | #r #F *
    31   ]
    32 ] qed.
    33 
    34 lemma after_n_result : ∀n,O,I,exec,g,s,P,inv.
    35   after_n_steps n O I exec g s inv P →
    36   ∃tr',s'.
    37     P tr' s' ∧
    38     after_n_steps n O I exec g s inv (λtr'',s''. 〈tr'',s''〉 = 〈tr',s'〉).
    39 #n #O #I #exec #g #s #P #inv #A
    40 cases (after_aux_result … A) #tr * #s' * #p #A'
    41 %{tr} %{s'} %{p} @A'
    42 qed.
    43 
    44 
    45 lemma after_1_of_n_steps' : ∀n,O,I,exec,g,tr,s',s.
    46   after_n_steps (S n) O I exec g s (λ_.true) (λtrx,sx. 〈trx,sx〉 = 〈tr,s'〉) →
    47   ∃tr1,tr2,s1.
    48   is_final … exec g s = None ? ∧
    49   step … exec g s = Value … 〈tr1,s1〉 ∧
    50   tr = tr1⧺tr2 ∧
    51   after_n_steps n O I exec g s1 (λ_.true) (λtrx,sx. 〈trx,sx〉 = 〈tr2,s'〉).
    52 #n #O #I #exec #g #tr #s' #s #A
    53 cases (after_1_of_n_steps … A)
    54 #tr1 * #s1 * * * #F #ST #_ #A'
    55 cases (after_n_result … A')
    56 #tr'' * #s'' * #E #A'' destruct
    57 % [2: % [2: % [2: % [ % [% [ @F | @ST ] | % ] | @A'' ] | skip ] | skip ] | skip ]
    58 qed.
    59 
    60 theorem steps_with_labels : ∀ge,ge'.
     4(* Combine the results about switch removal and labelling to provide a single
     5   result linking the input Clight program with the cost labelled Clight
     6   program. *)
     7
     8(* First lift the step result for labelling to a finite run of steps. *)
     9
     10lemma steps_with_labels : ∀ge,ge'.
    6111  related_globals_gen … label_fundef ge ge' →
    6212  ∀n,s1,s1',tr,s2.
     
    13888#tr #s #tr' #s' #E destruct %
    13989qed.
     90
     91(* Now build the coinduction simulation, taking one step to many after switch
     92   removal, then use steps_with_labels to take those to the cost labelled
     93   version. *)
    14094
    14195let corec build_exec
     
    210164] qed.
    211165
     166(* And deal with the start of the program to tie up everything nicely. *)
     167
    212168theorem switch_and_labelling_sim : ∀p.
    213169  let e1 ≝ exec_inf … clight_fullexec p in
Note: See TracChangeset for help on using the changeset viewer.