Das Axiom der Reflexivität besagt, dass jeder Term sich selbst
gleich ist. Es wird durch die Funktion eq_refl vermittelt.
Man wendet sie auf einen Term an, um den Beweisterm der Gleichheit
zu sich selbst zu erhalten.
Goal 0 = 0. Proof. assert (e := eq_refl 0). exact e. Qed. Goal exists n: nat, n = n. Proof. exists 0. exact (eq_refl 0). Qed.
Man erhält mit der Reflexivität nicht nur die Gleichheit von Atomen zu sich selbst, auch die beliebiger Terme zu sich selbst. Beispielsweise:
Goal forall (X Y: Type) (f: X -> Y) (x: X), (f x) = (f x). Proof. intros X Y. intro f. intro x. assert (e := eq_refl (f x)). exact e. Qed.
Reflexivität für sich allein bleibt langweilig. Interessante Folgerungen ergeben sich erst im Zusammenspiel mit weiteren Regeln.
Vermittels der Symmetrie lässt sich eine Hypothese folgendermaßen transformieren:
Goal forall a b: Type, a = b -> b = a. Proof. intros a b. intro h. apply eq_sym in h. exact h. Qed.
Möchte man einen neuen Bezeichner haben, geht man stattdessen so vor:
Goal forall a b: Type, a = b -> b = a. Proof. intros a b. intro eqab. assert (eqba := eq_sym eqab). exact eqba. Qed.
Rückwärtsschließen ist hier ebenfalls möglich:
Goal forall a b: Type, a = b -> b = a. Proof. intros a b. intro h. apply eq_sym. exact h. Qed.
Die Funktion eq_trans vermittelt das Transitivgesetz.
Sie wird auf die Beweisterme der beiden Gleichungen angewendet, um
den Beweisterm der dritten Gleichung zu erhalten.
Goal forall a b c: Type, a = b /\ b = c -> a = c. Proof. intros a b c. intro h. destruct h as (eqab, eqbc). assert (eqac := eq_trans eqab eqbc). exact eqac. Qed.
Hat man eine Gleichung x = y und zu einem Prädikat P die Aussage P(x), darf in der Aussage x durch y ersetzt werden, womit man P(y) erhält.
Als Schlussregel dargestellt lautet sie:
Γ ⊢ x = y Γ' ⊢ P(x)
──────────────────────
Γ, Γ' ⊢ P(y)
Man spricht auch von der Beseitigung der Gleichheit,
oder dem Induktionsprinzip der Gleichheit. Kodiert ist es durch
die Funktion eq_ind. Ihre Typsignatur
eq_ind: forall (X: Type) (x: X) (P: X -> Prop), P x -> forall y, x = y -> P y
darf man als ein wenig kompliziert bezeichnen. Man sollte bereits vorher wissen, was erreicht werden soll, sonst droht der Verlust von Überblick. Zumal ist die Reihenfolge der Argumente eine andere als die der klassischen Theorie. Wir können die Argumente allerdings mühelos in die übliche Reihenfolge bringen:
Theorem replacement (X: Type) (x y: X) (P: X -> Prop): x = y -> P x -> P y. Proof. intro eqxy. intro hx. exact (eq_ind x P hx y eqxy). Qed.
Ist die Ersetzungsregel vorhanden, stellt die Symmetrie ein
redundantes Axiom dar. Mit eq_ind findet sich nämlich:
Theorem eq_sym (A: Type) (x y: A): x = y -> y = x. Proof. intro h. exact (eq_ind x (fun t => t = x) (eq_refl x) y h). Qed.
Die Transitivität ist ebenfalls redundant:
Theorem eq_trans (A: Type) (x y z: A): x = y /\ y = z -> x = z. Proof. intro h. destruct h as (eqxy, eqyz). assert (f := eq_ind y (fun t => t = z) eqyz x). simpl in f. exact (f (eq_sym eqxy)). Qed.
Sind zwei Funktionen f, g gleich,
muss auch f(x) = g(x)
für jedes Argument x gelten. Um dies zu bestätigen,
muss man ein wenig um die Ecke denken. Nämlich ist die Applikation
einer Funktion auf ein festes x, also
φ ↦ φ(x), selbst wieder
eine Funktion, die sich vermittels f_equal auf beide
Seiten der Gleichung anwenden lässt.
Goal forall (X Y: Type) (f g: X -> Y) (x: X), f = g -> (f x) = (g x). Proof. intros X Y. intros f g. intro x. intro h. assert (e := f_equal (fun phi => phi x) h). simpl in e. exact e. Qed.
Die genutzte Funktion f_equal ist aus den
Axiomen eq_refl und eq_ind herleitbar.
Es findet sich:
Theorem f_equal (A B: Type) (f: A -> B) (x y: A): x = y -> f x = f y. Proof. intro h. assert (e := eq_refl (f x)). exact (eq_ind x (fun y => f x = f y) e y h). Qed.
Die Umformung der linken Seite in die rechte:
Require Import Coq.Arith.PeanoNat. Theorem double (x: nat): 2*x = x + x. Proof. rewrite Nat.mul_succ_l. rewrite Nat.mul_1_l. reflexivity. Qed. Theorem square (x: nat): x^2 = x*x. Proof. rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r. rewrite Nat.pow_0_r. rewrite Nat.mul_1_r. reflexivity. exact (le_n 0). assert (f := le_S 0 0). exact (f (le_n 0)). Qed. Theorem erste_binomische_Formel (a b: nat): (a + b)^2 = a^2 + 2*a*b + b^2. Proof. rewrite square. rewrite Nat.mul_add_distr_l. rewrite Nat.mul_add_distr_r. rewrite Nat.mul_add_distr_r. rewrite (Nat.mul_comm b a). rewrite <- Nat.add_assoc. rewrite (Nat.add_assoc (a*b)). rewrite <- Nat.mul_add_distr_l. rewrite <- double. rewrite Nat.mul_assoc. rewrite (Nat.mul_comm a 2). rewrite Nat.add_assoc. rewrite <- square. rewrite <- square. reflexivity. Qed.
Alternativ die Umformung der rechten Seite in die linke:
Theorem erste_binomische_Formel (a b: nat): (a + b)^2 = a^2 + 2*a*b + b^2. Proof. rewrite (square a). rewrite (square b). rewrite <- (Nat.mul_assoc 2 a b). rewrite double. rewrite Nat.add_assoc. rewrite <- Nat.mul_add_distr_l. rewrite <- Nat.add_assoc. rewrite <- Nat.mul_add_distr_r. rewrite (Nat.mul_comm (a + b) b). rewrite <- Nat.mul_add_distr_r. rewrite <- square. reflexivity. Qed.
Es wurden bereits einzelne Fähigkeiten von Computeralgebrasystemen
geschaffen. Mit der Taktik ring lassen sich
Polynome vereinfachen und Gleichungen zwischen Polynomen lösen.
Hiermit erhält man eine weitgehende Automatisierung.
Require Import Coq.Arith.Arith. Theorem square (x: nat): x^2 = x*x. Proof. rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r. rewrite Nat.pow_0_r. ring. auto. auto. Qed. Theorem erste_binomische_Formel (a b: nat): (a + b)^2 = a^2 + 2*a*b + b^2. Proof. repeat rewrite square. ring. Qed.
Die Variante für ganze Zahlen schließt die Verarbeitung von Potenzen mit ein.
Require Import ZArith. Local Open Scope Z_scope. Theorem erste_binomische_Formel (a b: Z): (a + b)^2 = a^2 + 2*a*b + b^2. Proof. ring. Qed.
Theorem eq_from_uq_cond (X: Type) (x y: X):
(forall (P: X -> Prop), P x -> P y) -> x = y.
Proof.
intro h.
assert (f := h (fun t => t = x)). simpl in f.
exact (eq_sym (f (eq_refl x))).
Print eq_rec.
Qed.
Theorem Leibniz_characterisation (X: Type) (x y: X):
x = y <-> (forall (P: X -> Prop), P x <-> P y).
Proof.
split.
* intro h. intro P.
apply (f_equal P) in h.
exact (eq_implies_bicond (P x) (P y) h).
* intro h. apply eq_from_uq_cond.
intro P. exact (proj1 (h P)).
Qed.
Wir zeigen zunächst, dass die Gleichheit zweier Aussagen ihre Äquivalenz impliziert. Dieser Umstand lässt sich aus der Ersetzungsregel
Γ ⊢ x = y Γ' ⊢ P(x)
──────────────────────
Γ, Γ' ⊢ P(y)
schlussfolgern. Mit ihr findet sich nämlich:
─────── ───────
Γ ⊢ A = B ⊢ A ⇒ A Γ ⊢ A = B ⊢ B ⇒ B
──────────────────── ────────────────────
Γ ⊢ A ⇒ B Γ ⊢ B ⇒ A
─────────────────────────────────
Γ ⊢ A ⇔ B
Die Implementierung hierzu ist:
Theorem cond_refl (A: Prop): A -> A. Proof. intro h. exact h. Qed. Theorem eq_implies_bicond (A B: Prop): (A = B) -> (A <-> B). Proof. intro h. split. * exact (eq_ind A (fun X => A -> X) (cond_refl A) B h). * exact (eq_ind B (fun X => B -> X) (cond_refl B) A (eq_sym h)). Qed.
Mit dem Extensionalitätsprinzip lässt sich die gewünschte generelle Ersetzungsregel herleiten:
Definition Substitution := forall (A B: Prop) (P: Prop -> Prop), (A <-> B) -> (P A <-> P B). Definition PropExtensionality := forall (A B: Prop), (A <-> B) -> A = B. Theorem prop_extensionality_implies_substitution: PropExtensionality -> Substitution. Proof. unfold PropExtensionality. unfold Substitution. intro exten. intros A B. intro P. intro e. assert (eqab := exten A B e). split. * intro h. exact (eq_ind A P h B eqab). * intro h. exact (eq_ind B P h A (eq_sym eqab)). Qed.
Umgekehrt gilt, dass die generelle Ersetzungsregel bereits das Extensionalitätsprinzip impliziert:
Theorem substition_implies_prop_extensionality: Substitution -> PropExtensionality. Proof. unfold Substitution. unfold PropExtensionality. intro subs. intros A B. intro e. apply eq_from_cond. intro P. exact (proj1 (subs A B P e)). Qed.
Eine bestimmte Form der Ersetzungsregel gilt an sich, gilt in jeder Hinsicht, ohne eine Form der Gleichheit als solche zu haben. Wir nennen sie die zulässige Ersetzungsregel, weil sie sich per struktureller Induktion bereits aus den Regeln und Axiomen der Logik herleiten lässt. Es bezeichne C[X:=A] die Ersetzung jedes Vorkommens der freien logischen Variable X in der Formel C durch die Formel A. Die Regel wird hiermit notiert als:
Γ ⊢ A ⇔ B
─────────────────────
Γ ⊢ C[X:=A] ⇔ C[X:=B]
Sie ist in der generellen enthalten, wobei
wir allerdings wie gezeigt das Extensionalitätsprinzip annehmen müssten.
Ohne dieses ist sie nicht direkt formulierbar. Das ist aber nicht
weiter schlimm. Bei Gleichungen benutzt man die Ersetzungsregel ohnehin
nur in indirekter Weise über die Taktik rewrite. Das Modul
Setoid befähigt uns nun, diese Taktik ebenfalls bezüglich
Äquivalenzen zu nutzen.
Require Import Setoids.Setoid. Goal forall A B C: Prop, (A <-> B) -> (C /\ A <-> C /\ B). Proof. intros A B C. intro h. rewrite h. reflexivity. Qed.
Zum Vergleich ein Beweis unter Bemühung der generellen Regel:
Goal Substitution -> forall A B C: Prop, (A <-> B) -> (C /\ A <-> C /\ B). Proof. intro subs. intros A B C. intro h. assert (f := subs A B (fun X => C /\ X)). simpl in f. exact (f h). Qed.
In der klassischen Logik stehen mit Setoid mithin die
Umformungen der booleschen Algebra zur Verfügung. Sie sind allerdings
recht mühselig. Wie bei den Grundrechenarten muss sogar das
Assoziativgesetz in expliziter Weise angewendet werden. Die Rechnung
A ∧ B ⇒ A ≡ ¬(A ∧ B) ∨ A ≡ ¬A ∨ B ∨ A ≡ (¬A ∨ A) ∨ B ≡ 1 ∨ B ≡ 1
wird beispielsweise wie folgt formalisiert.
Require Import Setoids.Setoid. Require Import Logic.Classical. (* Benötigte Regeln der booleschen Algebra *) Theorem imp_char (A B: Prop): (A -> B) <-> ~A \/ B. Proof. tauto. Qed. Theorem and_de_morgan (A B: Prop): ~(A /\ B) <-> ~A \/ ~B. Proof. tauto. Qed. Theorem or_complement (A: Prop): A \/ ~A <-> True. Proof. tauto. Qed. Theorem or_extremal (A: Prop): A \/ True <-> True. Proof. tauto. Qed. Goal forall A B: Prop, A /\ B -> A. Proof. intros A B. rewrite imp_char. rewrite and_de_morgan. rewrite or_comm. rewrite <- or_assoc. rewrite or_complement. rewrite or_comm. rewrite or_extremal. exact I. Qed.