====== Protokoll ======

Prüfer: Daniel, Lutz. Fragen nur von Daniel


===== Was macht contradiction =====

   - Antwort: Solved das Goal, wenn False im Kontext

   - Nachfrage: Was ist mit:
     
     H: 0 = 1
     ----------------------

   - Antwort: Geht net, nur mit inversion. contradiction will tatsächlich False (oder (A ∧ ¬A)) 

===== Wie implementiert man conjunction =====

   - Antwort: Induktiver Datentyp mit einem Konstruktor, der zwei Prämissen nimmt.

   - Frage: Wie prooft man es?
     
   - Antwort: split oder apply vom Konstructor

===== Was ist functional extensionality ====

   - forall x, f x = g x -> f = g

===== Wie haben wir Program-Equivalence definiert =====

   - Antwort:
     
     - Für expressions: Evaluieren auf das Gleiche
     - Für statements: Genau dann wenn das Eine mit state x terminiert, tuts das andere auch.

===== Was ist ein Hoare-Triple =====

    - { P } c { Q }
    - P, Q sind Assertions
    - P gilt auf st, c / st || st', Q gilt für st'

===== Schreibe die Hoare-Kalkül-Regeln hin =====

   - Hab skip, seq, if und while hingeschreiben, dann hat er gesagt, es passt schon

===== Beweisen sie ein Fakultätsprogramm in Hoare =====

   - Habe hingeschreben:

   #+BEGIN_EXAMPLE
   { y = n }
   X := 1;
   while (y > 0) then
     x := y * x; y := y - 1
   end
   { x = n! }

   - Anwenden: Seq, Assign, Consequence, While

   - Nachdem ich mit consequence die invariante hatte, hat er abgebrochen.

===== Was ist Big-Step vs Small-Step =====

   - Programm auf einmal komplett evaluieren vs. ec terminiertinzelne Evaluationsschritte

===== Was ist zB ein Vorteil von Small-Step =====

   - Implementierung von Parallel-Imp