 Timestamp:
 Apr 20, 2012, 12:52:31 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASMCosts.ma
r1892 r1894 1664 1664 qed. 1665 1665 1666 lemma blah: 1666 let rec odd_p 1667 (n: nat) 1668 on n ≝ 1669 match n with 1670 [ O ⇒ False 1671  S n' ⇒ even_p n' 1672 ] 1673 and even_p 1674 (n: nat) 1675 on n ≝ 1676 match n with 1677 [ O ⇒ True 1678  S n' ⇒ odd_p n' 1679 ]. 1680 1681 let rec n_even_p_to_n_plus_2_even_p 1682 (n: nat) 1683 on n: even_p n → even_p (n + 2) ≝ 1684 match n with 1685 [ O ⇒ ? 1686  S n' ⇒ ? 1687 ] 1688 and n_odd_p_to_n_plus_2_odd_p 1689 (n: nat) 1690 on n: odd_p n → odd_p (n + 2) ≝ 1691 match n with 1692 [ O ⇒ ? 1693  S n' ⇒ ? 1694 ]. 1695 [1,3: 1696 normalize #assm assumption 1697 2: 1698 normalize @n_odd_p_to_n_plus_2_odd_p 1699 4: 1700 normalize @n_even_p_to_n_plus_2_even_p 1701 ] 1702 qed. 1703 1704 let rec two_times_n_even_p 1705 (n: nat) 1706 on n: even_p (2 * n) ≝ 1707 match n with 1708 [ O ⇒ ? 1709  S n' ⇒ ? 1710 ] 1711 and two_times_n_plus_one_odd_p 1712 (n: nat) 1713 on n: odd_p ((2 * n) + 1) ≝ 1714 match n with 1715 [ O ⇒ ? 1716  S n' ⇒ ? 1717 ]. 1718 [1,3: 1719 normalize @I 1720 2: 1721 normalize 1722 >plus_n_Sm 1723 <(associative_plus n' n' 1) 1724 >(plus_n_O (n' + n')) 1725 cut(n' + n' + 0 + 1 = 2 * n' + 1) 1726 [1: 1727 // 1728 2: 1729 #refl_assm >refl_assm 1730 @two_times_n_plus_one_odd_p 1731 ] 1732 4: 1733 normalize 1734 >plus_n_Sm 1735 cut(n' + (n' + 1) + 1 = (2 * n') + 2) 1736 [1: 1737 normalize /2/ 1738 2: 1739 #refl_assm >refl_assm 1740 @n_even_p_to_n_plus_2_even_p 1741 @two_times_n_even_p 1742 ] 1743 ] 1744 qed. 1745 1746 let rec even_p_to_not_odd_p 1747 (n: nat) 1748 on n: even_p n → ¬ odd_p n ≝ 1749 match n with 1750 [ O ⇒ ? 1751  S n' ⇒ ? 1752 ] 1753 and odd_p_to_not_even_p 1754 (n: nat) 1755 on n: odd_p n → ¬ even_p n ≝ 1756 match n with 1757 [ O ⇒ ? 1758  S n' ⇒ ? 1759 ]. 1760 [1: 1761 normalize #_ 1762 @nmk #assm assumption 1763 3: 1764 normalize #absurd 1765 cases absurd 1766 2: 1767 normalize 1768 @odd_p_to_not_even_p 1769 4: 1770 normalize 1771 @even_p_to_not_odd_p 1772 ] 1773 qed. 1774 1775 lemma even_p_odd_p_cases: 1776 ∀n: nat. 1777 even_p n ∨ odd_p n. 1778 #n elim n 1779 [1: 1780 normalize @or_introl @I 1781 2: 1782 #n' #inductive_hypothesis 1783 normalize 1784 cases inductive_hypothesis 1785 #assm 1786 try (@or_introl assumption) 1787 try (@or_intror assumption) 1788 ] 1789 qed. 1790 1791 lemma two_times_n_plus_one_refl_two_times_n_to_False: 1667 1792 ∀m, n: nat. 1668 1793 2 * m + 1 = 2 * n → False. 1669 1794 #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) 1795 #assm 1796 cut (even_p (2 * n) ∧ even_p ((2 * m) + 1)) 1797 [1: 1798 >assm 1799 @conj 1800 @two_times_n_even_p 1801 2: 1802 * #_ #absurd 1803 cases (even_p_to_not_odd_p … absurd) 1804 #assm @assm 1805 @two_times_n_plus_one_odd_p 1806 ] 1681 1807 qed. 1682 1808 … … 1804 1930 lapply (eqb_true_to_refl … eqb_true_assm) 1805 1931 #refl_assm 1806 cases ( blah… refl_assm)1932 cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm) 1807 1933 2: 1808 1934 #eqb_false_assm … … 1823 1949 lapply (sym_eq ? (2 * acc_l) (2 * acc_r + 1) refl_assm) 1824 1950 refl_assm #refl_assm 1825 cases ( blah… refl_assm)1951 cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm) 1826 1952 2: 1827 1953 #eqb_false_assm
Note: See TracChangeset
for help on using the changeset viewer.