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

Final Exam \\
Tuesday 17 December 2019, 15:15--18:00, WN S-623 S-631 S-655 \\
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}{Variable substitution}{5+6}

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}

\subquestion{a}%
Complete the following recursive Lean definition of a function \li{subst} that
performs simultaneous substitution of variables. The application \li{subst ρ e}
simultaneously replaces every variable in \li{e} with a new subexpression: Each
occurrence of \li{Var x} is replaced with \li{ρ x}.

\begin{lstlisting}
    def subst (ρ : string → exp) : exp → exp
\end{lstlisting}

\begin{answer}
\begin{lstlisting}
    | (Var y)      := ρ y
    | (Num i)      := Num i
    | (Plus e₁ e₂) := Plus (subst e₁) (subst e₂)
\end{lstlisting}
\end{answer}

\subquestion{b}%
If we perform simultaneous substitution with \li{λx, Var x}, we should get the
identity function on expressions:

\begin{lstlisting}
    lemma subst_Var (e : exp) :
      subst (λx, Var x) e = e
\end{lstlisting}

Prove this fact by structural induction on \li{e}. Make sure to follow the proof
guidelines given on page~1.

\begin{answer}
After performing structural induction on \li{e}, we are left with three goals.

Goal 1: \li{subst (λx, Var x) (Var y) = Var y}.
By definition of \li{subst}, we have \\
\li{subst (λx, Var x) (Var y) = (λx, Var x) y = Var y}.

Goal 2: \li{subst (λx, Var x) (Num i) = Num i}.
This follows directly by definition of \li{subst}.

Goal 3: \li{subst (λx, Var x) (Plus e₁ e₂) := Plus e₁ e₂}.
The induction hypotheses are \\
(IH1) \li{subst (λx, Var x) e₁ = e₁} and
(IH2) \li{subst (λx, Var x) e₂ = e₂}. \\
By definition of \li{subst}, we have \\
\li{subst (λx, Var x) (Plus e₁ e₂) = Plus (subst (λx, Var x) e₁) (subst (λx, Var x) e₂)}. \\
Using IH1 and IH2, we can simply the right-hand side to \li{Plus e₁ e₂}, as
desired.

In Lean:

\begin{lstlisting}
    begin
      induction e,
      { rw [subst] },
      { rw [subst] },
      { rw [subst],
        rw e_ih_a,
        rw e_ih_a_1 }
    end
\end{lstlisting}
\end{answer}

\newpage
\question{2}{Identity monad}{4+7}

The \emph{identity monad} is a monad that simply stores a value of type \li{α},
without any special effects or computational strategy. In other words, it simply
provides a box containing a single value of type \li{α}. Viewed as a type
constructor, the identity monad is the identity function \li{λα : Type, α}. When
applying it to a type variable \li|α|, we end up with \li{(λα : Type, α) α},
i.e., \li{α} itself.

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

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

\begin{answer}
\li{λa, a}
\\[2\jot]
\li{λa f, f a}
\end{answer}

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

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

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

calc  (ma >>= id.pure) = id.pure ma
  by refl
... = ma
  by refl

calc  ((ma >>= f) >>= g) = (f ma >>= g) :
  by refl
... = g (f ma) :
  by refl
... = f ma >>= g :
  by refl
... = (ma >>= (λa, f a >>= g)) :
  by refl
\end{lstlisting}
\end{answer}

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

We introduce WHY, a new programming language that resembles the WHILE language
but that includes a few features that make students wonder, ``Why??''

The Lean definition of its abstract syntax tree follows:

\begin{lstlisting}
    inductive program : Type
    | skip {} : program
    | havoc   : string → program
    | seq     : program → program → program
    | choose  : program → program → program
    | loop    : program → program

    export program (skip havoc seq choose loop)
\end{lstlisting}

The \li{skip} and \li{seq S T} statements have the same syntax and semantics as
in the WHILE language. The notation \li{S ;; T} stands for \li{seq S T}.

The \li{havoc x} statement assigns a completely random value to the
variable~\li{x}.

The \li{choose S T} statement randomly executes either \li{S} or \li{T}. It
behaves like an \li{if}--\li{then}--\li{else} statement whose Boolean condition
is random.

The \li{loop S} statement behaves like a \li{while} loop whose Boolean condition
is random. It may exit at any point. For example, \li{loop S} could have the
same end-to-end behavior as \li{skip} or \li{S} or \li{S ;; S} or \li{S ;; S ;; S}
or \ldots\,.

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

\vskip\abovedisplayskip

\noindent\hfill
\AXC{\strut\li|(S, s) ⇒ (S', s')|}
\RL{\textsc{Seq-Step}}
\UIC{\strut\li|(S ;; T, s) ⇒ (S' ;; T, s')|}
\DP
\qquad
\AXC{\strut\strut}
\RL{\textsc{Seq-Skip}}
\UIC{\strut\li|(skip ;; T, s) ⇒ (T, s)|}
\DP
\hfill\hbox{}

\vskip\belowdisplayskip

\begin{answer}
\vskip\abovedisplayskip

\noindent\hfill
\AXC{\strut}
\RL{\textsc{Havoc}}
\UIC{\strut\li|(havoc x, s) ⇒ (skip, s[x ↦ n])|}
\DP
\hfill\hbox{}

\noindent\hfill
\AXC{\strut}
\RL{\textsc{Choose-First}}
\UIC{\strut\li|(choose S T, s) ⇒ (S, s)|}
\DP
\qquad
\AXC{\strut}
\RL{\textsc{Choose-Second}}
\UIC{\strut\li|(choose S T, s) ⇒ (T, s)|}
\DP
\hfill\hbox{}

\noindent\hfill
\AXC{\strut}
\RL{\textsc{Loop}}
\UIC{\strut\li|(loop S, s) ⇒ (choose (S ;; loop S) skip, s)|}
\DP
\hfill\hbox{}

\vskip\belowdisplayskip
\end{answer}

\subquestion{b}%
Specify the same small-step semantics as an inductive predicate by completing
the following Lean definition.

\begin{lstlisting}
    inductive small_step : program × state → program × state → Prop
    | seq_step {S T s s' S'} :
      small_step (S, s) (S', s') → small_step (S ;; T, s) (S ;; T, s')
    | seq_skip {T s} :
      small_step (skip ;; T, s) (T, s)
\end{lstlisting}

\begin{answer}
\begin{lstlisting}
    | havoc {x s n} :
      small_step (havoc x, s) (skip, s{x ↦ n})
    | choose_first {S T s} :
      small_step (choose S T, s) (S, s)
    | choose_second {S T s} :
      small_step (choose S T, s) (T, s)
    | loop {S s} :
      small_step (loop S, s) (choose (seq S (loop S)) skip, s)
\end{lstlisting}
\end{answer}

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

\begin{answer}
No. For example, starting from the configuration \li|(havoc "x", s)|,
we can end up in two different states: \li|s{"x" ↦ 0}| and \li|s{"x" ↦ 1}|.
\end{answer}

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

\begin{answer}
No. Consider the infinite execution
\li|(loop skip, s) ⇒ (choose (loop skip) skip, s) ⇒ (loop skip, s) ⇒ (choose (loop skip) skip, s) ⇒ ⋯|
\end{answer}

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

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

\begin{lstlisting}
    true : _    ℕ : _    Prop : _    Type : _
\end{lstlisting}

\begin{answer}
\begin{lstlisting}
true : Prop
ℕ : Type
Prop : Type
Type : Type 1
\end{lstlisting}
\end{answer}

\subquestion{b}%
Let \li{α : Type}. The composition \li{g ∘ f} of two functions \li{f, g : α → α}
is defined as the function \hbox{\li{λx, g (f x)}}. What is the neutral element
for \li{∘}, i.e., the function \li{h} such that \li{h ∘ f = f} and
\li{g ∘ h = g} for all \li{f, g : α → α}?

\begin{answer}
\li{λx, x}
\end{answer}

\subquestion{c}%
The type class \li|monoid| is defined as follows in Lean:
%
\begin{lstlisting}
    class 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}
%

Complete the following instantiation of \li{ℕ → ℕ} as a \li{monoid} by providing
a suitable definition of \li{one} and proofs of the \li{one_mul} and
\li{mul_one} properties:
%
\begin{lstlisting}
    instance monoid_comp : monoid (ℕ → ℕ) :=
    { mul := (λg f, g ∘ f),
      one := _,
      mul_assoc := sorry,
      mul_one := _,
      one_mul := _ }
\end{lstlisting}


\begin{answer}
\li{λx, x}

\li{one_mul}: \li{(λg f, g ∘ f) (λx, x) a = (λx, x) ∘ a = a} \\
\li{mul_one}: \li{(λg f, g ∘ f) a (λx, x) = a ∘ (λx, x) = a}

The second equality of both \li{one_mul} and \li{mul_one} is justified because
\li{(λx, x)} is the neutral, or identity, element for composition.
\end{answer}

\subquestion{d}%
The type class \li{group} is defined as follows in Lean:
%
\begin{lstlisting}
    class group (α : 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)
    (inv : α → α)
    (mul_left_inv : ∀a : α, mul (inv a) a = one)
\end{lstlisting}
%
Can the type \li{ℕ → ℕ} be instantiated as a \li{group},
using the same definition for \li{mul} and \li{one} as in question 4c?
Briefly explain your answer.

\begin{answer}
No, there is no possible definition of \li{inv} that would make
\li{mul_left_inv} true. This is because not all functions are invertible.
\end{answer}

\subquestion{e}%
We used the following definition for Cauchy sequences to construct the real numbers:
%
\begin{lstlisting}
    def is_cau_seq (f : ℕ → ℚ) : Prop :=
    ∀ε > 0, ∃N, ∀m ≥ N, abs (f N - f m) < ε
\end{lstlisting}

\kern-2\jot

Which function in this definition needs to be changed to construct the
\textit{p}-adic numbers?

\begin{answer}
\begin{lstlisting}
abs
\end{lstlisting}
\end{answer}

  % Other Ideas:
  % * Instantiate function composition as a monoid
  % * Instantiate nat.le as a linear\_order
  % * Instantiate nat as an add\_monoid
  % * Instantiate multiset/finset as a monoid
  % * max/min on nat as monoid

  % Instead of monoid, left\_cancel\_semigroup would also work.
  % Ask why it cannot be instantiated as a group.


\newpage
\question{5}{Palindromes}{6+7+6}

Palindromes are lists that read the same from left to right and from right to
left. For example, \li{[a, b, b, a]} and \li{[a, h, a]} are palindromes.

\subquestion{a}%
Define an inductive predicate that is \li{true} if and only if the list
passed as argument is a palindrome, by completing the Lean definition below:

\begin{lstlisting}
    inductive palindrome {α : Type} : list α → Prop
\end{lstlisting}

\kern-2\jot

The definition should distinguish three cases:
%
\begin{enumerate}
\item[1.] The empty list \li{[]} is a palindrome.

\item[2.] For any element \li{x : α}, the singleton list \li{[x]} is a palindrome.

\item[3.] For any element \li{x : α} and any palindrome
  \li{[y}$_\texttt{1}$\li{, ..., y}$_\texttt{\itshape n}$\li{]}, the list
  \li{[x, y}$_\texttt{1}$\li{, ..., y}$_\texttt{\itshape n}$\li{, x]} is a
  palindrome.
\end{enumerate}

\begin{answer}
\begin{lstlisting}
| nil : palindrome []
| single (x : α) : palindrome [x]
| sandwich (x : α) (xs : list α) (pal_xs : palindrome xs) :
  palindrome ([x] ++ xs ++ [x])
\end{lstlisting}
\end{answer}

\subquestion{b}%
Let \li{reverse} be the following operation:
%
\begin{lstlisting}
    def reverse {α : Type} : list α → list α
    | []        := []
    | (x :: xs) := reverse xs ++ [x]
\end{lstlisting}
%
Using \li{reverse}, prove that the reverse of a palindrome is also a palindrome:
%
\begin{lstlisting}
    lemma rev_palindrome {α : Type} (xs : list α) (pal_xs : palindrome xs) :
      palindrome (reverse xs)
\end{lstlisting}

\kern-2\jot

Make sure to follow the proof guidelines given on page~1. If it helps, you may
invoke the following lemma (without having to prove it):
%
\begin{lstlisting}
    lemma reverse_append_sandwich {α : Type} (x : α) (ys : list α) :
      reverse ([x] ++ ys ++ [x]) = [x] ++ reverse ys ++ [x]
\end{lstlisting}

\begin{answer}
We perform rule induction on the hypothesis \li{pal_xs}.

Goal 1: \li{palindrome (reverse [])}. Obvious by \li{palindrome.nil} since
\li{reverse [] = []}.

Goal 2: \li{palindrome (reverse [x])}. Obvious by \li{palindrome.single} since
\li{reverse [x] = [x]}.

Goal 3: \li{palindrome (reverse ([x] ++ xs ++ [x]))}. Hypothesis:
\li{palindrome xs}. Induction hypothesis: \li{palindrome (reverse xs)}.

\li{palindrome (reverse ([x] ++ xs ++ [x])) ↔ palindrome ([x] ++ reverse xs ++ [x])},
using the given \li{reverse_append_sandwich} lemma. Using the introduction
rule \li{palindrome.sandwich}, we reduce the new goal to
\li{palindrome (reverse xs)}, which holds by the induction hypothesis.

In Lean:

\begin{lstlisting}
    induction pal_xs,
    { exact palindrome.nil },
    { exact palindrome.single _ },
    { rw reverse_append_sandwich,
      apply palindrome.sandwich,
      apply pal_xs_ih }
\end{lstlisting}
\end{answer}

\subquestion{c}%
Prove that the lists \li{[]}, \li{[a, a]}, and \li{[a, b, a]} are palindromes,
corresponding to the following lemma statements in Lean:

\begin{lstlisting}
    lemma palindrome_nil {α : Type} :
      palindrome ([] : list α)

    lemma palindrome_aa {α : Type} (a : α) :
      palindrome [a, a]

    lemma palindrome_aba {α : Type} (a b : α) :
      palindrome [a, b, a]
\end{lstlisting}

\begin{answer}
\begin{lstlisting}
    palindrome.nil

    palindrome.sandwich a [] palindrome.nil

    palindrome.sandwich a [b] (palindrome.single b)
\end{lstlisting}
\end{answer}

\newpage
\question{6}{One-point rules}{5+5+3}

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 = 5 → p x} is equivalent to the much simpler \li{p 5}.

\subquestion{a}%
Prove the one-point rule for $\forall$. In your proof, identify clearly how the
quantifier is instantiated.

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

\begin{answer}
\begin{lstlisting}
    iff.intro
      (assume hall : ∀x : α, x = t → p x,
       show p t,
         begin
           apply hall t,
           refl
         end)
      (assume hp : p t,
       assume x : α,
       assume heq : x = t,
       show p x,
         begin
           rw heq,
           exact hp
         end)
\end{lstlisting}
\end{answer}

\subquestion{b}%
Prove the one-point rule for $\exists$. In your proof, identify clearly which
witness is supplied for the quantifier.

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

\begin{answer}
\begin{lstlisting}
    iff.intro
      (assume hex : ∃x : α, x = t ∧ p x,
       show p t,
         begin
           cases hex,
           cases hex_h,
           rw hex_h_left at hex_h_right,
           exact hex_h_right
         end)
      (assume hp : p t,
       show ∃x : α, x = t ∧ p x,
         begin
           apply exists.intro t,
           apply and.intro,
           { refl },
           { exact hp }
         end)
\end{lstlisting}
\end{answer}

\subquestion{c}%
Alyssa P. Hacker proposes the following alternative one-point rule for
$\forall$:

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

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 := @forall.one_point_rule' ℕ 0 (λ_, true),
      simp at this,
      specialize this 1,
      linarith
    end
\end{lstlisting}

Informally, by taking \li{p := λ_, true}, we end up with the proposition
\hbox{\li{(∀x : α, x = t ∧ true) ↔}} \li{true}. 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}

\vfill

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

\end{document}
