The template, with its real line numbers: the shared header (lines 1–17) and Module TM7 (lines 1626–1871, 246 lines). TM8 (line 1874) reuses the same proof text. Right column: where each piece went in our file. Raw: SOMDCv6.v.
1From BusyCoq Require Import Individual62 Longitudinal DivModCases.2Require Import ZifyNat Lia.3Require Import ZArith.4Require Import String.5Require Import List.
8Ltac esc :=9 (apply BoundedConfig.segRLs_c_spec with (T:=10^3); reflexivity) ||10 (apply BoundedConfig.sideRLs_c_spec with (T:=10^3); reflexivity) ||11 (eapply sideRLs_c_spec with (T:=10^6); [vm_compute; reflexivity | st; reflexivity]).
13Ltac ec := econstructor.…lines 18–1625: Modules TM1–TM6 (not shown)1626Module TM7.1627Definition tm := Eval compute in (TM_from_str "1RB0RC_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---").1628Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40).1629Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).
1634Notation hR := (B,@nil Sym).1635Notation hR' := (D,[1]).1636Notation hL := (C,@nil Sym).1637Notation h := [(hR,hL)].1638Notation h' := [(hR',hL)].
1643Fixpoint toRC ls :=1644match ls with1645| [] => 0inf1646| LD::ls => ld*>toRC ls1647| D0::ls => d0*>toRC ls1648| D1::ls => d1*>toRC ls1649end.
1663Inductive RIncs: H->nat->(list RD)->(list RD)->Prop :=1664| RIncs_hx_ld k r r':1665 RIncs hx (1+k) r r' ->1666 RIncs hx k (LD::r) (LD::r')16671668| RIncs_hx_d1 k r r':1669 RIncs h1 k r r' ->1670 RIncs hx k (D1::r) (LD::r')16711672| RIncs_hx_d0 k r r':1673 RIncs hx (1+k) r r' ->1674 RIncs hx k (D0::r) (LD::r')16751676| RIncs_h1_ld k r r':1677 RIncs hx (1+k) r r' ->1678 RIncs h1 (1+k) (LD::r) (LD::r')16791680| RIncs_h1_d1 k r r':1681 RIncs h1 k r r' ->1682 RIncs h1 (1+k) (D1::r) (LD::r')16831684| RIncs_h1_d0_0 k r r':1685 RIncs h1 k r r' ->1686 RIncs h1 (1+k*2) (D0::r) (D0::r')16871688| RIncs_h1_d0_1 k r r':1689 RIncs h1 k r r' ->1690 RIncs h1 (2+k*2) (D0::r) (D1::r')16911692| RIncs_h1_rh_0:1693 RIncs h1 0 [] [D1]16941695| RIncs_h1_rh_1 k r':1696 RIncs h1 k [] r' ->1697 RIncs h1 (1+k*2) [] (D0::r')1698| RIncs_h1_rh_2 k r':1699 RIncs h1 k [] r' ->1700 RIncs h1 (2+k*2) [] (D1::r')1701.
1703Ltac cat3 :=1704 eapply @segRLs_sideRLs_concat with (w1:=[_;_;_]) (w2:=[_;_;_]); [|eauto 1].17051706Ltac tr1 :=1707 rewrite lpow_add,app_assoc;1708 eapply segRLs_trans; [esx | ].17091710Ltac wal :=1711 eapply segRLs_wall''; esx.17121713Ltac tr2 :=1714 eapply sideRLs_trans; [esx | ].
1718Lemma RIncs_spec tp k r r':1719 RIncs tp k r r' ->1720 sideRLs tm (toH tp++h^^k) (toH' tp*>toRC r) (toRC r').1721Proof.1722 intro H.1723 induction H; intros; cbn[toH toH' toRC] in *.1724 - cat3; tr1; wal.1725 - tr2.1726 cat3; wal.1727 - cat3; tr1; wal.1728 - rewrite lpow_add,app_assoc.1729 eapply @segRLs_sideRLs_concat with (w1:=[_;_;_;_]) (w2:=[_;_;_]); [|eauto 1].1730 tr1; wal.1731 - rewrite lpow_add,app_assoc.1732 tr2.1733 cat3; wal.1734 - cat3.1735 rewrite app_nil_l.1736 am 2 1 k 1 1.1737 rewrite Nat.add_comm,lpow_add,Nat.mul_1_r.1738 tr2; eauto 1.1739 - cat3.1740 rewrite Nat.add_comm.1741 am 2 1 k 2 1.1742 rewrite Nat.add_comm,lpow_add,Nat.mul_1_r.1743 tr2; eauto 1.1744 - esc.1745 - rewrite lpow_add,app_assoc.1746 tr2.1747 cat3.1748 rewrite app_nil_l.1749 am 2 1 k 0 0.1750 - change (2+k*2) with (1+(1+k*2)).1751 rewrite lpow_add,app_assoc.1752 tr2.1753 cat3.1754 rewrite app_nil_l.1755 am 2 1 k 1 0.1756Qed.
1758Lemma RIncs_nxt_1 k:1759 exists r, RIncs h1 k [] r.1760Proof.1761 induction k using lt_wf_ind.1762 destruct k.1763 + ec. ec.1764 + destruct (mod2 k); subst.1765 * epose proof (H0 _ _) as [r I].1766 ec. ec. apply I.1767 * epose proof (H0 _ _) as [r I].1768 ec. ec. apply I.1769 Unshelve. all: lia.1770Qed.
177117721773Ltac solve_v2 :=1774 (epose proof (RIncs_nxt_1 _) as [r I]; repeat ec; try apply I).17751776Ltac solve_v1 H tp'0 k'0 H' :=1777 eapply H with (tp':=tp'0) (k':=k'0) in H';1778 try lia;1779 try (1780 destruct H' as [r'' I1];1781 repeat ec; try apply I1).1782
1783Lemma RIncs_nxt tp k r r' tp' k':1784 RIncs tp k r r' ->1785 match tp,tp' with1786 | hx,hx => k<=k'1787 | h1,h1 => k*2+1<=k'1788 | h1,hx => k+1<=k'1789 | _,_ => False1790 end ->1791 exists r'',1792 RIncs tp' k' r' r''.1793Proof.1794 gen tp k r' tp' k'.1795 induction r; intros.1796 {1797 gen tp r' tp' k'.1798 induction k using lt_wf_ind.1799 intros.1800 inverts H1; destruct tp'.1801 all: try lia.1802 - solve_v2.1803 - destruct (sub k' 1); [subst|lia].1804 solve_v2.1805 - solve_v1 H0 hx (1+k') H3.1806 - destruct (sub k' 1); [subst|lia].1807 destruct (mod2 c); subst.1808 + solve_v1 H0 h1 (a) H3.1809 + solve_v1 H0 h1 (a) H3.1810 - solve_v1 H0 h1 (k') H3.1811 - destruct (sub k' 1); [subst|lia].1812 solve_v1 H0 h1 (c) H3.1813 }1814 {1815 inverts H0; destruct tp'.1816 all: try lia.1817 - solve_v1 IHr hx (1+k') H7.1818 - solve_v1 IHr hx (1+k') H7.1819 - solve_v1 IHr hx (1+k') H7.1820 - solve_v1 IHr hx (1+k') H7.1821 - destruct (sub k' 1); [subst|lia].1822 solve_v1 IHr hx (1+c) H7.1823 - solve_v1 IHr hx (1+k') H7.1824 - destruct (sub k' 1); [subst|lia].1825 solve_v1 IHr hx (1+c) H7.1826 - solve_v1 IHr hx (1+k') H7.1827 - destruct (sub k' 1); [subst|lia].1828 destruct (mod2 c); subst.1829 + solve_v1 IHr h1 (a) H7.1830 + solve_v1 IHr h1 (a) H7.1831 - solve_v1 IHr h1 k' H7.1832 - destruct (sub k' 1); [subst|lia].1833 solve_v1 IHr h1 (c) H7.1834 }1835Qed.
1839Notation lh := (0inf<*<[1]).1844Lemma BigStep r r':1845 RIncs hx 0 r r' ->1846 S' r -->+ S' r'.1847Proof.1848 intros H.1849 apply RIncs_spec in H.1850 unfold S'.1851 eapply sideRLs_1 in H.1852 follow10 H.1853 es.1854Qed.
1856Lemma nonhalt: ~halts tm c0.1857Proof.1858 eapply multistep_nonhalt with (c':=S' [D1]).1859 1: esx.1860 eapply progress_nonhalt_cond with (P:=fun r => exists r', RIncs hx 0 r r').1861 2: repeat ec.1862 intros r [r' I1].1863 pose proof I1 as I2.1864 eapply RIncs_nxt with (tp':=hx) (k':=O) in I2.1865 2: lia.1866 exists r'; split.1867 - apply BigStep,I1.1868 - apply I2.1869Qed.