SOMDCv6.v: shared header + Module TM7

Verbatim copy of vendor/busycoq/verify/SOMDCv6.v (busycoq 0940bb9c, sha256 cff0e865a73cc42d…), lines 1–17 and 1626–1871. Line numbers and anchors (#L-<n>) are SOMDCv6.v's own. The left stripe says what happened to each line in our proof.

kept verbatim   changed   not in ours   equal after normalizing the TM string   The right column links to the matching line in ours.

1From BusyCoq Require Import Individual62 Longitudinal DivModCases.ours L10
2Require Import ZifyNat Lia.ours L11
3Require Import ZArith.ours L12
4Require Import String.ours L13
5Require Import List.ours L14
6
7
8Ltac esc :=ours L17
9 (apply BoundedConfig.segRLs_c_spec with (T:=10^3); reflexivity) ||ours L18
10 (apply BoundedConfig.sideRLs_c_spec with (T:=10^3); reflexivity) ||ours L19
11 (eapply sideRLs_c_spec with (T:=10^6); [vm_compute; reflexivity | st; reflexivity]).ours L20
12
13Ltac ec := econstructor.ours L22
14
15Ltac am a a' k b b' :=ours L24
16 applys_eq (segRLs_addmul_v2 a a' k b b'); unfold DH0; flia; esc.ours L25
17
lines 18–1625: Modules TM1, TM2, TM3, TM4, TM5, TM6 (not shown; full file)
1626Module TM7.
1627Definition tm := Eval compute in (TM_from_str "1RB0RC_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---").ours L27
1628Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40).ours L28
1629Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).ours L29
1630
1631Notation ld := [1;1;0].ours L31
1632Notation d0 := [0;0;0].ours L32
1633Notation d1 := [1;0;0].ours L33
1634Notation hR := (B,@nil Sym).ours L35
1635Notation hR' := (D,[1]).ours L36
1636Notation hL := (C,@nil Sym).ours L37
1637Notation h := [(hR,hL)].ours L38
1638Notation h' := [(hR',hL)].ours L39
1639
1640Inductive RD := LD|D0|D1.ours L41
1641Inductive H := hx|h1.ours L42
1642
1643Fixpoint toRC ls :=ours L44
1644match ls withours L45
1645| [] => 0infours L46
1646| LD::ls => ld*>toRC lsours L47
1647| D0::ls => d0*>toRC lsours L48
1648| D1::ls => d1*>toRC lsours L49
1649end.ours L50
1650
1651Definition toH' x :=ours L52
1652match x withours L53
1653| hx => []ours L54
1654| h1 => [1]ours L55
1655end.ours L56
1656
1657Definition toH x :=ours L58
1658match x withours L59
1659| hx => h'ours L60
1660| h1 => []ours L61
1661end.ours L62
1662
1663Inductive RIncs: H->nat->(list RD)->(list RD)->Prop :=ours L71
1664| RIncs_hx_ld k r r':ours L72
1665 RIncs hx (1+k) r r' ->ours L74
1666 RIncs hx k (LD::r) (LD::r')ours L75
1667
1668| RIncs_hx_d1 k r r':ours L77
1669 RIncs h1 k r r' ->ours L78
1670 RIncs hx k (D1::r) (LD::r')ours L79
1671
1672| RIncs_hx_d0 k r r':ours L81
1673 RIncs hx (1+k) r r' ->ours L82
1674 RIncs hx k (D0::r) (LD::r')ours L83
1675
1676| RIncs_h1_ld k r r':ours L85
1677 RIncs hx (1+k) r r' ->ours L87
1678 RIncs h1 (1+k) (LD::r) (LD::r')ours L88
1679
1680| RIncs_h1_d1 k r r':ours L90
1681 RIncs h1 k r r' ->ours L91
1682 RIncs h1 (1+k) (D1::r) (LD::r')ours L92
1683
1684| RIncs_h1_d0_0 k r r':ours L94
1685 RIncs h1 k r r' ->ours L95
1686 RIncs h1 (1+k*2) (D0::r) (D0::r')ours L96
1687
1688| RIncs_h1_d0_1 k r r':ours L98
1689 RIncs h1 k r r' ->ours L99
1690 RIncs h1 (2+k*2) (D0::r) (D1::r')ours L100
1691
1692| RIncs_h1_rh_0:ours L102
1693 RIncs h1 0 [] [D1]ours L103
1694
1695| RIncs_h1_rh_1 k r':ours L105
1696 RIncs h1 k [] r' ->ours L106
1697 RIncs h1 (1+k*2) [] (D0::r')ours L107
1698| RIncs_h1_rh_2 k r':ours L109
1699 RIncs h1 k [] r' ->ours L110
1700 RIncs h1 (2+k*2) [] (D1::r')ours L111
1701.ours L118
1702
1703Ltac cat3 :=ours L120
1704 eapply @segRLs_sideRLs_concat with (w1:=[_;_;_]) (w2:=[_;_;_]); [|eauto 1].ours L121
1705
1706Ltac tr1 :=ours L123
1707 rewrite lpow_add,app_assoc;ours L124
1708 eapply segRLs_trans; [esx | ].ours L125
1709
1710Ltac wal :=ours L127
1711 eapply segRLs_wall''; esx.ours L128
1712
1713Ltac tr2 :=ours L130
1714 eapply sideRLs_trans; [esx | ].ours L131
1715
1716Open Scope nat.ours L143
1717
1718Lemma RIncs_spec tp k r r':ours L174
1719 RIncs tp k r r' ->ours L175
1720 sideRLs tm (toH tp++h^^k) (toH' tp*>toRC r) (toRC r').ours L176
1721Proof.ours L177
1722 intro H.ours L178
1723 induction H; intros; cbn[toH toH' toRC] in *.ours L179
1724 - cat3; tr1; wal.
1725 - tr2.ours L185
1726 cat3; wal.ours L186
1727 - cat3; tr1; wal.ours L187
1728 - rewrite lpow_add,app_assoc.
1729 eapply @segRLs_sideRLs_concat with (w1:=[_;_;_;_]) (w2:=[_;_;_]); [|eauto 1].ours L189
1730 tr1; wal.
1731 - rewrite lpow_add,app_assoc.ours L194
1732 tr2.ours L195
1733 cat3; wal.ours L196
1734 - cat3.ours L197
1735 rewrite app_nil_l.ours L198
1736 am 2 1 k 1 1.ours L199
1737 rewrite Nat.add_comm,lpow_add,Nat.mul_1_r.ours L200
1738 tr2; eauto 1.ours L201
1739 - cat3.ours L202
1740 rewrite Nat.add_comm.ours L203
1741 am 2 1 k 2 1.ours L204
1742 rewrite Nat.add_comm,lpow_add,Nat.mul_1_r.ours L205
1743 tr2; eauto 1.ours L206
1744 - esc.ours L207
1745 - rewrite lpow_add,app_assoc.ours L208
1746 tr2.ours L209
1747 cat3.ours L210
1748 rewrite app_nil_l.ours L211
1749 am 2 1 k 0 0.ours L212
1750 - change (2+k*2) with (1+(1+k*2)).ours L213
1751 rewrite lpow_add,app_assoc.ours L214
1752 tr2.ours L215
1753 cat3.ours L216
1754 rewrite app_nil_l.ours L217
1755 am 2 1 k 1 0.ours L218
1756Qed.ours L221
1757
1758Lemma RIncs_nxt_1 k:ours L269
1759 exists r, RIncs h1 k [] r.ours L270
1760Proof.ours L271
1761 induction k using lt_wf_ind.ours L272
1762 destruct k.ours L273
1763 + ec. ec.ours L274
1764 + destruct (mod2 k); subst.ours L275
1765 * epose proof (H0 _ _) as [r I].ours L276
1766 ec. ec. apply I.ours L277
1767 * epose proof (H0 _ _) as [r I].ours L278
1768 ec. ec. apply I.ours L279
1769 Unshelve. all: lia.ours L280
1770Qed.ours L281
1771
1772
1773Ltac solve_v2 :=
1774 (epose proof (RIncs_nxt_1 _) as [r I]; repeat ec; try apply I).
1775
1776Ltac 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' with
1786 | hx,hx => k<=k'
1787 | h1,h1 => k*2+1<=k'
1788 | h1,hx => k+1<=k'
1789 | _,_ => False
1790 end ->
1791 exists r'',
1792 RIncs tp' k' r' r''.
1793Proof.ours L307
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.ours L349
1836
1837Open Scope sym.ours L538
1838
1839Notation lh := (0inf<*<[1]).ours L540
1840
1841Definition S' r :=ours L542
1842 lh {{{ (hR',R) }}} toH' hx *> toRC r.ours L543
1843
1844Lemma BigStep r r':ours L545
1845 RIncs hx 0 r r' ->ours L546
1846 S' r -->+ S' r'.ours L547
1847Proof.ours L548
1848 intros H.ours L549
1849 apply RIncs_spec in H.ours L550
1850 unfold S'.ours L551
1851 eapply sideRLs_1 in H.ours L552
1852 follow10 H.ours L553
1853 es.ours L554
1854Qed.ours L555
1855
1856Lemma nonhalt: ~halts tm c0.ours L560
1857Proof.ours L561
1858 eapply multistep_nonhalt with (c':=S' [D1]).ours L562
1859 1: esx.
1860 eapply progress_nonhalt_cond with (P:=fun r => exists r', RIncs hx 0 r r').ours L564
1861 2: repeat ec.
1862 intros r [r' I1].ours L571
1863 pose proof I1 as I2.
1864 eapply RIncs_nxt with (tp':=hx) (k':=O) in I2.
1865 2: lia.
1866 exists r'; split.ours L572
1867 - apply BigStep,I1.ours L573
1868 - apply I2.
1869Qed.ours L575
1870
1871End TM7.

Lines 1872–2121: Module TM8, whose body equals TM7's except the tm line (A1 = 0LC).