Coq : simulate function extensionality theorem

Question

Intuitively, when two functions g and h are equal for all x, we can imagine that g = h, and therefore replace all occurrences of f g into f h. This is what we call function extensionality. However, in Coq function extensionality is not added by default, so we need it, we need to add an axiom.

However, I'd like to avoid to use this axiom, and try to find a theorem that is equivalent in practive, that would look like "for all f that are inductive functions that output an inductive type, forall g and h, f g = f h". In particuliar, f cannot be identity, because the identity function is not an inductive type.

For now, when I need to do something like this, I need to manually handle all the cases of f, and it can be quite long. Do you know if I can write a theorem like this in pure Coq, or maybe if it's not possible, can I create a tactic that would generate this proof for all f ?

Thank you!

Answer 1

One example on how to build a "functional" structure that has extensionality is the finfun datatype in the Mathematical Components library.

Given a finite type T, a finitely-supported function {ffun T -> A} is just a #|T|.-tuple A, that is to say, a table assigning every element of T to some element A. You can overload application so f x := nth f (rank x) where rank x returns the "index" of x : T.

It is the case that ffunP: forall x, f x = g x <-> f = g forall f, g : {ffun T -> A}. Why? Indeed, the key point is that we represent such functions by tables, then Coq indeed can check that such "canonical" representation meets extensionality.

You will have to perform similar tricks to embed your structure with extensionality, which is usually painful, so that's why few people bother and just add the axiom. In particular, note that in order to have an extensional representation, you will need to construct "canonical" representatives of each object in the corresponding equality class.

For example, given some kind of lambda terms and renaming, you would need to canonically rename terms and construct a type that indicates that such term is in canonical form. This is not easy in general.