\documentclass[11pt]{letter}
\usepackage[utf8x]{inputenc}
\usepackage[margin=2.5cm]{geometry}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{bussproofs}
\usepackage{color}
\usepackage{enumitem}
\usepackage{graphicx}
\usepackage{stmaryrd}
\usepackage{version}
\usepackage{xspace}
\usepackage{wasysym}

%% BEGIN Times font etc.
\usepackage{mathptmx}
%\usepackage[scaled=.82]{beramono}
\usepackage[scaled=.865]{helvet}
%\usepackage{avant}
\DeclareSymbolFont{letters}{OML}{txmi}{m}{it}
%% END Times font etc.

\usepackage{color}
\definecolor{keywordcolor}{rgb}{0.7, 0.1, 0.1}   % red
\definecolor{commentcolor}{rgb}{0.4, 0.4, 0.4}   % grey
\definecolor{symbolcolor}{rgb}{0.0, 0.1, 0.6}    % blue
\definecolor{sortcolor}{rgb}{0.1, 0.5, 0.1}      % green

\usepackage{listings}
\def\lstlanguagefiles{lstleanbw.tex}
\lstset{language=lean}

\newcommand\question[3]{\let\questionnum=#1\bigskip{\large\textbf{Question #1.}\enskip #2{}\quad (#3 points)}\medskip}
\newcommand\subquestion[1]{\noindent\llap{\textbf{\questionnum#1.}\enskip}}

\let\li=\lstinline

\excludeversion{answer}
%\newenvironment{answer}{\begingroup\color{blue}\par\medskip\textbf{Answer:}\par\smallskip}{\endgroup}

\EnableBpAbbreviations
\def\ScoreOverhang{2pt}
\def\proofSkipAmount{\vskip 0pt}
\def\defaultHypSeparation{\hskip1em}

\begin{document}

Logical Verification 2018--2019 \\
Vrije Universiteit Amsterdam \\
Lecturers: dr.\ J.\,C. Blanchette and dr.\ J. H\"olzl
\hfill\smash{\makebox[0mm][r]{\includegraphics[height=10mm]{griffioen.png}}}

Final Exam \\
Tuesday 18 December 2018, 15:15--18:00, WN-Q112 \\
5 questions, 90 points \\
Answers may be given in English or Dutch

\renewcommand{\theenumi}{\alph{enumi}}

\bigskip\textbf{\large Proof Guidelines}\medskip

We expect detailed, rigorous, mathematical proofs, but we do not ask you to
write Lean proofs. You are welcome to use standard mathematical notation or
Lean structured commands (e.g., \li{assume}, \li{have}, \li{show}, \li{calc}).
You can also use tactical proofs (e.g., \li{intro}, \li{apply}), but then
please indicate some of the intermediate goals, so that we can follow the
chain of reasoning.

Major proof steps, especially applications of induction and invocation of the
induction hypothesis, must be stated explicitly. For each case of a proof by
induction, you must list the inductive hypotheses assumed (if any) and the
goal to be proved. Minor proof steps corresponding to \li{refl}, \li{simp}, or
arithmetic need not be justified if you think they are obvious (to humans),
but you should say which key lemmas they follow from.

You should be explicit whenever you use a function definition or an
introduction rule for an inductive predicate, especially for functions and
predicates that are specific to an exam question.

\begin{answer}
This version of the exam includes suggested answers, presented in blocks like
this one. Many of the proposed proofs are atypical in that they were developed
using Lean and are syntactically correct. Such proofs would be accepted at the
exam, but we realize that it is hard to develop correct Lean proofs on paper;
hence the flexible proof guidelines above.
\end{answer}

\medskip

\bigskip\textbf{\large In Case of Ambiguities or Errors in an Exam Question}\medskip

The staff present at the exam has the lecturers' phone numbers, in case of
questions or issues concerning a specific exam question. Nevertheless, we
strongly recommend that you work things out yourselves, stating explicitly any
ambiguity or error and explaining how you interpret or repair the question.
The more explicit you are, the easier it will be for the lecturers to grade
the question afterwards.


\newpage
\question{1}{Transitive closure}{3+3+5+7}

In mathematics, the transitive closure $\mathbin{R}^+$ of a binary
relation~$R$ over a set $A$ can be defined as the smallest solution satisfying
the following rules:

\begin{description}
\item[(base)] for all $a, b \in A$, if $a \mathrel{R} b$, then $a \mathrel{R}^+ b$;
\item[(step)] for all $a, b, c \in A$, if $a \mathrel{R} b$ and $b \mathrel{R}^+ c$,
  then $a \mathrel{R}^+ c$.
\end{description}

In Lean, we can define this concept as follows:

\begin{lstlisting}
  inductive tc₁ {α : Type} (r : α → α → Prop) : α → α → Prop
  | base : ∀a b, r a b → tc₁ a b
  | step : ∀a b c, r a b → tc₁ b c → tc₁ a c
\end{lstlisting}

\subquestion{a}%
Rule \textbf{(step)} makes it convenient to extend transitive chains by adding
links to the left. Another way to define the transitive closure
$\mathbin{R}^+$ would use the following rule instead of \textbf{(step)}, with
a preference for the right:

\begin{description}
\item[(pets)] for all $a, b, c \in A$, if $a \mathrel{R}^+ b$ and $b \mathrel{R} c$,
  then $a \mathrel{R}^+ c$.
\end{description}

Define, using Lean syntax, a predicate \li{tc₂} that embodies this alternative
definition.

\subquestion{b}%
Yet another definition of the transitive closure $\mathbin{R}^+$ would use the
following symmetric rule instead of \textbf{(step)} or \textbf{(pets)}:

\begin{description}
\item[(trans)] for all $a, b, c \in A$, if $a \mathrel{R}^+ b$ and $b \mathrel{R}^+ c$,
  then $a \mathrel{R}^+ c$.
\end{description}

Define, using Lean syntax, a predicate \li{tc₃} that embodies this alternative
definition.

\subquestion{c}%
Prove that \textbf{(step)} also holds as a lemma about
\li{tc₃} as defined in subquestion~1b above. In Lean syntax:

\begin{lstlisting}
  lemma tc₃_step {α : Type} (r : α → α → Prop) :
    ∀a b c : α, r a b → tc₃ r b c → tc₃ r a c
\end{lstlisting}

\subquestion{d}%
Prove by rule induction on the \li{tc₁} \li{r} \li{a} \li{b} premise below that
\textbf{(pets)} also holds as a lemma about \li{tc₁} as defined above.

\begin{lstlisting}
  lemma tc₁_pets {α : Type} (r : α → α → Prop) :
    ∀a b c : α, tc₁ r a b → r b c → tc₁ r a c
\end{lstlisting}

%\subquestion{e}%
%Prove by rule induction that rule~(trans) also holds about \li{tc₁} as defined
%above. In Lean syntax:
%
%\begin{lstlisting}
%  lemma tc₁_trans {α : Type} (r : α → α → Prop) :
%    ∀a b c : α, tc₁ r a b → tc₁ r b c → tc₁ r a c :=
%\end{lstlisting}

\newpage
\question{2}{Element count in a list}{5+6+7}

(For this question, we assume that we work in a classical logic, in which all
propositions are considered decidable and noncomputable functions are allowed.
In Lean, this is achieved by the following declarations:

\begin{lstlisting}
  local attribute [instance, priority 0] classical.prop_decidable

  noncomputable theory
\end{lstlisting}

\vskip-2.15\baselineskip

\noindent\kern12em)

Consider the following Lean definitions on the predefined \li{list} type:

\begin{lstlisting}
  def mem {α : Type} (a : α) : list α → Prop
  | []        := false
  | (x :: xs) := x = a ∨ mem xs

  def reverse {α : Type} : list α → list α
  | []        := []
  | (x :: xs) := reverse xs ++ [x]
\end{lstlisting}

\subquestion{a}%
Complete the following definition of a function \li{count} \li{a} \li{xs} that
returns the number of occurrences of a value \li{a} in a list \li{xs}.

\begin{lstlisting}
  def count {α : Type} (a : α) : list α → ℕ
\end{lstlisting}

\subquestion{b}%
Prove the following lemma, which relates the \li{count} function defined in
subquestion~2a with the \li{mem} function defined above.

\begin{lstlisting}
  lemma count_eq_zero_iff_not_mem {α : Type} (a : α) :
    ∀xs, count a xs = 0 ↔ ¬ mem a xs
\end{lstlisting}

\subquestion{c}%
Prove the following lemma, involving the \verb|reverse| function defined above.

\begin{lstlisting}
  lemma count_reverse_eq_count {α : Type} (a : α) :
    ∀xs : list α, count a (reverse xs) = count a xs
\end{lstlisting}

Make sure to state and prove any nontrivial auxiliary lemmas you may need to
reason about the \li{count} or \li{reverse} function.

\newpage
\question{3}{Finite multisets as quotients and subsets}{4+6+5+6+4}

(As for Question~2, for this question, we assume that we work in a classical
logic, in which all propositions are considered decidable and noncomputable
functions are allowed.)

A multiset (or bag) is a collection of elements that allows for multiple
(but finitely many) occurrences of its elements. For example,
$\{3, 5\} = \{5, 3\} \not= \{5, 3, 3\}$.

Finite multisets can be defined in at least two different ways. We will
explore these.

\subquestion{a}%
%
One way to define finite multisets is to start with a raw type of finite lists
and to consider only the \emph{number of occurrences} of elements in the lists,
ignoring the order in which elements occur. Following this scheme,
\li{[5, 3, 3]}, \li{[3, 5, 3]}, and \li{[3, 3, 5]} would be three
representations of the multiset $\{5, 3, 3\}$.

In Lean, this could be achieved as follows:

\begin{lstlisting}
  instance multiset₁.rel (α : Type) : setoid (list α) :=
  { r     := _,
    iseqv :=
    ⟨ (assume xs, by simp),
      (assume xs ys ys_xs x, by simp *),
      (assume xs ys zs xs_ys ys_zs, by simp *) ⟩ }

  def multiset₁ (α : Type) : Type := quotient (multiset₁.rel α)
\end{lstlisting}

However, there is a hole (\verb|_|) in the definition, standing for the term
specifying the equivalence relation \li{r} used for the quotient construction.

Supply the missing term. You may use the \li{count} function from
Question~2 if it helps.

\subquestion{b}%
Basic operations on multisets include the empty multiset ($\emptyset$),
the singleton multiset ($\{a\}$ for any element~$a$), and the sum of two
multisets ($A \uplus B$ for any multisets $A$ and $B$). The sum should be
defined so that the multiplicity of elements are added; for example, $\{1\}
\uplus \{1, 1\} = \{1, 1, 1\}$.

Fill in the three holes (\verb|_|) below to implement the basic multiset
operations.

\begin{itemize}
\item
For the first two holes, actual Lean terms are expected.

\item
For the third hole, state the property that must be proved and explain briefly
why it holds. You may assume reasonable lemmas about \li{count}.
\end{itemize}

\begin{lstlisting}
  def empty_mset₁ {α : Type} : multiset₁ α := ⟦[]⟧

  def singleton_mset₁ {α : Type} (a : α) : multiset₁ α := _

  def sum_mset₁ {α : Type} (A : multiset₁ α) (B : multiset₁ α) : multiset₁ α :=
  quotient.lift_on₂ A B _ _
\end{lstlisting}

\subquestion{c}%
Multisets over a type~\li{α} are isomorphic to the function space \li{α → ℕ},
in the same way that sets over~\li{α} are isomorphic to \li{α → Prop}.
Finite multisets correspond to functions with finite support.
The \emph{support} of a function~\verb|f| is defined formally as
\verb|{|\li{x | f x ≠ 0}\verb|}|.

Use Lean's subtype mechanism to introduce an alternative definition of finite
multisets by carving out the functions of finite support from the function space
\li{α → ℕ}, by filling in the hole (\verb|_|) below.

\begin{lstlisting}
  def multiset₂ (α : Type) : Type := _
\end{lstlisting}

Your definition may use the following predicate, which captures the notion of
a finite set:

\begin{lstlisting}
  inductive finite {α : Type} : set α → Prop
  | empty : finite ∅
  | singleton (a : α) : finite (insert a ∅)
  | union (A B : set α) (fin_A : finite A) (fin_B : finite B) : finite (A ∪ B)
\end{lstlisting}

\subquestion{d}%
Implement the basic operations described in subquestion~3b on the subtype
representation of multisets, by filling in the three holes (\verb|_|) below.
Supply any necessary proofs as well, informally, possibly by appealing to
the inductive definition of \li{finite} provided above.

\begin{lstlisting}
  def empty_mset₂ {α : Type} : multiset₂ α := _
  def singleton_mset₂ {α : Type} (a : α) : multiset₂ α := _
  def sum_mset₂ {α : Type} (A B : multiset₂ α) : multiset₂ α := _
\end{lstlisting}

\subquestion{e}%
Define a Lean function that converts the quotient representation of a multiset
to its subtype representation, by filling in the two holes (\verb|_|) below.

The second hole and parts of the first hole correspond to proof terms. For
each of these, state the property that must be proved and explain very briefly
why it should hold. You may assume reasonable lemmas about sets and the
\li{finite} predicate.

\begin{lstlisting}
  def mset₂_of_mset₁ {α : Type} (A : multiset₁ α) : multiset₂ α :=
  quotient.lift_on A _ _
\end{lstlisting}

\newpage
\question{4}{Hoare logic for DOWHILE language}{5+5+5}

We start by defining the abstract syntax of two variants of the WHILE
language. The first variant is the standard WHILE language as seen in class
(but now called \li{wl}):

\begin{lstlisting}
  inductive wl (σ : Type) : Type
  | skip {} : wl
  | assign  : (σ → σ) → wl
  | seq     : wl → wl → wl
  | ite     : (σ → Prop) → wl → wl → wl
  | while   : (σ → Prop) → wl → wl
\end{lstlisting}

The second variant is a ``DOWHILE'' language:

\begin{lstlisting}
  inductive dl (σ : Type) : Type
  | skip  {} : dl
  | assign   : (σ → σ) → dl
  | seq      : dl → dl → dl
  | unless   : dl → (σ → Prop) → dl
  | do_while : dl → (σ → Prop) → dl
\end{lstlisting}

The last two statements are new:

\begin{itemize}
\item \verb|unless| \verb|p| \verb|c| executes \verb|p| if \verb|c| is \emph{false} in
  the current state; otherwise it does nothing. This statement is inspired by
  Perl's \verb|unless| conditional.

\item \verb|do_while| \verb|p| \verb|c| first executes \verb|p|. Then, if
  \verb|c| is true in the resulting state, it reenters the loop and executes \verb|p| again,
  and continues executing \verb|p| until \verb|c| becomes false. The semantics is almost
  the same as \verb|while| \verb|c| \verb|p|, except that \verb|p| is always executed at
  least once, even if the condition is not true initially. This statement is inspired
  by C's and Java's \verb|do| \verb|{| \dots \verb|}| \verb|while| \verb|(|\dots\verb|)| loop.
\end{itemize}

\subquestion{a}%
Define a Lean function that translates a DOWHILE program to a WHILE program with the
same big-step semantics, by completing the following definition:

\begin{lstlisting}
  def wl_of_dl (σ : Type) : dl σ → wl σ
\end{lstlisting}

\subquestion{b}%
Give a sound and as-complete-as-possible partial correctness Hoare rule, or set of Hoare rules,
for the DOWHILE language's \verb|unless| statement.
Briefly justify how you derived the rule(s).
You may use the traditional rule format (with a horizontal bar) or Lean syntax
to specify the rule(s).

\emph{Hint:} One possible way to derive and justify your Hoare rule(s) is to apply the
translation function developed in subquestion~4a and then to apply standard
Hoare rules on the translation.

\subquestion{c}%
%
Give a sound and as-complete-as-possible partial correctness Hoare rule, or
set of Hoare rules, for the DOWHILE language's \verb|do_while| statement.
Briefly justify how you derived the rule(s).
You may use the traditional rule format or Lean syntax to specify the rule(s).

\newpage
\question{5}{Denational semantics of LOOP and REPEAT languages}{5+6+3}

\subquestion{a}%
The ``LOOP'' language is identical to WHILE, except that its looping
statement, called \li{loop}, executes its body an unspecified number of times
(zero or more times).

\begin{lstlisting}
  inductive ll (σ : Type) : Type
  | skip {} : ll
  | assign  : (σ → σ) → ll
  | seq     : ll → ll → ll
  | ite     : (σ → Prop) → ll → ll → ll
  | loop    : ll → ll
\end{lstlisting}

Complete the following relational denotational semantics, by filling in the
two holes (\verb|_|). You may use the transitive closure operator developed in
Question~1 to specify the semantics of a loop (instead of a fixpoint
operator).

\begin{lstlisting}
  def den (σ : Type) : ll σ → set (σ × σ)
  | ll.skip        := _
  | (ll.assign f)  := {st | st.2 = f st.1}
  | (ll.seq p q)   := den p ◯ den q
  | (ll.ite c p q) := (den p ⇃ c) ∪ (den q ⇃ (λs, ¬ c s))
  | (ll.loop p)    := _
\end{lstlisting}

\subquestion{b}%
The ``REPEAT'' language is identical to WHILE, except that it executes its
body a fixed number of times; for example, \li{repeat} \li{3} \li{p} executes
\li{p} three times in sequence.

\begin{lstlisting}
  inductive rl (σ : Type) : Type
  | skip {} : rl
  | assign  : (σ → σ) → rl
  | seq     : rl → rl → rl
  | ite     : (σ → bool) → rl → rl → rl
  | repeat  : ℕ → rl → rl
\end{lstlisting}

Complete the following functional denotational semantics, which executes a
REPEAT program from an initial state, returning a final state. Do not worry
yet about termination.

\begin{lstlisting}
  def run (σ : Type) : rl σ → σ → σ
  | rl.skip       s := s
  | (rl.assign f) s := f s
\end{lstlisting}

\subquestion{c}%
Now you may worry about termination. Does the \verb|run| function defined in
subquestion~5b terminate? If yes, explain briefly why (e.g., by providing a
well-founded relation or a measure that decreases with every recursive call).
If no, provide a counterexample (e.g., a program, an initial state, and a brief
explanation of what goes wrong).

\vfill

\em The grade for the exam is the total amount of points divided by 10, plus 1.

\end{document}
