When we try to prove that one general recursion defined in coq is actually correct, in the sense that the fixpoint gives exact the same result if we unfold it once. In words of Coq, it is
(well_founded R) gives a function that returns the proof that elements of type
A is accessible (in terms of
R). When proving the theorem, we would encounter in someplace that we need to prove that, function
F will always give the same result, even if the proof supplied to it for
forall y, R y x -> P x is different in the sense of Coq but identical in the sense of functional extensionality.
However, it’s strange that we need to prove such a thing when we haven’t touched it when we define the fixpoint through
Fix. The reason lies behind the definition of
Fix in the standard library.
Fix is given with the help of
The only difference is that,
well_founded R is omitted and at the end
forall x : A, Acc R x is added. I’ve stated that
well_founded R is a function that gives the proof for
Acc R x for any
x : A, which means these two terms are the same. Then comes the clue: the accessibility property adds to the complexity.
After analyzing the standard library, I founded the reason: For the definition of
Fix_F the proof is obtained through a lemma
Acc_inv, as the name suggest it obtain the proof of
y from the proof of
Fix is simply defined by
(fun (x : A) => Fix_F (Rwf x)), which has nothing related to recursion. However the theorem we want to prove is about recursion of
Fix. Obviously, the proof will fail without some more hypothesis. For the left hand side of the target, the hypothesis
Rwf is used only once, afterward the proof of
Acc is obtained by the
Acc_inv. On the right hand side the proof for
y is obtained by the
Rwf. The difference is the very reason for introduction of functional extensionality.
However there usually requires few efforts, as functional extensionality is quite straightforward property for most functions.