Die Konstruktion von Beweisen in Gallina stellt eine Form des natürlichen Schließens dar. Wie es sich genauer verhält, soll anhand von Beispielen erläutert werden. Zuvor sind aber ein paar für das bessere Verständnis erforderliche Begrifflichkeiten zu erklären. Es geht hierbei um Sequenzen und Schlussregeln.
Als Sequenz bezeichnet man die Metasprachliche Aussage »Unter den Annahmen aus Γ ist die Aussage A ableitbar«, die symbolisch kurz
Γ ⊢ A
geschrieben wird. Hierbei ist der Kontext Γ eine Ansammlung von Aussagen, die als endliche Liste oder als endliche Menge von Aussagen kodiert werden darf. Es ist klar, dass die Sequenz A ⊢ A, also beispielsweise
Es regnet ⊢ Es regnet
als gültig angenommen werden darf. Wir drücken das dadurch aus, dass eine solche Sequenz ohne Prämissen abgeleitet werden darf. Dies führt zu der folgenden Schlussregel:
| Axiom |
|---|
──────────── Γ, A, Γ' ⊢ A |
Insofern der Kontext als Menge kodiert ist, darf das Axiom gleichermaßen in der äquivalenten Form
| Axiom |
|---|
───────────
Γ ∪ {A} ⊢ A
|
beschrieben werden. Es gilt beispielsweise
∅ ∪ {Es regnet} ⊢ Es regnet.
Klar ist weiterhin, dass zu den Annahmen beliebig viele weitere hinzugefügt werden dürfen.
| Abschwächungsregel |
|---|
Γ ⊢ A ───────── Γ, Γ' ⊢ A |
Zur Anwendung der Abschwächungsregel ein Beispiel. Wir wollen zeigen, dass die scheinbar allgemeinere Regel
Γ ⊢ A Γ' ⊢ B ─────────────── Γ, Γ' ⊢ A ∧ B
eigentlich äquivalent zur speziellen Regel
Γ ⊢ A Γ ⊢ B ────────────── Γ ⊢ A ∧ B
ist. Die spezielle Regel ergibt sich aus der allgemeinen durch Gleichsetzen von Γ und Γ'. Um die allgemeine Regel aus der speziellen zu erhalten, wendet man nun einfach als Zwischenschritt die Abschwächungsregel an:
Γ ⊢ A Γ' ⊢ B
───────── ─────────
Γ, Γ' ⊢ A Γ, Γ' ⊢ B
──────────────────────
Γ, Γ' ⊢ A ∧ B
Es ist noch zu bemerken, dass die Aussagen in Sequenzen nicht unbedingt atomar sein müssen, sondern auch zusammengesetzt sein dürfen. Wenn wir beispielsweise den Modus ponens bezüglich Aussagen A, B als
A, (A ⇒ B) ⊢ B
ausdrücken, meinen wir eigentlich
φ, (φ ⇒ ψ) ⊢ ψ
für beliebige Formeln φ, ψ.
Die Einführungsregel der Implikation besagt, dass auf die Aussage A ⇒ B geschlossen werden darf, sofern B unter Annahme von A beweisbar ist. Die Beseitigungsregel entspricht dem Modus ponens.
| Einführung | Beseitigung |
|---|---|
Γ, A ⊢ B ───────── Γ ⊢ A ⇒ B |
Γ ⊢ A ⇒ B Γ ⊢ A
──────────────────
Γ ⊢ B
|
Entsprechende Regeln bestehen für Programmterme. Die Einführungsregel entspricht der Abstraktion, womit die Einführung einer anonymen Funktion gemeint ist. Die Beseitigungsregel entspricht der Applikation einer Funktion.
| Einführung | Beseitigung |
|---|---|
Γ, a: A ⊢ b: B ──────────────── Γ ⊢ a ↦ b: A → B |
Γ ⊢ f: A → B Γ ⊢ a: A
────────────────────────
Γ ⊢ f(a): B
|
Als einfaches Beispiel wollen wir uns davon überzeugen, dass es sich bei der Aussage A ⇒ B um eine tautologische handelt. Der Beweisbaum lässt sich in drei unterschiedlichen Formen darstellen:
| Formeln | Sequenzen | Seq. von Termen |
|---|---|---|
─── 1 A ────── ~1 A ⇒ A |
───── A ⊢ A ─────── ⊢ A ⇒ A |
─────────── a: A ⊢ a: A ────────────── ⊢ a ↦ a: A → A |
In Gallina schreibt sich das beweisende Programm so:
Definition proof: forall A: Type, A -> A := fun A => fun a => a.
Die Einführungsregel der Konjunktion besagt, dass auf eine Konjunktion zweier Aussagen geschlossen werden darf, sofern die beiden Aussagen beweisbar sind. Die Beseitigungsregel besagt, das von einer Konjunktion zweier Aussagen auf jede der beiden Aussagen geschlossen werden darf.
| Einführung | Beseitigung | Beseitigung |
|---|---|---|
Γ ⊢ A Γ ⊢ B ────────────── Γ ⊢ A ∧ B |
Γ ⊢ A ∧ B ────────── Γ ⊢ A |
Γ ⊢ A ∧ B ────────── Γ ⊢ B |
Der Beweis der tautologischen Aussage A ∧ B ⇒ A soll unser erstes Beispiel sein. Der schematische Beweis geht im Kalkül des natürlichen Schließens so:
| Formeln | Sequenzen | Seq. von Programmtermen |
|---|---|---|
───── 1
A ∧ B
─────
A
────────── ~1
A ∧ B ⇒ A
|
───────────── A ∧ B ⊢ A ∧ B ───────────── A ∧ B ⊢ A ─────────── ⊢ A ∧ B ⇒ A |
─────────────────────────
(a, b): A×B ⊢ (a, b): A×B
─────────────────────────
(a, b): A×B ⊢ a: A
─────────────────────
⊢ (a, b) ↦ a: A×B → A
|
In der ersten Form kommt eine Annahme vor, die weiter unten durch die Einführung der Implikation getilgt wird. Es kann in dieser Form also sein, dass eine Formel nur in einem Kontext von Annahmen gültig ist. In der zweiten Form enthalten die Sequenzen die Buchführung der Annahmen explizit auf ihrer linken Seite. Jede beweisbare Sequenz stellt daher für sich allein ein Theorem dar. Die dritte Form zeigt die entsprechenden Sequenzen von Programmtermen.
Der konstruierte Programmterm gibt für sich bereits den Beweis wieder. Daher genügt die Niederschrift des Programmterms zur Kodierung des Beweises. In Gallina schreibt sich dies so:
Definition proof: forall A B: Type, A*B -> A := fun A B t => match t with (a, b) => a end.
Für A, B vom Typ Prop
bekommt der Beweis die Gestalt
Definition proof: forall A B: Prop, A /\ B -> A := fun A B t => match t with conj a b => a end.
Der Beweis der tautologischen Aussage A ⇒ B ⇒ A ∧ B soll als Beispiel für die Und-Einführung dienen. Im Wesentlichen besteht diese lediglich aus der Zusammensetzung des geordneten Paares, dessen Typ das Produkt A×B ist. Der Beweisbaum:
| Formeln | Sequenzen |
|---|---|
─── 1 ─── 2
A B
─────────
A ∧ B
────────── ~2
B ⇒ A ∧ B
────────────── ~1
A ⇒ B ⇒ A ∧ B
|
──────── ──────── A, B ⊢ A A, B ⊢ B ───────────────────── A, B ⊢ A ∧ B ───────────── A ⊢ B ⇒ A ∧ B ─────────────── ⊢ A ⇒ B ⇒ A ∧ B |
| Sequenzen von Programmtermen |
|---|
───────────────── ─────────────────
a: A, b: B ⊢ a: A a: A, b: B ⊢ b: B
───────────────────────────────────────
a: A, b: B ⊢ (a, b): A×B
──────────────────────────
a: A ⊢ b ↦ (a, b): B → A×B
─────────────────────────────
⊢ a ↦ b ↦ (a, b): A → B → A×B
|
Die Implementierung:
Definition proof: forall A B: Type, A -> B -> A*B := fun A B => fun a => fun b => (a, b).
Für A, B vom Typ Prop:
Definition proof: forall A B: Prop, A -> B -> A /\ B := fun A B => fun a => fun b => conj a b.
Die Einführungsregel der Disjunktion besagt, dass zu einer beweisbaren Aussage auf eine Disjunktion geschlossen werden darf, in der die Aussage auf der linken oder rechten Seite vorkommt. Die Beseitigungsregel erfordert, dass unter Fallunterscheidung zwischen linker und rechter Aussage der Disjunktion dieselbe Aussage bewiesen werden kann.
| Einführung | Einführung | Beseitigung |
|---|---|---|
Γ ⊢ A ────────── Γ ⊢ A ∨ B |
Γ ⊢ B ────────── Γ ⊢ A ∨ B |
Γ ⊢ A ∨ B Γ, A ⊢ C Γ, B ⊢ C
─────────────────────────────────
Γ ⊢ C
|
Die tautologische Aussage A ⇒ A ∨ B sei zu beweisen. Schematisch als Beweisbaum:
| Formeln | Sequenzen | Seq. von Programmtermen |
|---|---|---|
─── 1
A
─────
A ∨ B
────────── ~1
A ⇒ A ∨ B
|
─────
A ⊢ A
─────────
A ⊢ A ∨ B
───────────
⊢ A ⇒ A ∨ B
|
───────────
a: A ⊢ a: A
────────────────────
a: A ⊢ inl(a): A + B
───────────────────────
⊢ a ↦ inl(a): A → A + B
|
Der Disjunktion von zwei Aussagen entspricht die Summe von zwei Typen. Der ersten Regel zur Disjunktions-Einführung entspricht die linke Injektion des Terms.
Die Implementierung:
Definition proof: forall A B: Type, A -> A + B := fun A B => fun a => inl a.
Für A, B vom Typ Prop
gilt wieder eine analoge Formulierung:
Definition proof: forall A B: Prop, A -> A \/ B := fun A B => fun a => or_introl a.
Der folgende Beweis der Tautologie A ∨ B ⇒ B ∨ A dient als ein Beispiel, in dem eine Oder-Einführung vorkommt. Bei der Oder-Einführung wird eine Fallunterscheidung vorgenommen. Der Programmterm zu dieser Fallunterscheidung wird als Musterabgleich dargestellt.
| Natürliches Schließen von Sequenzen |
|---|
───── ─────
A ⊢ A B ⊢ B
───────────── ───────── ─────────
A ∨ B ⊢ A ∨ B A ⊢ B ∨ A B ⊢ B ∨ A
─────────────────────────────────────────
A ∨ B ⊢ B ∨ A
───────────────
⊢ A ∨ B ⇒ B ∨ A
|
| Sequenzen von Programmtermen |
|---|
─────────── ───────────
a: A ⊢ a: A b: B ⊢ b: B
─────────────────── ──────────────────── ────────────────────
s: A + B ⊢ s: A + B a: A ⊢ inr(a): B + A b: B ⊢ inl(b): B + A
───────────────────────────────────────────────────────────────────
s: A + B ⊢ match s {inl(a) ↦ inr(a), inr(b) ↦ inl(b)}: B + A
───────────────────────────────────────────────────────────────
⊢ s ↦ match s {inl(a) ↦ inr(a), inr(b) ↦ inl(b)}: A + B → B + A
|
Die Implementierung:
Definition proof: forall A B: Type, A + B -> B + A
:= fun A B => fun s => match s with
| inl a => inr a
| inr b => inl b
end.
Für A, B vom Typ Prop:
Definition proof: forall A B: Prop, A \/ B -> B \/ A
:= fun A B => fun s => match s with
| or_introl a => or_intror a
| or_intror b => or_introl b
end.
Auf ¬A darf geschlossen werden, wenn sich aus A die Kontradiktion, also ein Widerspruch ableiten lässt. Aus dieser Überlegung ergibt sich die Einführungsregel der Negation. Zur Beseitigung überlegt man sich, dass es widersprüchlich ist, sowohl auf ¬A als auch auf A zu schließen, was also zwingend zu einer Kontradiktion führen muss. Die Schlussregeln sind somit:
| Einführung | Beseitigung |
|---|---|
Γ, A ⊢ ⊥ ──────── Γ ⊢ ¬A |
Γ ⊢ ¬A Γ ⊢ A
───────────────
Γ ⊢ ⊥
|
Der Beweis der Kontrapositionsregel (A ⇒ B) ⇒ (¬B ⇒ ¬A) soll als Beispiel dienen. Der Beweisbaum:
| Sequenzen |
|---|
───────────── ─────
A ⇒ B ⊢ A ⇒ B A ⊢ A
─────── ──────────────────────
¬B ⊢ ¬B A ⇒ B, A ⊢ B
───────────────────────────
A ⇒ B, ¬B, A ⊢ ⊥
────────────────
A ⇒ B, ¬B ⊢ ¬A
───────────────
A ⇒ B ⊢ ¬B ⇒ ¬A
─────────────────────
⊢ (A ⇒ B) ⇒ (¬B ⇒ ¬A)
|
Die Negation ¬A kann man als A ⇒ ⊥ kodieren. Die Schlussregeln der Negation stellen sich damit als Spezialfälle der Schlussregeln der Implikation heraus. Ermittelt man noch die entsprechenden Terme, findet sich:
| Sequenzen von Termen |
|---|
─────────────────── ───────────
f: A → B ⊢ f: A → B a: A ⊢ a: A
─────────────────── ──────────────────────────────────
g: B → 0 ⊢ g: B → 0 f: A → B, a: A ⊢ f(a): B
───────────────────────────────────────────────────
f: A → B, g: B → 0, a: A ⊢ g(f(a)): 0
───────────────────────────────────────
f: A → B, g: B → 0 ⊢ a ↦ g(f(a)): A → 0
─────────────────────────────────────────────
f: A → B ⊢ g ↦ a ↦ g(f(a)): (B → 0) → (A → 0)
────────────────────────────────────────────────────
⊢ f ↦ g ↦ a ↦ g(f(a)): (A → B) → ((B → 0) → (A → 0))
|
Die Implementierung:
Inductive zero: Type :=. Definition proof: forall A B: Type, (A -> B) -> (B -> zero) -> (A -> zero) := fun A B => fun f => fun g => fun a => g (f a).
Die Kontraposition entpuppt sich somit als Spezialfall des Kettenschlusses. Dieser besagt, dass man von A ⇒ B und B ⇒ C auf A ⇒ C schließen darf. Um die Regel der Kontraposition zu erhalten, wird lediglich C := ⊥ eingesetzt.
| Einführung | Beseitigung |
|---|---|
Γ ⊢ A ───────── (x ∉ FV(Γ)) Γ ⊢ ∀x: A |
Γ ⊢ ∀x: A ─────────── Γ ⊢ A[x:=t] |
Wir wollen zunächst den Beweis der Aussage
A ∧ (∀x: P(x)) ⇒ (∀x: A ∧ P(x))
erbringen. Vom Prinzip her verläuft der Beweis fast trivial. Die Prämisse ist lediglich in ihre Bestandteile zu zerlegen und neu zu gruppieren:
| Natürliches Schließen von Sequenzen |
|---|
──────────────────
Γ ⊢ A ∧ (∀x: P(x))
────────────────── ──────────────────
Γ ⊢ A ∧ (∀x: P(x)) Γ ⊢ ∀x: P(x)
────────────────── ────────────
Γ ⊢ A Γ ⊢ P(x)
────────────────────────────────
Γ ⊢ A ∧ P(x)
──────────────────
Γ ⊢ (∀x: A ∧ P(x))
─────────────────────────────────
⊢ A ∧ (∀x: P(x)) ⇒ (∀x: A ∧ P(x))
Γ = {A ∧ (∀x: P(x))}
|
Es findet sich der entsprechende Programmterm
(a, p) ↦ (x ↦ (a, p(x))): A × (∏x. P(x)) → (∏x. A × P(x)).
Die Implementierung:
Definition proof: forall (A X: Type) (P: X -> Type), A*(forall x, P x) -> (forall x, A*(P x)) := fun A X P t => match t with (a, p) => fun x => (a, p x) end.
Für A, (P x) vom Typ Prop:
Definition proof: forall (A: Prop) (X: Type) (P: X -> Prop), A /\ (forall x, P x) -> (forall x, A /\ (P x)) := fun A X P t => match t with conj a p => fun x => conj a (p x) end.
| Einführung | Beseitigung |
|---|---|
Γ ⊢ A[x:=t] ─────────── Γ ⊢ ∃x: A |
Γ ⊢ ∃x: A Γ, A ⊢ B
───────────────────── (x ∉ FV(Γ, B))
Γ ⊢ B
|
Der Beweis der Tautologie A ∧ (∃x: P(x)) ⇒ (∃x: A ∧ P(x)) wird als Beispiel für den Umgang mit Existenzaussagen dienen. Der Beweisbaum:
| Natürliches Schließen von Sequenzen |
|---|
──────────────────
Γ ⊢ A ∧ (∃x: P(x))
────────────────── ───────────
Γ ⊢ A P(x) ⊢ P(x)
────────────────── ─────────────────────────────
Γ ⊢ A ∧ (∃x: P(x)) Γ, P(x) ⊢ A ∧ P(x)
────────────────── ────────────────────────
Γ ⊢ ∃x: P(x) Γ, P(x) ⊢ (∃x: A ∧ P(x))
──────────────────────────────────────────────────
Γ ⊢ (∃x: A ∧ P(x))
─────────────────────────────────
⊢ A ∧ (∃x: P(x)) ⇒ (∃x: A ∧ P(x))
Γ = {A ∧ (∃x: P(x))}
|
| Sequenzen von Termen |
|---|
───────────────
Γ ⊢ (a, (u, p))
─────────────── ─────────────────
Γ ⊢ a: A p: P(u) ⊢ p: P(u)
─────────────── ──────────────────────────────────
Γ ⊢ (a, (u, p)) Γ, p: P(u) ⊢ (a, p): A × P(u)
──────────────────── ──────────────────────────────────
Γ ⊢ (u, p): ∑x. P(x) Γ, p ⊢ (u, (a, p)): (∑x. A × P(x))
─────────────────────────────────────────────────────────────
Γ ⊢ (u, (a, p)): (∑x. A × P(x))
────────────────────────────────────────────────────────────
⊢ (a, (u, p)) ↦ (u, (a, p)): A × (∑x. P(x)) → (∑x. A × P(x))
Γ = {(a, (u, p)): A × (∑x. P(x))}
|
Die Implementierung:
Definition proof: forall (A X: Type) (P: X -> Type),
A*{x & P x} -> {x & prod A (P x)}
:= fun A X P t => match t with
| (a, existT _ u p) => existT _ u (a, p)
end.
Für A, (P x) vom Typ
Prop:
Definition proof: forall (A: Prop) (X: Type) (P: X -> Prop),
A /\ (exists x, P x) -> (exists x, A /\ (P x))
:= fun A X P t => match t with
| conj a (ex_intro _ u p) => ex_intro _ u (conj a p)
end.
Ein Term (u, p) vom Typ ∑x. P(x) ist wie folgt zu verstehen. Der Zeuge u belegt mit dem Beweis p vom Typ P(u), dass der Typ P(u) bewohnt ist. Weil also mindestens ein Summand bewohnt ist, muss mithin die Summe bewohnt sein. Anders betrachtet kann man die Summe auch als disjunkte Vereinigung unendlich vieler Summanden sehen, wobei u das Tag für den Wert p darstellt.
Anstelle von (u, p) schreibt man in Gallina
ex_intro _ u p. Die genaue Signatur
von ex_intro ist
ex_intro P u p bzw. @ex_intro X P u p
mit dem Prädikat P: X -> Prop, dem Zeugen
u: X und dem Beweis p: P u.
Es ist noch zu bemerken, dass es sich bei der für Sigma-Typen verwendeten Notation eigentlich nur um eine alternative Schreibweise handelt, die auf bereits vorhandene Konzepte der Sprache zurückgeführt wird:
| Syntaktischer Zucker | Bedeutung |
|---|---|
{x: X & P x}
| sigT (fun x: X => P x)
|
exists x: X, P x
| ex (fun x: X => P x)
|
Die Idee dabei ist, dass der Lambdakalkül mit den anonymen Funktionen bereits das Konzept gebundener Variablen enthält. Anstelle einen weiteren Ausdruck mit gebundenen Variablen einzuführen, kann man den Ausdruck daher als Anwendung eines Typkonstruktors auf eine anonyme Funktion darstellen.