I am trying to define a recursive predicate using well-founded fixpoints with the obligation to show F_ext when rewriting with Fix_eq. The CPDT says that most such obligations are dischargeable with straightforward proof automation, but unhappily this does not appear to be so for my predicate.
I have reduced the problem to the following lemma (from Proper (pointwise_relation A eq ==> eq) (@all A)). Is it provable in Coq without additional axioms?
Lemma ext_fa:
forall (A : Type) (f g : A -> Prop),
(forall x, f x = g x) ->
(forall x, f x) = (forall x, g x).
It can be shown with extensionality of predicates or functions, but since the conclusion is weaker than the usual one (f = g) I naively thought it would be possible to produce a proof without using additional axioms. After all, both sides of the equality only involve applications of f and g; how could any intensional differences be discerned?
Have I missed a simple proof or is the lemma unprovable?
You might be interested in this code I wrote a while ago, which includes variants of Fix_eq for various numbers of arguments, and don't depend on function extensionality. Note that you don't need to change Fix_F, and can instead just prove variants of Fix_eq.
To answer the question you asked, rather than solve your context, the lemma you state is called "forall extensionality".
It is present in Coq.Logic.FunctionalExtensionality, where the axiom of function extensionality is used to prove it. The fact that the standard library version uses an axiom to prove this lemma is, at the very least, strong evidence that it is not provable without axioms in Coq.
Here is a proof sketch of that fact. Since Coq is strongly normalizing*, every proof of x = y in the empty context is judgmentally equal to eq_refl. That is, if you can prove x = y in the empty context, then x and y are convertible. Let f x := inhabited (Vector.t (x + 1)) and let g x := inhabited (Vector.t (1 + x)). It is straightforward to prove forall x, f x = g x by induction on x. Therefore, if your lemma were true without axioms, we could get a proof of
(forall x, inhabited (Vector.t (x + 1))) = (forall x, inhabited (Vector.t (1 + x)))
in the empty context, and hence eq_refl ought to prove this statement. We can easily check and see that eq_refl does not prove this statement. So your lemma ext_fa is not provable without axioms.
Note that equality for functions and equality for types are severely under-specified in Coq. Essentially, the only types (or functions) that you can prove equal in Coq are the ones that are judgmentally equal (or, more precisely, the ones that are expressible as two judgmentally equal lambdas applied to provably-equal closed terms). The only types that you can prove not equal are the ones which are provably not isomorphic. The only functions that you can prove not equal are the ones which provably differ on some concrete element of the domain that you provide. There's a lot of space between the equalities that you can prove, and the inequalities you can prove, and you don't get to say anything about things in this space without axioms.
*Coq isn't actually strongly normalizing because there are some issues with coinductives. But modulo that, it's strongly normalizing.