Understanding Fix_eq in Coq

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

Fix : forall (A : Type) (R : A -> A -> Prop), well_founded R ->
forall P : A -> Type,
(forall x : A, (forall y : A, R y x -> P y) -> P x) ->
∀ x : A, P x
Fix Rwf P F x = F x (fun (y : A) (_ : R y x) => Fix Rwf P F y)

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.


Internally, Fix is given with the help of Fix_F:

Fix_F: forall (A : Type) (R : A -> A -> Prop) (P : A -> Type),
(forall x : A, (forall y : A, R y x -> P y) -> P x) ->
forall x : A, Acc R x -> P x

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.