- Timestamp:
- Oct 25, 2012, 4:36:07 PM (7 years ago)
- Location:
- src/joint
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/joint/Joint_jaap.ma
r2398 r2417 175 175 [ step_seq s ⇒ 176 176 match s with 177 [ CALL_ID l _ _ ⇒ cl_calll178 | extension_call _ ⇒ cl_call ? (* pointer stuff not yet implemented, it seems *)177 [ CALL_ID _ _ _ ⇒ cl_call 178 | extension_call _ ⇒ cl_call 179 179 | _ ⇒ cl_other 180 180 ] 181 181 | COND _ _ ⇒ cl_jump 182 182 ]. 183 cases daemon184 qed.185 183 186 184 record stmt_params : Type[1] ≝ -
src/joint/stacksize.ma
r2398 r2417 47 47 [ tal_base_not_return s1 s2 ex cl co ⇒ res 48 48 | tal_base_return s1 s2 ex cl ⇒ down ?? (lg top_f)::res 49 | tal_base_call s1p s1s s2 ex f clar tlr co ⇒49 | tal_base_call s1p s1s s2 ex cl f ca ar tlr co ⇒ 50 50 extract_list_from_tlr … lg f … tlr (up ?? (lg f)::res) 51 | tal_step_call end s1p s1s s1a s2 ex f clar tlr co tal ⇒51 | tal_step_call end s1p s1s s1a s2 ex cl f ca ar tlr co tal ⇒ 52 52 let res' ≝ extract_list_from_tlr … lg f … tlr (up ?? (lg f)::res) in 53 53 extract_list_from_tal … lg top_f … tal res' … … 81 81 ∀res.extract_list_from_tal p g lg top_f S1 e1 s1 s1' t1 res = 82 82 extract_list_from_tal p g lg top_f S2 e2 s2 s2' t2 res ≝ 83 match t1 with 84 [ tal_base_not_return st1 st1' ex cl co ⇒ ? 85 | tal_base_return st1 st1' ex cl ⇒ ? 86 | tal_base_call st1p st1s st1' ex cl f ca ar tlr1 co ⇒ ? 87 | tal_step_call end st1p st1s st1 st1' ex cl f ca ar tlr1 co tal1 ⇒ ? 88 | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ? 89 ]. 90 [ cases t2 91 [ #st2 #st2' #tll2 normalize #Hsim @(tll_rel_extract_equal … Hsim) 92 | #st2 #st2' #st2'' #tll2 #tlr2 normalize #abs cases abs 93 ] 94 | cases t2 95 [ #st2 #st2' #tll2 normalize #abs cases abs 96 | #st2 #st2' #st2'' #tll2 #tlr2 normalize #Hsim #res 97 >(tll_rel_extract_equal p g lg top_f … (proj1 ?? Hsim) res) 98 @(tlr_rel_extract_equal … (proj2 ?? Hsim)) 99 ] 100 | cases t2 #ends' #st2 #st2' #tal2 #co' normalize * #H1 #H2 101 @(tal_rel_extract_equal … H2) 102 | cases t2 103 [ #st2 #st2' #ex' #cl' #co' normalize #Hsim #res % 104 | #st2 #st2' #ex' #cl' * #abs destruct (abs) 105 | #st2p #st2s #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' normalize * #H1 * #st2mid * 106 #taa * #H * #G * #K inversion taa in ⊢ ?; 107 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) 108 | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct 109 normalize #abs destruct (abs) 110 ] 111 | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' #tal2 normalize * 112 #H1 * #st2mid * #taa * #H * #G * #K inversion taa in ⊢ ?; 113 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) 114 | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct 115 normalize #abs destruct (abs) 116 ] 117 | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid * #taa 118 * #H * #G * #K inversion taa in ⊢ ?; 119 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) 120 | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 121 destruct normalize #Hsim cases daemon (* use injectivity from Hsim? *) 122 ] 123 ] 124 | cases t2 125 [ #st2 #st2' #ex' #cl' #co' normalize * #abs destruct (abs) 126 | #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' #tal2 129 normalize * #H1 * #st2mid * #taa * #H * #G inversion taa in ⊢ ?; 130 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) 131 | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct 132 normalize #abs destruct (abs) 133 ] 134 | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid 135 * #taa * #H * #G inversion taa in ⊢ ?; 136 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) 137 | #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 144 [ * * #H3 #H2 #H4 | #H2 ] 145 inversion taa in ⊢ ?; 146 [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize normalize in H3; destruct (H3) 147 | #st2'' #st2''' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct 148 normalize in H3; destruct (H3) 149 | #st2mid''' #eq1 #eq2 #eq3 destruct normalize normalize in H1; destruct (H1) 150 | #st2'' #st2''' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct 151 normalize in H1; destruct (H1) 152 ] 153 | #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) 158 | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 159 destruct normalize * #tal2 * * #H1 destruct (H1) 160 | #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? *) 162 | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 163 destruct normalize * #abs destruct (abs) 164 ] 165 | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' #tal2 166 normalize * #H1 * #st2mid * #taa * #st2mid' * #H * * [2: #st2mid'' *] #J * #f 167 * #G * #K * #tlr2' * #L 168 inversion taa in ⊢ ?; 169 [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * #tal2' * * #H1 #H2 #H3 #res 170 cases daemon 171 | #st2p' #st2p'' #st2mid'; #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 172 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 #eq3 175 destruct normalize * #abs destruct (abs) 176 ] 177 | #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 197 normalize * * #abs destruct (abs) 198 ] 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) 205 ] 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 212 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 215 destruct normalize * * #abs destruct (abs) 216 ] 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 231 [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 ] 252 ] 253 qed. 254 255 (* let rec tlr_rel_max_equal (p: params) (g: list ident) 256 (lg: ident → joint_internal_function p g) (top_f: ident) 257 S1 S2 s1 s1' s2 s2' t1 t2 on t1: 258 tlr_rel S1 s1 s1' S2 s2 s2' t1 t2 → 259 max_stacksize p g (extract_list_from_tlr p g lg top_f S1 s1 s1' t1 []) = 260 max_stacksize p g (extract_list_from_tlr p g lg top_f S2 s2 s2' t2 []) ≝ 261 match t1 with 262 [ tlr_base st1 st1' tll1 ⇒ ? 263 | tlr_step st1 st1' st1'' tll1 tlr1 ⇒ ? 264 ] 265 and tll_rel_extract_equal (p: params) (g: list ident) 266 (lg: ident → joint_internal_function p g) (top_f: ident) 267 S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1: 268 t1 ≈ t2 → 269 max_stacksize p g (extract_list_from_tll p g lg top_f S1 e1 s1 s1' t1 []) = 270 max_stacksize p g (extract_list_from_tll p g lg top_f S2 e2 s2 s2' t2 []) ≝ 271 match t1 with 272 [ tll_base ends st1 st1' tal1 co ⇒ ? 273 ] 274 and tal_rel_extract_equal (p: params) (g: list ident) 275 (lg: ident → joint_internal_function p g) (top_f: ident) 276 S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1: 277 t1 ≈ t2 → 278 max_stacksize p g (extract_list_from_tal p g lg top_f S1 e1 s1 s1' t1 []) = 279 max_stacksize p g (extract_list_from_tal p g lg top_f S2 e2 s2 s2' t2 []) ≝ 83 280 match t1 with 84 281 [ tal_base_not_return st1 st1' ex cl co ⇒ ? … … 88 285 | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ? 89 286 ]. 90 [ cases t291 [ #st2 #st2' #tll2 normalize #Hsim @(tll_rel_extract_equal … Hsim)92 | #st2 #st2' #st2'' #tll2 #tlr2 normalize #abs cases abs93 ]94 | cases t295 [ #st2 #st2' #tll2 normalize #abs cases abs96 | #st2 #st2' #st2'' #tll2 #tlr2 normalize #Hsim #res97 >(tll_rel_extract_equal p g lg top_f … (proj1 ?? Hsim) res)98 @(tlr_rel_extract_equal … (proj2 ?? Hsim))99 ]100 | cases t2 #ends' #st2 #st2' #tal2 #co' normalize * #H1 #H2101 @(tal_rel_extract_equal … H2)102 | cases t2103 [ #st2 #st2' #ex' #cl' #co' normalize #Hsim #res %104 | #st2 #st2' #ex' #cl' * #abs destruct (abs)105 | #st2p #st2s #st2' #ex' #f' #cl' #ar' #tlr2 #co' normalize * #H1 * #st2mid *106 #taa * #H * #G * #K inversion taa in ⊢ ?;107 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)108 | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct109 normalize #abs destruct (abs)110 ]111 | #ends' #st2p #st2s #st2 #st2' #ex' #f' #cl' #ar' #tlr2 #co' #tal2 normalize *112 #H1 * #st2mid * #taa * #H * #G * #K inversion taa in ⊢ ?;113 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)114 | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct115 normalize #abs destruct (abs)116 ]117 | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid * #taa118 * #H * #G * #K inversion taa in ⊢ ?;119 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)120 | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3121 destruct normalize #Hsim cases daemon (* use injectivity from Hsim? *)122 ]123 ]124 | cases t2125 [ #st2 #st2' #ex' #cl' #co' normalize * #abs destruct (abs)126 | #st2 #st2' #ex' #cl' normalize * #H1 #H2 #res %127 | #st2p #st2s #st2' #ex' #f' #cl' #ar' #tlr2 #co' normalize * #abs destruct (abs)128 | #ends' #st2p #st2s #st2 #st2' #ex' #f' #cl' #ar' #tlr2 #co' #tal2129 normalize * #H1 * #st2mid * #taa * #H * #G inversion taa in ⊢ ?;130 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)131 | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct132 normalize #abs destruct (abs)133 ]134 | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid135 * #taa * #H * #G inversion taa in ⊢ ?;136 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)137 | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3138 destruct normalize #Hsim cases daemon (* use injectivity from Hsim? *)139 ]140 ]141 | cases t2142 [ #st2 #st2' #ex' #cl' #co' normalize * #_ * #st2mid * #taa143 * #st2mid' * #H * #f' * #G * #K * #tlr2 * #L * #H1 #H2 inversion taa in ⊢ ?;144 [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize normalize in H1; destruct (H1)145 | #st2'' #st2''' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct146 normalize in H1; destruct (H1)147 ]148 | #st2 #st2' #ex' #cl' normalize * #abs destruct (abs)149 | #st2p #st2s #st2' #ex' #f' #cl' #ar' #tlr2 #co' normalize * #_ * #st2mid *150 #taa * #st2mid' * #H * #f'' * #G * #K * #tlr2' * #L inversion taa in ⊢ ?;151 [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #H1 #H2 #res152 >(tlr_rel_extract_equal p g lg f … H2) cases daemon (* use injectivity and H1? *)153 | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3154 destruct normalize * #abs destruct (abs)155 ]156 | #ends' #st2p #st2s #st2 #st2' #ex' #f' #cl' #ar' #tlr2 #co' #tal2157 normalize * #H1 * #st2mid * #taa * #st2mid' * #H * #f * #G * #K * #tlr2' * #L158 inversion taa in ⊢ ?;159 [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #abs destruct (abs)160 | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3161 destruct normalize * #abs destruct (abs)162 ]163 | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid *164 #taa * #st2mid' * #H * #f * #G * #K * #tlr2 * #L inversion taa in ⊢ ?;165 [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #abs destruct (abs)166 | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3167 destruct normalize * #H1 #H2 #res cases daemon (* do something with H1 and H2 *)168 ]169 ]170 | cases t2171 [ #st2 #st2' #ex' #cl' #co' normalize * #st2mid * #taa * #st2_fun * #st2_after_fun172 * #H * #f' * #G * #K * #tlr2 * #L * #tl2 inversion taa in ⊢ ?;173 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)174 | #st2p #st2p' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct175 normalize * * #abs destruct (abs)176 ]177 | #st2 #st2' #ex' #cl' normalize * #st2mid * #taa * #st2_fun * #st2_after_fun178 * #H * #f' * #G * #K * #tlr2 * #L * #tl2 inversion taa in ⊢ ?;179 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)180 | #st2p #st2p' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct181 normalize * * #abs destruct (abs)182 ]183 | #st2p #st2s #st2' #ex' #f' #H #ar' #tlr2 #co' normalize * #st2mid * #taa184 * #st2_fun * #st2_after_fun * #H' * #f'' * #G * #K * #tlr2' * #L * #tl2185 inversion taa in ⊢ ?;186 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)187 | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3188 destruct normalize * * #abs destruct (abs)189 ]190 | #ends' #st2p #st2s #st2 #st2' #ex' #f' #cl' #ar' #tlr2 #co' #tal2191 normalize * #st2mid * #taa * #st2_fun * #st2_after_fun * #H * #f'' *192 #G * #K * #tlr2' * #L * #tl2 inversion taa in ⊢ ?;193 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 #res194 >(tlr_rel_extract_equal … H2) cases daemon (* injectivity needed again *)195 | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3196 destruct normalize * * #abs destruct (abs)197 ]198 | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #st2mid * #taa *199 #st2_fun * #st2_after_fun * #H * #f' * #G * #K * #tlr2' * #L * #tl2200 inversion taa in ⊢ ?;201 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)202 | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3203 destruct normalize * * #H1 #H2 #H3 #res cases daemon (* look into this *)204 ]205 ]206 | cases t2207 [ #st2 #st2' #ex' #cl' #co' normalize #Hsim #res208 @(tal_rel_extract_equal p g lg top_f … Hsim)209 | #ss #fs #ex' #cl' normalize #Hsim #res210 @(tal_rel_extract_equal p g lg top_f … Hsim)211 | #st2p #st2s #st2' #ex' #f' #H #ar' #tlr2 #co' normalize #Hsim #res212 @(tal_rel_extract_equal p g lg top_f … Hsim)213 | #ends' #st2p #st2s #st2 #st2' #ex' #f' #cl' #ar' #tlr2 #co' #tal2214 normalize #Hsim #res @(tal_rel_extract_equal p g lg top_f … Hsim)215 | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize #Hsim #res216 @(tal_rel_extract_equal p g lg top_f … Hsim)217 ]218 ]219 qed.220 221 let rec tlr_rel_max_equal (p: params) (g: list ident)222 (lg: ident → joint_internal_function p g) (top_f: ident)223 S1 S2 s1 s1' s2 s2' t1 t2 on t1:224 tlr_rel S1 s1 s1' S2 s2 s2' t1 t2 →225 max_stacksize p g (extract_list_from_tlr p g lg top_f S1 s1 s1' t1 []) =226 max_stacksize p g (extract_list_from_tlr p g lg top_f S2 s2 s2' t2 []) ≝227 match t1 with228 [ tlr_base st1 st1' tll1 ⇒ ?229 | tlr_step st1 st1' st1'' tll1 tlr1 ⇒ ?230 ]231 and tll_rel_extract_equal (p: params) (g: list ident)232 (lg: ident → joint_internal_function p g) (top_f: ident)233 S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:234 t1 ≈ t2 →235 max_stacksize p g (extract_list_from_tll p g lg top_f S1 e1 s1 s1' t1 []) =236 max_stacksize p g (extract_list_from_tll p g lg top_f S2 e2 s2 s2' t2 []) ≝237 match t1 with238 [ tll_base ends st1 st1' tal1 co ⇒ ?239 ]240 and tal_rel_extract_equal (p: params) (g: list ident)241 (lg: ident → joint_internal_function p g) (top_f: ident)242 S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:243 t1 ≈ t2 →244 max_stacksize p g (extract_list_from_tal p g lg top_f S1 e1 s1 s1' t1 []) =245 max_stacksize p g (extract_list_from_tal p g lg top_f S2 e2 s2 s2' t2 []) ≝246 match t1 with247 [ tal_base_not_return st1 st1' ex cl co ⇒ ?248 | tal_base_return st1 st1' ex cl ⇒ ?249 | tal_base_call st1p st1s st1' ex f cl ar tlr1 co ⇒ ?250 | tal_step_call end st1p st1s st1 st1' ex f cl ar tlr1 co tal1 ⇒ ?251 | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ?252 ].253 287 cases daemon (* next proof *) 254 qed. 288 qed. *) 255 289 256 290
Note: See TracChangeset
for help on using the changeset viewer.