Examiners: Tadeusz Litak, Christoph Rauch

The atmosphere was super relaxed and friendly, all of us had a few laughs. Several minor hickups and uncertainty of some details didn't matter at all.

Q: Does `contradiction` solve the following goal?

    Theorem x : true = false -> False.
    Proof.
      intros.

Q: Which tactic does solve it?

Q: Another one?

Q: What is the difference between `induction` and `inversion`?

Q: What does `induction` do that `inversion` doesn't?

Q: Is the following code correct?

  Inductive no_repeats : (l : list) -> Prop :=
  | nor_once : forall x l, appears_not_in x l -> no_repeats l -> no_repeats (x::l)
  | nor_forgot : forall x l, no_repeats l -> no_repeats (x::l)

[The second constructor might have been different, I can't remember the details]

`appears_not_in` was also defined and did what it sounds like.

Q: What is a hoare triple, what does it assert?

Q: Write down some hoare rules.

Q: [after writing down the sequence rule] Something more interesting?

Q: [after writing down the assignment rule] How about the rule for `while`?

Q: We talked about the simply-typed lambda calculus. What is the difference between our notions of terms in normal form and values?

Q: Which theorem connects types, normal forms and stuckness?

Q: [after stating a form of the progress theorem] We had another theorem involving types and reduction.

Q: Alright, that's the preservation theorem. Next, I have some new reduction/typing rules, choose one and state if determinism, preservation and progress are preserved.

1.
   
   ---------------- (ST_Foo1)   ------------- (ST_Foo2)
    (\x. x) => foo               foo => true

2.
   
   --------------------------------- (ST_IfTrue')
     if true then t0 else t1 => true

3. can't recall, something involving a typing rule

Q: [after elaborating on the first ruleset] Choose one more.

Q: Oh, I asked you about these additional rules, but I didn't even ask you about the basic ones. Show me the rules for abstraction and application.

Q: I'm not sure what more to ask you. Can you write down an annotated version of the swap program using only two variables?

We stopped after I backwards-reasoned one instance of the assignment rule (which took several attempts).


----

The text below has been written by a student from the future different from the author of the exam protocol above!

Here is some working Coq code for the no_repeats inductive question:

<code>
Fixpoint appears_not_in {X: Type} (x: X) (l: list X): Prop := match l with
| nil => True
| cons y ys => (x <> y) /\ (appears_not_in x ys)
end.

Inductive no_repeats {X: Type} : list X -> Prop :=
| nor_empty: no_repeats nil
| nor_cons: forall x l, appears_not_in x l -> no_repeats l -> no_repeats (x::l).
</code>