Dimostrazione della mappa id = id in idris?

Question

Sto appena iniziando a giocare con idris e teorema dimostrando in generale. Posso seguire la maggior parte degli esempi di prove di fatti di base su Internet, quindi ho voluto provare qualcosa di arbitrario per conto mio. Quindi, voglio scrivere un termine la prova per la seguente proprietà di base della mappa:

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

Intuitivamente, posso immaginare come la prova dovrebbe funzionare: Prendere una lista L arbitraria e analizzare le possibilità di mappa id l. Quando sono vuoto, è ovvio; quando l è non vuoto si basa sul concetto che l'applicazione di funzione preserva l'uguaglianza. Quindi, posso fare qualcosa di simile:

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

E 'come una dichiarazione per tutti. Come posso trasformarlo in una prova dell'uguaglianza delle funzioni coinvolte?

Answer 1

Non è possibile. La teoria dei tipi di Idris (come quella di Coq e di Agda) non supporta l'estensionalità generale. Date due funzioni f e g che "comportano lo stesso", non sarai mai in grado di provare Not (f = g), ma sarai in grado di provare solo f = g se f e g sono definiti uguali, fino a equivalenza alfa ed eta o così. Sfortunatamente, le cose peggiorano solo se si considerano le funzioni di ordine superiore; c'è un teorema su tale nella libreria standard di Coq, ma non riesco a trovarlo o ricordarlo in questo momento.