Changeset 1894


Ignore:
Timestamp:
Apr 20, 2012, 12:52:31 PM (7 years ago)
Author:
mulligan
Message:

Closed a hole in the proof by deriving a contradiction using even_p and odd_p

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1892 r1894  
    16641664qed.
    16651665
    1666 lemma blah:
     1666let rec odd_p
     1667  (n: nat)
     1668    on n ≝
     1669  match n with
     1670  [ O ⇒ False
     1671  | S n' ⇒ even_p n'
     1672  ]
     1673and even_p
     1674  (n: nat)
     1675    on n ≝
     1676  match n with
     1677  [ O ⇒ True
     1678  | S n' ⇒ odd_p n'
     1679  ].
     1680
     1681let 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  ]
     1688and 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  ]
     1702qed.
     1703
     1704let 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  ]
     1711and 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  ]
     1744qed.
     1745
     1746let 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  ]
     1753and 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  ]
     1773qed.
     1774
     1775lemma 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  ]
     1789qed.
     1790
     1791lemma two_times_n_plus_one_refl_two_times_n_to_False:
    16671792  ∀m, n: nat.
    16681793    2 * m + 1 = 2 * n → False.
    16691794  #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  ]
    16811807qed.
    16821808
     
    18041930        lapply (eqb_true_to_refl … eqb_true_assm)
    18051931        #refl_assm
    1806         cases (blah … refl_assm)
     1932        cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm)
    18071933      |2:
    18081934        #eqb_false_assm
     
    18231949        lapply (sym_eq ? (2 * acc_l) (2 * acc_r + 1) refl_assm)
    18241950        -refl_assm #refl_assm
    1825         cases (blah … refl_assm)
     1951        cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm)
    18261952      |2:
    18271953        #eqb_false_assm
Note: See TracChangeset for help on using the changeset viewer.