Prüfer: Daniel Gorín, Lutz Schröder
löst pressburger-arithmetik
antwort wäre gewesen:
Inductive ex (X:Type) (P : X->Prop) : Prop := ex_intro : forall (witness:X), P witness -> ex X P.
hab mich bissi vertan, und
Inductive ex {X : Type} (x : X) ...
angefangen, so dass wir einen kleinen ausflug nach „welchen typ hat der ausdruck »X > 5«? (nat → Prop) gemacht haben.
Axiom, das sagt, dass wenn forall x. f x = g x, dann ist f = g. ist in coq so nicht beweisbar, weil nur dinge für die man einen beweis konstruieren kann beweisbar sind.
Axiom funny: exists (X Y : Type) (x : X) (f g : X -> Y), f x = g x -> f = g.
also functional extensionality, nur mit existenz- statt allquantor.
tripel aus vorbedingung, codestück und nachbedingung. wenns gültig ist, dann sagts, dass falls vorbedingung gilt, und codestück terminiert, dannach nachbedingung gilt.
(hoare_asgn) --------------------------- {{[X/s]P}} X := s {{P}}
for-schleife allgemein
FOR (C1; guard; C2) { C3 }
hoare-tripel
{{P'}}C1{{P}} {{P}} WHILE guard DO C3; C2 END {{P ∧ ¬guard}} ---------------------------------------------------------------- {{P'}} FOR (C1; guard; C2) { C3 } {{P ∧ ¬guard}}
damit war die zeit auch schon rum, leider (auch etwas zu daniels überraschung), und die ganzen coolen dinge, wie typ-foo (progress, typerhaltung) und lambda-zeugs kamen garned dran
zusammen mit meinem übungsabgabenergebnis von umgerechnet 2.4 wars am ende ne 2.0