`well_founded_induction_type` vs `Fix`

[dunnl]

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?

[ybertot]

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.