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

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

Mock Exam \\
Thursday 32 Movember 2018, 15:15--18:00, WN-Y666 \\
5 problems, 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}

\newpage
\question{1}{List concatenation and reversal}{6+5+4+6}

Consider the following Lean function on lists:

\begin{lstlisting}
  def concat {α : Type} : list (list α) → list α
  | []          := []
  | (xs :: xss) := xs ++ concat xss
\end{lstlisting}

\subquestion{a}%
Prove the following lemma about concatenation:

\begin{lstlisting}
  lemma map_concat {α β : Type} (f : α → β) :
    ∀xss : list (list α), map f (concat xss) = concat (map (map f) xss)
\end{lstlisting}
%
You may assume basic lemmas about \li{map}, including its definition:

\begin{lstlisting}
  def map {α β : Type} (f : α → β) : list α → list β
  | []        := []
  | (x :: xs) := f x :: map xs
\end{lstlisting}

\begin{answer}
\begin{lstlisting}
| []          := by refl
| (xs :: xss) :=
  calc map f (concat (xs :: xss)) = map f (xs ++ concat xss) : by rw concat
  ... = map f xs ++ map f (concat xss) : by simp
  ... = map f xs ++ concat (map (map f) xss) : by rw map_concat
  ... = concat (map f xs :: map (map f) xss) : by rw concat
  ... = concat (map (map f) (xs :: xss)) : by simp
\end{lstlisting}
\end{answer}

\subquestion{b}%
Give the definition in Lean of a \li{reverse} function that takes a list in
argument and returns it with its elements in reverse order.

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

\subquestion{c}%
Complete the \emph{statements} of the following properties that describes
the behavior of \li{concat} and \li{reverse} (defined above) with respect to
the append operator (\li{++}), by filling in the holes (\verb|_|). These
properties should describe how \li{concat} and \li{reverse} distribute over
\li{++}. You are \emph{not} asked to prove the properties.

\begin{lstlisting}
  lemma concat_snoc {α : Type} :
    ∀(xs : list α) (xss : list (list α)), concat (xss ++ [xs]) = _

  lemma reverse_append {α : Type} :
    ∀xs ys : list α, reverse (xs ++ ys) = _
\end{lstlisting}

\begin{answer}
\begin{lstlisting}
concat xss ++ xs
reverse ys ++ reverse xs
\end{lstlisting}
\end{answer}

\subquestion{d}%
Prove the following lemma, using the above definitions and properties.

\begin{lstlisting}
  lemma reverse_concat {α : Type} :
    ∀xss : list (list α), reverse (concat xss) =
      concat (reverse (map reverse xss))
\end{lstlisting}

\begin{answer}
\begin{lstlisting}
| []          := by refl
| (xs :: xss) :=
  calc reverse (concat (xs :: xss)) = reverse (xs ++ concat xss) : by refl
  ... = reverse (concat xss) ++ reverse xs : by rw reverse_append
  ... = concat (reverse (map reverse xss)) ++ reverse xs : by rw reverse_concat
  ... = concat (reverse (map reverse xss) ++ [reverse xs]) : by rw concat_snoc
  ... = concat (reverse (reverse xs :: map reverse xss)) : by rw reverse
  ... = concat (reverse (map reverse (xs :: xss))) : by refl
\end{lstlisting}
\end{answer}

\newpage
\question{2}{Sorted lists}{6+4+4}

\subquestion{a}%
Define in Lean an inductive predicate \li{sorted} that takes a list of natural
numbers as argument and that returns \texttt{true} if and only if that list is
sorted in increasing order. The definition should distinguish three cases:

\begin{itemize}
\item The empty list is sorted.

\item Any list of length 1 is sorted.

\item A list $[x_1, x_2, \dots, x_n]$ of length $n \ge 2$ is sorted if
  $x_1 \le x_2$ and $[x_2, \dots, x_n]$ is sorted.
\end{itemize}

\begin{answer}
\begin{lstlisting}
inductive sorted : list ℕ → Prop
| nil : sorted []
| single {x : ℕ} : sorted [x]
| two_or_more {x y : ℕ} {xs : list ℕ} (xy : x ≤ y) (yxs : sorted (y :: xs)) :
  sorted (x :: y :: xs)
\end{lstlisting}
\end{answer}

\subquestion{b}%
Prove the following four lemmas to test your definition.

\begin{lstlisting}
  example : sorted []
  example : sorted [2]
  example : sorted [3, 5]
  example : sorted [7, 9, 9, 11]
\end{lstlisting}

\begin{answer}
\begin{lstlisting}
example : sorted [] :=
  sorted.nil

example : sorted [2] :=
  sorted.single

example : sorted [3, 5] :=
  sorted.two_or_more dec_trivial sorted.single

example : sorted [7, 9, 9, 11] :=
  sorted.two_or_more dec_trivial
    (sorted.two_or_more dec_trivial
      (sorted.two_or_more dec_trivial
        sorted.single))
\end{lstlisting}
\end{answer}

\subquestion{c}%
Not all lists are sorted. Prove the following counterexample.

\begin{lstlisting}
  example : ¬ sorted [17, 13]
\end{lstlisting}

\begin{answer}
\begin{lstlisting}
assume s : sorted [17, 13],
have 17 ≤ 13 := match s with sorted.two_or_more xy yxs := xy end,
have ¬ (17 ≤ 13) := dec_trivial,
show false, from by contradiction
\end{lstlisting}
\end{answer}

\newpage
\question{3}{Program equivalence}{6+5+5}

Consider the following WHILE language:

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

In the following, we fix a type \li{σ} of states.

Recall the big-step semantic predicate \li{(p, s) ⟹ t} and the following notion of
program equivalence:

\begin{lstlisting}
  def program_equiv (p₁ p₂ : program σ) : Prop :=
  ∀s t, (p₁, s) ⟹ t ↔ (p₂, s) ⟹ t
\end{lstlisting}

We use the abbreviation \li{p₁ ≈ p₂} for \li{program_equiv p₁ p₂}.

\subquestion{a}%
Prove the following program equivalence, which can be used by a compiler to
exchange the `then' and the `else' branches of an `if' statement.

\begin{lstlisting}
  example {p q : program σ} {c : σ → Prop} :
    ite c p q ≈ ite (λs, ¬ c s) q p
\end{lstlisting}

\begin{answer}
\begin{lstlisting}
begin
  intros s t,
  apply iff.intro,
  repeat {
    intro h,
    cases h,
    { apply big_step.ite_false; cc },
    { apply big_step.ite_true; cc } }
end
\end{lstlisting}

Intuitively, proving the equivalence amounts to proving two implications:
\[\hbox{\li{(ite c p q, s) ⟹ t → (ite (λs, ¬ c s) q p, s) ⟹ t}}\]
and
\[\hbox{\li{(ite (λs, ¬ c s) q p, s) ⟹ t → (ite c p q, s) ⟹ t}}\]
where \li{s} and \li{t} are fixed but unknown.

Let us focus on the first goal. The condition \li{c} is either true or false
in state \li{s}. If it is true, then the hypothesis \li{(ite (λs, ¬ c s) q p, s) ⟹ t}
must have been proved using the \li{ite_true} rule from the big-step
semantics, and we apply the \li{ite_false} rule to prove the desired
conclusion. This works because \li{¬¬ c s} is true if \li{c s} is true. If the
condition is false, the hypothesis must have been proved using \li{ite_false},
and we apply \li{ite_true} to prove the conclusion, analogously.

The case of the second goal is completely analogous and therefore omitted.
\end{answer}

\subquestion{b}%
By appealing to the big-step semantics, explain why infinite loops never exit,
a property that can be stated formally as follows.

\begin{lstlisting}
  lemma big_step_while_true {p : program σ} {s t : σ} :
    ¬ ⟨while (λ_, true) p, s⟩ ⟹ t
\end{lstlisting}

\begin{answer}
\begin{lstlisting}
begin
  generalize eq : (while (λ_, true) p, s) = qs,
  intro h,
  induction h generalizing s; cases eq,
  { apply h_ih_hw, refl },
  { apply h_hs, trivial }
end
\end{lstlisting}

Admittedly, the above is not very readable. The idea is to assume
\li{⟨while (λ_, true) p, s⟩ ⟹ t} and show that this leads to a contradiction.
We perform an induction on the rules of the big-step semantics. The only two
possible cases, syntactically, are the case where the condition
\li{(λ_, true)} is true in \li{s} and the case where it is false. Clearly, the second
case is impossible (\li{(λ_, true) s = true}). Remains the first case.

By the big-step semantics, there must exist a state \li{u} such that
\[\hbox{\li{⟨p, s⟩ ⟹ u}}\qquad\hbox{and}\qquad \hbox{\li{⟨while (λ_, true) p, u⟩ ⟹ t}}.\]
But by the (second) induction hypothesis, we also know that
\[\hbox{\li{¬ ⟨while (λ_, true) p, u⟩ ⟹ t}}.\]
Contradiction.
\end{answer}

\subquestion{c}%
Use the above lemma to prove the following program equivalence, which can be
used to eliminate dead code in an optimizer.

\begin{lstlisting}
  example {p p' : program σ} :
    seq (while (λ_, true) p) p' ≈ while (λ_, true) p
\end{lstlisting}

\begin{answer}
\begin{lstlisting}
begin
  intros s t,
  apply iff.intro,
  { intro h, cases h, exact absurd h_h₁ big_step_while_true },
  { intro h, exact absurd h big_step_while_true }
end
\end{lstlisting}

Intuitively, to prove the property, we must prove two implications:
\[\hbox{\li{(seq (while (λ_, true) p) p', s) ⟹ t → (while (λ_, true) p, s) ⟹ t}}\]
and
\[\hbox{\li{(while (λ_, true) p, s) ⟹ t → (seq (while (λ_, true) p) p', s) ⟹ t}}\]

The second goal is easier. From the assumption \li{while (λ_, true) p, s) ⟹ t},
we immediately have a contradiction with the lemma \li{big_step_while_true}
proved above.

For the first goal, from the assumption \li{seq (while (λ_, true) p) p', s) ⟹ t},
we obtain the existence of a state \li{u} such that
\[\hbox{\li{(while (λ_, true) p, s) ⟹ u}}\qquad\hbox{and}\qquad\hbox{\li{(p', u) ⟹ t}}\]
The first property contradicts \li{big_step_while_true}.

\end{answer}

\newpage
\question{4}{Finite sets}{4+6+6}

\subquestion{a}%
Define an inductive predicate \li{finite} in Lean that returns \li{true} if
and only if its argument is a finite set (of type \li{set α}).
The definition should distinguish two cases:

\begin{itemize}
\item The empty set is finite.

\item If $A$ is finite, then $\{a\} \cup A$ is finite.
\end{itemize}

Put the definition in a namespace called \li{v1}.

\begin{answer}
\begin{lstlisting}
namespace v1

inductive finite {α : Type} : set α → Prop
| empty : finite ∅
| insert (a : α) (A : set α) (fin_A : finite A) : finite (insert a A)

end v1
\end{lstlisting}

(Instead of \li{insert a A}, we would also accept the traditional syntax
\verb|{|a\verb|}|\li{ ∪ A}.)
\end{answer}

\subquestion{b}%
Give an alternative Lean definition for \li{finite}, this time distinguishing
three cases:

\begin{itemize}
\item The empty set is finite.

\item The singleton set $\{a\}$ is finite.

\item If $A$ and $B$ are finite, then $A \cup B$ is finite.
\end{itemize}

Put the definition in a namespace called \li{v2}.

\begin{answer}
\begin{lstlisting}
namespace v2

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 v2
\end{lstlisting}
\end{answer}

\subquestion{c}%
As a step towards proving the two definitions equivalent, prove the following
lemma about \li{v1.finite}:

\begin{lstlisting}
  namespace v1

  lemma finite.union {α : Type} :
    ∀A B : set α, finite A → finite B → finite (A ∪ B) :=

  end v1
\end{lstlisting}

\begin{answer}
\begin{lstlisting}
namespace v1

-- basic lemmas we assume
@[simp] lemma union_empty_left {α : Type} {A : set α} :
  ∅ ∪ A = A := sorry
@[simp] lemma insert_union {α : Type} {a : α} {A B : set α} :
  insert a A ∪ B = insert a (A ∪ B) := sorry

lemma finite.union {α : Type} :
  ∀A B : set α, finite A → finite B → finite (A ∪ B) :=
begin
  intros A B fin_A fin_B,
  induction fin_A,
  { simp,
    exact fin_B },
  { simp,
    apply finite.insert,
    exact fin_A_ih }
end

end v1
\end{lstlisting}

Intuitively, we perform an induction on \li{finite A}. There are two cases.

If \li{A} is empty, then we have \li{A ∪ B = B}; hence the goal is
simply \li{finite B}, which we have by assumption (\li{fin_B}).

If \li{A} is of the form \verb|{|a\verb|}|\li{ ∪ A'}, then the goal is
to prove \verb|finite ({|a\verb|}|\li{ ∪ A') ∪ B}. The induction hypothesis tells
us that \verb|finite (A' ∪ B)|.

Clearly, we have \verb|({|a\verb|}|\li{ ∪ A') ∪ B = }\verb|{|a\verb|}|\li{ ∪ (A' ∪ B)}.
We can use the second introduction rule for \li{finite} (called
\li{finite.insert} above) to prove this, leaving the proof obligation
\verb|finite (A' ∪ B)|. This is exactly the induction hypothesis.
\end{answer}

\newpage
\question{5}{Finite sets as quotients}{6+3+5+5+4}

Finite sets can be defined in various ways. One way is to start with a raw type
of finite lists and take the quotient over the equivalence relation
\li{r := λxs ys, ∀x, x ∈ xs ↔ x ∈ ys}, meaning that two lists are put in the same
equivalence class if they contain exactly the same elements.

In Lean, this could be done as follows:

\begin{lstlisting}
  instance fin_set.rel (α : Type) : setoid (list α) :=
  { r     := λxs ys, ∀x, x ∈ xs ↔ x ∈ ys,
    iseqv := _ }

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

However, there is a hole (\verb|_|) in the definition, standing for a proof
that the relation \li{r} is an equivalence relation (i.e., is reflexive,
symmetric, and transitive).

\subquestion{a}%
State and prove the three properties that capture the fact that \li{r} is an
equivalence relation.

\begin{answer}
The properties can be stated as follows:

\begin{lstlisting}
lemma r_reflexive (xs : list α) : r xs xs
lemma r_symmetric (xs ys : list α) : r xs ys → r ys xs
lemma r_transitive (xs ys zs : list α) : r xs ys → r ys zs → r xs zs
\end{lstlisting}

By expanding the definition of \li{r}, we basically exploit the fact that
\li{↔} is itself an equivalence relation, proving each of the three properties
of \li{r} by appealing to the analogous property of \li{↔}.

For those who care, the hole in the \li{fin_set.rel} proof above can be filled
as follows:

\begin{lstlisting}
⟨ (assume xs, by simp),
  (assume xs ys ys_xs x, by simp *),
  (assume xs ys zs xs_ys ys_zs, by simp *) ⟩
\end{lstlisting}
\end{answer}

\subquestion{b}%
The empty finite set can be defined in Lean as follows:

\begin{lstlisting}
  def fin_empty {α : Type} : fin_set α := ⟦[]⟧
\end{lstlisting}

Inspired by the above, define a \li{fin_singleton} operation that, given an
element~$a$, returns a singleton of type \li{fin_set α} containing that
element.

\begin{answer}
\begin{lstlisting}
def fin_singleton {α : Type} (a : α) : fin_set α := ⟦[a]⟧
\end{lstlisting}
\end{answer}

\subquestion{c}%
Next, define the union operator on \li{fin_set α} by filling the hole
(\verb|_|) in the following definition:

\begin{lstlisting}
  def fin_union {α : Type} (A B : fin_set α) : fin_set α :=
  quotient.lift_on₂ A B (λas bs, ⟦as ++ bs⟧) _
\end{lstlisting}

The hole has type
\[\hbox{\li{∀as₁ as₂ bs₁ bs₂ : list α, r as₁ bs₁ → r as₂ bs₂ → ⟦as₁ ++ as₂⟧ = ⟦bs₁ ++ bs₂⟧}}\]

\begin{answer}
By soundness of quotients (\li{quotient.sound}), it suffices to prove that
\[\hbox{\li{r (as₁ ++ as₂) (bs₁ ++ bs₂)}}\]
By unfolding the definition of \li{r}, we obtain the goal
\[\hbox{\li{x ∈ as₁ ++ as₂ ↔ x ∈ bs₁ ++ bs₂}}\]

In the left-to-right direction, we have \li{x ∈ as₁ ++ as₂} and must prove
\li{x ∈ bs₁ ++ bs₂}. By case analysis on the hypothesis, we have either
\li{x ∈ as₁} or \li{x ∈ as₂}. In the first subcase, we prove \li{x ∈ bs₁} by
exploiting the hypothesis \li{r as₁ bs₁}; hence \li{x ∈ bs₁ ++ bs₂}.
The second subcase is analogous but first proves \li{x ∈ bs₂}.

The right-to-left direction is entirely analogous.

In Lean:

\begin{lstlisting}
begin
  intros as₁ bs₁ as₂ bs₂ as₁_bs₁ as₂_bs₂,
  apply quotient.sound,
  intro x,
  simp,
  apply iff.intro,
  { intro h,
    cases h,
    { apply or.intro_left,
      rw ←as₁_bs₁ x,
      assumption },
    { apply or.intro_right,
      rw ←as₂_bs₂ x,
      assumption } },
  { intro h,
    cases h,
    { apply or.intro_left,
      rw as₁_bs₁ x,
      assumption },
    { apply or.intro_right,
      rw as₂_bs₂ x,
      assumption } }
end
\end{lstlisting}
\end{answer}

\subquestion{d}%
Is the following property provable or not? If yes, please argue why.
If no, give a counterexample (specifying concrete values for \li{α} and
\li{A}).

\begin{lstlisting}
  lemma exists_list_of_fin_set {α : Type} (A : fin_set α) :
    ∃xs : list α, A = ⟦xs⟧
\end{lstlisting}

\begin{answer}
The property is provable. Without loss of generality, \li{A} can be expressed
as \li{⟦ys⟧} for some list \li{ys}. (In Lean, this step appeals to the
misnamed lemma \li{quotient.induction_on}.) We can then take \li{ys} as the
witness for \li{xs}. The proof is then by reflexivity of \li{=}.

In Lean:

\begin{lstlisting}
lemma exists_list_of_fin_set {α : Type} (A : fin_set α) :
  ∃xs : list α, A = ⟦xs⟧ :=
begin
  apply quotient.induction_on A,
  intro,
  apply exists.intro,
  refl
end
\end{lstlisting}
\end{answer}

\subquestion{e}%
Explain what the following definition achieves. Why do you think it might be
useful?

\begin{lstlisting}
  noncomputable def list_of_fin_set {α : Type} (A : fin_set α) : list α :=
  @classical.some (list α) (λxs, A = ⟦xs⟧) (exists_list_of_fin_set A)
\end{lstlisting}

\begin{answer}
The function converts a finite set \li{A} into an arbitrary list that contains
the same element. It can be useful to repair mismatches in APIs (for example,
if an API requires a list but all we have is a finite set).
\end{answer}



\vfill

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

\end{document}
