Changeset 2426 for src/joint/stacksize.ma
 Timestamp:
 Oct 31, 2012, 5:36:51 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/stacksize.ma
r2417 r2426 2 2 include "joint/semantics.ma". 3 3 include "common/Executions.ma". 4 include "common/StructuredTraces.ma". 4 5 5 6 inductive call_ud (p: params) (globals: list ident): Type [0] ≝ … … 47 48 [ tal_base_not_return s1 s2 ex cl co ⇒ res 48 49  tal_base_return s1 s2 ex cl ⇒ down ?? (lg top_f)::res 49  tal_base_call s1p s1s s2 ex cl f ca ar tlr co ⇒ 50 extract_list_from_tlr … lg f … tlr (up ?? (lg f)::res) 51  tal_step_call end s1p s1s s1a s2 ex cl f ca ar tlr co tal ⇒ 52 let res' ≝ extract_list_from_tlr … lg f … tlr (up ?? (lg f)::res) in 50  tal_base_call s1p s1s s2 ex cl ar tlr co ⇒ 51 extract_list_from_tlr … lg (as_call_ident ? «s1p,cl») … tlr 52 (up ?? (lg (as_call_ident ? «s1p,cl»))::res) 53  tal_step_call end s1p s1s s1a s2 ex cl ar tlr co tal ⇒ 54 let res' ≝ extract_list_from_tlr … lg (as_call_ident ? «s1p,cl») … tlr 55 (up ?? (lg (as_call_ident ? «s1p,cl»))::res) in 53 56 extract_list_from_tal … lg top_f … tal res' 54 57  tal_step_default end s1p s1i s1e ex tal cl co ⇒ … … 84 87 [ tal_base_not_return st1 st1' ex cl co ⇒ ? 85 88  tal_base_return st1 st1' ex cl ⇒ ? 86  tal_base_call st1p st1s st1' ex cl f caar tlr1 co ⇒ ?87  tal_step_call end st1p st1s st1 st1' ex cl f caar tlr1 co tal1 ⇒ ?89  tal_base_call st1p st1s st1' ex cl ar tlr1 co ⇒ ? 90  tal_step_call end st1p st1s st1 st1' ex cl ar tlr1 co tal1 ⇒ ? 88 91  tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ? 89 92 ]. … … 103 106 [ #st2 #st2' #ex' #cl' #co' normalize #Hsim #res % 104 107  #st2 #st2' #ex' #cl' * #abs destruct (abs) 105  #st2p #st2s #st2' #ex' #cl' # f' #ca' #ar' #tlr2 #co' normalize * #H1 * #st2mid *108  #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #H1 * #st2mid * 106 109 #taa * #H * #G * #K inversion taa in ⊢ ?; 107 110 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) … … 109 112 normalize #abs destruct (abs) 110 113 ] 111  #ends' #st2p #st2s #st2 #st2' #ex' #cl' # f' #ca' #ar' #tlr2 #co' #tal2 normalize *114  #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 normalize * 112 115 #H1 * #st2mid * #taa * #H * #G * #K inversion taa in ⊢ ?; 113 116 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) … … 119 122 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) 120 123  #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 121 destruct normalize #Hsim cases daemon (* use injectivity from Hsim? *) 124 destruct normalize #Hsim destruct (Hsim) (* getting somewhere. Use Hind? *) 125 cases daemon 122 126 ] 123 127 ] … … 125 129 [ #st2 #st2' #ex' #cl' #co' normalize * #abs destruct (abs) 126 130  #st2 #st2' #ex' #cl' normalize * #H1 #H2 #res % 127  #st2p #st2s #st2' #ex' #cl' # f' #ca' #ar' #tlr2 #co' normalize * #abs destruct (abs)128  #ends' #st2p #st2s #st2 #st2' #ex' #cl' # f' #ca' #ar' #tlr2 #co' #tal2131  #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #abs destruct (abs) 132  #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 129 133 normalize * #H1 * #st2mid * #taa * #H * #G inversion taa in ⊢ ?; 130 134 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) … … 136 140 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) 137 141  #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 138 destruct normalize #Hsim cases daemon (* use injectivity from Hsim? *) 139 ] 140 ] 141  cases t2 142 [ #st2 #st2' #ex' #cl' #co' normalize * #_ * #st2mid * #taa 143 * #st2mid' * #H * * [2: #st2mid'' *] #J * #f' * #G * #K * #tlr2 * #L * #H1 142 destruct normalize #Hsim destruct (Hsim) 143 cases daemon (* use Hind again? *) 144 ] 145 ] 146  cases t2 147 [ #st2 #st2' #ex' #cl' #co' normalize * #_ * #st2mid * #G * #ident_eq * #taa 148 * #st2mid' * #H * * [2: #st2mid'' *] #K * #tlr2 * #L * #H1 144 149 [ * * #H3 #H2 #H4  #H2 ] 145 150 inversion taa in ⊢ ?; … … 152 157 ] 153 158  #st2 #st2' #ex' #cl' normalize * #abs destruct (abs) 154  #st2p #st2s #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' normalize * #_ * #st2mid * 155 #taa * #st2mid' * #H * * [2: #st2mid'' *] #J * #f'' * #G * #K * #tlr2' * #L 156 inversion taa in ⊢ ?; 157 [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #tal2 * * #H1 destruct (H1) 159  #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #_ * #st2mid * #G 160 * #ident_eq * #taa * #st2mid' * #H * * [2: #st2mid'' *] #K * #tlr2' * #L 161 [* #tl2] 162 inversion taa in ⊢ ?; 163 [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs) 158 164  #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 159 destruct normalize * #tal2 * * #H1 destruct (H1)165 destruct normalize * * #abs destruct (abs) 160 166  #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #H1 #H2 #res 161 >(tlr_rel_extract_equal p g lg f … H2) cases daemon (* use injectivity and H1? *) 167 >(tlr_rel_extract_equal p g lg … H2) destruct (H1) 168 >ident_eq % 162 169  #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 163 170 destruct normalize * #abs destruct (abs) 164 171 ] 165  #ends' #st2p #st2s #st2 #st2' #ex' #cl' # f' #ca' #ar' #tlr2 #co' #tal2166 normalize * #H1 * #st2mid * #taa * #st2mid' * #H * * [2: #st2mid'' *] #J * #f167 * #G * #K * #tlr2' * #L168 inversion taa in ⊢ ?; 169 [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * #tal2' * * #H1 #H2 #H3#res170 cases daemon171  #st2p' #st2p'' #st2mid'; #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3172 destruct normalize * #tal2' * * #H1 destruct (H1)173  #st2mid''' #eq1 #eq2 #eq3 destruct normalize * #abs destruct (abs)174  #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3175 destruct normalize * #abs destruct (abs)172  #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 normalize 173 * #H1 * #st2mid * #G * #ident_eq * #taa * #st2mid' * #H * * [2: #st2mid'' *] 174 #K * #tlr2' * #L [* #tl2] 175 inversion taa in ⊢ ?; 176 [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * [*] #H1 #H2 [#H3] #res 177 destruct (H1) >(tlr_rel_extract_equal … H2) >ident_eq 178 (* to do here: destruct tl2: 3 cases by contradiction, 1 by equality and 1 by 179 * not sure yet *) cases daemon 180 2,4: #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 181 destruct normalize * * [#abs destruct (abs)] #H2 #res <ident_eq 182 >(tlr_rel_extract_equal … H2) cases daemon (* stumped here *) 176 183 ] 177 184  #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid * 178 #taa * #st2mid' * #H * * [2: #stmid'' * ] #J * #f * #G * #K * #tlr2 * #L 179 inversion taa in ⊢ ?; 180 [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * #tal2' * * #H1 destruct (H1) 181  #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 182 destruct normalize * #tal2' * * #H1 #H2 #H3 #res cases daemon 183  #st2mid''' #eq1 #eq2 #eq3 destruct normalize * #abs destruct (abs) 184  #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 185 destruct normalize * #H1 #H2 #res cases daemon (* do something with H1 and H2 *) 186 ] 187 ] 188  cases t2 189 [ #st2 #st2' #ex' #cl' #co' normalize * #st2mid * #taa * #st2_fun * 190 #st2_after_fun * * [#H  #st2mid'] * #J * #f' * #G * #K * #tlr2 * #L [2: * #tl2] 191 inversion taa in ⊢ ?; 192 [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * * #H1 destruct (H1) 193  #st2p #st2p' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct 194 normalize * * #H1 destruct (H1) 195  #st2mid'' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs) 196  #st2p #st2p' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct 185 #G * #ident_eq * #taa * #st2mid' * #H * * [2: #stmid'' * ] #K * #tlr2 * #L 186 [* #tl2] 187 inversion taa in ⊢ ?; 188 [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * [*] #H1 #H2 [#H3] #res 189 destruct (H1) 190 2,4: #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 191 destruct normalize * [*] #H1 #H2 [#H3] #res destruct (H1) <ident_eq 192 >(tlr_rel_extract_equal … H2) cases daemon (* stumped again *) 193 ] 194 ] 195  cases t2 196 [ #st2 #st2' #ex' #cl' #co' normalize * #st2mid * #G * #ident_eq * #taa * 197 #st2mid' * #H * * [#_  #st2mid''] * #K * #tlr2 * #L [2: * #tl2] 198 inversion taa in ⊢ ?; 199 [1,3: #st2mid'' #eq1 #eq2 #eq3 destruct normalize * * #H1 destruct (H1) 200 2,4: #st2p #st2p' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 201 destruct normalize * * #H1 destruct (H1) 202 ] 203  #st2 #st2' #ex' #cl' normalize * #st2mid * #G * #ident_eq * #taa * #st2mid' 204 * #H * * [#abs destruct (abs)] #st2mid' * #K * #tlr2 * #L * #tl2 205 inversion taa in ⊢ ?; 206 [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs) 207  #st2p #st2p' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct 197 208 normalize * * #abs destruct (abs) 198 209 ] 199  #st2 #st2' #ex' #cl' normalize * #st2mid * #taa * #st2mid' * #H * 200 [ * #abs destruct (abs)  * #st2mid'' * #J * #f' * #G * #K * #tlr2 * #L * #tl2 201 inversion taa in ⊢ ?; 202 [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs) 203  #st2p #st2p' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct 204 normalize * * #abs destruct (abs) 210  #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #st2mid * #G * 211 #ident_eq * #taa * #st2mid' * #H * * [ #_  #st2mid'' ] * #K * #tlr2' * #L 212 [2: * #tl2] 213 inversion taa in ⊢ ?; 214 [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 #res 215 destruct (H1) >ident_eq >(tlr_rel_extract_equal … H3) 216 cases tal1 in H2; 217 [ #ss #sf #ex'' #cl'' #co'' normalize #_ % 218  #ss #sf #ex'' #cl'' normalize #abs cases abs 219  #st1p' #st1s #sf #ex'' #cl'' #ar'' #tlr1' #co'' normalize #abs cases abs 220  #end' #st1p' #st1s' #st1a' #sf #ex'' #cl'' #ar'' #tlr1' #co' #tal1' 221 normalize #abs cases abs 222  #end' #st1p' #st1i #st1e #ex'' #tal1' #cl'' #co'' normalize 223 cases daemon (* use induction here, but no *) 205 224 ] 206 ] 207  #st2p #st2s #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' normalize * #st2mid * #taa 208 * #st2mid' * #H * * [ #_  #st2mid'' ] * #J * #f'' * #G * #K * #tlr2' * #L [2: * #tl2] 209 inversion taa in ⊢ ?; 210 [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs) 211  #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 225 2,4: #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 212 226 destruct normalize * * #abs destruct (abs) 213  #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 cases daemon 214  #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 227 ] 228  #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 229 normalize * #st2mid * #G * #ident_eq * #taa * #st2mid' * #H * * 230 [ #H1  #st2mid''] * #K * #tlr2' * #L [2: * #tl2] inversion taa in ⊢ ?; 231 [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 #res 232 destruct (H1) >ident_eq >(tal_rel_extract_equal … H2) 233 >(tlr_rel_extract_equal … H3) % 234 2,4: #st2p' #st2p'' #st2mid''' #ex''' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 215 235 destruct normalize * * #abs destruct (abs) 216 236 ] 217  #ends' #st2p #st2s #st2 #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' #tal2 218 normalize * #st2mid * #taa * #st2mid' * #ex'' * * [ #_  #st2mid''] * #J * 219 #f'' * #G * #K * #tlr2' * #L [2: * #tl2] inversion taa in ⊢ ?; 220 [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 #res 221 cases daemon (* injectivity needed again *) 222  #st2p' #st2p'' #st2mid''' #ex''' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 223 destruct normalize * * #abs destruct (abs) 224  #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs) cases daemon 225 (* huh? *) 226  #st2p' #st2p'' #st2mid''' #ex''' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 227 destruct normalize * * #abs destruct (abs) cases daemon (* huh2? *) 228 ] 229  #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #st2mid * #taa * 230 #st2mid' * #H * * [ #He  #st2mid'' ] * #J * #f' * #G * #K * #tlr2' * #L 237  #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #st2mid * #G * 238 #ident_eq * #taa * #st2mid' * #H * * [ #He  #st2mid'' ] * #K * #tlr2' * #L 231 239 [2: * #tl2] inversion taa in ⊢ ?; 232 [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs) 233  #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 234 destruct normalize * * #H1 #H2 #H3 #res cases daemon (* look into this *) 235  #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs) 236  #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 237 destruct normalize * * #H1 #H2 #H3 #res cases daemon 238 ] 239 ] 240  cases t2 241 [ #st2 #st2' #ex' #cl' #co' normalize #Hsim #res 242 @(tal_rel_extract_equal p g lg top_f … Hsim) 243  #ss #fs #ex' #cl' normalize #Hsim #res 244 @(tal_rel_extract_equal p g lg top_f … Hsim) 245  #st2p #st2s #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' normalize #Hsim #res 246 @(tal_rel_extract_equal p g lg top_f … Hsim) 247  #ends' #st2p #st2s #st2 #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' #tal2 248 normalize #Hsim #res @(tal_rel_extract_equal p g lg top_f … Hsim) 249  #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize #Hsim #res 250 @(tal_rel_extract_equal p g lg top_f … Hsim) 251 ] 240 [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs) 241 2,4: #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 242 destruct normalize * * #H1 #H2 #H3 #res destruct (H1) 243 >(tlr_rel_extract_equal … H3) <ident_eq normalize cases daemon 244 (* look further here *) 245 ] 246 ] 247  cases t2 248 [ #st2 #st2' #ex' #cl' #co' 249  #ss #fs #ex' #cl' 250  #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' 251  #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 252  #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' 253 ] 254 normalize #Hsim #res @(tal_rel_extract_equal p g lg top_f … Hsim) 252 255 ] 253 256 qed. … … 263 266  tlr_step st1 st1' st1'' tll1 tlr1 ⇒ ? 264 267 ] 265 and tll_rel_ extract_equal (p: params) (g: list ident)268 and tll_rel_max_equal (p: params) (g: list ident) 266 269 (lg: ident → joint_internal_function p g) (top_f: ident) 267 270 S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1: … … 272 275 [ tll_base ends st1 st1' tal1 co ⇒ ? 273 276 ] 274 and tal_rel_ extract_equal (p: params) (g: list ident)277 and tal_rel_max_equal (p: params) (g: list ident) 275 278 (lg: ident → joint_internal_function p g) (top_f: ident) 276 279 S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
Note: See TracChangeset
for help on using the changeset viewer.