Sammlung von Coq-Übungen
Beschreibung
Ich versuche bzw. habe hier versucht, eine Mini-Sammlung an Coq-Übungen zu erstellen. Diese sind teilweise bewusst einfach, um sich an die Standard-Taktiken zu gewöhnen.
Aufbau
Die Files bauen teilweise inhaltlich aufeinander auf, sodass es sinnvoll ist, diese in einer bestimmten Reihenfolge zu bearbeiten. Ich versuche das durch die Spalte "Abhängigkeiten" in der File-Liste darzustellen.
File-Liste
| File | Beschreibung | Anmerkungen | Abhängigkeiten |
|---|---|---|---|
| IntroElim | Im Prinzip eine Sammlung der grundlegenden Einführungs- und Eliminierungsregeln, ähnlich zum Fitch-Kalkül. | ||
| Laws | Eine Sammlung verschiedener Gesetze der klassischen Logik | IntroElim | |
| SomeExamples | Verschiedene zusammengewürfelte Beispiele. | Laws | |
| Forall | Simple Beispiele zu Allquantoren | IntroElim | |
| Exists | Simple Beispiele zu Existenzquantoren | IntroElim | |
| Groups | Anwendungsbeispiel für First-Order-Logic | Die Darstellung von Gruppen, wie ich sie hier benutze, ist meinen Augen nicht wirklich praktisch für die Weiterverwendung. Vielmehr dient die Darstellung der expliziten Nutzung von möglichst vielen Elementen von FOL. | Forall, Exists |
| Induction | Der Versuch, Induktion anschaulich mit Hilfe von Coq an Beispielen zu zeigen. | Könnte etwas komplex zum Einstieg sein. Verständnis von FOL in Coq hilfreich. | LawsFOL |
Installation
Dieses Projekt benötigt keine detailreiche Installationsanleitung, man kann es einfach auf Gitlab klonen:
git clone git@gitlab.cs.fau.de:oc59yqul/coq-exercises.gitUsage
Dieses Projekt dient zum Üben von Coq-Beweisen. Entsprechend sind die Beweise noch nicht vorhanden, sondern sollen aktiv eingefügt werden. Insbesondere stellt dieses Projekt also keine Library oder sonst etwas dar.
Tipps zur Bearbeitung
- Die einzelne Theoreme sind jeweils noch nicht bewiesen. Um die Files sinnvoll zu bearbeiten, sollte man die Zeile
Admitted.durch einen entsprechenden Beweis gefolgt vonQed.ersetzen. - Die Verwendung von
tauto.ist hilfreich, um sich von der Beweisbarkeit eines Theorems zu überzeugen. Achtung: Wenntauto.das aktuelle Goal nicht löst, heißt das nicht zwingend, dass es unlösbar ist.tauto.arbeitet nur auf rein logischen Aussagen. - Mit dem Befehl
Restart.kann man den Beweis des aktuellen Theorems zurücksetzen. Das ist nützlich, um verschiedene Beweismethoden aufzuschreiben. - Mit
unfold "~ _".kann man die Coq-Definition der Negation sichtbar machen.
Contributing
Ich freue mich über konkrete Verbesserungsvorschläge. Diese können
- völlig unkonkret über Issues oder
- konkret über Patches oder Merge Requests
eingebracht werden. Bei Bedarf füge ich einzelne Personen auch gerne als Developer dem Repo hinzu, falls dies den Workflow erleichtert.
Aktuelle TODO's
Eine (sicherlich nicht vollständige Liste) ist hier zu finden:
- Alle Issues, die bisher nicht assigned sind.
-
Induction.v könnte man auf verschiedene Weisen erweitern:
- Weitere Funktionen selbst definieren, dazu geben wir ein paar Tests (Beispiele und Theoreme) vor. Vermutlich ähnlich zu zu SemProg/Software Foundations vom Prinzip her, macht aber vermutlich auch Sinn, Beispiele für solche rekursiven Definition gibt es ja schon.
- Weitere rekursive Datentypen, eventuell auch mal eine Struktur ohne irgendeinen größeren Hintergrund.
Feedback & Kritik
Auch mit Blick auf eine Erweiterung der Aufgaben hier freue ich mich über potenzielles Feedback, z.B. per Mail oder Issue. Es ist interessant zu wissen, welchen Nutzen dieses kleine Projekt hat.
Kontakt
Ich bin u.A. per E-Mail erreichbar.