# `well_founded_induction_type` vs `Fix`

If I am not mistaken, Coq.Init.Wf defines two transparent terms of precisely the same type, `well_founded_induction_type` and `Fix`. I understand how these functions “work” but I am not sure what the distinction is. Is there a strong reason to prefer `well_founded_induction_type` when writing proofs?

It seems that `Fix` is oriented towards defining recursive functions due to the rewriting lemma `Fix_eq`. I also see that there are several functions named `well_founded_induction_<foo>` with several values of `foo`, so these are clearly intended as induction principles. But in what sense then is `well_founded_induction_type` more oriented towards proofs than `Fix`? In the recursion chapter of CPDT, Chlipala defines a function by `Fix` and concludes the chapter with a comment I find cryptic:

One more piece of the full picture is missing. To go on and prove correctness of mergeSort, we would need more than a way of unfolding its definition. We also need an appropriate induction principle matched to the well-founded relation. Such a principle is available in the standard library, though we will say no more about its details here. `Check well_founded_induction`.

But I think any proof using `well_founded_induction_<foo>` could just as easily be written with `Fix`.

So why bother defining the induction principles?

Short answer: yes `Fix` supersedes `well_founded_induction_type` and is more practical thanks to the `Fix_eq` companion theorem.

well_founded_induction and Fix coexist for historical reasons. Well founded induction existed first, and was advertised, mainly by Christine Paulin-Mohring, as the best way to define general recursive function in Coq. This relied extensively on dependent types: the approach that Christine Paulin-Mohring advertised is that everything you need to know about the function you are defining should be expressed in the type of this function.

So if you need to define a function that works on any argument satisfying a predicate `P : A -> Prop` and returning a value of type `B x`. you would need to define, using `well_funded_induction` a function of type
`forall x: A, P x -> B x`
Of course, this would look very much like a proof by induction, …

I was quite unhappy with this siutation: if somebody defined a function in that way and forgot to state an important property of the result as part of `B`, you had no other solution that redoing the definition, thus obtaining a different object, etc. I wished to have way to do more proofs on an already defined function.

For me the quintessential property that a recursively defined function enjoys is that it is a fixed-point of the “defining equation”. So, with Antonia Balaa who worked on a Phd under my supervision at the time, we embarked on looking for a way to prove that fixed point equation. We toiled on the problem for quite some time, and to be frank, I believe it is Loïc Pottier who gave us the solution. We wrote an article on this that was published at the TPHOLS conference in 2000 (Portland Oregon). This article was based on the pre-existing `well_founded_induction` concept.

When reading this article, Christine Paulin figured out that the proof of the article could be made simpler if the definition of `well_founded_induction` was changed slightly, so she implemented `Fix` and `Fix_eq` in the Coq system. and we all agreed that `Fix` could indeed replace `well_founded_induction`, but the replacement was never enacted.

Just for the record, Antonia Balaa and I kept working on fixed point equations and this work lead to the `Function` command that is still present in Coq today (beginning of 2020), but should be superseded by `Equations` in the future.

3 Likes