# Skelet #34 and #35 – Coq proof

Curious how difficult it would be to write a formal proof of non-halting for an individual machine, I decided to give it a go. I picked Skelet #34 and formalized the proof on @sligocki’s blog.

You can find my Coq proof here – the parts of interest will probably be the definition of the TM, and the final non-halting theorem.

Formal proofs have the tendency to expose small gaps in handwritten proofs, though rarely compromising the big ideas of the argument. This one was no different.

First, in the proof of Lemma 10:

I leave this proof as an exercise to the reader. We have already proven the case of `a = 1` in the Counter Phase section. The proof for `a = 0` is very similar.

In fact, Counter Phase makes use of the `a = 0` case, and it is `a = 1` we must carefully consider.

Secondly, the proof of Corollary 11 isn’t valid as written:

Lemma 10: If `b(m) > 1` and `b(n) > 1`, then `L(n) <C 101a R(m) -> L(n+1) <C 101a R(m+1)` for any `a` in `{0, 1}`.

Corollary 11: For all `k`, `a` in `{0, 1}`, and `m` such that `b(m) > 2^k - 1`, then `0000^k <C 101a R(m) -> 1000^k <C 101a R(t)` where `t = m + 2^k - 1`.

This follows directly from Lemma 10 when you note that the condition `b(m) > 2^k - 1` assures that you can apply Lemma 10 `2^k - 1` times.

The general idea is that `L(0) = 0000^k`, and so we count in binary until we reach `2^k - 1`. Except, Lemma 10 requires that `b(n) > 1`, i.e. that we don’t cross a power-of-two boundary. And we are crossing many such boundaries!

In fact, if you take a closer look, you’ll notice that in fact `L(0)` is not `0000^k`, but the empty string. Corollary 11 would be valid as written when surrounded by empty tape on both sides, but that is not the context in which it is used.

If you did the exercise left to the reader in the proof of Lemma 10, you might wonder why the assumption of `b(n) > 1` is even there – it is a bit subtle (I got confused by this at first), but for a rewrite rule like this to make sense, both sides need to have the same length – and that won’t be the case if we cross a power-of-two boundary.

The problem can be fixed by defining `L_k(n)`, which is the `k`-bit, fixed-width counter:

``````L_0(0) = empty string
L_{k + 1}(2*n) = L_k(n) 0000
L_{k + 1}(2*n+1) = L_k(n) 1000
``````

Having proven Skelet #34, we also get Skelet #35 for free – the same proof Just Works if we change the definition of the TM, as the only details that change are the ones that have been automated away with Coq tactics.

All this took quite some effort, mostly because the problem domain creates opportunities to use all three of Coq’s natural number types – `nat`, `positive` and `N`. The interactions can be gnarly.

This is to say that for now I’ll probably work on formally-verified deciders, as that just seems more pleasant, but I’m open to suggestions of what other machines would most benefit from a similar proof – i.e. which ones are least likely to be solved by a decider in the end.

4 Likes

Thank you for this, I’m excited to look into the Coq when I get a chance. I am both excited that someone else dug into this proof enough to find the warts and also embarrassed that I still had these errors. I’m glad the basic idea carried through even if the precise language didn’t

1 Like