Prove map id = id in idris?

问题:

I'm just starting playing with idris and theorem proving in general. I can follow most of the examples of proofs of basic facts on the internet, so I wanted to try something arbitrary by my own. So, I want to write a proof term for the following basic property of map:

map : (a -> b) -> List a -> List b
prf : map id = id

Intuitively, I can imagine how the proof should work: Take an arbitrary list l and analyze the possibilities for map id l. When l is empty, it's obvious; when l is non-empty it's based on the concept that function application preserves equality. So, I can do something like this:

prf' : (l : List a) -> map id l = id l

It's like a for all statement. How can I turn it into a proof of the equality of the functions involved?

回答1:

You can't. Idris's type theory (like Coq's and Agda's) does not support general extensionality. Given two functions f and g that "act the same", you will never be able to prove Not (f = g), but you will only be able to prove f = g if f and g are defined the same, up to alpha and eta equivalence or so. Unfortunately, things only get worse when you consider higher-order functions; there's a theorem about such in the Coq standard library, but I can't seem to find or remember it right now.