Negativity

On Tuesday, I stayed home sick with a cold-and/or-flu (thus missing a class that might have held some information I hadn't yet gotten from the original paper); but people on the Internet were arguing about religion. As they often do. And, as they often do, someone said “it’s true technically you can’t prove a negative”.

This is, of course, false. Negatives can be proven, even without the law of the excluded middle, and even without your logic having a primitive concept of “not”. In, say, the Calculus of Inductive Constructions, “not P” is “P → False”, where “False” is an inductive predicate with no constructors, so you get your ex falso quodlibet just from case analysis, and it's all terribly pretty.

Anyway. Negatives. Even without this newfangled lambda-cube stuff, you can prove that the square root of 2 is irrational, which is to say that there do not exist integers p and q, where q ≠ 0, such that p² = 2 q². This was first done around 500 BC, and the person responsible was drowned. Modern Internet religion arguments are, thankfully(?), much tamer.

So, last year, when I was first learning about the Coq proof assistant, I used it to obtain a machine-checkable proof of just that negative. Knowledgeable readers will notice that I independently reinvented part of the NArith library there, because I didn't know about the original.

Thus, what better to do on such a Tuesday, while feverish and generally out of it, but fiddle with an esoteric logic? Which is why I now have a much shorter proof, though I didn't bother mapping it back to the Peano numbers like I did with the other one.

The next obvious thing is, of course, to prove irrational the square roots of other numbers than 2. Or all of them! Or at least all the primes, because it's only in prime bases that the count of trailing zeroes (ctz ≈ bsf) interacts with multiplication in the way needed. (Hints: 2*5=10, 9*9=81.) And that I eventually gave up on.

But, first, I defined subtraction using specification types: given natural numbers a and b, return either c and a proof that a = b + c, or a proof that a < b. And then division: given n and d and a proof of d > 0, return either q and a proof that n = d * q, or a proof that no such q exists.

That last one sounds trivial, but of course it isn't; there's no excluded middle, but, perhaps more to the point, the proof of that “it is or it isn't” can be converted into an actual, runnable, proven-correct OCaml program which does the division. Not that that's very practically useful — it works on Peano numbers and does repeated subtraction (which in turn is repeated decrement).

But it does mark the first time I've successfully used Coq's support for strong induction. Twice, for the division and then for the count-trailing-zeroes, which... or, maybe instead of trying to gloss it into English, I'll just post the original type:

Definition ctz_spec : forall n b, 1 < b -> { e |
  (exists2 m, 0 < m & n = expt b e * m) &
  (forall e' m, e < e' -> 0 < m -> n <> expt b e' * m) } + { n = 0 }.