# When is a proof not a proof?

*By:*.

*Published: .*

*Categories: dependent-types functional-programming proofs blogosphere.*

When is a proof not a proof? When you think you’ve proven one thing, but actually, you’ve proven something else.

In the last post, I addressed a good question raised in the first half of David Owens II’s article “Dependent Types: I’m Missing Something”, where he addresses my discussion of dependent types.

This post looks at the latter half,
which talks about an example drawn from
early in the chapter
“Introducing Inductive Types”
of Adam Chlipala’s *Certified Programming with Dependent Types.*

This example is interesting in part because it is actually not an example of a dependent type, so it’s something we can talk about almost entirely in terms of Swift, absent the computer-assisted theorem proving that is Coq’s special sauce. Tackling theorems in Swift is a perfect fit for a generative testing framework.

## Putting the example in context

The book has introduced a `bool`

type as an example of defining
an enumeration type.
It then defines a function `negb`

that performs Boolean negation
to demonstrate function definition using pattern matching.
The book then proceeds to prove a couple theorems about the
`negb`

function as part of teaching the reader how to do proofs using Coq.

## Rewriting the example in Swift

`bool`

is not a dependent type, so Swift and SwiftCheck are up to the task.

The book doesn’t get to dependent types till 5 chapters later.
`bool`

is an enumeration type, and `negb`

relies on non-dependent
pattern matching, all of which Swift can do.
This means we can pretty directly translate the example definitions and
theorem from Gallina into Swift:

```
enum Bool_ {
case True
case False
}
func negb(b: Bool_) -> Bool_ {
switch b {
case .True: return .False
case .False: return .True
}
}
/// Generative testing of the `negb_inverse` theorem's claim.
func testNegbInverse() {
property("negb is its own inverse") <- forAll { (b: Bool_) in
return negb(negb(b)) == b
}
}
extension Bool_: Arbitrary {
static var arbitrary : Gen<Bool_> {
return Gen.oneOf([Gen.pure(.True), Gen.pure(.False)])
}
}
```

I’ve translated the `negb_inverse`

theorem into
a SwiftCheck test
and provided a generator of arbitrary `Bool_`

values
for the test generator to use.

Running the test as-is gives:

```
Test Case '-[NegbTests.NegbTests testTheoremNegbInverse]' started.
*** Passed 100 tests
.
```

You can run this and see for yourself by cloning my Negb project repository.

## Mistaken proof

David’s concern is that,
“Itâ€™s up to the programmer to realize that we have actually not created all of the proofs required to prove correctness.”
This concern arises from his thinking that the proof for
`negb_inverse`

goes through
even if you alter `negb`

so it always returns `true`

.

The version of `negb`

he defines that always returns `true`

actually already fails at the `negb_inverse`

theorem,
without need to proceed to trying to prove `negb_ineq`

.

You can see this in practice by pasting the bogus `negb`

definition into
`coqtop`

and then trying to complete the proof of the theorem,
but you can probably convince yourself without needing to do that
simply by considering the `false`

case.

The theorem’s claim is that `negb(negb(b)) == b`

.
In the false case, with the always-true `negb`

, we get:

```
negb(negb(b)) == b // the negb_inverse claim
--> consider the case where b = false
negb(negb(false)) == false
--> evaluate the inner negb application
negb(true) == false
--> evaluate the remaining negb application
true == false
--> contradiction! <--
```

If you flip the `case .True: return .False`

to
`return .True`

in the Swift version of `negb`

,
you’ll see it quickly find this failing case
using the test, as well:

```
Test Case '-[NegbTests.NegbTests testTheoremNegbInverse]' started.
*** Failed! Proposition: negb is its own inverse
Falsifiable (after 1 test):
False
*** Passed 0 tests
.
```

If you go the `coqtop`

route,
you’ll be able to discharge the `true`

case with `simpl. trivial.`

,
but using the `simpl.`

tactic in the false case leaves you
at the end step of our reasoning above,
trying to prove that `true = false`

.

If you’re in `coqtop`

, you’ll also quickly notice that
the proof David copied in for `negb_inverse`

was incomplete.
`destruct.`

leaves you with two subgoals left to prove,
corresponding to a version of the theorem with `b`

instantiated at each case of the enum.
You can complete the proof via `reflexitivity. Qed.`

,
which the book gets to a half-page later after some discussion.

## Proving the right thing and human misapprehension

A sound system won’t draw bogus conclusions, but that doesn’t mean we can’t misinterpret our own claims, whether they’ve been proven true or not.

David’s core concern about knowing you’ve proved what you want to prove is a real problem.

The problem doesn’t appear where he thought it did, in a theorem that he knew shouldn’t be provable but he thought still was.

The problem shows up in the same place that it did with the dependently typed flipped Boolean discussion, where the human is giving names and external meaning to the mathematical expression. In a sound system, the proofs we provide will be correct, but we can still misunderstand what the theorem we have just proved really means.

If we’re building on top of that proof, that misunderstanding will undoubtedly come to light as we try to use it to prove new claims. We just won’t be able to make a chain of reason from what we want to prove to what we did prove, because our new goal will depend on what we thought we proved, which was something different.

If what we thought we proved was the final achievement of our development, though, then we might not run into trouble till we try to actually use it to do something. Then we’ll see it breakdown at runtime, when it does what it in fact tells us on its face it does, which just so happens not to be what we read it as doing.