↑Programmieren in Gallina

Taktiken

Inhaltsverzeichnis

1. Hilfsbefehle
2. Assistiertes Schließen
3. Vorwärtsschließen
4. Definition vermittels Taktiken
5. Kunstgriffe
6. Taktiken für Allquantoren
7. Taktiken für Existenzquantoren

Hilfsbefehle

Assistiertes Schließen

Rüchwärtsschließen. Man arbeitet sich also von der Wurzel des Beweisbaums bis zu Blättern durch.

Γ ⊢ ?: A    Γ ⊢ ?: B
────────────────────
    Γ ⊢ ?: A∧B

Γ, a: A, b: B ⊢ ?: C
────────────────────
  Γ, h: A∧B ⊢ ?: C

Γ, a: A ⊢ ?: B
──────────────
 Γ ⊢ ?: A → B

Γ ⊢ f: A → B    Γ ⊢ ?: A
────────────────────────
        Γ ⊢ ?: B

 Γ ⊢ ?: A
──────────
Γ ⊢ ?: A∨B

 Γ ⊢ ?: B
──────────
Γ ⊢ ?: A∨B

Γ ⊢ h: A∨B    Γ, a: A ⊢ :?    Γ, b: B ⊢ :?
──────────────────────────────────────────
                  Γ ⊢ ?:

Kurzes Beispiel:

───────────────── exact a
a: A, b: B ⊢ a: A
───────────────── destruct h as (a, b)
  h: A∧B ⊢ a: A
────────────────── intro h
⊢ (h ↦ a): A∧B → A

Die Implementierung:

Theorem projl (A B: Prop):
  A /\ B -> A.
Proof.
  intro h.
  destruct h as (a, b).
  exact a.
Qed.

Die integrierte Entwicklungsumgebung zeigt hierbei nach jedem Schritt die verbleibenden Ziele und die vorhandenen Antezedenzen an.

Vorwärtsschließen

Beim Rückwärtsschließen führt man verbleibende Ziele bei einfacheren Teilbeweisen schrittweise auf Unterziele zurück.

Theorem contraposition (A B: Prop):
  (A -> B) -> (~B -> ~A).
Proof.
  (* unfold not. *)
  intro h. intro nb. intro a.
  apply nb. apply h. exact a.
Qed.

In der integrierten Entwicklungsumgebung sieht man den folgenden Verlauf der verbleibenden Ziele:

Die Taktik assert ermöglicht es nun, innerhalb des Rückwärtsschließens abschnittsweise ein Vorwärtsschließen zu vollführen. Dies geschieht, indem einem neuen Bezeichner ein Term zugewiesen wird, den man mit den im Kontext vorhandenen Variablen konstruiert. Der Bezeichner steht daraufhin ebenfalls als Variable im Kontext zur Verfügung. Der Vorgang läuft also gleichermaßen ab, wie die Zuweisung in der Programmierung.

Theorem contraposition (A B: Prop):
  (A -> B) -> (~B -> ~A).
Proof.
  intro h. intro nb. intro a.
  assert (b := h a).
  assert (contradiction := nb b).
  exact contradiction.
Qed.

Die Konstruktion des Terms lässt sich auch in einem Rutsch bewältigen:

  intro h. intro nb. intro a.
  exact (nb (h a)).

Oder man gibt auf Anhieb den gesamten Beweisterm an:

  exact (fun h nb a => nb (h a)).

Zum Vergleich die Zuweisung:

fun h nb a => let b := h a in nb b

Zu beachten wäre noch, dass assert die innere Struktur des notierten Terms vergessen lässt. Es bleibt nur die Information übrig, dass eine Variable mit einem bestimmten Typ konstruiert werden konnte. Möchte man den Term beibehalten, ersetzt man den Befehl assert schlicht durch pose oder set. Bei set wird zusätzlich im Ziel die Substitution jedes Vorkommens der Terms durch die Variable vorgenommen. Vermittels unfold lässt sich die Variable wieder durch den ursprünglichen Term ersetzen.

Theorem contraposition (A B: Prop):
  (A -> B) -> (~B -> ~A).
Proof.
  intro h. intro nb. intro a.
  pose (b := h a).
  pose (contradiction := nb b).
  unfold b in contradiction.
  exact contradiction.
Qed.

Definition vermittels Taktiken

Bisher wurde die Definition einer Funktion in der Form

Definition f (n: nat): nat := 2*n.

notiert. Alternativ dürfen zur Konstruktion eines Terms ebenfalls Taktiken zum Einsatz kommen. Man notiert:

Definition f (n: nat): nat.
Proof.
  assert (y := 2*n).
  exact y.
Defined.

Kunstgriffe

In das Maschinenwerk der Taktiken wurde einige Funktionalität verbaut, die die Erstellung von Beweisen ergonomischer macht.

Die Taktik intros ermöglicht es, die durch intro bewerkstelligte Einführung einer Annahme und die mit destruct bewerkstelligte Zerlegung dieser in einem Zug auszuführen. Hiermit bleibt erspart, die Annahme mit einer Hilfsvariable benennen zu müssen.

Goal forall A B: Prop,
  A /\ B -> B /\ A.
Proof.
  intro A. intro B. intro h.
  destruct h as (a, b).
  exact (conj b a).
Qed.

Goal forall A B: Prop,
  A /\ B -> B /\ A.
Proof.
  intros A B (a, b).
  exact (conj b a).
Qed.

Außerdem sind destruct und intros fähig, geschachtelte Konstruktionen in einem Zug zu zerlegen. Dadurch wird nochmals eine Verkürzung und eine Einsparung von Hilfsvariablen erreicht.

Goal forall A B C: Prop,
  A /\ B /\ C -> C /\ B /\ A.
Proof.
  intros A B C. intro h.
  destruct h as (a, hr).
  destruct hr as (b, c).
  exact (conj c (conj b a)).
Qed.

Goal forall A B C: Prop,
  A /\ B /\ C -> C /\ B /\ A.
Proof.
  intros A B C. intro h.
  destruct h as (a, (b, c)).
  exact (conj c (conj b a)).
Qed.

Weiterhin kann man repeat vor split setzen, um Konjunktionen von mehr als zwei Aussagen in einem Rutsch in Unterziele aufzutrennen.

Goal forall A B C: Prop,
  A /\ B /\ C -> C /\ B /\ A.
Proof.
  intros A B C (a, (b, c)).
  split.
  * exact c.
  * split.
    - exact b.
    - exact a.
Qed.

Goal forall A B C: Prop,
  A /\ B /\ C -> C /\ B /\ A.
Proof.
  intros A B C (a, (b, c)).
  repeat split.
  * exact c.
  * exact b.
  * exact a.
Qed.

Unter Umständen tut repeat split mehr als man möchte. Man kann die Aufteilung aber auch genau kontrollieren, indem man repeat split gegen

split; [| split]

ersetzt. Das Semikolon-Tactical darin bewirkt, dass die Taktik hinter dem Semikolon auf jedes durch die Taktik vor dem Semikolon erzeugte Unterziel angewendet wird. Soll es zu jedem der Unterziele eine eigene Taktik sein, werden diese in eckige Klammern gesetzt und durch einen senkrechten Strich getrennt. Weil in unserem Fall ein zusätzliches split nur auf das zweite Unterziel angewendet werden soll, entfällt die Taktik vor dem Strich.

Die Taktiken trivial, auto und tauto erstellen verbleibende Beweisschritte in bestimmten Situationen automatisch.

Goal forall A B: Prop,
  A /\ B -> B /\ A.
Proof.
  intros A B. intro h.
  destruct h as (a, b).
  exact (conj b a).
Qed.

Goal forall A B: Prop,
  A /\ B -> B /\ A.
Proof.
  intros A B (a, b). auto.
Qed.

Taktiken für Allquantoren

Die Einführung der Allquantifizierung wird rückwärts über intro x vorgenommen, das bedeutet soviel wie »Sei x fest, aber beliebig«. Zu diesem x dürfen dann allquantifizierte Antezedenzen spezialisiert werden, womit man Allquantifizierungen beseitigt. Dies geschieht, indem man die allquantifizierte Aussage, als abhängige Funktion betrachtet, auf die Variable appliziert.

Beispiel. Der Beweis des Theorems

(∀x. A(x) ∧ B(x)) ⇔ (∀x. A(x)) ∧ (∀x. B(x))

ist gesucht.

Theorem universal_quant_conj (X: Type) (A B: X -> Prop):
  (forall x, A x /\ B x) <-> (forall x, A x) /\ (forall x, B x).
Proof.
  split.
  * intro h. split.
    - intro x. assert (hx := h x). exact (proj1 hx).
    - intro x. assert (hx := h x). exact (proj2 hx).
  * intro h. intro x. split.
    - exact (proj1 h x).
    - exact (proj2 h x).
Qed.

Nochmals der gleiche Beweis, aber mit reinem Rückwärtsschließen formuliert:

Theorem universal_quant_conj (X: Type) (A B: X -> Prop):
  (forall x, A x /\ B x) <-> (forall x, A x) /\ (forall x, B x).
Proof.
  split.
  * intro h. split.
    - intro x. apply h.
    - intro x. apply h.
  * intros (hA, hB). intro x. split.
    - apply hA.
    - apply hB.
Qed.

Anstelle intro x kann man auch intro u schreiben, womit die Unterscheidung zwischen der gebundenen Variable x und dem Parameter u, über dem man argumentiert, klargestellt wird.

Taktiken für Existenzquantoren

Beispiel. Der Beweis des Theorems

(∃x. A(x) ∧ B(x)) ⇒ (∃x. A(x)) ∧ (∃x. B(x))

ist gesucht.

Theorem existential_quant_conj (X: Type) (A B: X -> Prop):
  (exists x, A x /\ B x) -> (exists x, A x) /\ (exists x, B x).
Proof.
  intro h.
  destruct h as (x, ab).
  destruct ab as (a, b).
  split.
  - exists x. exact a.
  - exists x. exact b.
Qed.