 Timestamp:
 Apr 19, 2012, 6:09:01 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASMCosts.ma
r1891 r1892 1585 1585 nat_of_bitvector (S n) (hd:::tl) = (2 ^ n) * nat_of_bool hd + nat_of_bitvector n tl. 1586 1586 1587 axiom plus_refl_to_refl_lor_refl:1588 ∀m, m', n, n': nat.1589 m + m' = n + n' → (m = n ∧ m' = n') ∨ (m = n' ∧ m' = n).1590 1591 1587 axiom mult_refl_to_refl_lor_refl: 1592 1588 ∀m, m', n, n': nat. 1593 1589 m * m' = n * n' → (m = n ∧ m' = n') ∨ (m = n' ∧ n = m'). 1594 1590 1595 axiom Vector_inv_ind_2: 1596 ∀a: Type[0]. 1591 (* 1592 lemma BitVector_inv_ind_2: 1597 1593 ∀n: nat. 1598 ∀left: Vector an.1599 ∀right: Vector an.1600 ∀P: (∀m: nat. Vector a m → Vector am → Prop).1601 (n ≃ 0 → (left ≃ VEmpty a) → (right ≃ VEmpty a)→ (P 0 [[ ]] [[ ]])) →1594 ∀left: Vector bool n. 1595 ∀right: Vector bool n. 1596 ∀P: (∀m: nat. Vector bool m → Vector bool m → Prop). 1597 (n ≃ O → left ≃ VEmpty bool → right ≃ VEmpty bool → (P 0 [[ ]] [[ ]])) → 1602 1598 (∀m: nat. 1603 ∀hd, hd': a.1604 ∀tl, tl': Vector am.1599 ∀hd, hd': bool. 1600 ∀tl, tl': Vector bool m. 1605 1601 (n ≃ m → left ≃ tl → right ≃ tl' → P m tl tl') → 1606 1602 (n ≃ S m → left ≃ hd:::tl → right ≃ hd':::tl' → P (S m) (hd:::tl) (hd':::tl'))) → 1607 1603 P n left right. 1604 #n #left 1605 elim left 1606 [1: 1607 #right #P #base #step 1608 >(BitVector_O right) 1609 @base 1610 try % 1611 >(BitVector_O right) % 1612 2: 1613 #n' #hd #tl #inductive_hypothesis #right #P #base #step 1614 cases (BitVector_Sn … right) 1615 #hd' #right_tail_exists_assm 1616 cases right_tail_exists_assm #right_tl #right_tl_refl 1617 destruct @step try % 1618 #n_refl' #left_refl #right_refl destruct 1619 @inductive_hypothesis 1620 *) 1621 1622 include "arithmetics/div_and_mod.ma". 1623 1624 lemma n_plus_1_n_to_False: 1625 ∀n: nat. 1626 n + 1 = n → False. 1627 #n elim n 1628 [1: 1629 normalize #absurd destruct(absurd) 1630 2: 1631 #n' #inductive_hypothesis normalize 1632 #absurd @inductive_hypothesis /2/ 1633 ] 1634 qed. 1635 1636 lemma one_two_times_n_to_False: 1637 ∀n: nat. 1638 1=2*n→False. 1639 #n cases n 1640 [1: 1641 normalize #absurd destruct(absurd) 1642 2: 1643 #n' normalize #absurd 1644 lapply (injective_S … absurd) absurd #absurd 1645 /2/ 1646 ] 1647 qed. 1648 1649 lemma generalized_nat_cases: 1650 ∀n: nat. 1651 n = 0 ∨ n = 1 ∨ ∃m: nat. n = S (S m). 1652 #n 1653 cases n 1654 [1: 1655 @or_introl @or_introl % 1656 2: 1657 #n' cases n' 1658 [1: 1659 @or_introl @or_intror % 1660 2: 1661 #n'' @or_intror %{n''} % 1662 ] 1663 ] 1664 qed. 1665 1666 lemma blah: 1667 ∀m, n: nat. 1668 2 * m + 1 = 2 * n → False. 1669 #m #n 1670 elim m elim n 1671 normalize 1672 [1: 1673 #absurd destruct(absurd) 1674 2,3: 1675 #m' #inductive_hypothesis <plus_n_Sm <plus_n_O 1676 #absurd destruct(absurd) 1677 4: 1678 #m' #inductive_hypothesis #n' 1679 <plus_n_Sm <plus_n_Sm <plus_n_Sm 1680 #absurd destruct(absurd) 1681 qed. 1682 1683 (* 1684 lemma two_times_m_plus_one_refl_2_times_n_to_m_refl_0_land_n_refl_1: 1685 ∀m, n: nat. 1686 2 * m + 1 = 2 * n → m = 0 ∧ n = 1. 1687 (* 1688 #m #n 1689 lapply (generalized_nat_cases m) 1690 lapply (generalized_nat_cases n) 1691 #n_assms #m_assms 1692 cases n_assms 1693 [1: 1694 #left_n_assms 1695 cases left_n_assms #n_O_refl destruct 1696 normalize cases m normalize 1697 [1,3: 1698 #absurd destruct(absurd) 1699 2,4: 1700 #m' normalize 1701 <plus_n_Sm <plus_n_Sm #absurd 1702 destruct(absurd) 1703 ] 1704 2: 1705 #right_n_assms 1706 cases m_assms 1707 [1: 1708 #left_m_assms 1709 cases left_m_assms 1710 [1: 1711 #m_0_refl destruct normalize 1712 cases n 1713 [1: 1714 normalize 1715 #absurd destruct(absurd) 1716 2: 1717 #n' normalize 1718 <plus_n_Sm #absurd 1719 destruct(absurd) 1720 ] 1721 2: 1722 #m_1_refl destruct normalize 1723 cases n 1724 [1: 1725 normalize #absurd destruct(absurd) 1726 2: 1727 #n' <plus_n_Sm #assm 1728 lapply (injective_S … assm) 1729 assm #assm lapply (injective_S … assm) 1730 cases n' 1731 [1: 1732 normalize #absurd destruct(absurd) 1733 2: 1734 #n'' normalize <plus_n_Sm #absurd destruct(absurd) 1735 ] 1736 ] 1737 ] 1738 2: 1739 #right_m_assms cases right_n_assms cases right_m_assms 1740 #n' #n_assm #m' #m_assm destruct normalize 1741 <plus_n_Sm <plus_n_Sm <plus_n_Sm <plus_n_O <plus_n_O <plus_n_O <plus_n_Sm 1742 <plus_n_Sm #assm destruct(assm) 1743 ] 1744 ] 1745 1746 #relevant_m 1747 cases relevant_m 1748 relevant_m 1749 [1: 1750 lapply(generalized_nat_cases n) 1751 #relevant_n 1752 cases relevant_n 1753 relevant_n 1754 [1: 1755 #relevant_n cases relevant_n 1756 #n_assm #relevant_m cases relevant_m 1757 #m_assm destruct normalize 1758 #absurd destruct(absurd) 1759 2: 1760 #relevant_m cases relevant_m 1761 *) 1762 cases daemon 1763 qed. 1764 *) 1765 1766 lemma nat_of_bitvector_aux_injective: 1767 ∀n: nat. 1768 ∀l, r: BitVector n. 1769 ∀acc_l, acc_r: nat. 1770 nat_of_bitvector_aux n acc_l l = nat_of_bitvector_aux n acc_r r → 1771 acc_l = acc_r ∧ l ≃ r. 1772 #n #l 1773 elim l #r 1774 [1: 1775 #acc_l #acc_r normalize 1776 >(BitVector_O r) normalize /2/ 1777 2: 1778 #hd #tl #inductive_hypothesis #r #acc_l #acc_r 1779 normalize normalize in inductive_hypothesis; 1780 cases (BitVector_Sn … r) 1781 #r_hd * #r_tl #r_refl destruct normalize 1782 cases hd cases r_hd normalize 1783 [1: 1784 #relevant 1785 cases (inductive_hypothesis … relevant) 1786 #acc_assm #tl_assm destruct % // 1787 lapply (injective_plus_l ? ? ? acc_assm) 1788 acc_assm #acc_assm 1789 change with (2 * acc_l = 2 * acc_r) in acc_assm; 1790 lapply (injective_times_r ? ? ? ? acc_assm) /2/ 1791 4: 1792 #relevant 1793 cases (inductive_hypothesis … relevant) 1794 #acc_assm #tl_assm destruct % // 1795 change with (2 * acc_l = 2 * acc_r) in acc_assm; 1796 lapply(injective_times_r ? ? ? ? acc_assm) /2/ 1797 2: 1798 #relevant 1799 change with ((nat_of_bitvector_aux r (2 * acc_l + 1) tl) = 1800 (nat_of_bitvector_aux r (2 * acc_r) r_tl)) in relevant; 1801 cases (eqb_decidable … (2 * acc_l + 1) (2 * acc_r)) 1802 [1: 1803 #eqb_true_assm 1804 lapply (eqb_true_to_refl … eqb_true_assm) 1805 #refl_assm 1806 cases (blah … refl_assm) 1807 2: 1808 #eqb_false_assm 1809 lapply (eqb_false_to_not_refl … eqb_false_assm) 1810 #not_refl_assm cases not_refl_assm #absurd_assm 1811 cases (inductive_hypothesis … relevant) #absurd 1812 cases (absurd_assm absurd) 1813 ] 1814 3: 1815 #relevant 1816 change with ((nat_of_bitvector_aux r (2 * acc_l) tl) = 1817 (nat_of_bitvector_aux r (2 * acc_r + 1) r_tl)) in relevant; 1818 cases (eqb_decidable … (2 * acc_l) (2 * acc_r + 1)) 1819 [1: 1820 #eqb_true_assm 1821 lapply (eqb_true_to_refl … eqb_true_assm) 1822 #refl_assm 1823 lapply (sym_eq ? (2 * acc_l) (2 * acc_r + 1) refl_assm) 1824 refl_assm #refl_assm 1825 cases (blah … refl_assm) 1826 2: 1827 #eqb_false_assm 1828 lapply (eqb_false_to_not_refl … eqb_false_assm) 1829 #not_refl_assm cases not_refl_assm #absurd_assm 1830 cases (inductive_hypothesis … relevant) #absurd 1831 cases (absurd_assm absurd) 1832 ] 1833 ] 1834 ] 1835 qed. 1608 1836 1609 1837 lemma nat_of_bitvector_destruct: … … 1614 1842 l_hd = r_hd ∧ nat_of_bitvector n l_tl = nat_of_bitvector n r_tl. 1615 1843 #n #l_hd #r_hd #l_tl #r_tl 1616 @(Vector_inv_ind_2 bool n l_tl r_tl) 1617 [1: 1618 #length_refl #l_tl_refl #r_tl_refl 1619 destruct 1620 cases l_hd cases r_hd 1621 normalize 1622 try (#absurd destruct(absurd)) 1623 @conj % 1624 2: 1625 #m #l_hd' #r_hd' #l_tl' #r_tl' #inductive_hypothesis 1626 #n_refl #l_tl_refl #r_tl_refl 1627 destruct 1628 1629 elim l_tl 1630 [1: 1631 #r_tl 1632 >(BitVector_O r_tl) 1633 normalize 1634 cases l_hd cases r_hd 1635 normalize 1636 try (#absurd destruct(absurd)) 1637 @conj % 1638 2: 1639 #n' #hd #tl #inductive_hypothesis #r_tl 1640 cases (BitVector_Sn … r_tl) #hd' #tl_hypothesis' 1641 cases tl_hypothesis' #tl' #tl_refl' 1642 >tl_refl' 1643 cases daemon 1644 ] 1645 qed. 1646 1647 axiom Vector_inv_ind_2: 1648 ∀a: Type[0]. 1649 ∀n: nat. 1650 ∀left: Vector a n. 1651 ∀right: Vector a n. 1652 ∀P: (∀m: nat. Vector a m → Vector a m → Prop). 1653 (n ≃ 0 → (left ≃ VEmpty a) → (right ≃ VEmpty a) → (P 0 [[ ]] [[ ]])) → 1654 (∀m: nat. 1655 ∀hd, hd': a. 1656 ∀tl, tl': Vector a m. 1657 (n ≃ m → left ≃ tl → right ≃ tl' → P m tl tl') → 1658 (n ≃ S m → left ≃ hd:::tl → right ≃ hd':::tl' → P (S m) (hd:::tl) (hd':::tl'))) → 1659 P n left right. 1844 normalize 1845 cases l_hd cases r_hd 1846 normalize 1847 [4: 1848 /2/ 1849 1: 1850 #relevant 1851 cases (nat_of_bitvector_aux_injective … relevant) 1852 #_ #l_r_tl_refl destruct /2/ 1853 2,3: 1854 #relevant 1855 cases (nat_of_bitvector_aux_injective … relevant) 1856 #absurd destruct(absurd) 1857 ] 1858 qed. 1660 1859 1661 1860 lemma BitVector_cons_injective:
Note: See TracChangeset
for help on using the changeset viewer.