Wenn ich Function verwende, um eine nicht-strukturell rekursive Funktion in Coq zu definieren, verhält sich das resultierende Objekt merkwürdig, wenn eine bestimmte Berechnung angefordert wird. Anstatt das Ergebnis direkt anzugeben, gibt die Eval compute in ... -Direktive einen ziemlich langen (typischerweise 170 000 Zeilen) Ausdruck zurück. Es scheint, dass Coq nicht alles auswerten kann und daher einen vereinfachten (aber langen) Ausdruck anstelle nur eines Wertes zurückgibt.
Das Problem scheint von der Art zu kommen, wie ich die von Function generierten Verpflichtungen nachweise. Zuerst dachte ich, das Problem käme von den undurchsichtigen Begriffen, die ich benutzt habe, und ich habe alle Lemmas in transparente Konstanten umgewandelt. Gibt es übrigens eine Möglichkeit, die in einem Begriff auftretenden undurchsichtigen Begriffe aufzulisten? Oder eine andere Möglichkeit, undurchsichtige Lemmas in transparente zu verwandeln?
Ich bemerkte dann, dass das Problem genauer aus dem Beweis kam, dass die verwendete Reihenfolge begründet ist. Aber ich habe seltsame Ergebnisse.
Zum Beispiel definiere ich log2 für die natürlichen Zahlen, indem ich wiederholt div2 anwende. Hier ist die Definition:
Ich bekomme zwei Beweispflichten. Der erste überprüft, dass n die Beziehung lt in den rekursiven Aufrufen berücksichtigt und leicht bewiesen werden kann.
Der zweite prüft, ob lt eine fundierte Bestellung ist. Dies ist bereits in der Standardbibliothek nachgewiesen. Das entsprechende Lemma ist Coq.Arith.Wf_nat.lt_wf .
Wenn ich diesen Beweis verwende, verhält sich die resultierende Funktion normal. Eval compute in log24 10. gibt 3 zurück.
Aber wenn ich den Beweis selbst machen will, bekomme ich dieses Verhalten nicht immer. Erstens, wenn ich den Beweis mit Qed anstelle von Defined beende, ist das Ergebnis der Berechnung (selbst bei kleinen Zahlen) ein komplexer Ausdruck und keine einzelne Zahl. Also verwende ich Defined und versuche, nur transparente Lemmas zu verwenden.
Hier ist Lemma1 ein Beweis für die fundierte Induktion der natürlichen Zahlen. Auch hier kann ich bereits vorhandene Lemmas verwenden, zB lt_wf_ind , lt_wf_rec , lt_wf_rec1 in Coq.Arith.Wf_nat oder sogar well-founded lt . Das erste funktioniert nicht, es scheint, weil es undurchsichtig ist. Die drei anderen arbeiten.
Ich habe versucht, es direkt unter Verwendung der Standardinduktion auf die natürlichen Zahlen nat_ind zu beweisen. Dies ergibt:
Mit diesem Beweis (und einigen Varianten davon) hat log2 das gleiche seltsame Verhalten. Und dieser Beweis scheint nur transparente Objekte zu verwenden, also ist das Problem vielleicht nicht da.
Wie kann ich ein Function definieren, das verständliche Ergebnisse zu bestimmten Werten liefert?
Ich habe es geschafft, den Ort zu lokalisieren, der Probleme verursacht: es ist inversion H2. in lemma1 . Es stellt sich heraus, dass wir diese Fallanalyse nicht benötigen und intuition kann den Beweis beenden (es stimmt nicht mit dem Muster " H2 " überein):
Wenn wir lemma1 mit diesem Beweis verwenden, ergibt sich die Berechnung von log2 10 in 3 .
Übrigens, hier ist meine Version von lt_wf2 (es lässt uns auch berechnen):
Ich glaube das Mithilfe von Coqs Bewertungsmechanismen in Wut erläutert ein Blogbeitrag von Xavier Leroy diese Art von Verhalten.
es eliminiert den Beweis der Gleichheit zwischen den Köpfen, bevor es über die Schwänze zurückkehrt und schließlich entscheidet, ob eine Linke oder eine Rechte erzeugt werden soll. Dies macht den linken / rechten Teil des Endergebnisses abhängig von einem Beweisterm, der im Allgemeinen nicht reduziert wird!
In unserem Fall eliminieren wir den Beweis der Ungleichheit ( inversion H2. ) im Beweis von lemma1 und der Function Mechanismus macht unsere Berechnungen von einem Beweisausdruck abhängig. Daher kann der Bewerter nicht fortfahren, wenn n & gt; 1.
Und der Grund dafür, dass inversion H1. im Lemmagrund keinen Einfluss auf Berechnungen hat, ist, dass für n = 0 und n = 1 , log2 n im match Ausdruck als Basisfälle definiert sind.
Um diesen Punkt zu veranschaulichen, lassen Sie mich ein Beispiel zeigen, wenn wir die Auswertung von log2 n auf allen Werten n und n + 1 unserer Wahl verhindern können, wo n > 1 und nirgendwo sonst !
Wenn Sie dieses modifizierte Lemma in der Definition von log2 verwenden, sehen Sie, dass es überall außer n = 4 und n = 5 berechnet. Nun, fast überall - Berechnungen mit großen nat s können zu einem Stapelüberlauf oder einem Segmentierungsfehler führen, wie Coq uns warnt:
Warnung: Beim Arbeiten mit Stack kommt es zu einem Überlauf oder Segmentierungsfehler große Zahlen in nat (beobachtete Schwelle kann von 5000 bis 70000 variieren abhängig von Ihren Systemgrenzen und dem ausgeführten Befehl).
Und damit log2 für n = 4 und n = 5 auch für den obigen "fehlerhaften" Beweis funktioniert, könnten wir log2 wie folgt ändern
am Ende die notwendigen Beweise hinzufügen.
Der "fundierte" Beweis muss transparent sein und darf sich nicht auf Mustervergleiche auf Beweisobjekten verlassen, da der
Function -Mechanismus tatsächlich das lt_wf -Lemma verwendet, um den abnehmenden Abschlussschutz zu berechnen. Wenn wir uns den Ausdruck von Eval ansehen (in einem Fall, in dem die Auswertung keinen nat liefert), sehen wir etwas in dieser Richtung:
%Vor%
Es ist leicht zu sehen, dass x0 : Prop , also beim Extrahieren des Funktionsprogramms log2 in, sagen wir OCaml, gelöscht wird, aber der interne Evaluierungsmechanismus von Coq muss es verwenden, um die Beendigung sicherzustellen.
Das Reduktionsverhalten von Funktionen, die durch eine fundierte Rekursion in Coq definiert sind, ist im Allgemeinen nicht sehr gut, selbst wenn Sie Ihre Beweise für transparent erklären. Der Grund dafür ist, dass Begründungsargumente in der Regel mit komplizierten Beweisklauseln durchgeführt werden müssen. Da diese Beweisbegriffe letztendlich in fundierten rekursiven Definitionen auftauchen, wird die "Vereinfachung" Ihrer Funktion dazu führen, dass all diese Beweisbegriffe erscheinen, wie Sie bemerkt haben.
Es ist einfacher, sich auf benutzerdefinierte Taktiken und Lemmas zu verlassen, um auf diese Weise definierte Funktionen zu reduzieren. Erstens würde ich empfehlen, Program Fixpoint über Function zu bevorzugen, weil Letzteres viel älter ist und (glaube ich) weniger gut gepflegt wird. Sie würden also eine solche Definition erhalten:
Jetzt müssen Sie nur die program_simpl -Taktik verwenden, um Aufrufe von log2 zu vereinfachen. Hier ist ein Beispiel:
Tags und Links coq