Karte beweisen id = id in idris?

Question

Ich fange gerade an zu spielen mit Idris und Theorem Beweisen im Allgemeinen. Ich kann den meisten Beispielen von Beweisen für grundlegende Fakten im Internet folgen, also wollte ich etwas Eigenes ausprobieren. Also, ich will einen Beweis Begriff für die folgende grundlegende Eigenschaft der Karte schreiben:

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

Intuitiv kann ich mich vorstellen, wie der Beweis funktionieren soll: Nehmen Ihnen eine beliebige Liste l und analysiert die Möglichkeiten für Karte ID l. Wenn ich leer bin, ist es offensichtlich; Wenn l nicht leer ist, basiert es auf dem Konzept, dass die Funktionsanwendung die Gleichheit erhält. Also, ich kann etwas tun:

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

Es ist wie eine ist für alle Aussage. Wie kann ich daraus einen Beweis für die Gleichheit der Funktionen machen?

Answer 1

Sie können nicht. Idris 'Typentheorie (wie Coqs und Agdas) unterstützt keine allgemeine Extensionalität. Bei zwei Funktionen f und g, die "gleich funktionieren", können Sie Not (f = g) nie beweisen, aber Sie können f = g nur dann beweisen, wenn f und g gleich definiert sind, bis hin zu Alpha und Eta. Leider werden die Dinge nur schlimmer, wenn man Funktionen höherer Ordnung in Betracht zieht; Es gibt einen solchen Satz in der Coq-Standardbibliothek, aber ich kann ihn jetzt nicht finden oder merken.