From informal proof to Coq: a tour of one kill file

1The whole file on one strip

Each band is one part of W5-3's proof, as wide as its share of the 530 lines. The key under it says what each part is and which beat shows it.

1. 1head1–22What the machine does, in prose. key lines
2. 2tm24–35The machine itself, on line 32 (beat 7). key lines
3. 3C, HF37–40The counter C n and the count configuration HF l r (beat 2). key lines
4. 4lemmas42–11512 short stretches of the run, like LEat (beat 2). key lines
5. 5count117–149One count: Cnt1, Cnt0, Cnt011 (beat 3). key lines
6. 6Q151–210A fixed-width counter, needed only inside BS5. key lines
7. 7walks212–310Many counts in a row, by induction (beat 3). key lines
8. 8BS1–BS5313–431The macro rules: eat configuration to the next (beat 3). key lines
9. 9init433–441The opening: blank tape to EC 2 4 (beat 5). key lines
10. 10J443–478The closure step_J: the invariant (beat 4). key lines
11. 11thm480–488The theorem nonhalt, 9 lines (beat 5). key lines
12. 12notes490–530Every rule again, on paper. key lines

Read the file from the bottom up and you get the informal proof from the top down. The theorem (line 480) needs an opening (435) and a closure (447). The closure needs the macro rules (331 to 431), and those need the walks (224 to 310) and the segment lemmas (46 to 115).

2One lemma is one run you can watch

(* EAT: EB, then the C/F sweep EAT0 over the whole word, then CS *)
Lemma LEat b r:
  HF (0inf <* [0;1]^^b) r -->+ 0inf <* [0;1]^^(b+2) <* [0;1;1] {{A}}> r.
Proof. unfold HF. es. Qed.

LEat says: from the tape on the left of -->+, the machine reaches the tape on the right. It holds for every b and every right side r. First, the four pieces of notation, each on W5-3's real tape.

The trap: a left list starts at the head

Row 3 is the trap. Coq keeps the left side as a list that starts at the head and runs left. So 0inf <* [0;1]^^2 is 1 0 1 0 on the tape, which is (10)². The file's header says the same: EC p N = HF (0^inf (10)^p) (C N) (line 17).

A right-hand list like [1;0;1;1] *> r starts next to the head (or at the head, in the {{A}}> form) and reads left to right, as written. Both notations are one busycoq function, Str_app:

Notation "xs *> r" := (Str_app xs r) (at level 25, right associativity).
Notation "l <* xs" := (Str_app xs l) (at level 24, left associativity, only parsing).

busycoq verify/Helper.v, lines 179–180: Str_app xs s puts the list xs in front of the side s, first item nearest the head.

LEat on the real run

Here is LEat at the moment it applies, with b = 2 and r = C 4: steps 171 to 190.

The brackets on the first and last rows show which piece of the lemma covers which cells. The eat never reads r, and it takes 4b + 11 steps (we checked b = 0 to 12).

What es sees: b left unknown

Coq cannot try every b one by one. So es treats (10)^b as one box, and r as another. It runs the cells outside the boxes one step at a time, and crosses a box in one jump with a shift rule (module 2): a rule for one copy of 10, used b times.

Each row is the real tape at b = 2 (the run above, steps in brackets), with the cells of (10)^b and of r drawn as boxes. The page checks the same five rows for b = 0 to 8.

3Lemmas chain into a macro rule

(* M2: N = 0 mod 4 *)
Lemma BS2 p n: EC p (n*4) -->+ EC (p+3+p mod 2) (n+p+4).
Proof.
  unfold EC.
  eapply progress_trans. 1: apply LEat.
  eapply progress_trans. 1: apply Y2C.
  eapply progress_trans. 1: apply (Cnt1 (0inf <* [0;1]^^(p+2) <* [1;1]) 0 (C n) _ (IncC n)).
  eapply pt_eq. 1: apply (Wk (p+2) 1 (1+n)).
  apply HF_eq. 2: f_equal; lia.
  f_equal. f_equal. lia.
Qed.

Each eapply progress_trans. 1: apply X. means: first run lemma X, then prove the rest. So the proof of BS2 is a list of lemmas laid end to end, and its last two lines check the arithmetic with lia. The bar is the real run from EC 2 4 (step 171) to EC 5 7 (step 457), cut where each lemma ends. Tap a piece to jump there.

LEat 171–190 · Y2C 190–203 · Cnt1 203–231 · then Wk 4 1 2 231–457: Cnt1, Cnt0, Cnt1, Cnt0, Cnt1

Wk 4 1 2 (line 350) covers the last five counts. Watch the lone 1 in the word on the left. Every two counts it moves two 10 pairs further left, and the counter goes up by one per count, from C 2 to C 7.

Induction: one lemma for every size

(* W(a,b): G((10)^a 1 (10)^b, C n) -> E(a+b+[a odd], n+a+1), a+1 counts *)
Lemma Wk a: forall b n,
  HF (0inf <* [0;1]^^a <* [1] <* [0;1]^^b) (C n) -->+
  HF (0inf <* [0;1]^^(a+b+a mod 2)) (C (n+a+1)).
Proof.
  induction a as [a IH] using lt_wf_ind. intros b n.
  destruct a as [|[|a]].

Wk is stated for every a (line 235), so Coq proves it by induction on a (line 239). For a = 0 and a = 1 the counts are done directly. For a ≥ 2 the proof runs W2 (two counts that move the lone 1 two pairs left) and then uses Wk itself for a − 2. Here a goes 4, 2, 0, as in the rows above.

4The invariant becomes one lemma

Lemma step_J p N: 1 <= N <= 2*p ->
  exists p' N', EC p N -->+ EC p' N' /\ 1 <= N' <= 2*p'.

step_J: if 1 ≤ N ≤ 2p (this is J), then EC p N runs to some EC p' N' where J holds again. Below is the real run: the blank tape, then every EC configuration up to step 2,731, with J checked and the macro rule that comes next.

The row at step 37 is a real EC configuration too: EC 0 1. But J fails there, because 1 ≤ 2·0 is false. That is why the opening runs on to EC 2 4.

The proof of step_J (lines 449–478) is this table: split N into cases, apply that case's macro rule, then let lia check 1 ≤ N' ≤ 2p'.

For BS5, write N/2 + 1 = (2m+1)·2^t+3: an odd number times a power of 2, at least 8. For example, N = 62 gives N/2 + 1 = 32 = 1·2⁵, so m = 0 and t = 2, and BS5 needs 2³ = 8 ≤ p + 7. (The file writes 2^t+1 as 2^(S t), line 388.)

5The last nine lines

This is the whole argument as a picture. The blank tape reaches a configuration with J. From every configuration with J, the machine moves on, in one step or more, to another with J. So it can never stop. The nine lines say exactly this:

Lemma nonhalt: ~halts tm c0.

Proof.
  eapply multistep_nonhalt. 1: apply init.

  change (EC 2 4) with ((fun x : nat*nat => let (p,N) := x in EC p N) (2,4)).

  apply progress_nonhalt_cond with (P := fun x : nat*nat => let (p,N) := x in 1 <= N <= 2*p).

  - intros [p N] HJ. destruct (step_J p N HJ) as [p' [N' [H1 H2]]].
    exists (p',N'). split; assumption.

  - lia.
Qed.

The opening is the one part Coq checks by running the concrete machine. init (line 435) makes it run these 171 steps from the blank tape and compare the result with EC 2 4. The brackets appear twice: at step 171, and at step 37, where the tape is EC 0 1 and J fails.

6Another start state: mirror and rename

A machine whose table is another machine's table seen in a mirror needs no new macro rules. It needs only a new opening, plus three busycoq lemmas.

W5-8b 1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF is such a machine. Mirror its table (swap L and R everywhere) and rename its states A→C, B→A, C→B (D, E, F stay): you get W5-8 1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF. W5-8b starts in A, which becomes C. Here is the proof as a picture, with each machine's real tape at step 20:

The two runs below share one set of controls. Their pictures are mirror images, row for row, across the dashed line. Only the colours differ, because the states are renamed: where W5-8b is in A (red), W5-8 is in C (blue).

Every cell of W5-8b, mirrored and renamed, is the matching cell of W5-8. The page computes this table from the two strings. Coq checks the same 12 cells in perm.

Definition phi (q : Q) : Q :=
  match q with
  | A => C | B => A | C => B | D => D | E => E | F => F
  end.

Lemma perm: Perm (flip tm) tmP phi.
Proof.
  split.
  - intros [] [] H; cbn in *; try discriminate; reflexivity.
  - intros [] [] s' d q' H; cbn in *; inversion H; subst; reflexivity.
Qed.

Lemma nonhalt: ~halts tm c0.
Proof.
  intros H.
  apply flip_halts in H.
  change (halts (flip tm) (A;; tape0)) in H.
  exact (nonhaltP (perm_halts _ _ _ _ _ perm H)).
Qed.

• phi (line 351) is the renaming, from W5-8b's states to W5-8's. In this file W5-8 is called tmP.
• perm (line 356): the mirrored table flip tm, renamed by phi, is tmP, cell for cell (the table above).
• nonhalt (line 363) is the picture: H is box 1, flip_halts gives box 2, perm_halts box 3, and nonhaltP (line 335) box 4.

So the macro rules carry over from W5-8's own proof. What is new is the opening from the new start state (W5-8 from C: 4,098,826 steps to its first macro configuration, line 148) and these 19 lines.

7The gate: what check_kill demands

A file counts as a kill only when tools/check_kill.sh prints PASS. It demands five things. Here they are with the matching lines of W5-3's real report:

[PASS] framework      (a) busycoq HEAD == tools/busycoq.pin, no tracked changes under verify/
       HEAD 0940bb9cf434ba68f0c025dabfde45a219999973 == pin; no tracked changes under verify/
[PASS] compile        (f) temp copy + appended checks compile within 1800s, flags from verify/_CoqProject
       compiled in 3.4s with all appended checks

[PASS] tm_text        (b) TM_from_str literal of the top-level `Definition tm` == <tm> byte for byte
       line 32: TM_from_str "1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC" == <tm> (41 bytes)

[PASS] theorem_text   (c) exactly one top-level `nonhalt : ~halts tm c0` (text)
       line 480: nonhalt : ~halts tm c0

[PASS] forbidden      (d) forbidden tokens anywhere in the file (comments and strings included)
       none of 30 forbidden patterns occur (ground rule 1's words: anywhere; command words: outside comments and strings; comments never split a token)

[PASS] assumptions    (e) Print Assumptions nonhalt within tools/assumptions_baseline.txt
       0 assumption(s), all in the baseline

[PASS] coqchk         (h) coqchk -norec re-checks the compiled candidate (VM/native steps included)
       coqchk -norec BB6Kill.Candidate ok (1.0s); its context summary lists nothing of the file's own
RESULT: PASS -- this is a kill

check_kill compares line 32 with the machine string it is given on the command line. We always give the entry copied from the holdout list, the machines no decider has settled: W5-3 is line 134 of the 740 list.

[PASS] forbidden
[PASS] tm_text
[PASS] theorem_text
RESULT: TEXT_ONLY_OK -- text-level checks only; NOT a kill verdict

[PASS] forbidden
[FAIL] tm_text
  file (line 32): '…---0RB'
  arg:            '…---0RC'
[PASS] theorem_text
RESULT: FAIL -- failed: tm_text

[FAIL] forbidden
  line 488 (code): `Admitted`
[PASS] tm_text
[PASS] theorem_text
RESULT: FAIL -- failed: forbidden

Reference: the file part by part

The key lines of each band of beat 1, exactly as in the file. Tap a part to open it.

    Configurations are taken 6 steps after the write-up's G form (after rule TS):
      HF l r  =  l <E 1 0 1 1 r,   EC p N  =  HF (0^inf (10)^p) (C N)  ( = E(p,N) ).

Definition tm := Eval compute in (TM_from_str "1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC").

(** C(n): n in binary, lowest digit first, 1 = 11, 0 = 00, leading 1 last.
    HF l r: E reads the last cell of l, followed by 1 0 1 1 and the right side r. *)
Definition C n := BinInc [1;1] n.
Definition HF (l r : side) := l <{{E}} [1;0;1;1] *> r.

(* the counter increment on C *)
Lemma RInc n l:
  l <* [1;1;0;1] {{A}}> C n -->+ HF l (C (1+n)).
Proof.
  unfold C, HF. apply RBinInc_spec. intros. apply RIncG.
Qed.

Lemma Cnt1 u b r r': Inc r r' ->
  HF (u <* [1] <* [0;1]^^b) r -->+ HF (u <* [0] <* [0;1]^^b) r'.
Proof. intros I. eapply progress_trans. 1: apply L1. apply I. Qed.

Fixpoint Dk (k x : nat) : list Sym :=
  match k with
  | O => []
  | S k' => (if Nat.odd x then [1;1] else [0;0]) ++ Dk k' (Nat.div2 x)
  end.

(* W(a,b): G((10)^a 1 (10)^b, C n) -> E(a+b+[a odd], n+a+1), a+1 counts *)
Lemma Wk a: forall b n,
  HF (0inf <* [0;1]^^a <* [1] <* [0;1]^^b) (C n) -->+
  HF (0inf <* [0;1]^^(a+b+a mod 2)) (C (n+a+1)).

Definition EC p N := HF (0inf <* [0;1]^^p) (C N).

(* M5: N = (2m+1) 2^(t+4) - 2 with t' = t+1 >= 1, precondition 2^t' <= p+7 *)
Lemma BS5 p m t: 2^(S t) <= p+7 ->
  EC p (((m*2+1)*2^(S (S (S t)))-1)*2) -->+ EC (p+8+t) (m+2^(S t)+t+2).

Lemma init: c0 -->* EC 2 4.
Proof.
  unfold EC, HF.
  replace (C 4) with ([0;0;0;0;1;1] *> 0inf) by reflexivity.
  change ([0;1]^^2) with [0;1;0;1].
  solve_init.
Qed.

Lemma step_J p N: 1 <= N <= 2*p ->
  exists p' N', EC p N -->+ EC p' N' /\ 1 <= N' <= 2*p'.

Lemma nonhalt: ~halts tm c0.

eat to eat                                                                  E(p, N) -> E(p', N')
M1  N odd                EAT,Y1; W(p+2,0)                                   p+2+[p odd],  (N+1)/2 + p + 3
M2  N = 0 (mod 4)        EAT,Y2; INC1; W(p+2,1)                             p+3+[p odd],  N/4 + p + 4
M3  N = 8m+2             EAT,Y3(0); OVF(0,0); W(p+4,0)                      p+4+[p odd],  m + p + 6