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

\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 2019--2020 \\
Vrije Universiteit Amsterdam \\
Lecturers: dr.\ J.\,C. Blanchette and drs.\ A. Bentkamp
\hfill\smash{\makebox[0mm][r]{\includegraphics[height=20mm]{griffioen.png}}}

Repeat Exam \\
4 February 2020, 18:30--21:15, NU-2B-11 \\
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. Minor proof steps corresponding to \mbox{\li{refl},}
\li{simp}, or \li{linarith} 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. Some 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}{Error monad}{4+4+5}

The \emph{error monad} is a monad stores either a value of type \li{α} or an
error of type \li{ε}. This corresponds to the following type:

\begin{lstlisting}
    inductive error (α ε : Type) : Type
    | good {} : α → error
    | bad  {} : ε → error

    export error (good bad)
\end{lstlisting}

\kern-2\jot

The error monad generalizes the option monad seen in the lecture. The \li{good}
constructor, corresponding to \li{some}, stores the current result of the
computation. But instead of having a single bad state \li{none}, the error monad
has many bad states of the form \li{bad e}, where \li{e} is an ``exception'' of
type \li{ε}.

\subquestion{a}%
Complete the Lean definitions of the \li{pure} and \li{bind} operations:

\begin{quote}
\li|def error.pure {α ε : Type} : α → error α ε|
\\[2\jot]
\li|def error.bind {α β ε : Type} : error α ε → (α → error β ε) → error β ε|
\end{quote}

\begin{answer}
\begin{lstlisting}
    good

    | (good a) f := f a
    | (bad e)  f := bad e
\end{lstlisting}
\end{answer}

\subquestion{b}%
Assume \li{ma >>= f} is syntactic sugar for \li{error.bind ma f}. Prove the
following two monadic laws. Your proofs should proceed step by step, with at
most one case distinction, rewrite rule, or definition expansion per step, so
that we can clearly see what happens.

\begin{quote}
\li|lemma error.pure_bind {α β ε : Type} (a : α) (f : α → error β ε) :| \\
\noindent\hbox{}\texttt{~~}\li|(error.pure a >>= f) = f a|
\\[2\jot]
\li|lemma error.bind_pure {α ε : Type} (ma : error α ε) :| \\
\noindent\hbox{}\texttt{~~}\li|(ma >>= error.pure) = ma|
\end{quote}

\begin{answer}
\begin{lstlisting}
    calc  (error.pure a >>= f) = good a >>= f :
      by refl
    ... = f a :
      by refl

    begin
      cases ma with a e,
      { calc  (good a >>= @error.pure _ ε)   -- `error.pure` would be acceptable
            = error.pure a :
          by refl
        ... = good a :
          by refl },
      { calc  (bad e >>= @error.pure α _)   -- `error.pure` would be acceptable
            = bad e :
          by refl }
    end
\end{lstlisting}
\end{answer}

\subquestion{c}%
Define the following two operations on the error monad, using Lean syntax:

\begin{quote}
\li|def error.throw {α ε : Type} : ε → error α ε|
\\[2\jot]
\li|def error.catch {α ε : Type} : error α ε → (ε → error α ε) → error α ε|
\end{quote}

The \li{throw} operation raises an exception \li{e}, leaving the monad in
a bad state storing \li{e} (i.e., \li{bad e}).

The \li{catch} operation can be used to recover from an earlier exception. If
the monad currently is in a bad state storing exception \li{e}, \li{catch}
invokes some exception-handling code (the second argument to \li{catch}),
passing \li{e} as argument; this code might raise a new exception. If \li{catch}
is applied to a good state, nothing happens---the monad remains in the good
state.

\begin{answer}
\begin{lstlisting}
    bad

    | (good a) h := good a
    | (bad e)  h := h e
\end{lstlisting}
\end{answer}

\newpage
\question{2}{Logical foundations and mathematics}{4+3+6+4+2}

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

\begin{lstlisting}
    [true, false, true] : _    option ℕ : _    ℤ : _    Sort 5 : _
\end{lstlisting}

\begin{answer}
\begin{lstlisting}
    [true, false, true] : list Prop
    option ℕ : Type
    ℤ : Type
    Sort 5 : Sort 6
\end{lstlisting}
\end{answer}

\subquestion{b}%
The function \li{max : ℕ → ℕ → ℕ} returns the larger one of two given natural numbers
(or either if they are equal). Complete the fourth case in the following
Lean definition:
%
\begin{lstlisting}
    def max : ℕ → ℕ → ℕ
    | 0            0            := 0
    | 0            (nat.succ b) := nat.succ b
    | (nat.succ a) 0            := nat.succ a
    | (nat.succ a) (nat.succ b) := _
\end{lstlisting}

\begin{answer}
\begin{lstlisting}
    | (nat.succ a) (nat.succ b) := nat.succ (max a b)
\end{lstlisting}
\end{answer}

\subquestion{c}%
The type class \li|add_monoid| is defined as follows in Lean:
%
\begin{lstlisting}
    class add_monoid (α : Type) :=
    (add       : α → α → α)
    (zero      : α)
    (add_assoc : ∀a b c : α, add (add a b) c = add a (add b c))
    (zero_add  : ∀a : α, add zero a = a)
    (add_zero  : ∀a : α, add a zero = a)
\end{lstlisting}

\kern-2\jot

Complete the following instantiation of \li{ℕ} with the operator \li{max} as an \li{add_monoid} by providing
a suitable definition of \li{zero} and proofs of the \li{zero_add} and
\li{add_zero} properties:
%
\begin{lstlisting}
    instance monoid_max : add_monoid ℕ :=
    { add       := max,
      zero      := _,
      add_assoc := sorry,
      zero_add  := _,
      add_zero  := _ }
\end{lstlisting}

\begin{answer}
\li{zero := 0}

Both \li{zero_add} and \li{add_zero} can be proved by a case distinction on
\li{a} and by unfolding the definition of \li{max} in each case. (In Lean:
\li{begin intro a, cases a; refl end})\\
\end{answer}

\subquestion{d}%
The function \li{min : ℕ → ℕ → ℕ} returns the smaller one of two given natural numbers.
Can \li{ℕ} be instantiated as an \li{add_monoid} using the operator \li{add := min}?
Briefly explain your answer.

\begin{answer}
No, there is no identity element for \li{min}.
\end{answer}

\subquestion{e}%
Using the representation of \textit{p}-adic numbers as left-infinite streams of
digits, compute the following addition in base \textit{p} $=$ 7:
\[\begin{array}{cr}
  &\ldots \hbox{66666666} \\
  +&\hbox{1} \\
  \hline
   \end{array}\] 

\begin{answer}
0
\end{answer}

\newpage
\question{3}{Even and odd}{4+4+8}

Consider the following inductive definition of even numbers:

\begin{lstlisting}
    inductive even : ℕ → Prop
    | zero             : even 0
    | plus_two {n : ℕ} : even n → even (n + 2)
\end{lstlisting}

\kern-2\jot

\subquestion{a}%
Define a similar predicate for odd numbers, by completing the Lean definition
below:

\begin{lstlisting}
    inductive odd : ℕ → Prop
\end{lstlisting}

\kern-2\jot

The definition should distinguish two cases, like \li{even}, and should
\textit{not} rely on \li{even}.

\begin{answer}
\begin{lstlisting}
    | one              : odd 1
    | plus_two {n : ℕ} : odd n → odd (n + 2)
\end{lstlisting}
\end{answer}

\subquestion{b}%
Give Lean proof terms for the propositions \li{odd 3} and \li{odd 5}, based on
your answer to question~3a.

\begin{answer}
\begin{lstlisting}
    lemma odd_3 :
      odd 3 :=
    odd.plus_two odd.one

    lemma odd_5 :
      odd 5 :=
    odd.plus_two odd_3
\end{lstlisting}
\end{answer}

\subquestion{c}%
Prove the following lemma by rule induction. Make sure to follow the guidelines
given on page~1.

\begin{lstlisting}
    lemma even_odd {n : ℕ} (h : even n) :
      odd (n + 1)
\end{lstlisting}

\begin{answer}
We perform the proof by rule induction on \li{h}.

Goal 1: \li{odd (0 + 1)}. Trivial using \li{odd.one} and the fact that
\li{0 + 1 = 1}.

Goal 2: \li{odd (n + 2 + 1)}. Induction hypothesis: \li{odd (n + 1)}. Trivial
using \li{odd.add_two} and some arithmetic massaging.

In Lean:

\begin{lstlisting}
    begin
      induction h,
      case even.zero {
        exact odd.one },
      case even.plus_two : m {
        have ih : odd (m + 1) := by assumption,
        exact odd.plus_two ih }
    end
\end{lstlisting}
\end{answer}

\newpage
\question{4}{One-point rules}{3+9}

One-point rules are lemmas that can be used to remove a quantifier from a
proposition when the quantified variable can effectively take only one value.
For example, \li{∀x, x = 6 → p x} is equivalent to the much simpler \li{p 6}.

\subquestion{a}%
Louis Reasoner proposes the following nonstandard one-point rule for
$\exists$:

\begin{lstlisting}
    axiom exists.one_point_rule' {α : Type} {t : α} {p : α → Prop} :
      (∃x : α, x = t → p x) ↔ p t
\end{lstlisting}

\kern-2\jot

What is wrong with this rule?

\begin{answer}
It can be used to prove \li{false}. In Lean:

\begin{lstlisting}
    lemma proof_of_false :
      false :=
    begin
      have := @exists.one_point_rule' ℕ 0 (λ_, false),
      simp at this,
      specialize this 1,
      linarith
    end
\end{lstlisting}

\kern-2\jot

Informally, by taking \li{p := λ_, false}, we end up with the proposition
\hbox{\li{(∃x : α, x = t → false) ↔}} \li{false}. After some simplification, we
get \li{¬ (∃x : α, ¬ x = t)}. By taking a type like \li{ℕ}, which has two
distinct values \li{0} and \li{1}, we can take \li{t := 0} and \li{x := 1},
resulting in the equation \li{0 = 1}, from which we can derive \li{false}.
\end{answer}

\subquestion{b}%
Prove the following lemma:

\begin{lstlisting}
    lemma forall_exists.one_point_rule {α : Type} {t : α} {p : α → Prop} :
      (∀x : α, x = t → p x) ↔ (∃x : α, x = t ∧ p x)
\end{lstlisting}

\kern-2\jot

In your proof, clearly identify how the quantifiers are instantiated.

\begin{answer}
\begin{lstlisting}
    iff.intro
      (assume hall : ∀x : α, x = t → p x,
       have hpt : p t :=
         begin
           apply hall t,
           refl
         end,
       show ∃x : α, x = t ∧ p x,
         begin
           apply exists.intro t,
           apply and.intro,
           { refl },
           { exact hpt }
         end)
      (assume hex : ∃x : α, x = t ∧ p x,
       assume x,
       assume hxt : x = t,
       show p x,
         begin
           cases hex with w h,
           cases h with hwt pw,
           rw hwt at pw,
           rw hxt,
           assumption
         end)
\end{lstlisting}

\kern-2\jot

You can also do it in two steps, proving
%
\[\hbox{\li{(∀x : α, x = t → p x) ↔ p t}\quad\hbox{and}\quad
  \li{(∃x : α, x = t ∧ p x) ↔ p t}}\]
%
separately and then joining the two.
\end{answer}

\newpage
\question{5}{Arithmetic expressions}{8+4}

Consider this simple type of arithmetic expressions:

\begin{lstlisting}
    inductive exp : Type
    | var  : string → exp
    | num  : ℤ → exp
    | plus : exp → exp → exp

    export exp (var num plus)
\end{lstlisting}

\kern-2\jot

The following evaluation function computes the numeric value of an expression
given an environment \li{env}:

\begin{lstlisting}
    def eval (env : string → ℤ) : exp → ℤ
    | (var x)      := env x
    | (num i)      := i
    | (plus e₁ e₂) := eval e₁ + eval e₂
\end{lstlisting}

\kern-2\jot

We want to rewrite arithmetic expressions such that
\li{plus} is regrouped to the right. That is, every subexpression of the form
\li{plus (plus e₁ e₂) e₃} should become
\li{plus e₁ (plus e₂ e₃)}. The function \li{regroup}, which relies on the
auxiliary function \li{shuffle}, performs this regrouping:

\begin{lstlisting}
    def shuffle : exp → exp → exp
    | (var x)      a := plus (var x) a
    | (num i)      a := plus (num i) a
    | (plus e₁ e₂) a := shuffle e₁ (shuffle e₂ a)

    def regroup : exp → exp
    | e := shuffle e (num 0)
\end{lstlisting}

\kern-2\jot

Note that \li{regroup} does not just regroup \li{plus} but also adds \li{0} at the
end. Thankfully, this has no impact on the numeric value of the expression.

\subquestion{a}%
Prove the following lemma about \li{shuffle} by structural induction.
Make sure to follow the guidelines given on page~1.

\begin{lstlisting}
    lemma eval_shuffle (env : string → ℤ) (e a : exp) :
      eval env (shuffle e a) = eval env e + eval env a
\end{lstlisting}

\begin{answer}
\begin{lstlisting}
    begin
      induction e generalizing a,
      case var : x {
        calc  eval env (shuffle (var x) a)
            = eval env (var x) + eval env a :
          by simp [shuffle, eval] },
      case num : i {
        calc  eval env (shuffle (num i) a)
            = eval env (num i) + eval env a :
          by simp [shuffle, eval] },
      case plus : e₀ e₁ ih₀ ih₁ {
        -- ih₀ : ∀a, eval env (shuffle e₀ a) = eval env e₀ + eval env a
        -- ih₁ : ∀a, eval env (shuffle e₁ a) = eval env e₁ + eval env a
        calc  eval env (shuffle (plus e₀ e₁) a)
            = eval env (shuffle e₀ (shuffle e₁ a)) :
          by refl
        ... = eval env e₀ + eval env (shuffle e₁ a) :
          by simp [ih₀]
        ... = eval env e₀ + eval env e₁ + eval env a :
          by simp [ih₁]
        ... = eval env (plus e₀ e₁) + eval env a :
          by simp [eval] }
    end
\end{lstlisting}
\end{answer}

\subquestion{b}%
Prove the following lemma via a step-by-step calculational proof, with at most
one rewrite rule or definition expansion per step, so that we can clearly see
what happens. Your proof may rely on the lemma \li{eval_shuffle} from
question~5a.

\begin{lstlisting}
    lemma eval_regroup (env : string → ℤ) (e : exp) :
      eval env (regroup e) = eval env e
\end{lstlisting}

\begin{answer}
\begin{lstlisting}
    calc  eval env (regroup e)
        = eval env (shuffle e (num 0)) :
      by refl
    ... = eval env e + eval env (num 0) :
      by rw eval_shuffle
    ... = eval env e :
      by simp [eval]
\end{lstlisting}
\end{answer}

\newpage
\question{6}{Big-step semantics}{6+6+3+3}

On the occasion of this repeat exam, we introduce REPEAT, a brand-new
programming language that resembles the WHILE language but whose defining
feature is a \li{repeat} loop.

The Lean definition of its abstract syntax tree follows:

\begin{lstlisting}
    inductive program : Type
    | skip {} : program
    | assign  : string → (state → ℕ) → program
    | seq     : program → program → program
    | unless  : (state → Prop) → program → program
    | repeat  : ℕ → program → program

    export program (skip assign seq unless repeat)
\end{lstlisting}

\kern-2\jot

The \li{skip}, \li{assign}, and \li{seq S T} statements have the same syntax and
semantics as in the WHILE language. We also write \li{S ;; T} for \li{seq S T}.

The \li{unless b S} statement executes \li{S} unless \li{b} is true---i.e., it
executes \li{S} if \li{b} is false. Otherwise, \li{unless b S} does nothing.
In particular, \li{unless (λ_, true) S} is
equivalent to \li{skip} (according to a big-step or a denotational semantics),
and \li{unless (λ_, false) S} is equivalent to \li{S}. This construct is
inspired by the Perl language.

The \li{repeat n S} statement executes \li{S} exactly \li{n} times. Thus,
\li{repeat 10 S} is equivalent to
\hbox{\li{S ;; S ;;}} \hbox{\li{S ;; S ;; S ;; S ;; S ;; S ;; S ;; S},}
and \li{repeat 0 S} is equivalent to \li{skip}.

\subquestion{a}%
Complete the following specification of a big-step semantics as derivation
rules.

\vskip\abovedisplayskip

\noindent\hfill
\AXC{\phantom{$\cdot$}}
\RL{\textsc{Skip}}
\UIC{\strut\li|(skip, s) ⟹ s|}
\DP
\qquad
\AXC{\phantom{$\cdot$}}
\RL{\textsc{Asn}}
\UIC{\strut\li|(assign x a, s) ⟹ s[x ↦ s(a)]|}
\DP
\hfill\hbox{}

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

\vskip\belowdisplayskip

\begin{answer}
\vskip\abovedisplayskip

\noindent\hfill
\AXC{\strut}
\RL{\textsc{Unless-True}\quad\hbox{if \li|b s|}}
\UIC{\strut\li|(unless b S, s) ⟹ s|}
\DP
\hfill\hbox{}

\noindent\hfill
\AXC{\strut\li|(S, s) ⟹ t|}
\RL{\textsc{Unless-False}\quad\hbox{if \li|\¬ b s|}}
\UIC{\strut\li|(unless b S, s) ⟹ t|}
\DP
\hfill\hbox{}

\noindent\hfill
\AXC{\strut}
\RL{\textsc{Repeat-Zero}}
\UIC{\strut\li|(repeat 0 x, s) ⟹ s|}
\DP
\hfill\hbox{}

\noindent\hfill
\AXC{\strut\li|(S, s) ⟹ t|}
  \AXC{\strut\li|(repeat n S, t) ⟹ u|}
\RL{\textsc{Repeat-Succ}}
\BIC{\strut\li|(repeat (n + 1) S, s) ⟹ u|}
\DP
\hfill\hbox{}

\vskip\belowdisplayskip
\end{answer}

\subquestion{b}%
Specify the same big-step semantics in Lean by completing the following
definition:

\begin{lstlisting}
    inductive big_step : program × state → state → Prop
    | skip {s} :
      big_step (skip, s) s
    | assign {x a s} :
      big_step (assign x a, s) (s{x ↦ a s})
    | seq {S T s t u} (h₁ : big_step (S, s) t) (h₂ : big_step (T, t) u) :
      big_step (S ;; T, s) u
\end{lstlisting}

\begin{answer}
\begin{lstlisting}
    | unless_true {b : state → Prop} {S s} (hcond : b s) :
      big_step (unless b S, s) s
    | unless_false {b : state → Prop} {S s t} (hcond : ¬ b s)
        (hbody : big_step (S, s) t) :
      big_step (unless b S, s) t
    | repeat_zero {S s} :
      big_step (repeat 0 S, s) s
    | repeat_succ {n S s t u}
        (hbody : big_step (S, s) t)
        (hrest : big_step (repeat n S, t) u) :
      big_step (repeat (n + 1) S, s) u
\end{lstlisting}
\end{answer}

\subquestion{c}%
Is the REPEAT language deterministic? Briefly explain your answer.

\begin{answer}
Yes. For any statement, only one rule can apply, and that rule's conclusion is
fully determined by its premises.
\end{answer}

\subquestion{d}%
Are REPEAT programs guaranteed to terminate? Briefly explain your answer.

\begin{answer}
Yes. Loops are the only construct that could be problematic, but \li{repeat}
loops are bounded by a constant number of iterations and could be translated
away by a preprocessor.
\end{answer}

\vfill

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

\end{document}
