Beweisen von Listentheoremen mit vollständiger Induktion – ein Beispiel

[ Gliederung ] [ Einführung ] [ Listenoperationen I ] [ Vollständige Induktion ] [ Listenoperationen II ] [ Literatur ]

Allgemein: Genau wie die natürlichen Zahlen, sind auch Listen aufgrund ihrer Struktur für Beweise mit vollständiger Induktion prädestiniert.
Wo wir bei natürlichen Zahlen als Induktionsanfang (im Folgenden I.A.) n=0 (oder n=1) einsetzen, verwenden wir bei Listen [].
Im Induktionsschritt (I.S.)wird nicht von n auf n+1 geschlossen, sondern von xs auf x:xs.
Die einzelnen Umrechnungsschritte erfolgen durch pattern-matching auf unsere Definitionsgleichungen.

Definitionen:

(++)       :: [a]->[a]->[a]
[]++ys     =  ys
(x:xy)++ys =  x:(xs++ys)

rev        :: [a]->[a]
rev[]      =  []
rev(x:xs)  =  rev xs ++ [x]  

Satz:
„rev (rev xs)=xs“ für alle endlichen Listen xs.

Bew.: Mit vollständiger Induktion.
I.A.: rev (rev []) = rev [] = []
I.S.: z.Z.: rev ( rev (x:xs)) = x:xs
Linke Seite:
      rev (rev (x:xs)) 
    =           {Definition von rev}
      rev (rev xs ++[x])
rechte Seite:
      x:xs
    =           {Induktionshypothese}
      x:rev (rev xs)
-> z.Z.: rev (rev xs ++[x]) = x:rev(rev xs)

-> Verallgemeinerung: Satz[2]: rev (ys ++[x]) = x:rev ys

Wir sind jetzt an einer Stelle angelangt, an der wir zum Beweis unseres Satztes einen anderen Satz beweisen müßen. Der oben stehende Satz erscheint plausibel, er läßt sich allerdings nicht direkt aus unseren Definitionen ableiten.
Es ist also ein erneuter Beweis mit vollständiger Induktion angebracht.

Bew.[2]: mit vollständiger Induktion
I.A.: rev([]++[x]) = rev([x]) = rev []++[x] = x:[] = x:rev []
I.S.: z.Z. rev ((y:ys) ++[x]) = x:rev (y:ys)
linke Seite:
      rev ((y:ys)++[x]
    =           {Definition von ++}
      rev (y:(ys++[x]))
    =           {Definition von rev}
      rev (ys++[x]) ++ [y]
    =           {Induktionsannahme}
      (x:rev ys) ++ [y]
    =           {Definition von ++}
      x: (rev ys ++[y])
    =           {Definition von rev}
      x: rev (y:ys)
[=rechte Seite]
q.e.d!

[ Gliederung ] [ Einführung ] [ Listenoperationen I ] [ Vollständige Induktion ] [ Listenoperationen II ] [ Literatur ]