Coq functional extensionality

Question

I have a goal with a function whose body I would like to rewrite, but some of the function arguments get in the way of the rewriting. I have recreated the situation with the identity function.

If the function is Defined, then it works, but when the function is a parameter and I have an axiom stating how to rewrite, I'm not able to rewrite.

I can only get it to work by assuming functional extensionality. Is it possible to somehow rewrite without assuming functional extensionality?

Axiom functional_extensionality: forall {A B} (f g:A->B) , (forall x, f x = g x) -> f = g.

Variables A B : Type.
Variable f : A -> B.

Definition Id (x : B) := x.         (* here my function is Defined *)

Goal (fun x => Id (f x)) = f.       (* I'd like to rewrite inside the fun *)

Proof. auto. Qed.                   (* This works (eta reduction). *)

Variable Id' : B -> B.              (* Here I don't have the function definition *)
Axiom ID     : forall x, Id' x = x. (* only proof that it does the same thing *)
Goal (fun x => Id' (f x)) = f. 
Proof.
  rewrite ID.                       (* this doesnt work *)
  eauto using functional_extensionality, ID. (* but this works *)

Answer 1

Unfortunately it is not possible to prove this without assuming functional extensionality; Coq requires that fun x => Id' (f x)) = fun x => f x holds "definitionally".

What does "definitionally" mean here? Briefly, it means that both terms must have the same normal form syntactically. Recall that in Coq, every term has a normal form induced (mainly) by beta reduction.

However, we only know that Id' x = x "judgementally". Thus, Coq can't perform the reduction Id' x ~> x, preventing both terms above from becoming equal "definitionally".

This is indeed a limitation of Coq's theory, which I understand is in place so type-checking remains decidable.

Another approach to completing this proof would be to derive that the only function satisfying this equation is fun x => x (parametricity). This would provide you a hypothesis Hid: ID' = (fun x => x) which you could use to complete the proof. Unfortunately Hid is not provable internally in Coq.