# \`well\_founded\_induction\_type\` vs \`Fix\`

**URL:** <https://discourse.rocq-prover.org/t/well-founded-induction-type-vs-fix/768>\
**Category:** Using Rocq\
**Created:** [April 12, 2020, 6:57pm UTC](https://discourse.rocq-prover.org/t/well-founded-induction-type-vs-fix/768 "2020-04-12T18:57:58Z")\
**Posts on this page:** 2\
**Page:** 1

<div class="post-metadata">

**Author:** ![dunnl](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/dunnl/32/296_2.png) [@dunnl](https://discourse.rocq-prover.org/u/dunnl)\
**Post date:** [April 12, 2020, 6:57pm UTC](https://discourse.rocq-prover.org/t/well-founded-induction-type-vs-fix/768/1 "2020-04-12T18:57:58Z")

</div>

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](http://adam.chlipala.net/cpdt/html/GeneralRec.html), 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?

---

<div class="post-metadata">

**Author:** ![ybertot](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ybertot/32/61_2.png) [@ybertot](https://discourse.rocq-prover.org/u/ybertot)\
**Post date:** [April 14, 2020, 7:23am UTC](https://discourse.rocq-prover.org/t/well-founded-induction-type-vs-fix/768/2 "2020-04-14T07:23:42Z")

</div>

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](https://www-sop.inria.fr/members/Yves.Bertot/Old-ftp-marelle/tphols2000.ps.gz) 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.