Show id = id card in idris?

Question

I am just starting to play with idris and the theorem proving in general. I can follow most examples of evidence of basic facts on the Internet, so I wanted to try something random on my own. So, I want to write a proof for the following basic mapping property:

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 the card identifier l. When l is empty, it is obvious; when l is not empty, it is based on the notion that a function application maintains equality. So, I can do something like this:

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

It is like an expression for everyone. How can I turn it into a proof of the equality of the functions involved?

Answer 1

You can not. A theory like Idris (e.g. Kok and Agda) does not support general extensiveness. Given two functions f and g that "act the same", you can never prove Not (f = g) , but you can prove f = g if f and g defined the same, up to alpha and this equivalence. Unfortunately, the situation only gets worse when you consider functions of a higher order; There is a theorem on such in the standard library of Coq, but I can not find or remember it right now.