SemProg Braindump SS22

Overall this braindump is quite similar to one submitted for SS16 with some minor discrepancies.

Some preliminary questions

Do you prefer vanilla ltac or ssreflect?

Ltac.

Can you name the difference between `destruct` and `induction` ?

Both give one sub-goal for each constructor of an inductive term.
induction also gives an induction hypothesis for any inductive constructor.

General questions

How would one define Implication, disjunction and conjunction in Coq?

Implication is given by the builtin function type.
Disjunction can be implemented by a inductive datatype with two constructors.
For Conjunction I first answer with dependent pairs, then give the more coqish answer of a datatype constructor with two arguments.

Can you give some types with decidable equality?

I name \(\mathbb{B}\) and \(\mathbb{N}\).

Can you state what decidable equality means?

For two terms \(x\) and \(y\) either \(x \equiv y\) or \(x \not\equiv y\).

What about a list of bools?

A list of a type with decidable equality also has decidable equality.

How would you go about proving this?

Pair-wise application of the decidable equality of the element type over the list.

Can you explain what the `auto` tactic does?

It tries to solve trivial goals with assumption and intros, then does a search for applicable theorems in a hint database.

What about hint databases?

You can define your own databases, that's about all I know.

What is the default?

I don't remember this part (I mean who does?). Apparently it's core.

What is the difference between `auto` and `eauto`?

eauto can also deal with existential variables.

Can you explain what it means for a proposition to be reflected?

I fail to remember this exactly but am allowed my time to reason about the question.
Eventually I talk about how a proposition in Prop can be reflected to one in Bool, thus automatically making it decidable.

Imp

Can you explain how we defined semantics for `Imp`?

I don't really remember what the examiner is referring to here and try to steer the conversation towards Hoare Triples.

Can you explain what a Hoare Triple is?

A Triple of precondition, program and post-condition.

Can you give me some examples for Hoare Rules?

I give the assignment and sequence rules.

Another, more interesting one?

I try to give the rule for while expressions, but fail to give the correct precondition.

What extensions to `Imp` did we define?

Parallel Imp.

Can you explain the small step semantics of this parallel `Imp` program? For example, so that the post-condition `X=15` holds?

<{
  X := 5
  PAR
    X := X + 5
  WITH
    X := X + 5
  END
}>

STLC

Some questions about small step semantics that I don't remember.

Can you name the most important meta-theorems we proved for STLC?

I give some version of the progress and preservation theorems.

What restrictions where particular to our definitions of these theorems?

Only about closed terms, as our substitution algorithm was not capture avoiding.

Can you give an annotated version of an Imp Program?

I choose the swap program and begin to lay out the implementation and corresponding Assertions.
After backwards-reasoning the last two assignments I am stopped and asked to step out for the examiners to discuss my grade.

Conclusion

Relaxed atmosphere, I am allowed to take my time to reason about answers I did not immediately recall from memory.
Final Grade 1.3 (1.3 in exam and 1.0 in homework after doing most of the early extra exercises and barely submitting anything for the last two).
I am rather satisfied, the most difficult part of the exam is to get the lecturer to respond to your messages (exam was in the first week of lectures of the following semester).