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 *)