Wykazać id mapy = id w idris?

Question

Właśnie zaczynam grać z idrisem i dowodzeniem twierdzeń w ogóle. Mogę śledzić większość przykładów dowodów podstawowych faktów w Internecie, więc chciałem spróbować czegoś samowolnego. Tak, chcę napisać próbny termin na następny podstawowych właściwości mapy:

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

Intuicyjnie, mogę sobie wyobrazić, jak dowód powinno działać: Weźmy dowolny lista L i analizować możliwości Map ID l. Kiedy l jest puste, to oczywiste; kiedy l nie jest pusta, opiera się na koncepcji, że aplikacja funkcjonalna zachowuje równość. Tak, mogę zrobić coś takiego:

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

To jak dla całego rachunku. Jak mogę go przekształcić w dowód równości zaangażowanych funkcji?

Answer 1

Nie możesz. Teoria typu Idrisa (taka jak Coq's i Agda) nie wspiera ogólnej ekstensjonalności. Biorąc pod uwagę dwie funkcje, które "działają tak samo", nigdy nie będziesz w stanie udowodnić, że Not (f = g), będziesz w stanie udowodnić, że f = g są zdefiniowane tak samo, aż do równoważności alfa i eta. Niestety, rzeczy się tylko pogarszają, gdy weźmiesz pod uwagę funkcje wyższego rzędu; istnieje twierdzenie o tym w standardowej bibliotece Coq, ale nie mogę tego teraz znaleźć ani zapamiętać.