Einführung in Denotational Design, Teil III: Einführung in Agda

Dieser Artikel ist der dritte einer Reihe über Denotational Design. In diesem Artikel lernen wir Agda kennen. Agda ist eine Programmiersprache mit einem sehr ausdrucksstarken Typsystem. Es lassen sich mit Agda fast beliebige formale Aussagen als Typen ausdrücken. Implementierungen – Werte dieser Typen – werden dadurch zu Beweisen, die zeigen, dass diese Aussagen auch zutreffend sind. Wir legen uns im Folgenden das Beispiel mit den binären Numeralen aus dem ersten Artikel vor und formalisieren es in Agda. Im nächsten Artikel wenden wir die hier dargestellten Inhalte auf unser Praxisbeispiel mit den Zeitreihen an.

Im ersten Artikel dieser Reihe hatten wir die natürlichen Zahlen untersucht. Genauer: Wir hatten gesehen, wie wir binäre Numerale – reine Symbole, zusammengesetzt aus Nullen und Einsen – in die natürlichen Zahlen übersetzen können und wie wir sicherstellen können, dass diese Übersetzung verträglich ist mit unserer intuitiven Vorstellung, was denn die natürlichen Zahlen eigentlich bedeuten. Unsere Übersetzung hatten wir durch folgendes Gleichungssystem beschrieben:

𝛍(0) = 0
𝛍(1) = 1
𝛍(x0) = 2 * 𝛍(x)
𝛍(x1) = 2 * 𝛍(x) + 1

Hier sind die Zeichen 0 und 1 auf der linken Seite lediglich Symbole ohne Bedeutung. Die Zeichen 0, 1 und 2 auf der rechten Seite der Gleichheitszeichen bedeuten die natürlichen Zahlen. x0 bzw. x1 auf der linken Seite bedeutet, dass für ein beliebiges Numeral x rechts eine Null bzw. Eins angehängt wird.

Was wir in unserem ersten Artikel dogmatisch vorausgesetzt haben – nämlich die Existenz und Funktionsweise der natürlichen Zahlen – wollen wir in diesem Artikel zunächst weiter formalisieren.

Eine Formalisierung der natürlichen Zahlen

Warum wollen wir überhaupt die natürlichen Zahlen weiter formalisieren? Immerhin hat doch jeder ein ausreichendes intuitives Verständnis vom Zählen, Addieren, Multiplizieren und so weiter, oder? Tatsächlich könnten wir uns für die reine Übersetzung von Numeralen in natürliche Zahlen auf die natürlichen Zahlen in der Agda-Standard-Library beziehen. Die Addition und Multiplikation sind dort bereits definiert und mehr brauchen wir für die Übersetzung gar nicht. Später wollen wir aber den Beweis führen, dass sich Operationen auf den Numeralen mit denen auf den natürlichen Zahlen decken und spätestens dann müssen wir ein Verständnis entwickeln, wie die natürlichen Zahlen in Agda repräsentiert sind. Es lohnt sich also, dass wir diese natürlichen Zahlen selbst definieren.

Unser Vorhaben mag aussichtslos scheinen. Wir wollen die eine Repräsentation der natürlichen Zahlen (binäre Numerale) auf eine andere Repräsentation überführen. Mehr können wir formal auch gar nicht erreichen. Um über die natürlichen Zahlen nachzudenken, benötigen wir immer eine konkrete Repräsentation dieser. Die reinen, abstrakten natürlichen Zahlen sind ohne konkrete Repräsentation gar nicht greifbar. Man könnte sagen, dass der Begriff der natürlichen Zahlen das Gemeinsame aller verschiedenen Repräsentationen ist.

Wir sind also dazu verdammt, mit konkreten Repräsentation der natürlichen Zahlen zu arbeiten. Es ist damit aber nicht gleich alles egal. Immerhin gibt es ungeschickte und geschicktere Repräsentationen. Die römischen Zahlen sind eine sehr komplizierte Repräsentation der natürlichen Zahlen (ohne die Null), die Dezimalzahlen oder Binärzahlen sind da schon deutlich nützlicher für theoretische Untersuchungen. Es gibt aber noch eine weitere Repräsentation, die alle anderen schlägt in Sachen Einfachheit. Jedes dreijährige Kind kennt diese Repräsentation: das Unärsystem.

Im Unärsystem wird eine Zahl einfach durch eine entsprechende Menge von Strichen beschrieben. Eins ist I, Zwei ist II, Drei ist III, Vier ist IIII und so weiter. Diese Bierdeckelnotation wollen wir zur Grundlage unserer Formalisierung nehmen. Wir verwenden die Programmiersprache Agda, um dieses Vorhaben umzusetzen. Agda ist eine Programmiersprache mit sog. Dependent Types. Das Typsystem von Agda lässt uns fast alle denkbaren Konstruktionen ausdrücken – insbesondere detaillierte Aussagen über die Korrektheit unseres Codes.

In Agda führen wir einen neuen Datentyp mit data ein. Die Syntax ist sehr ähnlich zu der von GADTs in Haskell. Wir definieren zwei Konstruktoren: Anstatt bei der Eins beginnen wir bei der Null und anstatt einer unendlichen Menge von Symbolen definieren wir einen Hochzähl-Kombinator.

data Nat : Set where
  zero : Nat
  suc : Nat -> Nat

Et voila, wir haben die natürlichen Zahlen definiert. Den ersten paar Zahlen können wir noch sprechendere Namen geben:

one : Nat
one = suc zero

two : Nat
two = suc one

three : Nat
three = suc two

Die Bedeutung dieser an sich bedeutungslosen Konstruktionen kommt erst dann richtig zum Tragen, wenn wir ein paar Operationen auf den natürlichen Zahlen definieren. Wir wollen beispielsweise zwei Zahlen addieren.

+ : Nat -> Nat -> Nat
+ x y = ?

Wir können bei der Implementierung von + nach Konstruktionsanleitung vorgehen. Wir schauen uns dazu an, auf welche zwei Arten das x zustandegekommen sein könnte. Nat ist ein Summentyp aus zwei Konstruktoren, also sollte unsere Definition auch auf diese beiden Fälle eingehen.

+ : Nat -> Nat -> Nat
+ zero y = ?
+ (suc x') y = ?

Der erste Fall zero + y ergibt y. Im zweiten Fall sollten wir einen rekursiven Aufruf wagen.

+ : Nat -> Nat -> Nat
+ zero y = y
+ (suc x') y = suc (+ x' y)

Die Multiplikation ist nicht viel komplexer:

* : Nat -> Nat -> Nat
* zero m = zero
* (suc n) m = (+ m (* n m))

Diese drei Codeblöcke – die Datendefinition, die Addition und die Multiplikation – können wir nicht weiter verifizieren. Hier müssen wir uns absolut sicher sein. Glücklicherweise ist die unäre Kodierung so trivial, dass uns diese Sicherheit nicht schwer fällt. Hätten wir eine binäre Kodierung als Grundlage der natürlichen Zahlen verwendet, sähe das schon anders aus.

Die Binärzahlen

Die eingangs beschriebene Definition der binären Numerale lässt sich fast wortwörtlich in Agda übersetzen.

data Bin : Set where
  0b : Bin
  1b : Bin
  at-0 : Bin -> Bin
  at-1 : Bin -> Bin

Die Datendefinition der unären Zahlen hatte nur zwei Fälle; hier haben wir vier. Allein dadurch sieht man schon, dass diese Repräsentation der natürlichen Zahlen deutlich aufwendiger ist. Auch bei der Definition einiger erster konkreter Zahlen müssen wir uns ein wenig mehr anstrengen:

10b : Bin
10b = at-0 1b

11b : Bin
11b = at-1 1b

100b : Bin
100b = at-0 (at-0 1b)

Im ersten Blogartikel hatten wir noch eine simple Operation auf den binären Numeralen definiert: Das Hochzählen.

inc : Bin -> Bin
inc 0b = 1b
inc 1b = 10b
inc (at-0 x) = at-1 x
inc (at-1 x) = at-0 (inc x)

Das ist zwar verständlicher Code, aber bei weitem nicht so trivial wie das Hochzählen in der unären Repräsentation. Dort wäre +1 bloß ein Synonym für den suc-Konstruktor.

Im ersten Blogartikel hatten wir dann bewiesen, dass inc auf den binären Numeralen genau diesem +1 auf den natürlichen Zahlen entspricht. Dazu benötigten wir eine Übersetzung der beiden Welten. Diese nannten wir die Denotation oder Bedeutungsfunktion 𝛍.

𝛍(0) = 0
𝛍(1) = 1
𝛍(x0) = 2 * 𝛍(x)
𝛍(x1) = 2 * 𝛍(x) + 1

Auch diese Definition können wir in Agda beinahe Eins-zu-Eins übernehmen.¹

𝛍 : Bin -> Nat
𝛍 0b = zero
𝛍 1b = one
𝛍 (at-0 x) = (* two (𝛍 x))
𝛍 (at-1 x) = (+ (* two (𝛍 x)) one)

Diese Bedeutungsfunktion ist wieder einer dieser Codeblöcke über deren Korrektheit wir uns schlicht sicher sein müssen. Kein Computer kann uns sagen, ob das wirklich das ist, was wir mit binären Numeralen meinen. Erst beim nächsten Schritt können wir uns maschinelle Untestützung erwarten.

inc===+1

Bevor wir gleich die semantische Übereinstimmung von inc und + one beweisen, basteln wir uns noch ein paar Werkzeuge, um überhaupt Aussagen über unseren Code treffen zu können. Die einfachste Art von Aussage, die wir treffen können, ist, dass zwei Codeschnipsel „äquivalent“ sind. Da wir daran interessiert sind, dass Agda uns statisch sagen kann, ob unser Code gleich ist, kann diese Äquivalenz aber nicht die einfache Laufzeit-Gleichheit == wie in Haskell sein. Nein, wir brauchen eine Gleichheit auf dem Typlevel.

Zur Erinnerung: Aussagen folgender Spielart möchten wir prüfen.

(=== (+ one two) three)
forall x y . (=== (+ x y) (+ y x))
forall x . (=== (𝛍 (inc x)) (+ x one))

Derartige Aussagen wollen wir in Typen überführen. Damit ist klar, dass === ein zweistelliger Typkonstruktor sein muss. Ein erster (scheiternder) Versuch:

data === (x : Nat) (y : Nat) : Set where
  construct : (=== x y)

Hier sagen wir, dass === ein zweistelliger Typkonstruktor ist, der zwei Dinge x und y vom Typen Nat nimmt und einen Typen (Set) zurückgibt. Hier sehen wir zum ersten Mal den Einsatz von Dependent Types. Das x könnte nämlich so was sein wie zero oder suc zero, also Werte und das ist schließlich auch das, was wir wollen, wenn wir einen Typen wie === (+ one two) three konstruieren:

yes : (=== (+ one two) three)
yes = construct

Dieser Code geht durch den Typchecker – aber das tut auch dieser Code:

weird : (=== (+ one one) three)
weird = construct

Das ist zwar folgerichtig; es ist aber nicht das, was wir erreichen wollten. Wir möchten nur wahre Aussagen konstruieren können. Oder anders ausgedrückt: Die obige Definition von === ist noch nicht das, was wir mit Gleichheit meinen – wir wollen nicht nur, dass gleiche Werte als gleich angesehen werden, sondern auch, dass ungleiche Werte nicht als gleich angesehen werden. Wir möchten also nur Werte konstruieren können, die Zeuge davon sind, dass x und y auch wirklich gleich sind. Das klingt nach einem endlosen Regress, deshalb versuchen wir‘s noch mal anders: Es kann überhaupt nur die Gleichheit von Werten bezeugt werden, wenn auf beiden Seiten des Gleichheitszeichens derselbe Wert steht. Diese Gleichheit ist eine rein reflexive Angelegenheit. Wir nennen unseren Konstruktor deshalb refl. Er muss diese Form haben: refl : (=== x x). Dann haut aber die Signatur des Typkonstruktors nicht mehr hin. Wir verlagern deshalb das zweite Argument auf die rechte Seite des Doppelpunkts und machen damit aus dem zweistelligen Typkonstruktor einen einstelligen, der aber eine Funktion auf dem Typlevel zurückgibt.

data === (x : Nat) : Nat -> Set where
  refl : ((=== x) x)

Der einzige Konstruktor refl ist dabei gar kein Wert vom Typ (=== x), was eine Funktion wäre, sondern die Typenfunktion wird direkt wieder auf x angewendet. Der Typ (=== x) beschreibt die sog. „Familie“ von Beweisen, dass ein Wert gleich x ist. Diese Familie ist nur „inhabited“ – hat also nur Werte – am Typindex x, also es ist nur x gleich x und der Beweis davon ist refl. Das heißt, ein Anwender kann zwar immer noch einen Typen wie (=== (+ one one) three) hinschreiben – behaupten kann man alles –, es ist jetzt bloß nicht mehr möglich, auch einen Wert von diesem Typen zu erzeugen, denn (+ one one) normalisiert zu (suc (suc zero)) und three ist (suc (suc (suc zero))).

Jetzt können wir endlich unser Korrektheitskriterium für inc ausdrücken:

inc===+1 : (x : Bin) -> (=== (𝛍 (inc x)) (+ (𝛍 x) one))
inc===+1 = ?

inc===+1 ist ein ganz gewöhnlicher Name. Namen in Agda können fast alles sein. Wir sagen hier, dass inc===+1 vom Typen (x : Bin) -> (=== (𝛍 (inc x)) (+ (𝛍 x) one)) ist, d.h. es ist eine Funktion von einem beliebigen binären Numeral zu einem Beweisobjekt, das bezeugt, dass eine Gleichheit besteht zwischen (𝛍 (inc x)) und (+ (𝛍 x) one). Es gibt nur einen einzigen Konstruktor, der eine solche Gleichheit bezeugen könnte, nämlich refl. Trotzdem wird die folgende Implementierung noch nicht funktionieren.

inc===+1 : (x : Bin) -> (=== (𝛍 (inc x)) (+ (𝛍 x) one))
inc===+1 x = refl

Agda gibt diese Fehlermeldung aus:

𝛍 (inc x) != + (𝛍 x) one of type Nat
when checking that the expression refl has type
=== (𝛍 (inc x)) (+ (𝛍 x) one)

!= ist dabei nicht die Negation unseres ===-Vergleichsoperators. Die Fehlermeldung sagt also nicht direkt, dass unser Beweisunterfangen zum Scheitern verurteilt ist. Die Fehlermeldung sagt nur, dass refl nicht als Beweisobjekt taugt, denn dazu müssten beide Seiten zu dem selben Term normalisieren, d.h. nach Einsetzung aller Definitionen müsste derselbe Term auf beiden Seiten von === stehen. Zumindest taugt refl nicht im Allgemeinen als ein solches Beweisobjekt. Für konkretere Aussagen klappt das schon:

inc10b : (=== (𝛍 (inc 10b)) (+ (𝛍 10b) one))
inc10b = refl

Hier haben wir das x in inc===+1 durch 10b konkretisiert. Wenn wir alle Funktionsanwendungen nach Definition auflösen (z.B. inc 10b = inc (at-0 1b) = at-1 1b), erhalten wir auf beiden Seiten des === das Ergebnis suc (suc (suc zero)). Der Konstruktor refl ist also anwendbar. Das gilt auch für die ersten beiden Fälle für inc===+1.

inc===+1 : (x : Bin) -> (=== (𝛍 (inc x)) (+ (𝛍 x) one))
inc===+1 0b = refl
inc===+1 1b = refl
inc===+1 (at-0 x) = refl
inc===+1 (at-1 x) = ?

Überraschenderweise ist der dritte Fall inc===+1 (at-0 x) ebenfalls unmittelbar erfüllbar, obwohl x dort als freie Variable vorkommt. Das liegt daran, dass auch hier die Normalisierung denselben Term liefert:

(𝛍 (inc (at-0 x))) =
(𝛍 (at-1 x)) =
(+ (* two (𝛍 x)) one)

… auf der linken Seite und …

(+ (𝛍 (at-0 x)) one) =
(+ (* two (𝛍 x)) one)

… auf der rechten Seite.

Nur im letzten Fall kann Agda den Beweis nicht automatisch führen, weil die Normalisierung – das Einsetzen von Definitionen – stecken bleibt. Wir können uns von Agda an der Stelle des Fragezeichens das Beweisziel anzeigen lassen:

Goal: === (+ (𝛍 (inc x)) (+ (𝛍 (inc x)) zero))
          (+ (+ (+ (𝛍 x) (+ (𝛍 x) zero)) one) one)

Hier sehen wir die zwei steckgebliebenen Terme. Das sieht kompliziert aus. Nachdem wir uns vom ersten Schock erholt haben, sehen wir aber, dass dort ganz offensichtlich zu vereinfachende Terme stehen: (+ (𝛍 (inc x)) zero) sollte sich ja wohl zu (𝛍 (inc x)) vereinfachen lassen. Wir erhalten dann:

Goal: === (+ (𝛍 (inc x)) (𝛍 (inc x)))
          (+ (+ (+ (𝛍 x) (𝛍 x)) one) one)

Nun machen wir hier ja Induktion, d.h. wir können voraussetzen, dass die Aussage (=== (𝛍 (inc x)) (+ (𝛍 x) one)) für das x hier schon bewiesen ist. Diese Gleichheit können wir oben einsetzen und erhalten:

Goal: === (+ (+ (𝛍 x) one) (+ (𝛍 x) one))
          (+ (+ (+ (𝛍 x) (𝛍 x)) one) one)

Jetzt stehen links und rechts des === schon dieselben Terme mit + verbunden, nur noch in unterschiedlicher Reihenfolge und Klammerung. Wir wissen aber, dass für Addition auf den unären Zahlen das Assoziativ- und Kommutativgesetz gelten.

Als Menschen sind wir also von der Geltung unserer Behauptung überzeugt. Agda ist es noch nicht. Das liegt daran, dass die Regeln, die wir eben angewandt haben, gar nicht bekannt sind. Die erste dieser Regeln – vielleicht die subtilste – ist die, dass wir aus einer Gleichheit von x und y und einer Gleichheit von y und z eine Gleichheit von x und z folgern können – dass === also transitiv ist. Wir nennen diese Regel trans und anstatt sie als Axiom zu bestimmen, beweisen wir sie:

trans : (x : Nat) -> (y : Nat) -> (z : Nat) -> (=== x y) -> (=== y z) -> (=== x z)
trans x y z refl refl = refl

Der Beweis ist trivial, aber trans ist trotzdem ein wichtiges Hilfsmittel.

Die nächste Regel, die wir oben verwendet haben, ist, dass zero ein neutrales Element der Addition ist, also dass gilt: (x : Nat) -> (=== (+ x zero) x).

zeroneutral : (x : Nat) -> (=== (+ x zero) x)
zeroneutral zero = refl
zeroneutral (suc x) = ?

Der Fall, dass x gleich zero ist, ist trivial bewiesen nach Normalisierung. Der Fall, dass x gleich suc x ist, erfordert den Beweis, dass (suc (+ x zero)) gleich (suc x) ist. Wir wissen nach Induktionsvoraussetzung, dass (+ x zero) gleich x ist, aber im Beweisziel sind beide Seiten noch durch ein suc eingewickelt. Wir brauchen eine weitere Regel, die besagt, dass aus einer Gleichheit von x und y auch eine Gleichheit von f x und f y folgt für beliebige Funktionen f. Diese Regel heißt Kongruenz und wir nennen sie cong.

cong : (f : Nat -> Nat) -> (x : Nat) -> (y : Nat) -> (=== x y) -> (=== (f x) (f y))
cong f x y refl = refl

Im Beweis für zeroneutral (suc x) müssen wir jetzt nur noch einsetzen.

zeroneutral : (x : Nat) -> (=== (+ x zero) x)
zeroneutral zero = refl
zeroneutral (suc x) = cong suc (+ x zero) x (zeroneutral x)

Nun fehlen noch das Assoziativgesetz …

+assoc : (x : Nat) -> (y : Nat) -> (z : Nat) -> (=== (+ x (+ y z)) (+ (+ x y) z))
+assoc zero y z = refl
+assoc (suc x) y z = cong suc (+ x (+ y z)) (+ (+ x y) z) (+assoc x y z)

… und Kommutativgesetz.

+commut : (x : Nat) -> (y : Nat) -> (=== (+ x y) (+ y x))
+commut x y = ?

Hierbei begegnet uns allerdings noch eine Subtilität. Wir machen einen Induktionsbeweis über x. Im zero Fall ist unser Beweisziel === y (+ y zero). Das haben wir doch scheinbar schon gezeigt mit zeroneutral, wenn auch anders herum. Wir brauchen also auch noch das Kommutativgesetz für ===. Das wird gern sym genannt, da es die Symmetrie von === zeigt.

sym : (x : Nat) -> (y : Nat) -> (=== x y) -> (=== y x)
sym x y refl = refl

Jetzt können wir die ersten Fälle für +commut implementieren.

+commut : (x : Nat) -> (y : Nat) -> (=== (+ x y) (+ y x))
+commut zero y = sym (+ y zero) y (zeroneutral y)
+commut (suc x) zero = cong suc (+ x zero) x (zeroneutral x)
+commut (suc x) (suc y) = ?

Das Beweisziel für den zweiten Fall ist (=== (suc (+ x y)) (+ y (suc x))). Wir gönnen uns noch einen letzten kleinen Helfer, der die Vertauschbarkeit von + und suc zeigt.

+suclr : (x : Nat) -> (y : Nat) -> (=== (+ x (suc y)) (+ (suc x) y))
+suclr zero y = refl
+suclr (suc x) y = cong suc (+ x (suc y)) (+ (suc x) y) (suclr x y)

Für den letzen Fall von +commut setzen wir nur noch alles zusammen.

+commut : (x : Nat) -> (y : Nat) -> (=== (+ x y) (+ y x))
+commut zero y = sym (+ y zero) y (zeroneutral y)
+commut (suc x) zero = cong suc (+ x zero) x (zeroneutral x)
+commut (suc x) (suc y) = cong
                            suc
                            (+ x (suc y))
                            (+ y (suc x))
                            (trans
                              (+ x (suc y))
                              (+ (suc x) y)
                              (+ y (suc x))
                              (+suclr x y)
                              (+commut (suc x) y))

Implizite Parameter

Ay caramba! Wir haben endlich bewiesen, dass das Kommutativgesetz für die Addition gilt. Dieser Beweis ist schon recht komplex und wir sind noch lang nicht bei unserem eigentlichen Beweisziel inc===+1 angekommen. Bevor wir uns diesem widmen, refaktorisieren wir unseren Kommutativitätsbeweis noch ein wenig. Bisher haben wir nämlich aus didaktischen Gründen jeden Beweis bis ins kleinste von Hand selbst durchgeführt. Agda kann aber oft selbst triviale Einsetzungen selbst vornehmen. Den Beweis für +commut oben können wir mit sog. Holes vereinfachen:

+commut2 : (x : Nat) -> (y : Nat) -> (=== (+ x y) (+ y x))
+commut2 zero y = sym _ _ (zeroneutral y)
+commut2 (suc x) zero = cong suc _ _ (zeroneutral x)
+commut2 (suc x) (suc y) = cong
                             suc
                             _
                             _
                             (trans
                               _
                               _
                               _
                               (+suclr _ _)
                               (+commut2 (suc x) y))

Ein Hole weist Agda an: Füll hier – wenn möglich – die einzige mögliche Lösung ein. Dank Typinferenz lässt sich diese Vereinfachung im Code oft anwenden. Wir können diese Vereinfachung sogar an der Definitionsstelle veranlassen, indem wir manche Parameter als implizit markieren. Dazu schreiben wir die Parameter nicht in normalen, runden Klammern, sondern in geschweiften. Anwendungen von trans, cong, etc. werden dadurch deutlich kürzer und damit lesbarer.

trans2 : {x : Nat} -> {y : Nat} -> {z : Nat} -> (=== x y) -> (=== y z) -> (=== x z)
trans2 refl refl = refl

cong2 : {x : Nat} -> {y : Nat} -> (f : Nat -> Nat) -> (=== x y) -> (=== (f x) (f y))
cong2 f refl = refl

sym2 : {x : Nat} -> {y : Nat} -> (=== x y) -> (=== y x)
sym2 refl = refl

+commut2 : (x : Nat) -> (y : Nat) -> (=== (+ x y) (+ y x))
+commut2 zero y = sym2 (zeroneutral y)
+commut2 (suc x) zero = cong2 suc (zeroneutral x)
+commut2 (suc x) (suc y) = cong2
                             suc
                             (trans2
                               (+suclr _ _)
                               (+commut2 (suc x) y))

Der finale Beweis

Etwas grundsätzlich neues kommt beim Beweis von inc===+1 nicht mehr. Wir setzen lediglich trans, cong, sym etc. zusammen. Der finale Beweis ist dann ein ziemliches Monstrum:

inc===+1 : (x : Bin) -> === (μ (inc x)) (+ (μ x) one)
inc===+1 0b = refl
inc===+1 1b = refl
inc===+1 (at-0 x) = refl
inc===+1 (at-1 x) = trans2 (+assoc (μ (inc x)) (μ (inc x)) zero)
                           (trans2 (zeroneutral (+ (μ (inc x)) (μ (inc x))))
                                   (trans2 (cong2 (λ y → (+ y (μ (inc x))))
                                                  (inc===+1 x))
                                           (trans2 (cong2 (λ y → (+ (+ (μ x) one) y))
                                                          (inc===+1 x))
                                                   (trans2 (+assoc (+ (μ x) one) (μ x) one)
                                                           (cong2 (λ y → (+ y one))
                                                                  (trans2 (+commut2 (+ (μ x) one) (μ x))
                                                                          (trans2 (+assoc (μ x) (μ x) one)
                                                                                  (cong2 (λ y → (+ y one))
                                                                                         (cong2 (λ y → (+ (μ x) y))
                                                                                                (sym2 (zeroneutral (μ x))))))))))))

Zusammenfassung

Dieser letzte Beweis ist wieder recht komplex. Wir könnten diesen Beweis noch vereinfachen und in eine deutlich verständlichere Form bringen. Die Agda-Standardbibliothek bringt bspw. Werkzeuge für sog. Equational-Reasoning mit. Diese Werkzeuge werden wir in einem der nächsten Artikel kennen lernen.

Auch wenn der finale Beweis einigermaßen komplex ist, hält sich der Gesamtaufwand für unser Unterfangen doch in Grenzen – zumindest in Anbetracht der Garantien, die wir bekommen. Die Definition der unären natürlichen Zahlen und die Definition von === haben wir oben nur aus didaktischen Gründen selbst programmiert. Normalerweise würden wir diese auch der Standardbibliothek entnehmen. Die Beweishilfsmittel, die wir selbst definiert haben, beziehen sich alle auf das Zusammenspiel von natürlichen Zahlen und ===. Auch diese Hilfsmittel sind in der Standardbibliothek bereits enthalten. Dann bleibt als eigentlicher neuer Code nur folgendes übrig:

data Bin : Set where
  0b : Bin
  1b : Bin
  at-0 : Bin -> Bin
  at-1 : Bin -> Bin

μ : Bin -> Nat
μ 0b = zero
μ 1b = one
μ (at-0 x) = (* two (μ x))
μ (at-1 x) = (+ (* two (μ x)) one)

inc : Bin -> Bin
inc 0b = 1b
inc 1b = 10b
inc (at-0 x) = at-1 x
inc (at-1 x) = at-0 (inc x)

inc===+1 : (x : Bin) -> === (μ (inc x)) (+ (μ x) one)
inc===+1 0b = refl
inc===+1 1b = refl
inc===+1 (at-0 x) = refl
inc===+1 (at-1 x) = ...

Das ist doch gar nicht schlecht. Die Definitionen für Bin und inc sind zwingend notwendig, wenn überhaupt etwas laufen soll. Die Denotation μ kann man in den meisten Programmiersprachen auch ausdrücken, um dann bspw. Unit-Tests formulieren zu können. In Agda gehen wir mit inc===+1 noch einen Schritt weiter und beweisen tatsächlich, dass sich unser inc wie +1 verhält. Mehr Verlässlichkeit geht nicht.