Changeset 2644
 Timestamp:
 Feb 7, 2013, 4:42:54 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/FEMeasurable.ma
r2618 r2644 64 64 λS,t,s. match t with [ e_step _ s' _ ⇒ s = s'  _ ⇒ False ]. 65 65 66 (* TODO: too many of these lemmas, slim it down*) 67 68 lemma split_trace_S : ∀fx:trans_system io_out io_in. ∀g,tr,s,n,a,b. 69 split_trace … (exec_inf_aux ?? fx g (Value … 〈tr,s〉)) (S n) = Some ? 〈a,b〉 → 70 ∃a'. a = 〈tr,s〉::a' ∧ 71 ((is_final … fx g s = None ? ∧ split_trace … (exec_inf_aux ?? fx g (step … fx g s)) n = Some ? 〈a',b〉) ∨ 72 (∃r. is_final … fx g s = Some ? r ∧ n = 0 ∧ a' = [ ] ∧ b = e_stop … tr r s)). 73 #fx #g #tr #s #n #a #b 74 >exec_inf_aux_unfold whd in ⊢ (??(????%?)? → ?); 75 cases (is_final … s) 76 [ whd in ⊢ (??%? → ?); cases (split_trace ?????) 77 [ #E whd in E:(??%%); destruct 78  * #a' #b' #E whd in E:(??%%); destruct 79 %{a'} %{(refl ??)} %1 %{(refl ??)} % 80 ] 81  #r cases n [2:#n'] whd in ⊢ (??%? → ?); #E destruct 82 %{[ ]} %{(refl ??)} %2 %{r} /4/ 83 ] qed. 84 85 lemma split_trace_S' : ∀fx:trans_system io_out io_in. ∀g,s,n,a,b. 86 split_trace … (exec_inf_aux ?? fx g (step … fx g s)) (S n) = Some ? 〈a,b〉 → 87 ∃tr,s'. step … fx g s = Value … 〈tr,s'〉 ∧ 88 ∃a'. a = 〈tr,s'〉::a' ∧ 89 ((is_final … fx g s' = None ? ∧ split_trace … (exec_inf_aux ?? fx g (step … fx g s')) n = Some ? 〈a',b〉) ∨ 90 (∃r. is_final … fx g s' = Some ? r ∧ n = 0 ∧ a' = [ ] ∧ b = e_stop … tr r s')). 91 #fx #g #s #n #a #b 92 cases (step … fx g s) 93 [ #o #i whd in ⊢ (??%? → ?); #E destruct 94  * #tr #s' #split %{tr} %{s'} %{(refl …)} @split_trace_S @split 95  #err #E whd in E:(??%%); destruct 96 ] qed. 97 98 lemma split_trace_1 : ∀fx:trans_system io_out io_in. ∀g,tr,s,a,b. 99 split_trace … (exec_inf_aux ?? fx g (Value … 〈tr,s〉)) 1 = Some ? 〈a,b〉 → 100 a = [〈tr,s〉] ∧ 101 ((is_final … fx g s = None ? ∧ b = exec_inf_aux ?? fx g (step … fx g s)) ∨ 102 (∃r. is_final … fx g s = Some ? r ∧ b = e_stop … tr r s)). 103 #fx #g #tr #s #a #b #split 104 cases (split_trace_S … split) 105 #a' * #E1 * 106 [ * #notfinal #split' whd in split':(??%?); destruct %{(refl ??)} 107 %1 %{notfinal} % 108  * #r * * * #final #_ #E2 #E3 destruct %{(refl ??)} 109 %2 %{r} %{final} % 110 ] qed. 111 112 113 lemma split_trace_SS : ∀fx:trans_system io_out io_in. ∀g,tr,s,n,a,b. 114 split_trace … (exec_inf_aux ?? fx g (Value … 〈tr,s〉)) (S (S n)) = Some ? 〈a,b〉 → 115 ∃a'. a = 〈tr,s〉::a' ∧ 116 is_final … fx g s = None ? ∧ 117 ∃tr',s'. step … fx g s = Value … 〈tr',s'〉 ∧ 118 split_trace … (exec_inf_aux ?? fx g (Value … 〈tr',s'〉)) (S n) = Some ? 〈a',b〉. 119 #fx #g #tr #s #n #a #b #splitSS 120 cases (split_trace_S … splitSS) 121 #a' * #E1 * 122 [ * #notfinal #splitS %{a'} % [ %{E1} @notfinal ] 123 cases (step … s) in splitS ⊢ %; 124 [ #o #i #E whd in E:(??%%); destruct 125  * #tr' #s' #splitS %{tr'} %{s'} %{(refl ??)} @splitS 126  #m #E whd in E:(??%%); destruct 127 ] 128  * #r * * * #final #En #Ea #Eb destruct 129 ] qed. 130 131 (* WIP commented out 66 132 lemma prefix_preserved : 67 133 ∀MS:meas_sim. … … 69 135 ∀INV:ms_inv MS g1 g2. 70 136 ∀max_allowed_stack. 71 ∀trace,trace',s1,s1'. 72 trace_starts ? trace s1 → 73 trace_starts ? trace' s1' → 137 ∀s1,s1',tr,tr'. 74 138 ms_rel MS g1 g2 INV s1 s1' → 139 140 let trace ≝ (exec_inf_aux ?? (pcs_exec … (ms_C1 MS)) g1 (Value … 〈tr,s1〉)) in 141 let trace' ≝ (exec_inf_aux ?? (pcs_exec … (ms_C2 MS)) g2 (Value … 〈tr',s1'〉)) in 142 75 143 ∀m,prefix,suffix. 76 split_trace ?trace m = Some ? 〈prefix,suffix〉 →144 split_trace … trace m = Some ? 〈prefix,suffix〉 → 77 145 le (max_stack (pcs_to_cs (ms_C1 MS) ? (ms_stack MS … INV)) prefix) max_allowed_stack → 146 78 147 ∃m',prefix',suffix'. 79 split_trace ? trace' m' = Some ? 〈prefix',suffix'〉 ∧ 80 le (max_stack (pcs_to_cs (ms_C2 MS) ? (ms_stack MS … INV)) prefix') max_allowed_stack ∧ 81 ∃s2,s2'. trace_starts ? suffix s2 ∧ trace_starts ? suffix' s2' ∧ 148 split_trace … trace' m' = Some ? 〈prefix',suffix'〉 ∧ 149 le (max_stack (pcs_to_cs (ms_C2 MS) ? (ms_stack MS … INV)) prefix') max_allowed_stack ∧ 150 151 ∃s2,s2',tr2,tr2'. 152 suffix = exec_inf_aux ?? (pcs_exec … (ms_C1 MS)) g1 (Value … 〈tr2,s2〉) ∧ 153 suffix' = exec_inf_aux ?? (pcs_exec … (ms_C2 MS)) g2 (Value … 〈tr2',s2'〉) ∧ 82 154 ms_rel MS g1 g2 INV s2 s2'. 155 * #C1 #C2 #compiled #inv #stack #rel #sim_normal #sim_call_return #sim_cost #sim_init 156 #g1 #g2 #INV #max #s1 #s1' #tr #tr' #REL 157 letin trace ≝ (exec_inf_aux ?????) 158 letin trace' ≝ (exec_inf_aux ?????) 159 #m0 160 @(nat_elim1 m0) 161 * 162 [ #_ #prefix #suffix #split whd in split:(??%?); destruct 163 #max_ok %{0} %{[]} %{trace'} 164 % [ % //  %{s1} %{s1'} %{tr} %{tr'} /3/ ] 165  * 166 [ (* m = 1; just extracts the current state *) 167 #_ #prefix #suffix #split #max_ok 168 cases (split_trace_1 … split) #E1 #foo 169 %{1} %{[〈tr',s1'〉]} %{(exec_inf_aux … (step … s1'))} 170 % [ % 171 #m #IH #prefix #suffix #split #max_ok 172 (* clean up first step? *) 173 cases (true_or_false_Prop … (pcs_labelled … s1)) 174 [ #CS cases (split_trace_S … split) #trace1 * #Etrace * 175 [ * #notfinal #split1 176 lapply (sim_cost … REL CS) 177 [ 3: whd in match (after_n_steps ????? s1 ??); 178 >(?:is_final ???? s1 = None ?) [ whd in ⊢ ((% → ?) → ?); 179 lapply (refl ? (pcs_classify … s1)) cases (pcs_classify … s1) in ⊢ (???% → ?); 180 [ 181  #CL 83 182 84 183 theorem measured_subtrace_preserved : … … 94 193 * * * * #split1 #split2 #subtrace_ok #terminates #max_ok 95 194 96 195 *)
Note: See TracChangeset
for help on using the changeset viewer.