 Timestamp:
 May 21, 2012, 10:33:26 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r1966 r1972 1311 1311 qed. 1312 1312 1313 lemma destruct_bug_fix :1313 lemma destruct_bug_fix_1: 1314 1314 ∀n: nat. 1315 1315 S n = 0 → False. 1316 1316 #n #absurd destruct(absurd) 1317 qed. 1318 1319 lemma destruct_bug_fix_2: 1320 ∀m, n: nat. 1321 S m = S n → m = n. 1322 #m #n #refl destruct % 1317 1323 qed. 1318 1324 … … 1324 1330 @(Vector_inv_ind bool 3 b (λn: nat. λv: Vector bool n. ∃l:bool.∃c:bool.∃r:bool. v ≃ [[l; c; r]])) 1325 1331 [1: 1326 #absurd @⊥ b @(destruct_bug_fix 2)1332 #absurd @⊥ b @(destruct_bug_fix_1 2) 1327 1333 >absurd % 1328 1334 2: … … 1330 1336 cut (n = 2) 1331 1337 [1: 1338 @destruct_bug_fix_2 1339 >size_refl % 1332 1340 2: 1333 #n_refl >n_refl in tl; 1334 cases daemon 1341 #n_refl >n_refl in tl; #V 1342 @(Vector_inv_ind bool 2 V (λn: nat. λv: Vector bool n. ∃c:bool. ∃r:bool. hd:::v ≃ [[hd; c; r]])) 1343 [1: 1344 #absurd @⊥ V @(destruct_bug_fix_1 1) 1345 >absurd % 1346 2: 1347 #n' #hd' #tl' #_ #size_refl' #hd_tl_refl' %{hd'} 1348 cut (n' = 1) 1349 [1: 1350 @destruct_bug_fix_2 >size_refl' % 1351 2: 1352 #n_refl' >n_refl' in tl'; #V' 1353 @(Vector_inv_ind bool 1 V' (λn: nat. λv: Vector bool n. ∃r: bool. hd:::hd':::v ≃ [[hd; hd'; r]])) 1354 [1: 1355 #absurd @⊥ V' @(destruct_bug_fix_1 0) 1356 >absurd % 1357 2: 1358 #n'' #hd'' #tl'' #_ #size_refl'' #hd_tl_refl'' %{hd''} 1359 cut (n'' = 0) 1360 [1: 1361 @destruct_bug_fix_2 >size_refl'' % 1362 2: 1363 #n_refl'' >n_refl'' in tl''; #tl''' 1364 >(Vector_O … tl''') % 1365 ] 1366 ] 1367 ] 1368 ] 1369 ] 1335 1370 ] 1336 cases daemon1337 1371 qed. 1338 1372
Note: See TracChangeset
for help on using the changeset viewer.