Hahn-Banach

Stream: maths

[Patrick Massot]

At the Big Proof 2 meeting, Marie Kerjean gave a nice talk about her proof of Hahn-Banach in Coq. She is a beginner who started to learn Coq/SSReflect only six months ago, as a post-doc working with @Assia Mahboubi. I thought it was a nice opportunity to learn how to translate from Coq to Lean, hoping she was not expert enough in SSReflect obfuscation to prevent me from understanding her code. For this experiment, I resisted the temptation to think about the proof, or to install Coq and watch the proof state evolving, I really followed the code, with only local adaptations. The original is at https://github.com/math-comp/analysis/blob/hb/hahn_banach.v (see also an abstract) and the translation at https://gist.github.com/PatrickMassot/328b58599618f8642da7fd45a5457f17. It took me about one day to do it, which I think is pretty encouraging. So there is hope to be able to port more things from mathcomp.

I hope this can be used a Rosetta stone. But of course it would also be interesting to learn from the proof itself, and maybe find a better way. There are two main independent questions: how to use classical logic? how to handle partial function? In particular she uses https://github.com/math-comp/analysis/blob/hb/hahn_banach.v#L21-L27 which is of course completely useless in Lean. Can we use the fact those things are more natural in Lean in order to make the proof nicer? About partial functions, the main trick of this formalization is to consider linear forms that are defined everywhere, but bounded only on a subspace, and handle partiality using relations. Could we use what @Jeremy Avigad did when he worked on calculus for partial functions? Last note: the statement is cheating a bit because the map to be extended is assumed linear everywhere (but bounded only on a subspace of course). So, in order to get the math version, we would need to prove that linear forms on subspaces can be extended as linear forms.

I hope some form of this can be PR'ed at some point, but let's discuss first.

[Scott Morrison]

Nice! Do you have a sense why your file is only 1/3 the length, if you were following the code? Is it that you found more prerequisites already available in mathlib, or was there genuinely some compression possible?

[Marie Kerjean]

Hi Scott ! One reason may be that our Coq proof spends some time proving a fixpoint lemma and Zorn (we wanted a new demonstration of Zorn using only the axiom of choice in Prop).

[Scott Morrison]

I see. Is there an axiomatic difference then in what Patrick did (pretending otherwise Lean and Coq have the same axioms?) Or did he already have that "stronger" version of Zorn available?

[Sebastien Gouezel]

Very nice! Except that the statement is not exactly the one we want, as you explain. To apply it to get the classical version, you would need to start from a linear functional on a subspace and extend it to the whole space, which means doing Zorn again (essentially with the same arguments except that you don't need to check the boundedness). I think a direct proof using just one Zorn instead of two would be more satisfactory (and shorter), but maybe harder to formalize?

[Sebastien Gouezel]

In fact I guess the very same proof works just under the assumption that the function is linear on the subspace. Then the extension problem becomes trivial (just put 0 or anything else outside).

[Marie Kerjean]

@Sebastien Gouezel Yes, indeed, that was the idea of the statement - any linear function on a subspace can be extended by 0 outside of this subspace. We should have commented that..

[Sebastien Gouezel]

In Patrick's version, f should be linear on the whole space, so he can't start from a linear functional on the subspace and extend it by 0 outside as this breaks linearity. What about your version?

[Patrick Massot]

It's the same in Marie's version. I thought she wanted to prove existence of supplement of subspaces (which is very much related, but not exactly the same, I think). But indeed we could probably modify the proof. Linearity outside the subspace can't be used in any serious way.

[Patrick Massot]

Scott, the difference is mainly Zorn. I also used https://github.com/leanprover-community/mathlib/blob/master/src/analysis/convex.lean#L567-L570, and maybe a couple of other small lemmas from mathlib.

[Patrick Massot]

About the global linearity issue: Assia just fixed the Coq version https://github.com/math-comp/analysis/commit/c5c2cfdef78aee5b85dfc9e7ba576573afbdf0a9

[Patrick Massot]

I'll fix my translation tomorrow if nobody does it while I sleep

[Patrick Massot]

But I'm still interested in more substantial improvements by experts here.

[Marie Kerjean]

Just to mention, Zorn is already proven in Mathcomp Analysis (classical_sets) and we were just interested in another proof. As shown by Assia, requiring linearity on subspaces just asks for minor modifications, but it might change a few things concerning the application of HB thm to normed spaces which we formalized too.

[Patrick Massot]

I updated my translation. Now the final statement is the reasonable one.