Skip to content

Commit 82d19dc

Browse files
naminnamin
committed
full paper_list example, at the end, pretty sluggish
1 parent 89a4053 commit 82d19dc

File tree

1 file changed

+191
-0
lines changed

1 file changed

+191
-0
lines changed

‎dev2015/dot21.v

+191
Original file line numberDiff line numberDiff line change
@@ -1630,6 +1630,197 @@ Proof.
16301630

16311631
Qed.
16321632

1633+
Example paper_list:
1634+
has_type
1635+
[]
1636+
(tobj 0
1637+
[(2, dfun 1 (tlet 2 (tobj 2 [(2, dfun 3 (tapp (tvar 2) 2 (tvar 3)));
1638+
(1, dfun 3 (tapp (tvar 2) 1 (tvar 3)));
1639+
(0, dmem TBot)])
1640+
(tvar 2)));
1641+
(1, dfun 1(*type T*) (tlet 2 (tobj 2
1642+
[(0, dfun 3(*hd*) (tlet 4 (tobj 4 [(0, dfun 5(*tl*) (tlet 6 (tobj 6
1643+
[(2, dfun 7 (tvar 5)); (1, dfun 7 (tvar 3));
1644+
(0, dmem (TSel (varF 1) 0))]) (tvar 6)))]) (tvar 4)))]) (tvar 2)));
1645+
(0, dmem (TBind (TAnd
1646+
(TAll 2 TTop (TAnd (TSel (varB 2) 0) (TBind (TMem 0 TBot (TSel (varB 2) 0)))))
1647+
(TAnd
1648+
(TAll 1 TTop (TSel (varB 1) 0))
1649+
(TMem 0 TBot TTop)))))
1650+
])
1651+
(TBind (TAnd
1652+
(TAll 2 TTop (TAnd (TSel (varB 1) 0) (TBind (TMem 0 TBot TBot))))
1653+
(TAnd
1654+
(TAll 1 (TMem 0 TBot TTop)
1655+
(TAll 0 (TSel (varB 0) 0)
1656+
(TAll 0 (TAnd (TSel (varB 2) 0) (TBind (TMem 0 TBot (TSel (varB 2) 0))))
1657+
(TAnd (TSel (varB 3) 0) (TBind (TMem 0 TBot (TSel (varB 3) 0)))))))
1658+
(TMem 0
1659+
TBot
1660+
(TBind (TAnd
1661+
(TAll 2 TTop (TAnd (TSel (varB 2) 0) (TBind (TMem 0 TBot (TSel (varB 2) 0)))))
1662+
(TAnd
1663+
(TAll 1 TTop (TSel (varB 1) 0))
1664+
(TMem 0 TBot TTop)))))))).
1665+
Proof.
1666+
apply t_sub with (T1:=
1667+
(TBind (TAnd
1668+
(TAll 2 TTop (TAnd (TSel (varB 1) 0) (TBind (TMem 0 TBot TBot))))
1669+
(TAnd
1670+
(TAll 1 (TMem 0 TBot TTop)
1671+
(TAll 0 (TSel (varB 0) 0)
1672+
(TAll 0 (TAnd (TSel (varB 2) 0) (TBind (TMem 0 TBot (TSel (varB 2) 0))))
1673+
(TAnd (TSel (varB 3) 0) (TBind (TMem 0 TBot (TSel (varB 3) 0)))))))
1674+
(TMem 0
1675+
(TBind (TAnd
1676+
(TAll 2 TTop (TAnd (TSel (varB 2) 0) (TBind (TMem 0 TBot (TSel (varB 2) 0)))))
1677+
(TAnd
1678+
(TAll 1 TTop (TSel (varB 1) 0))
1679+
(TMem 0 TBot TTop))))
1680+
(TBind (TAnd
1681+
(TAll 2 TTop (TAnd (TSel (varB 2) 0) (TBind (TMem 0 TBot (TSel (varB 2) 0)))))
1682+
(TAnd
1683+
(TAll 1 TTop (TSel (varB 1) 0))
1684+
(TMem 0 TBot TTop))))))))).
1685+
eapply t_obj.
1686+
eauto. compute. reflexivity.
1687+
1688+
eapply dt_fun with (T1:=TTop) (T2:=(TAnd (TSel (varB 1) 0) (TBind (TMem 0 TBot TBot)))).
1689+
apply t_let with (Tx:=(TBind (TAnd (TAll 2 TTop TBot) (TAnd (TAll 1 TTop TBot) (TMem 0 TBot TBot))))).
1690+
eapply t_obj.
1691+
eauto. compute. reflexivity.
1692+
eapply dt_fun with (T1:=TTop) (T2:=TBot).
1693+
simpl. unfold open at 3. simpl. eapply t_app.
1694+
eapply t_sub. eapply t_var. compute. reflexivity. crush_wf.
1695+
apply stp_and11. crush_wf. crush_wf. crush2. crush2.
1696+
eapply dt_fun with (T1:=TTop) (T2:=TBot).
1697+
simpl. unfold open at 3. simpl. eapply t_app.
1698+
eapply t_sub. eapply t_var. compute. reflexivity. crush_wf.
1699+
apply stp_and12. apply stp_and11. crush_wf. crush_wf. crush2. crush2. crush2.
1700+
eapply dt_mem. eapply dt_nil. eauto. simpl. reflexivity. eauto. eauto.
1701+
simpl. reflexivity. eauto. eauto. simpl. reflexivity.
1702+
crush_wf. crush_wf. eauto.
1703+
simpl. unfold open at 2. simpl.
1704+
eapply t_sub. eapply t_var. compute. eauto. crush_wf.
1705+
eapply stp_and2. eapply stp_sel2. compute. reflexivity. crush2.
1706+
eapply stp_and12. eapply stp_and12.
1707+
eapply stp_mem. eapply stp_bindx. eauto. crush_cl. crush_cl.
1708+
unfold open. simpl. crush_wf. unfold open. simpl.
1709+
1710+
apply stp_and2. eapply stp_and11. eapply stp_all. crush_wf. eauto. crush_cl. crush_cl.
1711+
unfold open. simpl. crush_wf. unfold open. simpl. eapply stp_bot. crush_wf. crush_wf.
1712+
eapply stp_and12. eapply stp_and2. eapply stp_and11. eapply stp_all. crush_wf. eauto.
1713+
crush_cl. crush_cl. unfold open. simpl. crush_wf. unfold open. simpl. eapply stp_bot.
1714+
crush_wf. crush_wf. eapply stp_and12. eapply stp_mem. crush_wf. crush2. crush_wf.
1715+
crush_wf. eapply stp_top. crush_wf. crush_wf. crush_wf.
1716+
1717+
crush_wf.
1718+
1719+
eapply stp_bindx. eauto. crush2. crush2. crush_wf.
1720+
unfold open. simpl. eapply stp_and12. eapply stp_and12. crush_wf. crush_wf. crush_wf.
1721+
unfold open. simpl. crush_wf.
1722+
1723+
eapply dt_fun with (T1:=(TMem 0 TBot TTop))
1724+
(T2:=(TAll 0 (TSel (varB 0) 0)
1725+
(TAll 0 (TAnd (TSel (varB 2) 0) (TBind (TMem 0 TBot (TSel (varB 2) 0))))
1726+
(TAnd (TSel (varB 3) 0) (TBind (TMem 0 TBot (TSel (varB 3) 0))))))).
1727+
apply t_let with (Tx:=(TBind
1728+
(TAll 0 (TSel (varF 1) 0)
1729+
(TAll 0 (TAnd (TSel (varF 0) 0) (TBind (TMem 0 TBot (TSel (varF 1) 0))))
1730+
(TAnd (TSel (varF 0) 0) (TBind (TMem 0 TBot (TSel (varF 1) 0)))))))).
1731+
eapply t_obj.
1732+
eauto. compute. reflexivity.
1733+
eapply dt_fun with (T1:=(TSel (varF 1) 0))
1734+
(T2:=(TAll 0 (TAnd (TSel (varF 0) 0) (TBind (TMem 0 TBot (TSel (varF 1) 0))))
1735+
(TAnd (TSel (varF 0) 0) (TBind (TMem 0 TBot (TSel (varF 1) 0)))))).
1736+
apply t_let with (Tx:=(TBind (TAll 0 (TAnd (TSel (varF 0) 0) (TBind (TMem 0 TBot (TSel (varF 1) 0))))
1737+
(TAnd (TSel (varF 0) 0) (TBind (TMem 0 TBot (TSel (varF 1) 0))))))).
1738+
eapply t_obj.
1739+
eauto. compute. reflexivity.
1740+
eapply dt_fun with (T1:=(TAnd (TSel (varF 0) 0) (TBind (TMem 0 TBot (TSel (varF 1) 0)))))
1741+
(T2:=(TAnd (TSel (varF 0) 0) (TBind (TMem 0 TBot (TSel (varF 1) 0))))).
1742+
apply t_let with (Tx:=(TBind (TAnd
1743+
(TAll 2 TTop (TAnd (TSel (varF 0) 0) (TBind (TMem 0 TBot (TSel (varF 1) 0)))))
1744+
(TAnd (TAll 1 TTop (TSel (varF 1) 0)) (TMem 0 (TSel (varF 1) 0) (TSel (varF 1) 0)))))).
1745+
eapply t_obj.
1746+
eauto. compute. reflexivity.
1747+
eapply dt_fun with (T1:=TTop) (T2:=(TAnd (TSel (varF 0) 0) (TBind (TMem 0 TBot (TSel (varF 1) 0))))).
1748+
simpl. unfold open. simpl. crush2.
1749+
eapply dt_fun with (T1:=TTop) (T2:=(TSel (varF 1) 0)).
1750+
simpl. unfold open. simpl. crush2.
1751+
eapply dt_mem. eapply dt_nil. eauto. simpl. reflexivity. eauto. eauto.
1752+
simpl. reflexivity. eauto. eauto. simpl. reflexivity. crush_wf. crush_wf. eauto.
1753+
simpl. unfold open. simpl.
1754+
eapply t_sub.
1755+
eapply t_var. compute. eauto. crush_wf.
1756+
1757+
eapply stp_and2. eapply stp_sel2. compute. reflexivity. crush_cl.
1758+
eapply stp_and12. eapply stp_and12. eapply stp_mem. eapply stp_bindx.
1759+
eauto. crush2. crush2.
1760+
unfold open. simpl. crush_wf.
1761+
unfold open. simpl.
1762+
eapply stp_and2. eapply stp_and11.
1763+
eapply stp_all. crush_wf. eauto. crush2. crush2.
1764+
unfold open. simpl. crush_wf. unfold open. simpl.
1765+
eapply stp_and2. eapply stp_and11. crush_wf. crush_wf. eapply stp_and12.
1766+
eapply stp_bindx. eauto. crush_cl. crush_cl. crush_wf. unfold open. simpl.
1767+
eapply stp_mem. crush_wf. unfold open. simpl.
1768+
eapply stp_sela2. compute. reflexivity. crush_cl.
1769+
eapply stp_and12. eapply stp_and12. crush2. crush_wf. crush_wf. crush_wf. crush_wf.
1770+
crush_wf.
1771+
eapply stp_and12. eapply stp_and2. eapply stp_and11. eapply stp_all. crush_wf. eauto.
1772+
crush_cl. crush_cl. unfold open. simpl. crush_wf. unfold open. simpl.
1773+
eapply stp_sela2. compute. reflexivity. crush_cl.
1774+
eapply stp_and12. eapply stp_and12. crush2. crush_wf. crush_wf. crush_wf. crush_wf.
1775+
eapply stp_and12. crush2. crush_wf. crush_wf. eapply stp_top. crush_wf. crush_wf.
1776+
crush_wf. eapply stp_bindx. eauto. crush_cl. crush_cl. crush_wf. unfold open. simpl.
1777+
crush_wf. eapply stp_bindx. eauto. crush_cl. crush_cl. unfold open. simpl. crush_wf.
1778+
unfold open. simpl.
1779+
eapply stp_and12. eapply stp_and12. crush2. crush_wf. crush_wf. crush_wf.
1780+
1781+
eapply dt_nil. eauto. eauto. simpl. reflexivity. crush_wf. crush_wf.
1782+
eauto.
1783+
unfold open. simpl.
1784+
assert (open (varF 4)
1785+
(TAll 0 (TAnd (TSel (varF 0) 0) (TBind (TMem 0 TBot (TSel (varF 1) 0))))
1786+
(TAnd (TSel (varF 0) 0) (TBind (TMem 0 TBot (TSel (varF 1) 0))))) =
1787+
(TAll 0 (TAnd (TSel (varF 0) 0) (TBind (TMem 0 TBot (TSel (varF 1) 0))))
1788+
(TAnd (TSel (varF 0) 0) (TBind (TMem 0 TBot (TSel (varF 1) 0)))))) as A. {
1789+
compute. reflexivity.
1790+
}
1791+
rewrite <- A at 3. apply t_var_unpack. apply t_var. compute. reflexivity. crush_wf.
1792+
crush_wf. unfold open. simpl. crush_wf.
1793+
eapply dt_nil. eauto. eauto. simpl. reflexivity. crush_wf. crush_wf. crush2.
1794+
1795+
unfold open. simpl.
1796+
assert (open (varF 2) (TAll 0 (TSel (varF 1) 0)
1797+
(TAll 0
1798+
(TAnd (TSel (varF 0) 0) (TBind (TMem 0 TBot (TSel (varF 1) 0))))
1799+
(TAnd (TSel (varF 0) 0) (TBind (TMem 0 TBot (TSel (varF 1) 0)))))) =
1800+
(TAll 0 (TSel (varF 1) 0)
1801+
(TAll 0
1802+
(TAnd (TSel (varF 0) 0) (TBind (TMem 0 TBot (TSel (varF 1) 0))))
1803+
(TAnd (TSel (varF 0) 0) (TBind (TMem 0 TBot (TSel (varF 1) 0))))))) as B. {
1804+
compute. reflexivity.
1805+
}
1806+
rewrite <- B at 2. apply t_var_unpack. apply t_var. compute. reflexivity. crush_wf.
1807+
unfold open. simpl. crush_wf. unfold open. simpl. crush_wf.
1808+
1809+
eapply dt_mem. eapply dt_nil. eauto. simpl. reflexivity. eauto. eauto. simpl. reflexivity.
1810+
1811+
eauto. eauto. simpl. reflexivity.
1812+
crush_wf. crush_wf.
1813+
1814+
eapply stp_bindx. eauto. crush_cl. crush_cl. crush_wf.
1815+
unfold open. simpl. eapply stp_and2.
1816+
eapply stp_and11; crush_wf.
1817+
eapply stp_and12. eapply stp_and2.
1818+
eapply stp_and11; crush_wf. eapply stp_and12.
1819+
eapply stp_mem. eapply stp_bot. crush_wf. crush_wf. crush_wf.
1820+
crush_wf.
1821+
1822+
Qed.
1823+
16331824

16341825
(* ############################################################ *)
16351826
(* Proofs *)

0 commit comments

Comments
 (0)