Herbrand's Unification Theorem

Stream: lean4

[Julien Marquet]

Hello,

I proved (over the course of a 2 weeks' ~speedrun) Herbrand's [1] unification theorem [2] in the special case of the terms that appear in GoI flows [3] [4].

See the statement here !

---

I am interested in formalizing flows [3] [4], which are object that allow to present low-level computations in a satisfactory way (up to my understanding).
The first step towards this goal is this theorem that I proved.

I tried to formalize the theorem as quickly as possible, so the code is far from being perfect... but I will (at some point within the next 9 months) get back to it and clean it up.

There may be some things around here (nontrivial inductions, finiteness and lower bounds) that may be relevant for mathlib4 if they were cleaned up a bit, I'm willing to spend some time at some point in a fairly near future on it if you think this is worth the effort.

The repo is here : https://github.com/thejohncrafter/flows !

---

[1] : Lectures on Herbrand, with historical notes https://arxiv.org/pdf/0902.4682.pdf

[2] : Jacques Herbrand's dissertation (in French), pp. 96-97

[3] : Geometry of Interaction analyzed with flows https://www.normalesup.org/~bagnol/notes/goi-torino.pdf

[4] : Notes on unification using flows (in French) https://www.normalesup.org/~bagnol/notes/unification.pdf (in French)

[Franz Kronseder]

Hello Julien.Marquet :) Thank you for contributing this Herbrand-Stuff here ...
FYI I have been passionate amateur consumer of the leanprover-zulip-chats about MathLib-Worlds since XMas-2020...
I remember hearing abt Herbrand-Universes while learning "Programming in Prolog" during my TUM-Inf years in the early 1980s.
... looking fwd to refreshing my school-french reading-skill by reading your (in French) URLs ...
Cheers from Muenchen-Moosach, Franz