Wir verwenden JsCoq um Rocq in HTML Webseiten verwenden zu können. Verwendung:
Wir beginnen mit einfachen Aussagen in Rocq und Taktiken um mit Aussagen umzugehen.
In Rocq heißen Aussagen Prop und mit (X:Prop) legen wir fest, dass X eine Aussage ist. Wenn X
eine Aussage ist, schreiben wir (H:X)
um X anzunehmen und diese Annahme bekommt den Namen H.
Mit der Taktik assumption beweisen wir eine Aussage, die wir bereits als Annahme gegeben haben.
Die Aussage True ist immer wahr und kann mit der Taktik trivial bewiesen werden.
Wenn X und Y Aussagen sind ist X/\Y die Konjunktion von X und Y.
Um eine Konjunktion zu beweisen, müssen beide Teile der Konjunktion bewiesen werden.
Die Taktik split teilt eine zu beweisende Konjunktion in ihre beiden Teilaussagen auf und
erzeugt für jede ein neues Goal.
Mit dem Strich '-' deuten wir an, dass wir eines dieser Goals beweisen.
Wenn wir eine Konjunktion als Annahme haben, zerlegt die Taktik destruct die Konjunktion in
ihre beiden
Teilaussagen. In den rechteckigen Klammern werden die Namen für die Teilannahmen angegeben.
Die Aussage x = y besagt dass x und y gleich sind. Die Aussage x = x kann mit der
Taktik reflexivity bewiesen werden.
Mit (x:nat) legen wir fest, dass x eine natürliche Zahl ist.
Hat man H: x = y als Annahme, ersetzt die Taktik rewrite H alle Vorkommen von x
in der zu beweisenden Aussage durch y.
Jetzt seid ihr dran! In dieser Übung sollt ihr euch mit oben vorgestellten Taktiken vertraut machen.
In diesem Abschnitt betrachten wir Listen. Zur Einfachheit beschränken wir und auf Listen von natürlichen Zahlen. Wir definieren Listen wie folgt:
Üblicherweise schreibt man nicht cons x xs sondern x :: xs.
Folgendes Kommando aktiviert diese Notation in Rocq.
Wir beginnen mit einfachen Funktionen auf Listen. Mit match implementieren wir eine
Fallunterscheidung, ob eine Liste durch nil oder durch cons erzeugt wurde. Im Fall
für cons geben die beiden folgenden Namen die Variable für die Zahl und die restliche Liste an.
Funktionen können in Rocq auch Aussagen erzeugen. Folgende Funktion erzeugt eine Aussage, die gültig ist,
wenn die gegebene Liste nicht leer ist:
Diese Funktion berechnet die Länge einer Liste. Die Funktion inc erhöht eine gegebene
Zahl um eins. Das Schlüsselwort Fixpoint ist wichtig um Rocq mitzuteilen dass es sich um eine
rekursive Funktion handelt.
Mit eval simpl in können wir in Rocq einen Ausdruck auswerten, z.B. die Länge einer konkreten
Liste berechnen:
In Rocq können wir Ausdrücke teilweise auswerten, wenn nicht alle Parameter einer Funktion bekannt sind. Mit
Section und Variable können wir festlegen, dass xs eine Variable ist.
Definiert eine Funktion map, die eine Funktion f: nat -> nat auf die Elemente einer Liste
anwendet.
Bisher haben wir nur Funktionen auf Listen definiert. Nun wollen wir Eigenschaften dieser Funktionen
beweisen.
Wir haben bereits gesehen dass nil ++ xs zu xs evaluiert. Allerdings evaluiert
xs ++ nil nicht zu xs, da xs nicht bekannt ist.
Um zu beweisen dass xs ++ nil = xs benötigen wir strukturelle Induktion.
Die Taktik induction xs as [|x xs'] führt eine Induktion über die Liste xs aus. In den eckigen
Klammern werden die Namen angegeben. Im Fall für nil müssen keine Variablen vergeben werden, im Fall für
cons wird die Zahl x und die restliche Liste xs' genannt. Die Induktionshypothese bekommt den Namen IHxs'.
Mit der Taktik simpl wird ein Ausdruck vereinfacht. Das ist ähnlich zu der Evaluierung mit
Eval.
Beweist, dass |xs ++ ys| = |xs| + |ys|.
Beweist, dass map mit app verträglich ist:
JsCoq's homepage is at github https://github.com/jscoq/jscoq ¡Salut!