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?