commented add_assoc

ind/Intro.v

@@ -159,25 +159,66 @@ Fixpoint atom_occurs (f : formula) (a : string) : BOOL :=
    gleiche geblieben. *)
 
 (** * (Strukturelle) Induktion *)
-(* TODO *)
+(** Induktion ist nun das korrespondierende Beweisprinzip für rekursive
+   Funktionen. Mit Rekursion definiert man eine Funktion, indem man für jeden
+   Konstruktor eine Definitionsvorschrift angibt. Mit Induktion gibt man einen
+   Beweis für jeden Konstruktor an, um eine Aussage für alle Elemente der 
+   induktiven Struktur zu beweisen. Schauen wir uns das direkt praktisch an: *)
+
 Theorem add_assoc :
   forall (n1 n2 n3 : NAT),
     add n1 (add n2 n3) = add (add n1 n2) n3.
+(** Wir haben jetzt das [Theorem] niedergeschrieben, das wir beweisen wollen.
+   Wir wollen also zeigen, dass die Addition [add], die wir oben definiert
+   haben, assoziativ ist, also dass [n1 + (n2 + n3)] = (n1 + n2) + n3] für alle
+   [n1],[n2] und [n3] gilt. Mittels [Proof] leiten wir nun den Beweis ein. *)
 Proof.
+  (** Mit [intros n1] leiten wir den Beweis mit den typischen Worten "Sei [n1]
+     eine natürliche Zahl [NAT]." ein. *)
   intros n1.
+  (** Kommen wir nun zum spannenden Teil: Induktion über (die natürliche Zahl)
+     [n1]. Durch das Pattern [[|n1' IH]] benennen wir die "kleineren" Argumente:
+     - Im ersten Fall nehmen wir [n1 = zero] an, weshalb wir hier keine neuen
+       Variablen haben.
+     - Im zweiten Fall nehmen wir [n1 = succ (n1')] an, weshalb wir [n1']
+       benannt haben. Außerdem geben wir der _Induktionshypothese_ den Namen
+       [IH]. *)
   induction n1 as [|n1' IH].
   -
+    (** Fall 1, oft auch _Induktionsanfang_ genannt. (Auch wenn ich persönlich
+       diese Benennung für nicht notwendig halte.) Weil wir hier den Fall
+       betrachten, dass [n1 = zero], müssen wir noch zeigen, dass für alle [n2]
+       und [n3] gilt, dass [0 + (n2 + n3) = (0 + n2) + n3]. Dazu führen wir nun
+       zunächst die beiden [NAT]'s [n2] und [n3] mittels [intros n2 n3] ein. *)
     intros n2 n3.
+    (** Die Taktik [simpl] vereinfacht das Beweisziel. Dies ist hier möglich,
+       weil die Funktion [add] ausgewerted werden kann, weil die Struktur des
+       ersten Arguments ([zero]) bekannt ist. *)
     simpl.
+    (** Da nun links und rechts das gleiche steht, gilt diese Gleichung. Dies
+       zeigen wir mittels [reflexivity]. *)
     reflexivity.
   -
+    (** Nun zu Fall 2, oft auch _Induktionsschritt_ genannt. (Auch diese
+       Benennung halte ich persönlich für nicht notwendig.) Weil wir hier den
+       Fall betrachten, dass [n1 = succ(n1')], müssen wir (unter Annahme der
+       [IH]) zeigen, dass [(n1' + 1) + (n2 + n3) = ((n1' + 1) + n2) + n3] für
+       alle [n2] und [n3] gilt. Wir verfahren wie im ersten Fall: *)
     intros n2 n3.
     simpl.
+    (** Durch [specialize] spezialisieren wir nun die IH auf unser aktuelles
+       Beweisziel. Mit [rewrite IH] können wir diese Gleichung zum Umschreiben
+       des Beweisziels verwenden.
+       
+       Kurze Frage zum Nachdenken: Warum ist die [IH] allquantifiziert über
+       [n2] und [n3]? Wäre das auch bei Pen&Paper-Beweisen der Fall? *)
     specialize IH with (n2 := n2) (n3 := n3).
     rewrite IH.
     reflexivity.
 Qed.
 
+(* TODO *)
+
 Lemma add_zero_r : 
   forall (n : NAT), 
     add n zero = n.