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

\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

\def\lstlanguagefiles{lstleanbw.tex}
\lstset{language=lean}
\lstMakeShortInline|

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

\makeatletter

\renewcommand\lst@visiblespace{\ensuremath{\;}}
\newcommand\li{\lstinline[showspaces=true]}

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

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

\begin{document}

Logical Verification 2022--2023 \\
Vrije Universiteit Amsterdam \\
Lecturers: dr.\ J.\,C. Blanchette and J.\,B. Limperg
\hfill\smash{\makebox[0mm][r]{\includegraphics[height=20mm]{griffioen.png}}}

Final Exam (v3) \\
Tuesday 20 December 2022, 08:30--11:15, WN-S623 S631 S655 \\
6 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, including 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 \textbf{inductive hypotheses} assumed (if any) and
the goal to be proved. Unless otherwise specified, minor proof steps
corresponding to \mbox{\li{refl},} \li{simp}, or \li{linarith} need not be
justified if you think they are obvious, but you should say which key lemmas
they depend on.

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.
\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 lecturer's phone number, 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}{Functional programming}{5+4+7}

\subquestion{a}%
Complete the following definition of the function |cycle|:
\begin{lstlisting}
    def cycle {α : Type} : ℕ → list α → list α
\end{lstlisting}
Given a natural number |n| and a list |xs|, |cycle n xs| is a list containing
|n| copies of the elements of |xs|. For example:

\begin{lstlisting}
    cycle 2 ["I", "love", "exams"] = ["I", "love", "exams", "I", "love", "exams"]
    cycle 0 [1, 2] = []
\end{lstlisting}

You may use the append operator \li|++|. If you use other functions, give their
definitions as well.

\begin{answer}
\begin{lstlisting}
| 0       _  := []
| (n + 1) xs := xs ++ cycle n xs
\end{lstlisting}
\end{answer}

\subquestion{b}%
Write the Lean code for a lemma stating that every element of the list
|cycle n xs| is also an element of |xs|, for all |n| and |xs|. You do not have
to prove the lemma. You can use the binary operator |∈| of type
|Πα, α → list α → Prop| in the lemma statement.

\begin{answer}
\begin{lstlisting}
lemma cycle_mem {α : Type} (n : ℕ) (xs : list α) :
  ∀x : α, x ∈ cycle n xs → x ∈ xs
\end{lstlisting}
\end{answer}

\subquestion{c}%
Consider the following |join| function, which concatenates a list of lists:

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

Prove the following lemma about |join| by induction:

\begin{lstlisting}
    lemma join_append {α : Type} (xss yss : list (list α)) :
      join (xss ++ yss) = join xss ++ join yss
\end{lstlisting}

For each case of the induction, clearly indicate the inductive hypotheses
assumed and the goal to be proved.

\begin{answer}
The proof is by structural induction on \li{xss}.

Case \li{xss = []} (base case). \\
The goal is \li{join ([] ++ yss) = join [] ++ join yss}.

For the left-hand side of the goal, we have \\
\noindent\phantom{\li|=|} \li{join ([] ++ yss)} \\
\li{= join yss}\qquad (by definition of \li{++})

For the right-hand side, we have \\
\noindent\phantom{\li|=|} \li{join [] ++ join yss} \\
\li{= [] ++ join yss}\qquad (by definition of \li{join}) \\
\li{= join yss}\qquad (by definition of \li{++})

Thus both sides are equal.

Case \li{xss = xs :: xss'} (inductive step). \\
The goal is \li{join ((xs :: xss') ++ yss) = join (xs :: xss') ++ join yss}. \\
The induction hypothesis is
\li{join (xss' ++ yss) = join xss' ++ join yss}.

For the left-hand side of the goal, we have \\
\noindent\phantom{\li|=|} \li{join ((xs :: xss') ++ yss)} \\
\li{= join (xs :: (xss' ++ yss))}\qquad (by basic property of \li{++}) \\
\li{= xs ++ join (xss' ++ yss)}\qquad (by definition of \li{join}) \\
\li{= xs ++ (join xss' ++ join yss)}\qquad (by induction hypothesis) \\
\li{= xs ++ join xss' ++ join yss}\qquad (by associativity of \li{++})

For the right-hand side, we have \\
\noindent\phantom{\li|=|} \li{join (xs :: xss') ++ join yss} \\
\li{= xs ++ join xss' ++ join yss}\qquad (by definition of \li{join})

Thus both sides are equal. QED.
\end{answer}

\newpage
\question{2}{Logic}{8+8}

\subquestion{a}%
Give a detailed proof of the following lemma. Make sure to emphasize and clearly
label every step corresponding to the introduction or elimination of a
quantifier or connective.

\begin{lstlisting}
    lemma not_exists_forall_not {α : Type} {p : α → Prop} :
      (¬ ∃x, p x) → ∀y, ¬ p y
\end{lstlisting}

\begin{answer}
Assume \li{hnex : ¬ ∃x, p x} (i.e., \li{(∃x, p x) → false}). \\
Fix \li{y : α}. \\
Assume \li{hpy : p y}. \\
We must show \li{false}. \\
By \li{hnex}, it suffices to prove \li{∃x, p x}. \\
(In other words: We \relax{apply} \li{hnex}, giving rise to the subgoal
\li{∃x, p x}.) \\
At this point, we apply the \li{∃}-introduction rule with the witness \li{y}. \\
We must then show \li{p y}. This follows from \li{hpy}. QED
\end{answer}

\subquestion{b}%
Give a detailed proof of the following lemma. Make sure to emphasize and clearly
label every step corresponding to the introduction or elimination of a
quantifier or connective.

\begin{lstlisting}
    lemma or_forall_forall_or {α : Type} {p q : α → Prop} :
      (∀x, p x) ∨ (∀x, q x) → ∀x, p x ∨ q x
\end{lstlisting}

\begin{answer}
Assume \li{hor : (∀x, p x) ∨ (∀x, q x)}. \\
Fix \li{x : α}. \\
We must show \li{p x ∨ q x}.

Perform an \li{∨}-elimination on \li{hor}.

Case \li{hp : ∀x, p x}: \\
From \li{hp}, derive \li{p x} by ∀-elimination (by instantiating \li{x} with
\li{x}).
To prove \li{p x ∨ q x}, by \li{∨}-left-introduction it suffices to show
\li{p x}, which we have.

Case \li{hq : ∀x, q x}: \\
From \li{hq}, derive \li{q x} by ∀-elimination (by instantiating \li{x} with
\li{x}).
To prove \li{p x ∨ q x}, by \li{∨}-right-introduction it suffices to show
\li{q x}, which we have. QED
\end{answer}

\newpage
\question{3}{Semantics}{4+3+9}

We introduce the \textsc{RNG} language, a variant of the \textsc{WHILE} language
with nondeterministic variable assignment and a restricted form of |while|
loops. It has the following kinds of statements:

\begin{itemize}
  \item |skip| does nothing;
  \item |x := [z₁, ..., z|$_n$|]| assigns \emph{one of} the integers |z|$_i$,
        chosen at random, to the variable |x|. If $n$| = 0|, the program blocks;
  \item |S ; T| executes the statement |S| followed by the statement |T|;
  \item |while_nonzero x do S| executes the statement |S| repeatedly until the
        variable |x| becomes zero.
\end{itemize}

In Lean, we can model the \textsc{RNG} language's abstract syntax as follows:

\begin{lstlisting}
    inductive stmt : Type
    | skip          : stmt
    | assign        : string → list ℤ → stmt
    | seq           : stmt → stmt → stmt
    | while_nonzero : string → stmt → stmt
\end{lstlisting}
The infix syntax \li{S ;; T} abbreviates \li{stmt.seq S T}.

The big-step semantics of \textsc{RNG} relates a program |S|~|:|~|stmt| and an
initial state |s|~|:| |string|~|→|~|ℤ| with a possible final state |t|~|:|
|string|~|→|~|ℤ|. We write |(S,|~|s)|~|⇒| |t| if the program |S|, when run in
the initial state |s|, may terminate in the final state |t|.

\subquestion{a}%
Dana Hacker claims that the following derivation rule should be part of the
big-step semantics of \textsc{RNG}.

\vskip\abovedisplayskip

\noindent\hfill
\RL{\textsc{Seq\_Wrong}}
\AXC{\li|(S, s) ⇒ t|}
\AXC{\li|(T, s) ⇒ t|}
\BIC{\strut\li|(S ; T, s) ⇒ t|}
\DP
\hfill\hbox{}

\vskip\belowdisplayskip

Explain why this rule is wrong.

\begin{answer}
Both hypotheses start in the same state and end in the same state, executing
\li{S} and \li{T} in lockstep instead of in sequence.
\end{answer}

\subquestion{b}%
Despite common sense, Dana wants you to translate her
\textsc{Seq\_Wrong} rule to Lean. Add an introduction rule corresponding to
\textsc{Seq\_Wrong} to the following inductive predicate.

\begin{lstlisting}
    def state : Type := string → ℤ

    inductive big_step : stmt × state → state → Prop
\end{lstlisting}

\begin{answer}
\begin{lstlisting}
| seq_wrong {S T s t} :
  big_step (S, s) t → big_step (T, s) t → big_step (stmt.seq S T, s) t
\end{lstlisting}
\end{answer}

\subquestion{c}%
Complete the following specification of a big-step semantics for RNG by giving
the missing derivation rules for |assign|, |seq|, and |while_nonzero|.
% If you need any operations on states, define them as well.

\vskip\abovedisplayskip

\noindent\hfill
\RL{\textsc{Skip}}
\AXC{\phantom{.}}
\UIC{\strut\li|(skip, s) ⇒ s|}
\DP
\hfill\hbox{}

\vskip\belowdisplayskip

\begin{answer}

\vskip\abovedisplayskip

\noindent\hfill
\RL{\textsc{Assign}\quad if \li|i ∈ \{1, ..., n\}|}
\AXC{\phantom{.}}
\UIC{\strut\li$(x := [z_1, ..., z_n], s) => s[x |-> z_i]$}
\DP
\hfill\hbox{}

\smallskip

\noindent\hfill
\RL{\textsc{Seq}}
\AXC{\li|(S, s) ⇒ t|}
\AXC{\li|(T, t) ⇒ u|}
\BIC{\strut\li|(S ; T, s) ⇒ u|}
\DP
\hfill\hbox{}

\smallskip

\noindent\hfill
\RL{\textsc{WhileNonzeroStop}\quad\li{if s(x) = 0}}
\AXC{\phantom{.}}
\UIC{\strut\li|(while_nonzero x do S, s) ⇒ s|}
\DP
\hfill\hbox{}

\smallskip

\noindent\hfill
\RL{\textsc{WhileNonzeroCont}\quad\li{if s(x) ≠ 0}}
\AXC{\strut\li|(S, s) => t|}
  \AXC{\strut\li|(while_nonzero x do S, t) => u|}
\BIC{\strut\li|(while_nonzero x do S, s) ⇒ u|}
\DP
\hfill\hbox{}
\end{answer}

\newpage
\question{4}{List predicates}{6+4+8}

\subquestion{a}%
For a predicate |p|~|:| |α|~|→|~|Prop| and a list |xs|~|:| |list|~|α|, we
define the predicate |all p xs| that is true if and only if every element of
|xs| satisfies |p|. Complete the following definition of |all| as an inductive
predicate.

\begin{lstlisting}
    inductive all {α : Type} (p : α → Prop) : list α → Prop
\end{lstlisting}

\begin{answer}
\begin{lstlisting}
| nil         : all []
| cons {x xs} : p x → all xs → all (x :: xs)
\end{lstlisting}

\textbf{Alternative:}

\begin{lstlisting}
| intro {xs} : (∀x, x ∈ xs → p x) → all xs
\end{lstlisting}
\end{answer}

\subquestion{b}%
Similarly, we define the predicate |any p xs| which is true if and only if there
exists an element of |xs| that satisfies |p|:

\begin{lstlisting}
    inductive any {α : Type} (p : α → Prop) : list α → Prop
    | here {x xs}  : p x → any (x :: xs)
    | there {x xs} : any xs → any (x :: xs)
\end{lstlisting}

The same predicate can also be defined using |all|. Give a simple, nonrecursive
definition:

\begin{lstlisting}
    def anyd {α : Type} (p : α → Prop) (xs : list α) : Prop
\end{lstlisting}

\begin{answer}
\begin{lstlisting}
:= ¬ all (λx, ¬ p x) xs
\end{lstlisting}
\end{answer}

\subquestion{c}%
Yet another way to define |any| is as a recursive function:

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

Prove by induction that |any p xs| implies |anyf p xs|. For each case of the
induction, clearly indicate the inductive hypotheses assumed and the goal to be
proved.

\begin{lstlisting}
    lemma any_anyf {α : Type} {p : α → Prop} {xs : list α} :
      any p xs → anyf p xs
\end{lstlisting}

\begin{answer}
Assume \li{hany : any p xs}. \\
The proof is by rule induction on the hypothesis \li{hany}.

Case \li{here}: \\
We have \li{hp : p x}. \\
We must show \li{anyf p (x :: xs)}.

By definition of \li{anyf}, it suffices to show \li{p x ∨ anyf p xs}. \\
The left disjunct follows by \li{hp}.

Case \li{there}: \\
We have \li{hany : any p xs}. \\
We must show \li{anyf p (x :: xs)}. \\
The induction hypothesis is \li{any p xs → anyf p xs}.

By definition of \li{anyf}, it suffices to show \li{p x ∨ anyf p xs}. \\
The right disjunct follows by the induction hypothesis and \li{hany}.

\textbf{Alternative:}

The proof is by structural induction on \li{xs}.

Case \li{xs = []} (base case): \\
The goal is \li{any p [] → anyf p []}.

Assume \li{hany : any p []}. \\
Perform a case distinction on \li{hany}. \\
None of \li{here} or \li{there} apply, so there is nothing to prove.

Case \li{xs = x :: xs'} (induction step): \\
The goal is \li{any p (x :: xs) → anyf p (x :: xs)}. \\
The induction hypothesis is \li{any p xs → anyf p xs}.

Assume \li{hany : any p (x :: xs)}. \\
Perform a case distinction on \li{hany}. Two subcases arise:

Subcase \li{here}: \\
We have \li{hp : p x}. \\
We must show \li{anyf p (x :: xs)}. \\
By definition of \li{anyf}, it suffices to show \li{p x ∨ anyf p xs}. \\
The left disjunct follows by \li{hp}.

Subcase \li{there}: \\
We have \li{hany : any p xs}. \\
We must show \li{anyf p (x :: xs)}. \\
By definition of \li{anyf}, it suffices to show \li{p x ∨ anyf p xs}. \\
We will prove the right disjunct. By the induction hypothesis, it suffices
to show \li{any p xs}, which corresponds to \li{hany}. QED
\end{answer}

\newpage
\question{5}{Mathematics in Lean}{4+5+4+2}

\subquestion{a}%
What are the types of the following Lean expressions?

\begin{lstlisting}
    ["What", "is", "my", "type?"]     true     Prop     (λα, set α → list α)
\end{lstlisting}

\begin{answer}
\li|list string| \\
\li|Prop| \\
\li|Type| \\
\li|Type → Type| (or \li|Type u → Type u|)
\end{answer}

\subquestion{b}%
The type class |monoid| of monoids is defined as follows in Lean:

\begin{lstlisting}
    @[class] structure monoid (α : Type) :=
    (mul       : α → α → α)
    (one       : α)
    (mul_assoc : ∀a b c, mul (mul a b) c = mul a (mul b c))
    (one_mul   : ∀a, mul one a = a)
    (mul_one   : ∀a, mul a one = a)
\end{lstlisting}

The type of Booleans can be viewed as a monoid, with |ff| as |one| and
disjunction \li{||} as |mul|. Complete the following instance
definition accordingly. For the first two fields, give a Lean term. For the
other three fields, state the property that needs to be proved to define the
field and very briefly explain why it holds.

\begin{lstlisting}
    @[instance] def or_monoid : monoid bool :=
    { mul       := ...,
      one       := ...,
      mul_assoc := ...,
      mul_one   := ...,
      one_mul   := ... }
\end{lstlisting}

\begin{answer}
\begin{lstlisting}
mul       := (||),
one       := ff,
mul_assoc := ∀a b c, (a || b) || c = a || (b || c),
  -- disjunction is associative, as can be seen from a truth table
mul_one   := ∀a, ff || a = a,
  -- falsity is a neutral element for disjunction
one_mul   := ∀a, a || ff = a
  -- falsity is a neutral element for disjunction
\end{lstlisting}
\end{answer}

\subquestion{c}%
The relation |same_parity| relates two natural numbers if they are
either both even or both odd:

\begin{lstlisting}
    inductive same_parity : ℕ → ℕ → Prop
    | even {m n} : even m → even n → same_parity m n
    | odd {m n}  : odd m → odd n → same_parity m n
\end{lstlisting}

Prove that |same_parity| is symmetric.

\begin{lstlisting}
    lemma same_parity_symm :
      ∀m n : ℕ, same_parity m n → same_parity n m
\end{lstlisting}

\begin{answer}
Fix \li{m}, \li{n : ℕ}. \\
Assume \li{hsp : same_parity m n}. \\
We must show \li{same_parity n m}.

Perform a case distinction on \li{hsp}.

Case \li{even}: \\
We have \li{hm : even m} and \li{hn : even n}. \\
We apply the introduction rule \li{same_parity.even} on \li{hn} and \li{hm} to
show \li{same_parity n m}.

Case \li{odd}: \\
We have \li{hm : odd m} and \li{hn : odd n}. \\
We apply the introduction rule \li{same_parity.odd} on \li{hn} and \li{hm} to
show \li{same_parity n m}.
QED
\end{answer}

\subquestion{d}%
In addition to being symmetric, the relation |same_parity| is also reflexive and
transitive, and is therefore an equivalence relation. We use it to form the
quotient |parity|:

\begin{lstlisting}
    @[instance] def same_parity.rel : setoid ℕ :=
    { r     := same_parity,
      iseqv := ... }

    def parity :=
    quotient same_parity.rel
\end{lstlisting}

How many distinct inhabitants does |parity| have? Briefly justify your
answer.

\begin{answer}
The type \li{parity} has two inhabitants, corresponding to the two equivalence
classes of the relation \li{same_parity}. The even numbers form one equivalence
class and the odd numbers form the other equivalence class.
\end{answer}

\newpage
\question{6}{Monads}{4+5}

Recall that a monad is lawful if its |pure| and |bind| operations satisfy the
three laws given by the |lawful_monad| type class below. We use |ma >>= f| as
syntactic sugar for |bind ma f|.

\begin{lstlisting}
    @[class] structure lawful_monad (m : Type → Type) [monad m] :=
    (pure_bind {α β : Type} (a : α) (f : α → m β) :
       (pure a >>= f) = f a)
    (bind_pure {α : Type} (ma : m α) :
       (ma >>= pure) = ma)
    (bind_assoc {α β γ : Type} (f : α → m β) (g : β → m γ) (ma : m α) :
       ((ma >>= f) >>= g) = (ma >>= (λa, f a >>= g)))
\end{lstlisting}

\subquestion{a}%
Prove that the following lemma holds for any lawful monad. Your proof should be
step-by-step calculational, with at most one rewrite rule per step, so that we
can clearly see what happens.

\begin{lstlisting}
    lemma pure_bind_bind_bind {m : Type → Type} [monad m] [lawful_monad m]
        {α β γ δ : Type} (a : α) (mb : m β) (f : β → m γ) (g : γ → m δ) :
      pure a >>= (λa, mb >>= (λb, f b >>= g)) = (mb >>= f) >>= g
\end{lstlisting}

\begin{answer}
\phantom{\li|=| }\li{pure a >>= (λa, mb >>= (λb, f b >>= g))} \\
\li{= (λa, mb >>= (λb, f b >>= g)) a}\qquad (by \li{pure_bind}) \\
\li{= mb >>= (λb, f b >>= g)}\qquad (by $\beta$-reduction) \\
\li{= (mb >>= f) >>= g}\qquad (by \li{bind_assoc} in reverse) \\
QED
\end{answer}

\subquestion{b}%
Does the following statement hold for arbitrary lawful monads? If so, give a
proof sketch. If not, give a counterexample and briefly explain why it is a
counterexample.

\begin{lstlisting}
    lemma reordering {m : Type → Type} [monad m] [lawful_monad m] {α : Type}
        (ma : m α) (f g : α → m α) :
      ((ma >>= f) >>= g) = ((ma >>= g) >>= f)
\end{lstlisting}

\begin{answer}
As a counterexample, take \li{m} to be the identity monad, \li{α} to be \li{ℕ},
\li{ma} to be \li{0}, \li{f} to be \li{λx, x + 1}, and \li{g} to be
\li{λx, 2 * x}. Then the left-hand side is equal to \li{2}, whereas the
right-hand side is equal to \li{1}.
\end{answer}

\vfill

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

\end{document}
