Changeset 1892


Ignore:
Timestamp:
Apr 19, 2012, 6:09:01 PM (7 years ago)
Author:
mulligan
Message:

Lots of work from today

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1891 r1892  
    15851585    nat_of_bitvector (S n) (hd:::tl) = (2 ^ n) * nat_of_bool hd + nat_of_bitvector n tl.
    15861586
    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 
    15911587axiom mult_refl_to_refl_lor_refl:
    15921588  ∀m, m', n, n': nat.
    15931589    m * m' = n * n' → (m = n ∧ m' = n') ∨ (m = n' ∧ n = m').
    15941590
    1595 axiom Vector_inv_ind_2:
    1596   ∀a: Type[0].
     1591(*
     1592lemma BitVector_inv_ind_2:
    15971593  ∀n: nat.
    1598   ∀left: Vector a n.
    1599   ∀right: Vector a n.
    1600   ∀P: (∀m: nat. Vector a m → Vector a m → 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 [[ ]] [[ ]])) →
    16021598    (∀m: nat.
    1603      ∀hd, hd': a.
    1604      ∀tl, tl': Vector a m.
     1599     ∀hd, hd': bool.
     1600     ∀tl, tl': Vector bool m.
    16051601       (n ≃ m → left ≃ tl → right ≃ tl' → P m tl tl') →
    16061602       (n ≃ S m → left ≃ hd:::tl → right ≃ hd':::tl' → P (S m) (hd:::tl) (hd':::tl'))) →
    16071603    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
     1622include "arithmetics/div_and_mod.ma".
     1623
     1624lemma 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  ]
     1634qed.
     1635
     1636lemma 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  ]
     1647qed.
     1648
     1649lemma 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  ]
     1664qed.
     1665
     1666lemma 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)
     1681qed.
     1682
     1683(*
     1684lemma 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
     1763qed.
     1764*)
     1765
     1766lemma 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  ]
     1835qed.
    16081836
    16091837lemma nat_of_bitvector_destruct:
     
    16141842      l_hd = r_hd ∧ nat_of_bitvector n l_tl = nat_of_bitvector n r_tl.
    16151843  #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  ]
     1858qed.
    16601859
    16611860lemma BitVector_cons_injective:
Note: See TracChangeset for help on using the changeset viewer.