- Timestamp:
- Jul 19, 2012, 6:45:52 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/SimplifyCasts.ma
r2184 r2219 214 214 | SimOk : (∀a:A. r1 = OK ? a → r2 = OK ? a) → res_sim A r1 r2 215 215 | SimFail : (∃err. r1 = Error ? err) → res_sim A r1 r2. 216 217 (* Trick to reduce checking time by eliminating a load of costly automation. 218 It would be nice to do this by refactoring the type and code instead, but we 219 don't want to spend lots of time on something that already works. *) 220 221 lemma SimFailNicely : ∀A,err,r2. res_sim A (Error ? err) r2. 222 #A #err #r2 @SimFail %{err} % 223 qed. 216 224 217 225 (* Invariant of simplify_expr *) … … 1126 1134 cases Hexpr_sim 1127 1135 [ 2: (* Case where the evaluation of e1 as an expression fails *) 1128 normalize * #err #Hfail >Hfail normalize nodelta @ (SimFail ???) /2 by ex_intro/1136 normalize * #err #Hfail >Hfail normalize nodelta @SimFailNicely 1129 1137 | 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *) 1130 1138 #Hsim %1 * #val #trace normalize #Hstep … … 1156 1164 cases Hexpr_sim 1157 1165 [ 2: (* Case where the evaluation of e1 as an lvalue fails *) 1158 normalize * #err #Hfail >Hfail normalize nodelta @ (SimFail ???) /2 by ex_intro/1166 normalize * #err #Hfail >Hfail normalize nodelta @SimFailNicely 1159 1167 | 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *) 1160 1168 #Hsim %1 * * #block #offset #trace normalize #Hstep … … 1183 1191 cases Hlvalue_sim 1184 1192 [ 2: (* Case where the evaluation of e1 as an expression fails *) 1185 * #err #Hfail @SimFail whd in match (exec_expr ????); >Hfail normalize nodelta /2 by ex_intro/1193 * #err #Hfail whd in match (exec_expr ????); >Hfail @SimFailNicely 1186 1194 | 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *) 1187 1195 #Hsim %1 * #val #trace whd in match (exec_expr ????); #Hstep … … 1206 1214 ] 1207 1215 | 2: (* Proving preservation of the semantics of lvalues. *) 1208 @SimFail /2 by ex_intro/1216 @SimFailNicely 1209 1217 ] 1210 1218 | 17: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq … … 1212 1220 whd in match (exec_expr ge en m (Expr ??)); 1213 1221 cases Hexpr_sim 1214 [ 2: * #error #Hexec >Hexec normalize nodelta @SimFail /2 by ex_intro/1222 [ 2: * #error #Hexec >Hexec normalize nodelta @SimFailNicely 1215 1223 | 1: cases (exec_expr ge en m e1) 1216 [ 2: #error #Hexec normalize nodelta @SimFail /2 by ex_intro/1224 [ 2: #error #Hexec normalize nodelta @SimFailNicely 1217 1225 | 1: * #val #trace #Hexec 1218 1226 >(Hexec ? (refl ? (OK ? 〈val,trace〉))) … … 1220 1228 ] 1221 1229 ] 1222 | 2: @SimFail /2 by ex_intro/1230 | 2: @SimFailNicely 1223 1231 ] 1224 1232 | 18: destruct elim (bool_conj_inv … Hdesired_eq) #Hdesired_lhs #Hdesired_rhs -Hdesired_eq … … 1323 1331 whd in match (exec_expr ????); whd in match (exec_expr ????); 1324 1332 cases Hexpr_sim_lhs 1325 [ 2,4,6,8: * #error #Herror >Herror @SimFail /2 by refl, ex_intro/1333 [ 2,4,6,8: * #error #Herror >Herror @SimFailNicely 1326 1334 | *: cases (exec_expr ge en m lhs) 1327 [ 2,4,6,8: #error #_ @SimFail /2 by refl, ex_intro/1335 [ 2,4,6,8: #error #_ @SimFailNicely 1328 1336 | *: * #lval #ltrace #Hsim_lhs normalize nodelta 1329 1337 cases Hexpr_sim_rhs 1330 [ 2,4,6,8: * #error #Herror >Herror @SimFail /2 by refl, ex_intro/1338 [ 2,4,6,8: * #error #Herror >Herror @SimFailNicely 1331 1339 | *: cases (exec_expr ge en m rhs) 1332 [ 2,4,6,8: #error #_ @SimFail /2 by refl, ex_intro/1340 [ 2,4,6,8: #error #_ @SimFailNicely 1333 1341 | *: * #rval #rtrace #Hsim_rhs 1334 1342 whd in match (exec_expr ??? (Expr (Ebinop ???) ?)); … … 1342 1350 ] 1343 1351 ] 1344 | *: @SimFail /2 by refl, ex_intro/1352 | *: @SimFailNicely 1345 1353 ] 1346 1354 (* Jump to the cast cases *) … … 1350 1358 (* exec_expr simulation *) 1351 1359 [ 1,3,5,7,9,11,13,15: cases Hexec_sim 1352 [ 2,4,6,8,10,12,14,16: destruct * #error #Hexec_fail @SimFailwhd in match (exec_expr ge en m ?);1353 >Hexec_fail /2 by refl, ex_intro/1360 [ 2,4,6,8,10,12,14,16: destruct * #error #Hexec_fail whd in match (exec_expr ge en m ?); 1361 >Hexec_fail @SimFailNicely 1354 1362 | 1,3,5,7,9,11,13,15: #Hsim @SimOk * #val #trace <Hexpr_eq >Hdesc_eq 1355 1363 whd in match (exec_expr ge en m ?); #Hstep … … 1373 1381 ] 1374 1382 ] 1375 | 2,4,6,8,10,12,14,16: destruct @SimFail /2 by refl, ex_intro/1383 | 2,4,6,8,10,12,14,16: destruct @SimFailNicely 1376 1384 ] 1377 1385 | 24: destruct inversion (Hcastee_inv ge en m) … … 1416 1424 #src_sz #src_sg #Htype_castee #Htype_castee2 #Hsmaller_eval #_ #Hinv_eq 1417 1425 @(Inv_eq ???????) // 1418 [ 1, 4: >Htype_castee2 //1419 | 2, 5: (* Prove simulation for exec_expr *)1426 [ 1,3: >Htype_castee2 // 1427 | 2,4: (* Prove simulation for exec_expr *) 1420 1428 whd in match (exec_expr ??? (Expr ??)); 1421 1429 cases (exec_expr ge en m castee) in Hsmaller_eval; 1422 1430 [ 2,4: (* erroneous evaluation of the original expression *) 1423 #error #Hsmaller_eval @SimFail @(ex_intro … error) //1431 #error #Hsmaller_eval @SimFailNicely 1424 1432 | 1,3: * #val #trace normalize nodelta >Htype_castee 1425 1433 lapply (exec_cast_inv val src_sz src_sg cast_sz cast_sg m) 1426 1434 cases (exec_cast m val (Tint src_sz src_sg) (Tint cast_sz cast_sg)) 1427 [ 2,4: #error #_ #_ @SimFail /2 by ex_intro/1435 [ 2,4: #error #_ #_ @SimFailNicely 1428 1436 | 1,3: #result #Hinversion elim (Hinversion result (refl ??)) 1429 1437 #val_int * #Hval_eq #Hresult_eq … … 1434 1442 destruct @SimOk normalize #a #H @H ] 1435 1443 ] ] 1436 | 3,6: @SimFail /2 by refl, ex_intro/1437 1444 ] ] 1438 1445 | 26,28: destruct … … 1447 1454 #result_flag #Hresult #Htype_eq #Hsim_expr #Hsim_lvalue #_ #Hinv 1448 1455 @(Inv_eq ???????) // 1449 [ 1,3: (* Simulation for exec_expr *)1450 1456 whd in match (exec_expr ??? (Expr ??)); 1451 1457 whd in match (exec_expr ??? (Expr ??)); 1452 1458 cases Hsim_expr 1453 [ 2,4: * #error #Hexec_err >Hexec_err @SimFail @(ex_intro … error) //1459 [ 2,4: * #error #Hexec_err >Hexec_err @SimFailNicely 1454 1460 | 1,3: #Hexec_ok 1455 1461 cases (exec_expr ge en m castee) in Hexec_ok; 1456 [ 2,4: #error #Hsim @SimFail normalize nodelta /2/1462 [ 2,4: #error #Hsim @SimFailNicely 1457 1463 | 1,3: * #val #trace #Hsim normalize nodelta 1458 1464 >Htype_eq >(Hsim 〈val,trace〉 (refl ? (OK ? 〈val,trace〉))) normalize nodelta … … 1460 1466 ] 1461 1467 ] 1462 | 2,4: @SimFail /2 by refl, ex_intro/1463 ]1464 1468 ] 1465 1469 | 29: destruct elim (Hcastee_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq … … 1467 1471 whd in match (exec_expr ??? (Expr ??)); 1468 1472 whd in match (exec_expr ??? (Expr ??)); 1469 [ 1:cases Hsim_expr1470 [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by refl, ex_intro/1473 cases Hsim_expr 1474 [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely 1471 1475 | 1: #Hexec_ok @SimOk * #val #trace 1472 1476 cases (exec_expr ge en m castee) in Hexec_ok; … … 1478 1482 ] 1479 1483 ] 1480 | 2: @SimFail /2 by refl, ex_intro/1481 ]1482 1484 | 37: destruct elim (bool_conj_inv … Hdesired_eq) #Hdesired_true #Hdesired_false -Hdesired_eq 1483 1485 inversion (Htrue_inv ge en m) … … 1543 1545 [ 1,3,5: whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); 1544 1546 cases (exec_expr ge en m cond) in Hsim_expr_cond; 1545 [ 2,4,6: #error #_ @SimFail /2 by ex_intro/1547 [ 2,4,6: #error #_ @SimFailNicely 1546 1548 | 1,3,5: * #cond_val #cond_trace normalize nodelta 1547 1549 cases (exec_expr ge en m cond1) … … 1555 1557 #Hcond_eq normalize nodelta destruct (Hcond_eq) 1556 1558 >Htype_cond_eq cases (exec_bool_of_val cond_val (typeof cond1)) 1557 [ 2,4,6: #error @SimFail normalize /2 by refl, ex_intro /1559 [ 2,4,6: #error @SimFailNicely 1558 1560 | 1,3,5: * (* true branch *) 1559 1561 [ 1,3,5: … … 1561 1563 normalize in match (m_bind ?????); 1562 1564 cases Hsim_expr_true 1563 [ 2,4,6: * #error #Hexec_fail >Hexec_fail @SimFail /2 by refl, ex_intro/1565 [ 2,4,6: * #error #Hexec_fail >Hexec_fail @SimFailNicely 1564 1566 | 1,3,5: cases (exec_expr ge en m iftrue) 1565 [ 2,4,6: #error #_ normalize nodelta @SimFail /2 by refl, ex_intro/1567 [ 2,4,6: #error #_ normalize nodelta @SimFailNicely 1566 1568 | 1,3,5: * #val_true #trace_true normalize nodelta #Hsim 1567 1569 >(Hsim 〈val_true,trace_true〉 (refl ? (OK ? 〈val_true,trace_true〉))) … … 1573 1575 normalize in match (m_bind ?????); 1574 1576 cases Hsim_expr_false 1575 [ 2,4,6: * #error #Hexec_fail >Hexec_fail normalize nodelta @SimFail /2 by refl, ex_intro/1577 [ 2,4,6: * #error #Hexec_fail >Hexec_fail normalize nodelta @SimFailNicely 1576 1578 | 1,3,5: cases (exec_expr ge en m iffalse) 1577 [ 2,4,6: #error #_ normalize nodelta @SimFail /2 by refl, ex_intro/1579 [ 2,4,6: #error #_ normalize nodelta @SimFailNicely 1578 1580 | 1,3,5: * #val_false #trace_false normalize nodelta #Hsim 1579 1581 >(Hsim 〈val_false,trace_false〉 (refl ? (OK ? 〈val_false,trace_false〉))) … … 1586 1588 ] 1587 1589 ] 1588 | 2,4,6: @SimFail /2 by ex_intro/1590 | 2,4,6: @SimFailNicely 1589 1591 ] 1590 1592 | 41,42: destruct … … 1595 1597 whd in match (exec_expr ??? (Expr ??)); 1596 1598 cases Hsim_expr_lhs 1597 [ 2,4: * #error #Hexec_fail >Hexec_fail normalize nodelta @SimFail /2 by refl, ex_intro/1599 [ 2,4: * #error #Hexec_fail >Hexec_fail normalize nodelta @SimFailNicely 1598 1600 | 1,3: cases (exec_expr ge en m lhs) 1599 [ 2,4: #error #_ @SimFail /2 by refl, ex_intro/1601 [ 2,4: #error #_ @SimFailNicely 1600 1602 | 1,3: * #lhs_val #lhs_trace #Hsim normalize nodelta 1601 1603 >(Hsim 〈lhs_val,lhs_trace〉 (refl ? (OK ? 〈lhs_val,lhs_trace〉))) 1602 1604 normalize nodelta >Htype_eq_lhs 1603 1605 cases (exec_bool_of_val lhs_val (typeof lhs1)) 1604 [ 2,4: #error normalize @SimFail /2 by refl, ex_intro/1606 [ 2,4: #error normalize @SimFailNicely 1605 1607 | 1,3: * 1606 1608 whd in match (m_bind ?????); … … 1609 1611 @SimOk #a #H @H 1610 1612 | 1,4: cases Hsim_expr_rhs 1611 [ 2,4: * #error #Hexec >Hexec @SimFail /2 by refl, ex_intro/1613 [ 2,4: * #error #Hexec >Hexec @SimFailNicely 1612 1614 | 1,3: cases (exec_expr ge en m rhs) 1613 [ 2,4: #error #_ @SimFail /2 by refl, ex_intro/1615 [ 2,4: #error #_ @SimFailNicely 1614 1616 | 1,3: * #rhs_val #rhs_trace -Hsim #Hsim 1615 1617 >(Hsim 〈rhs_val,rhs_trace〉 (refl ? (OK ? 〈rhs_val,rhs_trace〉))) … … 1622 1624 ] 1623 1625 ] 1624 | 2,4: @SimFail /2 by ex_intro/1626 | 2,4: @SimFailNicely 1625 1627 ] 1626 1628 | 43: destruct … … 1642 1644 cases (typeof rec_expr1) normalize nodelta 1643 1645 [ 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ] 1644 [ 1,2,3,4,5,8,9: @SimFail /2 by refl, ex_intro/1646 [ 1,2,3,4,5,8,9: @SimFailNicely 1645 1647 | 6,7: cases Hsim_lvalue 1646 [ 2,4: * #error #Herror >Herror normalize in ⊢ (??%?); @SimFail /2 by refl, ex_intro/1648 [ 2,4: * #error #Herror >Herror normalize in ⊢ (??%?); @SimFailNicely 1647 1649 | 1,3: cases (exec_lvalue ge en m rec_expr) 1648 [ 2,4: #error #_ normalize in ⊢ (??%?); @SimFail /2 by refl, ex_intro/1650 [ 2,4: #error #_ normalize in ⊢ (??%?); @SimFailNicely 1649 1651 | 1,3: #a #Hsim >(Hsim a (refl ? (OK ? a))) 1650 1652 whd in match (m_bind ?????); … … 1657 1659 cases (typeof rec_expr1) normalize nodelta 1658 1660 [ 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ] 1659 [ 1,2,3,4,5,8,9: @SimFail /2 by refl, ex_intro/1661 [ 1,2,3,4,5,8,9: @SimFailNicely 1660 1662 | 6,7: cases Hsim_lvalue 1661 [ 2,4: * #error #Herror >Herror normalize in ⊢ (??%?); @SimFail /2 by refl, ex_intro/1663 [ 2,4: * #error #Herror >Herror normalize in ⊢ (??%?); @SimFailNicely 1662 1664 | 1,3: cases (exec_lvalue ge en m rec_expr) 1663 [ 2,4: #error #_ normalize in ⊢ (??%?); @SimFail /2 by refl, ex_intro/1665 [ 2,4: #error #_ normalize in ⊢ (??%?); @SimFailNicely 1664 1666 | 1,3: #a #Hsim >(Hsim a (refl ? (OK ? a))) 1665 1667 whd in match (m_bind ?????); … … 1694 1696 whd in match (exec_expr ??? (Expr ??)); 1695 1697 cases Hsim_expr 1696 [ 2: * #error #Hexec_error >Hexec_error @SimFail /2 by ex_intro/1698 [ 2: * #error #Hexec_error >Hexec_error @SimFailNicely 1697 1699 | 1: cases (exec_expr ge en m e1) 1698 [ 2: #error #_ @SimFail /2 by ex_intro/1700 [ 2: #error #_ @SimFailNicely 1699 1701 | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #He2_exec >He2_exec 1700 1702 @SimOk #a #H @H 1701 1703 ] 1702 1704 ] 1703 | 3: @SimFail /2 by ex_intro/1705 | 3: @SimFailNicely 1704 1706 ] 1705 1707 ] … … 1709 1711 whd in match (exec_expr ??? (Expr ??)); 1710 1712 cases Hsim_expr 1711 [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/1713 [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely 1712 1714 | 1: cases (exec_expr ge en m e1) 1713 [ 2: #error #_ @SimFail /2 by ex_intro/1715 [ 2: #error #_ @SimFailNicely 1714 1716 | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hsim2 >Hsim2 @SimOk #a #H @H ] 1715 1717 ] … … 1734 1736 [ 1,2: 1735 1737 cases Hsim_expr 1736 [ 2,4: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/1738 [ 2,4: * #error #Hexec_fail >Hexec_fail @SimFailNicely 1737 1739 | 1,3: cases (exec_expr ge en m e1) 1738 [ 2,4: #error #_ @SimFail /2 by ex_intro/1740 [ 2,4: #error #_ @SimFailNicely 1739 1741 | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H @SimOk #a #H @H ] ] 1740 1742 | 3: // ] … … 1746 1748 whd in match (exec_expr ??? (Expr ??)); 1747 1749 cases Hsim_lvalue 1748 [ 2: * #error #Hlvalue_fail >Hlvalue_fail @SimFail /2 by ex_intro/1750 [ 2: * #error #Hlvalue_fail >Hlvalue_fail @SimFailNicely 1749 1751 | 1: cases (exec_lvalue ge en m e1) 1750 [ 2: #error #_ @SimFail /2 by ex_intro/1752 [ 2: #error #_ @SimFailNicely 1751 1753 | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H @SimOk #a #H @H ] ] 1752 | 2: @SimFail /2 by ex_intro/1754 | 2: @SimFailNicely 1753 1755 | 3: // ] 1754 1756 | 52: (* Unop *) destruct … … 1759 1761 whd in match (exec_expr ??? (Expr ??)); 1760 1762 cases Hsim_expr 1761 [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/1763 [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely 1762 1764 | 1: cases (exec_expr ge en m e1) 1763 [ 2: #error #_ @SimFail /2 by ex_intro/1765 [ 2: #error #_ @SimFailNicely 1764 1766 | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H @SimOk 1765 1767 >Htype_eq #a #H @H ] ] 1766 | 2: @SimFail /2 by ex_intro/1768 | 2: @SimFailNicely 1767 1769 | 3: // ] 1768 1770 | 53: (* Binop *) destruct … … 1774 1776 whd in match (exec_expr ??? (Expr ??)); 1775 1777 cases Hsim_expr_lhs 1776 [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/1778 [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely 1777 1779 | 1: cases (exec_expr ge en m lhs) 1778 [ 2: #error #_ @SimFail /2 by ex_intro/1780 [ 2: #error #_ @SimFailNicely 1779 1781 | 1: #lhs_value #Hsim_lhs cases Hsim_expr_rhs 1780 [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/1782 [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely 1781 1783 | 1: cases (exec_expr ge en m rhs) 1782 [ 2: #error #_ @SimFail /2 by ex_intro/1784 [ 2: #error #_ @SimFailNicely 1783 1785 | 1: #rhs_value #Hsim_rhs 1784 1786 lapply (Hsim_lhs lhs_value (refl ? (OK ? lhs_value))) … … 1790 1792 ] 1791 1793 ] 1792 | 2: @SimFail /2 by ex_intro/1794 | 2: @SimFailNicely 1793 1795 | 3: // 1794 1796 ] … … 1805 1807 [ 1: whd in match (exec_expr ??? (Expr ??)); 1806 1808 cases (exec_expr ge en m castee) in Hsmaller; 1807 [ 2: #error #_ @SimFail /2 by ex_intro/1809 [ 2: #error #_ @SimFailNicely 1808 1810 | 1: * #val #trace normalize nodelta >Hsrc_type_eq 1809 1811 lapply (exec_cast_inv val src_sz src_sg cast_sz cast_sg m) 1810 1812 cases (exec_cast m val ??) 1811 [ 2: #error #_ #_ @SimFail /2 by ex_intro/1813 [ 2: #error #_ #_ @SimFailNicely 1812 1814 | 1: #result #Hinversion elim (Hinversion result (refl ??)) 1813 1815 #val_int * #Hval_eq #Hcast … … 1819 1821 ] 1820 1822 ] 1821 | 2: @SimFail /2 by ex_intro/1823 | 2: @SimFailNicely 1822 1824 | 3: >Htarget_type_eq // 1823 1825 ] … … 1833 1835 whd in match (exec_expr ??? (Expr ??)); 1834 1836 cases Hsim_expr 1835 [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/1837 [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely 1836 1838 | 1: cases (exec_expr ??? castee) 1837 [ 2: #error #_ @SimFail /2 by ex_intro/1839 [ 2: #error #_ @SimFailNicely 1838 1840 | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hexec_ok >Hexec_ok 1839 1841 @SimOk >Htype_eq #a #H @H ] 1840 1842 ] 1841 | 2: @SimFail /2 by ex_intro/1843 | 2: @SimFailNicely 1842 1844 | 3: // 1843 1845 ] … … 1854 1856 whd in match (exec_expr ??? (Expr ??)); 1855 1857 cases Hsim_exec_cond 1856 [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/1858 [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely 1857 1859 | 1: cases (exec_expr ??? cond) 1858 [ 2: #error #_ @SimFail /2 by ex_intro/1860 [ 2: #error #_ @SimFailNicely 1859 1861 | 1: * #condb #condtrace #Hcond_sim lapply (Hcond_sim 〈condb, condtrace〉 (refl ? (OK ? 〈condb, condtrace〉))) 1860 1862 #Hcond_ok >Hcond_ok >Htype_eq_cond 1861 1863 normalize nodelta 1862 1864 cases (exec_bool_of_val condb (typeof cond1)) 1863 [ 2: #error @SimFail /2 by ex_intro/1865 [ 2: #error @SimFailNicely 1864 1866 | 1: * whd in match (m_bind ?????); whd in match (m_bind ?????); 1865 1867 normalize nodelta 1866 1868 [ 1: (* true branch taken *) 1867 1869 cases Hsim_exec_true 1868 [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/1870 [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely 1869 1871 | 1: cases (exec_expr ??? iftrue) 1870 [ 2: #error #_ @SimFail /2 by ex_intro/1872 [ 2: #error #_ @SimFailNicely 1871 1873 | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H 1872 1874 @SimOk #a #H @H … … 1875 1877 | 2: (* false branch taken *) 1876 1878 cases Hsim_exec_false 1877 [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/1879 [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely 1878 1880 | 1: cases (exec_expr ??? iffalse) 1879 [ 2: #error #_ @SimFail /2 by ex_intro/1881 [ 2: #error #_ @SimFailNicely 1880 1882 | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H 1881 1883 @SimOk #a #H @H … … 1886 1888 ] 1887 1889 ] 1888 | 2: @SimFail /2 by ex_intro/1890 | 2: @SimFailNicely 1889 1891 | 3: // 1890 1892 ] … … 1896 1898 whd in match (exec_expr ??? (Expr ??)); 1897 1899 [ 1,4: cases Hsim_exec_lhs 1898 [ 2,4: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/1900 [ 2,4: * #error #Hexec_fail >Hexec_fail @SimFailNicely 1899 1901 | 1,3: cases (exec_expr ??? lhs) 1900 [ 2,4: #error #_ @SimFail /2 by ex_intro/1902 [ 2,4: #error #_ @SimFailNicely 1901 1903 | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hlhs >Hlhs >Htype_eq_lhs 1902 1904 normalize nodelta elim a #lhs_val #lhs_trace 1903 1905 cases (exec_bool_of_val lhs_val (typeof lhs1)) 1904 [ 2,4: #error @SimFail /2 by ex_intro/1906 [ 2,4: #error @SimFailNicely 1905 1907 | 1,3: * whd in match (m_bind ?????); whd in match (m_bind ?????); 1906 1908 [ 2,3: @SimOk // 1907 1909 | 1,4: cases Hsim_exec_rhs 1908 [ 2,4: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/1910 [ 2,4: * #error #Hexec_fail >Hexec_fail @SimFailNicely 1909 1911 | 1,3: cases (exec_expr ??? rhs) 1910 [ 2,4: #error #_ @SimFail /2 by ex_intro/1912 [ 2,4: #error #_ @SimFailNicely 1911 1913 | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrhs >Hrhs >Htype_eq_rhs 1912 1914 @SimOk #a #H @H … … 1917 1919 ] 1918 1920 ] 1919 | 2,5: @SimFail /2 by ex_intro/1921 | 2,5: @SimFailNicely 1920 1922 | 3,6: // 1921 1923 ] … … 1930 1932 [ 2: #sz #sg | 3: #fl | 4: #ty' | 5: #ty #n | 6: #tl #ty' 1931 1933 | 7: #id #fl | 8: #id #fl | 9: #id ] 1932 try (@SimFail /2 by ex_intro/)1934 try (@SimFailNicely) 1933 1935 cases Hsim_lvalue 1934 [ 2,4: * #error #Hlvalue_fail >Hlvalue_fail @SimFail /2 by ex_intro/1936 [ 2,4: * #error #Hlvalue_fail >Hlvalue_fail @SimFailNicely 1935 1937 | 1,3: cases (exec_lvalue ge en m rec_expr) 1936 [ 2,4: #error #_ @SimFail /2 by ex_intro/1938 [ 2,4: #error #_ @SimFailNicely 1937 1939 | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hexec >Hexec 1938 1940 @SimOk #a #H @H ] … … 1942 1944 [ 2: #sz #sg | 3: #fl | 4: #ty' | 5: #ty #n | 6: #tl #ty' 1943 1945 | 7: #id #fl | 8: #id #fl | 9: #id ] 1944 try (@SimFail /2 by ex_intro/)1946 try (@SimFailNicely) 1945 1947 cases Hsim_lvalue 1946 [ 2,4: * #error #Hlvalue_fail >Hlvalue_fail @SimFail /2 by ex_intro/1948 [ 2,4: * #error #Hlvalue_fail >Hlvalue_fail @SimFailNicely 1947 1949 | 1,3: cases (exec_lvalue ge en m rec_expr) 1948 [ 2,4: #error #_ @SimFail /2 by ex_intro/1950 [ 2,4: #error #_ @SimFailNicely 1949 1951 | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hexec >Hexec 1950 1952 @SimOk #a #H @H ] … … 1958 1960 [ 1: 1959 1961 cases Hsim_expr 1960 [ 2: * #error #Hexec >Hexec @SimFail /2 by ex_intro/1962 [ 2: * #error #Hexec >Hexec @SimFailNicely 1961 1963 | 1: cases (exec_expr ??? e1) 1962 [ 2: #error #_ @SimFail /2 by ex_intro/1964 [ 2: #error #_ @SimFailNicely 1963 1965 | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H 1964 1966 @SimOk #a #H @H ] … … 2176 2178 | 11,12: #ty #e1 #e2 #Hsim1 #Hsim2 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); 2177 2179 cases Hsim1 2178 [ 2,4: * #error #Hfail >Hfail @SimFail /2 by ex_intro/2180 [ 2,4: * #error #Hfail >Hfail @SimFailNicely 2179 2181 | 1,3: cases (exec_expr ge en m e1) 2180 [ 2,4: #error #_ @SimFail /2 by ex_intro/2182 [ 2,4: #error #_ @SimFailNicely 2181 2183 | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite normalize nodelta 2182 2184 cases (exec_bool_of_val ??) 2183 [ 2,4: #erro @SimFail /2 by ex_intro/2185 [ 2,4: #erro @SimFailNicely 2184 2186 | 1,3: * whd in match (m_bind ?????); whd in match (m_bind ?????); 2185 2187 [ 2,3: @SimOk // … … 2229 2231 #ty normalize in match (is_not_lvalue ?); 2230 2232 [ 3,4,13: #Habsurd @(False_ind … Habsurd) ] #_ 2231 @SimFail /2 by ex_intro/2233 @SimFailNicely 2232 2234 ] qed. 2233 2235 … … 2243 2245 * * try // 2244 2246 cases (exec_expr ge en m (Expr ??)) 2245 try (#error #_ #_ #_ @SimFail /2 by ex_intro/)2247 try (#error #_ #_ #_ @SimFailNicely) 2246 2248 * #val #trace #Hsim_expr #Hsim_lvalue #Htype_eq 2247 2249 try @(simulation_transitive ???? Hsim_expr (proj1 ?? (sim_related_globals ge ge' en m Hrelated) ?)) … … 2259 2261 * * try // 2260 2262 cases (exec_lvalue ge en m (Expr ??)) 2261 try (#error #_ #_ #_ @SimFail /2 by ex_intro/)2263 try (#error #_ #_ #_ @SimFailNicely) 2262 2264 * #val #trace #Hsim_expr #Hsim_lvalue #Htype_eq 2263 2265 (* Having to distinguish between exec_lvalue' and exec_lvalue is /ugly/. *)
Note: See TracChangeset
for help on using the changeset viewer.