This post dissects a very short yet fascinating and enigmatic proof that can be found in the Logic module of the standard library of the Lean proof verifier:

theorem iff_not_self : ¬(a ↔ ¬a)
  | H => let f h := H.1 h h
         f (H.2 f)

OK, the fact being proved isn’t enigmatic — it’s stating that a proposition’s truth value is never the same as its own negation’s — but the proof thereof sure is. If that looks to you like some incomprehensible formal logic circling to eat its own tail, that’s because it kinda is.

However, it’s written extremely densely, which inhibits comprehension — which is sad, because the way it works is very interesting. It’s quite the rabbit hole, though, so let’s take our trusty spade and start digging. The very first thing we encounter is that Lean implicitly converts the ¬(a ↔ ¬a) into (a ↔ ¬a) → False. This is because Lean uses dependent type theory to represent logical statements and their proofs, so we need to discuss how these kinds of theories are used with formal logic.

Lean isn’t alone is doing this. Type theories are a common way to implement formal logic in proof assistants/verifiers, by having the types represent mathematical statements and instances of a type represent a proof of that type. An advantage of this technique is that a proof of P∧Q is trivial to generate from proofs of P and Q by modelling it with a type constructor as a product type, and similarly, a proof of P∨Q modeled as a sum type is trivial to construct from a proof of either P or Q. Also, everyone who’s programmed has some intuition regarding type theory even if they’ve never studied it.

There are disadvantages as well, though. It’s very easy to get confused between the various abstract ensembles of types, the specific types you’re working with, and the instances of these types you’re trying to construct. Problems spanning across these levels usually have solutions that are very short (slightly tweaking a statement to trigger pattern matching, or finding just the right arguments to a type constructor) but difficult to find. And while the proof assistants can often provide hinting within any one level, they generally can’t provide any guidance in spanning across them.

The other big disadvantage is they don’t handle negation as well as they handle the rest of the logical constructs. This is because there’s no relationship between a proof of P and of ¬P since at most one will exist, and having no relationship in logic means there’s nothing for a type theory to model. The typical way to handle this is to introduce False as either an instance of type Bool or as a type which by definition has no instances, and make it subject to special rules like False→P holds for every proposition P and there are no tautologies Q for which Q→False holds. Once False is defined, ¬P gets defined to be P→False.

And that’s why we’re now looking at

theorem iff_not_self : (a ↔ ¬a) → False
  | H => let f h := H.1 h h
         f (H.2 f)

The next question is what is that | doing there? I can’t find this in Lean’s documentation anywhere, which seems to always show theorems being proven by assigning them a proof with :=. (Lean’s syntax is undocumented and I’m not the only one bothered by that.) Experimentation indicates this is a function builder syntax, which we can write with typical lambda notation by

theorem iff_not_self : (a ↔ ¬a)→False :=
  λ H => let f h := H.1 h h
         f (H.2 f)

What’s this? Our theorem is a function? In this case, yes, because of how implication is handled. The way it works is that P→Q is modeled as function mapping proofs of P into proofs of Q. Here, we have a function that maps proofs of a ↔ ¬a to proofs of False. Does this mean we get to see a proof of False? Only if we can provide the function with a proof of a ↔ ¬a — but those don’t exist. Constructing a function that maps P to False is constructing a refutation of P, which serves as a proof of ¬P.

It might be clearer to add a type annotation to H:

theorem iff_not_self : (a ↔ ¬a)→False :=
  λ H:(a ↔ ¬a) => 
      let f h := H.1 h h
      f (H.2 f)

Or maybe it just adds clutter. That probably depends on how familiar you are with Lean (or closely related systems like Coq). For this article, I’ll keep them in the proofs, while retaining awareness that Lean can infer them automatically.

The next thing we dig up are the mysterious fields of H, H.1 and H.2. It directly follows from P↔Q that P→Q and Q→P, so for convenience Lean makes those available as the fields 1 and 2 of “Iff types”. We can give those names, and include the unnecessary but clarifying type annotations:

theorem iff_not_self : (a ↔ ¬a)→False :=
  λ H:(a ↔ ¬a) =>
      have ana : a → ¬a := H.1
      have naa : ¬a → a := H.2
      let f h := ana h h
      f (naa f)

Up until now, our digging has been tedious de-sugaring of Lean syntax and annotating of directly inferable types. But now we hit paydirt and actually get to the fun bit: doing logic! First, it’ll be helpful to convert the ¬a into a→False and give a name to naa f:

theorem iff_not_self : (a ↔ ¬a)→False :=
  λ H:(a ↔ ¬a) =>
      have ana : a → (a→False) := H.1
      have naa : (a→False) → a := H.2
      let f h := ana h h
      let naaf := naa f
      f naaf

This reveals what’s going on with that f function. ana is a function which takes two proofs of a and returns a proof of False. So what f does is takes a proof of a (called h) and calls ana with it twice, returning the resulting proof of False, giving f the type a→False. We can annotate that:

theorem iff_not_self : (a ↔ ¬a)→False :=
  λ H:(a ↔ ¬a) =>
      have ana : a → (a→False) := H.1
      have naa : (a→False) → a := H.2
      have f : a→False := λ h => ana h h
      let naaf := naa f
      f naaf

What does naa do? It takes a function that refutes a and returns a proof of a. And we just saw that f is a function which refutes a! So naaf := (naa f) is a proof of a.

Finally, since f is a function that maps proofs of a to False, f naaf is a proof of False. Wait, earlier I said that there were no proofs of False, yet here one is. The thing is the proof was constructed from a proof of a ↔ ¬a (named H), so what we’ve really proven is that (a ↔ ¬a)→False, i.e., ¬(a ↔ ¬a), and QED.

So, here we see an extremely elegant proof that uses gemination (ana h h) to generate a refutation (f : a→False) that establishes an attestation (naaf := naa f) that generates a contradiction (f naaf). And all that elegance is hidden away because it’s written as ¬(a ↔ ¬a) | H => let f h := H.1 h h; f (H.2 f) from a misplaced value on extreme brevity.