# Skelet #33 doesn't halt - Coq proof

A few weeks ago, I saw a few machines that weren’t formally proven yet, in particular, Skelet #15, #17, #26, and #33. @meithecatte and I finished formalizing the proof that Skelet #33 (11896833) doesn’t halt, and the proof is available here. Thanks to @meithecatte for proving `Theorem nonhalt` and cleaning up the proof!

In the rest of this post, I will give an overview of the formal proof. The proof begins similarly to Skelet #34’s proof, but the proof diverged after I introduced `invariant(n, m)`. This invariant made the TM configurations easier to reason about, and made the 3 theorems `step_reset` + `do_reset` + `E_next` work properly.

## Counter phase

These definitions were copied over:

• `b(n)` is the first non-negative integer such that `n + b(n)` contains only 1’s in base-2. For example, `b(15) = 0` and `b(16) = 15`. (Note: `b(0)` is not defined)
• `L(n)` is a tape defined by `L(0) = 0^∞`, `L(2n) = L(n) 0000`, and `L(2n+1) = L(n) 1000`.
• `R(n)` is a tape defined by `R(0) = 0^∞`, `R(2n) = 10 R(n)`, and `R(2n+1) = 11 R(n)`.
• `K(n)` is a tape defined by `K(0) = 0^∞`, `K(2n) = K(n) 0000`, and `K(2n+1) = K(n) 0100`. Note that `L(n) = K(n) 0` for all `n`.

These definitions were slightly modified to fit Skelet #33:

• `D(n, m) = L(n) <C 101010 R(m)`. `D(n, m)` represents a counter phase configuration.
• `E(n, m) = K(n) <C 1010 R(m)`. `E(n, m)` represents a reset phase configuration.

First, we analyze the configuration `D(n, m)`. Depending on `m`, the machine will follow either `D_inc` or `start_reset`.

• Lemma `D_inc`. If `m` contains a 0 in base-2, then `D(n, m) ⊢* D(n+1, m+1)`.
• Theorem `start_reset`. If `m` contains only 1’s in base-2, then `D(n, m) ⊢* E(n+1, 2(m+1)+1)`.

In summary, if the machine starts on `D(n, m)`, it will repeatedly follow `D_inc` to get to `D(n+b(m), m+b(m))` (see `D_inc` and `D_finish` in the proof). Since `m+b(m)` contains only 1’s in base-2, the machine will follow `start_reset`.

Now that the counter phase `D(*, *)` is analyzed, let’s move on to the reset phase `E(*, *)`.

## Reset phase

`E(n, m)` is easy to analyze when `n` is odd.

Lemma `step_reset_odd`. Let `n`, `m` be positive integers. Then `E(2n+1, m) ⊢* E(n, 4m+2)`.
Proof. Simulate the machine. `E(2n+1, m) = K(n) 0100 <C 1010 R(m) ⊢* K(n) <C 1010 1011 R(m) = E(n, 4m+2)`. □

The general case requires more setup:

• Let `leads(n)` be the statement that either `n = 1`, or `n` starts with `11` in base-2.
• Suppose `q ≥ 0` and `0 ≤ r < 2^q`. Then `leads(3 * 2^q + r)`.
• Let `invariant(n, m)` be the statement that `leads(n)` is true, and `b(m) = 3 * 2^q + r` for some `q ≥ 0` and `2n ≤ r < 2^q`.

Theorem `step_reset`. Let `n > 1` and `m ≥ 1`. Suppose `invariant(n, m)` is true. Then there exist `1 ≤ n' < n` and `m' ≥ 1` such that `E(n, m) ⊢* E(n', m')` and `invariant(n', m')` is true.

Proof

Factor `n` as `n = 2^k (2n'+1)` for some `k ≥ 0` and `n' ≥ 0`. Define `m' = (2(2(2^k - 1) + m) + 1) * 4^k + 1`. We claim that `n'` and `m'` satisfy the theorem.

• Proof that `n' ≥ 1`. For the sake of contradiction, suppose `n' = 0`. As a result, `n = 2^k`. Since `n > 1`, it follows that `leads(n)` is false. This contradicts `invariant(n, m)`.
• Proof that `n' < n`. This follows from `n = 2^k (2n'+1)`.
• Proof that `m' ≥ 1`. This follows from the definition of `m'`.
• Proof that `E(n, m) ⊢* E(n', m')`. This follows from a sequence of steps:
• `E(n, m) = E(2^k (2n'+1), m) = K(n') 0100 0000^k <C 1010 R(m)`
• `K(n') 0100 0000^k <C 1010 R(m) ⊢* K(n') 0100 1000^k <C 1010 R(2(2^k - 1) + m)` (see `LaR_max`). Also, the right side does not overflow because `b(m) = 3 * 2^q + r > r ≥ 2n > 2(2^k - 1)`.
• The machine runs on `0100 1000^k <C 1010` and eventually reaches `E(n', m')`. See `eat_bin_max` and `drop_KI` for more details.
• Proof that `leads(n')` is true. Note that `n = 2^k (2n'+1)` and `leads(n)` is true. Trailing 0’s don’t matter, so `leads(2n'+1)` is true. Lastly, since `n' ≥ 1`, a little bit of work shows that `leads(n')` is true.
• Proof that `b(m') = 3 * 2^q' + r'` for some `q' ≥ 0` and `2n' ≤ r' < 2^q'`. For this proof, use `q' = q+2k+2` and `r' = 2^(2k+2) * (r-2(2^k - 1)) + 3 * 2^(2k) - 2`. See the proof for more details. □

Here’s a more useful version of Theorem `step_reset`.

Corollary `do_reset`. Let `n ≥ 1` and `m ≥ 1`. Suppose `invariant(n, m)` is true. Then there exists `m' ≥ 1` such that `E(n, m) ⊢* E(1, m')` and `leads(b(m'))` is true.
Proof. Use strong induction on `n`. For `n = 1`, use `m' = m`. From `invariant(1, m)`, it follows that `b(m) = 3 * 2^q + r` where `r < 2^q`, and therefore, `leads(b(m))`. This finishes the base case. For `n > 1`, apply `step_reset` to go to a smaller case. □

Here’s the theorem that brings all of the previous work together.

Theorem `E_next`. Let `m ≥ 1` and suppose `leads(b(m))` is true. Then there exists `m' ≥ 1` such that `E(1, m) ⊢^+ E(1, m')` and `leads(b(m'))` is true.

Proof

Firstly, direct simulation shows that `E(1, m) ⊢^+ D(0, 2m+1)`. Follow `D_finish` to reach `D(b(2m+1), 2m+1+b(2m+1))`. Follow `start_reset` to reach `E(b(2m+1)+1, 4m+5+2b(2m+1))`. This simplifies to `E(2b(m)+1, 4(m+b(m)+1)+1)`. Follow `step_reset_odd` to reach `E(b(m), 16(m+b(m)+1)+6)`. Following `do_reset` is enough to finish the proof, but we still need to show that `invariant(b(m), 16(m+b(m)+1)+6)` is true. Here’s the proof that the invariant is true:

• Proof that `leads(b(m))` is true. This is already given.
• Proof that `b(16(m+b(m)+1)+6) = 3 * 2^q + r` for some `q ≥ 0` and `2b(m) ≤ r < 2^q`. First, let `m+b(m)+1 = 2^k` for some `k ≥ 1`. Then `b(16(m+b(m)+1)+6) = b(2^(k+4)+6) = 2^(k+4)-7 = 3 * 2^(k+2) + (2^(k+2)-7)`. Therefore, `q = k+2` and `r = 2^(k+2)-7`. Lastly, Coq proved the inequality `2b(m) ≤ r` using just `lia`. □

Theorem `nonhalt`. Skelet #33 does not halt.
Proof. The machine reaches `E(1, 17)`. Also, `leads(b(17)) = leads(14)` is true. The conditions of Theorem `E_next` are satisfied. Apply Theorem `E_next` infinitely. □

2 Likes