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.
## 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.
@@ -16,26 +22,37 @@ Die Files bauen teilweise inhaltlich aufeinander auf, sodass es sinnvoll ist, di
| 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 |
## Makefile
## Installation
Dieses Projekt benötigt keine detailreiche Installationsanleitung, man kann es einfach auf [Gitlab](https://gitlab.cs.fau.de/oc59yqul/coq-exercises) klonen:
Das Projekt enthält ein `Makefile`. _Ich bin kein Experte für Makefiles. Ich freue mich entsprechend über Verbesserungsvorschläge hierzu!_
Durch Ausführung von `make all` werden alle Coq-Dateien kompiliert, außerdem finden sich unter `/public` entsprechende HTML-Files.
## Usage
## Tipps zur Bearbeitung
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 von `Qed.` ersetzen.
- Die Verwendung von `tauto.` ist hilfreich, um sich von der Beweisbarkeit eines Theorems zu überzeugen. _Achtung: Wenn `tauto.` 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.
## Feedback & Kritik
## Contributing
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.
Ich freue mich über konkrete Verbesserungsvorschläge. Diese können
- völlig unkonkret über Issues oder
- konkret über Patches oder Merge Requests
## Mitmachen
eingebracht werden. Bei Bedarf füge ich einzelne Personen auch gerne als Developer dem Repo hinzu, falls dies den Workflow erleichtert.
Ich bin kein Experte in vielerlei Hinsicht. Deshalb freue ich mich über (fast) jede Hilfe. Einfach melden, ggf. einfach eine "Access Request" stellen oder per Mail (siehe Profil) melden.
### Aktuelle TODO's
Eine (sicherlich nicht vollständige Liste) ist hier zu finden:
...
...
@@ -43,3 +60,11 @@ Eine (sicherlich nicht vollständige Liste) ist hier zu finden:
-[Induction.v](src/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](ole.elliger@fau.de) erreichbar.
