\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}}}

Repeat Exam \\
Tuesday 5 February 2019, 18:30--21:15, WN-S655 \\
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 may use standard mathematical notation or
Lean structured commands (e.g., \li{assume}, \li{have}, \li{show}, \li{calc}).
You may 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}{WHILE language with print}{6+6+6}

Consider the following Lean definition of the syntax of the ``PRINT
language,'' a variant of the familiar WHILE language featuring a \verb|print|
statement, which sends a string to the standard output channel:

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

\subquestion{a}%
%
The big-step semantics relation \li{⟹} relates pairs $(p, s)$, where $p$ is
a program to execute and $s$ an initial variable state, with pairs $(m, t)$, where $m$ is the
output message and $t$ is the final state. Intuitively, $(p, s)$~\li{⟹} $(m, t)$ means
that ``starting in a state $s$, executing $p$ ends in the state $t$,
printing $m$ in the process.'' For example:
\[\text{\li{(seq (print "ab") (print "ba"), s) ⟹ ("abba", s)}}\]
%
Give the big-step semantics rules (in traditional rule format or Lean
syntax) covering the statements \verb|skip|, \verb|print|, and \verb|seq|.

\subquestion{b}%
%
The small-step semantics relation \li{⟶} relates tuples $(p, (m, s))$, where
$p$ is the program to execute, $m$ is the initial contents of the output channel,
and $s$ is the initial variable state, with tuples $(p', (m', s'))$,
where $m'$ is $m$ extended with any output produced while executing one
step of $p$. For example:
%
\begin{align*}
                & \texttt{(seq (print "cada") (print "bra"), ("abra", s))}
\\[-\jot]
\longrightarrow~ & \texttt{(seq skip (print "bra"), ("abracada", s))}
\\[-\jot]
\longrightarrow~ & \texttt{(print "bra", ("abracada", s))}
\\[-\jot]
\longrightarrow~ & \texttt{(skip, ("abracadabra", s))}
\end{align*}
%
Give the small-step semantics rules (in traditional rule format or Lean
syntax) covering the statements \verb|skip|, \verb|print|, and \verb|seq|.

\subquestion{c}%
%
Program equivalence \li{≈} is defined in terms of the big-step semantics in
the usual way:
%
\[\hbox{\li{p₁} \li{≈} \li{p₂}\; if and only~if \;\li{∀s mt, (p₁, s) ⟹ mt ↔ (p₂, s) ⟹ mt}.}\]
%
Prove or disprove the equivalences below. In the ``prove'' case, give an
informal argument for both directions of the equivalence. In the ``disprove''
case, give a counterexample, including instantiations of the variables
occurring in the equivalences and in the definition of \li{≈}, and explain why
it is a counterexample.

\begin{enumerate}
\item[1.] \li{while b do skip ≈ skip}
\item[2.] \li{seq (seq p q) r ≈ seq p (seq q r)}
\item[3.] \li{print m ≈ skip}
\end{enumerate}

\newpage
\question{2}{2--3 trees}{4+6+4+7}

Consider the following Lean definition of 2--3 trees as an inductive type:
%
\begin{lstlisting}
  inductive tree (α : Type) : Type
  | empty {} : tree
  | bin      : α → tree → tree → tree
  | ter      : α → tree → tree → tree → tree
\end{lstlisting}

\subquestion{a}%
%
Complete the following Lean definition. The \verb|map_tree| function should
apply its argument \li{f} to all values of type \li{α} stored in the tree and
otherwise preserve the tree's structure.
%
\begin{lstlisting}
  def map_tree {α β : Type} (f : α → β) : tree α → tree β
\end{lstlisting}

\subquestion{b}%
%
Prove the following lemma about your definition of \li{map_tree}.
%
\begin{lstlisting}
  lemma map_tree_id {α : Type} :
    ∀t : tree α, map_tree (λx : α, x) t = t
\end{lstlisting}

\subquestion{c}%
Complete the following Lean definition. The \verb|set_tree| function should
return the set of all values of type \li{α} stored in the tree. In your
answer, you may use traditional set notations regardless of whether they are
actually supported by Lean.
%
\begin{lstlisting}
  def set_tree {α : Type} : tree α → set α
\end{lstlisting}

\subquestion{d}%
%
A \emph{congruence rule} is a lemma that can be used to lift an equivalence
relation between terms to the same terms occurring under a common context.
Congruence rules for equality are built into Lean's logic. In the following
example, the equivalence relation is \verb|=|, the terms are \verb|f| and
\verb|g|, and the context is \verb|map_tree|~{\dots}~\verb|t|:
%
\begin{lstlisting}
  lemma map_tree_congr_weak {α β : Type} (f g : α → β) (f = g) (t : tree α) :
    map_tree f t = map_tree g t :=
  by simp *
\end{lstlisting}
%
Regrettably, the above rule is not as flexible as it could be. As long as \li{f}
and \li{g} are equal for all values~\li{x : α} stored in \li{t}, we have
\,\li{map_tree f t = map_tree g t},
even if \li{f} and \li{g} disagree on other \li{α}~values. Inspired by
this observation, prove the following stronger congruence rule.
%
\begin{lstlisting}
  lemma map_tree_congr_strong {α β : Type} (f g : α → β) :
    ∀t : tree α, (∀x, x ∈ set_tree t → f x = g x) → map_tree f t = map_tree g t
\end{lstlisting}

\newpage
\question{3}{Hoare logic gone wild}{4+4+8}

Consider the standard WHILE language, as described in the lecture, and the
following definition of partial-correctness Hoare triples:
\[\hbox{\verb|{* P *} p {* Q *}|\; if and only if \;\li{∀s t, P s → (p, s) ⟹ t → Q t}.}\]

\subquestion{a}%
Louis Reasoner proposes the following Hoare rule for reasoning about
\verb|while| loops:

\begin{lstlisting}
  lemma while_intro_lr (h : {* P *} p {* P *}) :
    {* P *} while c p {* λs, P s ∧ ¬ c s *}
\end{lstlisting}

Is this rule sound? Is it complete? Justify your answer to each question with
a brief proof sketch or a counterexample.

\subquestion{b}%
Alyssa P. Hacker and Ben Bitdiddle cannot agree on what a sound and complete
consequence rule for Hoare logic should look like. Ms.\ Hacker believes the
correct rule is as follows:
%
\begin{lstlisting}
  lemma consequence_aph (h : {* P *} p {* Q *})
      (hp : ∀s, P' s → P s) (hq : ∀s, Q s → Q' s) :
    {* P' *} p {* Q' *}
\end{lstlisting}
%
Mr.\ Bitdiddle is convinced that she has exchanged the premise~\verb|h| and
the conclusion. He claims the correct rule is
%
\begin{lstlisting}
  lemma consequence_bb (h : {* P' *} p {* Q' *})
      (hp : ∀s, P' s → P s) (hq : ∀s, Q s → Q' s) :
    {* P *} p {* Q *}
\end{lstlisting}
%
Who is right? Why?

\subquestion{c}%
The standard Hoare rule for reasoning about \li{if}--\li{then}--\li{else}
statements is as follows:
%
\begin{lstlisting}
  lemma ite_intro
      (h₁ : {* λs, P s ∧   c s *} p₁ {* Q *})
      (h₂ : {* λs, P s ∧ ¬ c s *} p₂ {* Q *}) :
    {* P *} ite c p₁ p₂ {* Q *}
\end{lstlisting}
%
Eva Lu Ator has come up with an alternative rule, where the premises'
preconditions are variables:
%
\begin{lstlisting}
  lemma ite_intro_ela
      (h₁ : {* R₁ *} p₁ {* S *})
      (h₂ : {* R₂ *} p₂ {* S *}) :
    {* λs, (c s ∧ R₁ s) ∨ (¬ c s ∧ R₂ s) *} ite c p₁ p₂ {* S *}
\end{lstlisting}
%
Prove that Ms.\ Lu Ator's rule is equivalent to the standard rule.

\emph{Hint:} Equivalence can be established by deriving each rule from the
other, \emph{without} expanding the definition of Hoare triples. You can
exploit basic properties of the logical connectives and the correct Hoare
consequence rule from subquestion 3b.

\newpage
\question{4}{Binary trees as a subset type}{3+5+3+4+5}

Recall the Lean definition of 2--3 trees from Question~2:
%
\begin{lstlisting}
  inductive tree (α : Type) : Type
  | empty {} : tree
  | bin      : α → tree → tree → tree
  | ter      : α → tree → tree → tree → tree
\end{lstlisting}

\subquestion{a}%
%
A \emph{binary tree} is a 2--3 tree that is built without using the \li{ter}
constructor. Complete the following Lean definition of an inductive predicate
that captures this concept.
%
\begin{lstlisting}
  inductive is_binary {α : Type} : tree α → Prop
  | empty : is_binary empty
\end{lstlisting}

\subquestion{b}%
%
Prove that applying the \li{map_tree} function from subquestion~2a preserves
the binary nature of a binary tree. Formally:
%
\begin{lstlisting}
  lemma is_binary_map_tree {α β : Type} {f : α → β} :
    ∀t : tree α, is_binary t → is_binary (map_tree f t)
\end{lstlisting}

\subquestion{c}%
%
Use Lean's subtype mechanism to define the type \verb|btree|~\li{α} of binary
trees by carving out the binary trees from the 2--3 trees, by filling in the
hole (\verb|_|) below.
%
\begin{lstlisting}
  def btree (α : Type) : Type := _
\end{lstlisting}

\subquestion{d}%
%
Basic operations on binary trees include the empty binary tree and the binary
node constructor, which takes an \li{α} value and two binary trees and returns
a binary tree.

Fill in the two holes (\verb|_|) below to implement these operations.

Parts of the holes correspond to proof terms. For each of these, state the
property that must be proved and explain very briefly why it should hold.

\begin{lstlisting}
  def empty_btree {α : Type} : btree α := _
  def bin_btree {α : Type} (a : α) (l r : btree α) : btree α := _
\end{lstlisting}

\subquestion{e}%
%
The \li{map_tree} and \li{set_tree} operations defined in subquestions 2a and
2c can be used to define the corresponding operators on binary trees.

Fill in the two holes (\verb|_|) below to implement these operations.

Part of the second hole corresponds to a proof term. State the property that
must be proved and explain very briefly why it should hold.

\begin{lstlisting}
  def set_btree {α : Type} (t : btree α) : set α := _
  def map_btree {α β : Type} (f : α → β) (t : btree α) : btree β := _
\end{lstlisting}

\newpage
\question{5}{Reflexive symmetric closure}{4+7+4}

In mathematics, the reflexive symmetric closure $\Leftrightarrow^=$ of a
binary relation~$\Rightarrow$ over a set $A$ is defined as the smallest
relation satisfying the following rules:

\begin{description}
\item[(base)] for all $a, b \in A$, if $a \Rightarrow b$, then $a \Leftrightarrow^= b$;
\item[(refl)] for all $a \in A$, $a \Leftrightarrow^= a$;
\item[(symm)] for all $a, b \in A$, if $a \Leftrightarrow^= b$, then
  $b \Leftrightarrow^= a$.
\end{description}

\subquestion{a}%
%
Completing the Lean definition below of a predicate \li{rsc} whose
introduction rules closely follow the rules \textbf{(base)}, \textbf{(refl)},
and \textbf{(symm)}:
%
\begin{lstlisting}
  inductive rsc {α : Type} (r : α → α → Prop) : α → α → Prop
\end{lstlisting}

\subquestion{b}%
%
Prove that the reflexive symmetric closure of a relation $\Rightarrow$ that is
reflexive and symmetric is equivalent to the relation $\Rightarrow$ itself. Formally:
%
\begin{lstlisting}
  lemma refl_symm_imp_rsc_iff {α : Type} {r : α → α → Prop}
      (refl_r : ∀a, r a a) (symm_r : ∀a b, r a b → r b a) :
    ∀a b : α, rsc r a b ↔ r a b
\end{lstlisting}

\emph{Hint}: Start with the easy direction. For the other direction, use rule
induction.

\subquestion{c}%
%
Use the lemma \verb|refl_symm_imp_rsc_iff| from subquestion~5b to derive
\verb|rsc|'s idempotence. Formally:
%
\begin{lstlisting}
  lemma rsc_rsc_iff_rsc {α : Type} {r : α → α → Prop} :
    ∀a b : α, rsc (rsc r) a b ↔ rsc r a b
\end{lstlisting}

\vfill

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

\end{document}
