Changeset 2338 for src/common
 Timestamp:
 Sep 26, 2012, 10:17:32 AM (8 years ago)
 Location:
 src/common
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Executions.ma
r2206 r2338 41 41 whd in ⊢ (??(λ_.???%?)); >(plus_not_final … P2) 42 42 cases (IH F3) #tr'' #S' %{tr''} /2/ 43 ] qed. 44 45 (* And similarly for after_n_steps *) 46 47 lemma after_inv : ∀FE:fullexec io_out io_in. 48 ∀n,g,P,s. 49 after_n_steps (S n) … FE g s P → 50 ∃tr,s'. 51 P tr s' ∧ 52 match is_final ?? FE g s' with 53 [ Some r ⇒ ∃tr'. 54 steps ? tr (exec_inf_aux … FE g (step … FE g s)) 55 (e_stop ??? tr' r s') 56  None ⇒ 57 steps ? tr (exec_inf_aux … FE g (step … FE g s)) 58 (exec_inf_aux … FE g (step … FE g s')) 59 ]. 60 #FE #n #g #P 61 (* Rather nasty generalisation *) 62 #s whd in ⊢ (% → ?); cases (is_final … s) [2: #r * ] whd in ⊢ (% → ?); #AW 63 cut (∃tr,s'. P (E0⧺tr) s' ∧ ?) [3: #H @H  skip ] 64 generalize in match E0 in AW ⊢ %; generalize in match s; s 65 elim n 66 [ #s #tr whd in ⊢ (% → %); 67 cases (step … s) [ #o #K *  3: #m * ] 68 * #tr' #s' #AW %{tr'} %{s'} %{AW} 69 lapply (refl ? (is_final … s')) cases (is_final … s') in ⊢ (???% → %); 70 [ #NF whd >exec_inf_aux_unfold whd in ⊢ (???%?); >NF @steps_step 71  #r #F whd %{tr'} >exec_inf_aux_unfold whd in ⊢ (???%?); >F whd in ⊢ (???%?); @steps_stop 72 ] 73  #n' #IH #s #tr whd in ⊢ (% → ?); 74 cases (step … s) [ #o #K *  3: #m * ] * #tr1 #s1 75 whd in ⊢ (% → ?); lapply (refl ? (is_final … s1)) cases (is_final … s1) in ⊢ (???% → %); 76 [ 2: #r #_ * ] #NF1 whd in ⊢ (% → ?); #AW1 77 cases (IH s1 ? AW1) 78 #tr' * #s' * #p #H1 %{(tr1⧺tr')} %{s'} 79 lapply (refl ? (is_final … s')) cases (is_final … s') in ⊢ (???% → %); 80 [ #NF <Eapp_assoc %{p} whd >exec_inf_aux_unfold whd in ⊢ (???%?); >NF1 81 @steps_steps >NF in H1; // 82  #r #F <Eapp_assoc %{p} whd >exec_inf_aux_unfold whd in ⊢ (??(λ_.???%?)); >NF1 83 >F in H1; whd in ⊢ (% → ?); * #tr1 #H1 %{tr1} 84 @steps_steps @H1 85 ] 43 86 ] qed. 44 87 
src/common/SmallstepExec.ma
r2203 r2338 17 17 [ O ⇒ Value ??? 〈E0, s〉 18 18  S n' ⇒ ! 〈t1,s1〉 ← step ?? exec g s; 19 repeat n' ?? exec g s1 19 ! 〈tn,sn〉 ← repeat n' ?? exec g s1; 20 Value ??? 〈t1⧺tn,sn〉 20 21 ]. 21 22 … … 51 52 ]. 52 53 54 (* A third version of making several steps (!) 55 56 The idea here is to have a computational definition of reducing serveral 57 steps then showing some property about the resulting trace and state. By 58 careful use of let rec we can ensure that reduction stops in a sensible 59 way whenever the number of steps or the step currently being executed is 60 not (reducible to) a value. 61 62 For example, we state a property to prove by something like 63 64 ∃n. after_n_steps n … clight_exec ge s (λtr,s'. <some property>) 65 66 then start reducing by giving the number of steps and reducing the 67 definition 68 69 %{3} whd 70 71 and then whenever the reduction gets stuck, the currently reducing step is 72 the third subterm, which we can reduce and unblock with (for example) 73 rewriting 74 75 whd in ⊢ (??%?); >EXe' 76 77 and at the end reduce with whd to get the property as the goal. 78 79 There's an inversionlike result to get back the information contained in 80 the proof in Executions.ma. 81 82 *) 83 84 record await_value_stuff : Type[2] ≝ { 85 avs_O : Type[0]; 86 avs_I : avs_O → Type[0]; 87 avs_exec : trans_system avs_O avs_I; 88 avs_g : global ?? avs_exec 89 }. 90 91 let rec await_value (avs:await_value_stuff) 92 (v:IO (avs_O avs) (avs_I avs) (trace × (state ?? (avs_exec avs) (avs_g avs)))) 93 (P:trace → state ?? (avs_exec avs) (avs_g avs) → Prop) on v : Prop ≝ 94 match v with 95 [ Value ts ⇒ P (\fst ts) (\snd ts) 96  _ ⇒ False 97 ]. 98 99 let rec after_aux (avs:await_value_stuff) 100 (n:nat) (s:state ?? (avs_exec avs) (avs_g avs)) (tr:trace) 101 (P:trace → state ?? (avs_exec avs) (avs_g avs) → Prop) 102 on n : Prop ≝ 103 match n with 104 [ O ⇒ P tr s 105  S n' ⇒ 106 match is_final … s with 107 [ None ⇒ 108 await_value avs (step ?? (avs_exec avs) (avs_g avs) s) (λtr',s. 109 after_aux avs n' s (tr ⧺ tr') P) 110  _ ⇒ False 111 ] 112 ]. 113 114 definition after_n_steps : nat → 115 ∀O,I. ∀exec:trans_system O I. ∀g:global ?? exec. 116 state ?? exec g → 117 (trace → state ?? exec g → Prop) → Prop ≝ 118 λn,O,I,exec,g,s,P. after_aux (mk_await_value_stuff O I exec g) n s E0 P. 119 120 lemma after_n_covariant : ∀n,O,I,exec,g,P,Q. 121 (∀tr,s. P tr s → Q tr s) → 122 ∀s. 123 after_n_steps n O I exec g s P → 124 after_n_steps n O I exec g s Q. 125 #n #O #I #exec #g #P #Q #H whd in ⊢ (? → % → %); generalize in match E0; elim n 126 [ normalize /2/ 127  #n' #IH #tr #s 128 normalize cases (is_final … s) normalize [ 2: #_ * ] cases (step O I exec g s) normalize /4/ 129 ] qed. 130 131 (* for joining a couple of these together *) 132 133 lemma after_n_m : ∀n,m,O,I,exec,g,P,Q,s,s'. 134 after_n_steps m O I exec g s' Q → 135 after_n_steps n O I exec g s (λtr1,s1. s' = s1 ∧ (∀tr'',s''. Q tr'' s'' → P (tr1⧺tr'') s'')) → 136 after_n_steps (n+m) O I exec g s P. 137 #n #m #O #I #exec #g #P #Q whd in ⊢ (? → ? → ? → % → %); generalize in match E0; elim n 138 [ #tr #s #s' #H whd in ⊢ (% → %); * #E destruct #H2 139 whd in H; <(E0_right tr) generalize in match E0 in H ⊢ %; 140 generalize in match s; s 141 elim m 142 [ #s #tr' whd in ⊢ (% → %); @H2 143  #m' #IH #s #tr' whd in ⊢ (% → %); 144 cases (is_final … s) [2: #r * ] 145 whd in ⊢ (% → %); 146 cases (step O I exec g s) [1,3: normalize //] * #tr'' #s'' whd in ⊢ (% → %); >Eapp_assoc @IH ] 147  #n' #IH #tr #s #s' #H whd in ⊢ (% → %); 148 cases (is_final … s) [2: #r * ] 149 whd in ⊢ (% → %); 150 cases (step O I exec g s) [1,3: normalize // ] 151 * #tr1 #s1 whd in ⊢ (% → %); @IH @H 152 ] qed. 153 154 53 155 (* A (possibly nonterminating) execution. *) 54 156 coinductive execution (state:Type[0]) (output:Type[0]) (input:output → Type[0]) : Type[0] ≝
Note: See TracChangeset
for help on using the changeset viewer.