## The problem

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

1 | Fix : forall (A : Type) (R : A -> A -> Prop), well_founded R -> |

where `(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.

## Analysis

Internally, `Fix`

is given with the help of `Fix_F`

:

1 | Fix_F: forall (A : Type) (R : A -> A -> Prop) (P : A -> Type), |

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 `Acc`

for `y`

from the proof of `Acc`

for `x`

, while `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.