\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 2021--2022 \\
Vrije Universiteit Amsterdam \\
Lecturer: dr.\ J.\,C. Blanchette
\hfill\smash{\makebox[0mm][r]{\includegraphics[height=20mm]{griffioen.png}}}

Resit Exam 1 \\
Tuesday 15 February 2022, 18:45--21:00, NU-3B07 \\
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. We present proofs in a textual style, but other styles (e.g., closer
to Lean) are also allowed.
\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}{3+4+7}

Consider the type \li{btree} of binary trees where each node is either an empty
leaf or an inner node with two child trees:
\begin{lstlisting}
    inductive btree : Type
    | empty : btree
    | node  : btree → btree → btree
\end{lstlisting}

The height of a tree is the largest number of nodes along a path from the root
node to a leaf:
\begin{lstlisting}
    def height : btree → ℕ
    | btree.empty      := 0
    | (btree.node l r) := 1 + max (height l) (height r)
\end{lstlisting}

\subquestion{a}%
Complete the definition below of the function \lstinline{btree.with_height}.
Given a natural number \mbox{\lstinline{n},} \lstinline{btree.with_height n} should
be a tree of height \lstinline{n}.
You do not need to prove that your definition has the desired property.
\begin{lstlisting}
    def btree.with_height : ℕ → btree
\end{lstlisting}

\begin{answer}
\begin{lstlisting}
    | 0 := btree.empty
    | (n+1) := btree.node btree.empty (btree.with_height n)
\end{lstlisting}
\end{answer}

\subquestion{b}%
Write a Lean definition of an inductive predicate \lstinline{is_balanced : btree → Prop}
that determines if a tree is balanced. A tree is balanced if it is empty or if for
each node in the tree, its two subtrees have the same height. You can use the
\lstinline{height} function.

\begin{answer}
\begin{lstlisting}
inductive is_balanced : btree → Prop
| empty : is_balanced btree.empty
| node : ∀l r, is_balanced l → is_balanced r → height l = height r →
    is_balanced (btree.node l r)
\end{lstlisting}
\end{answer}

\subquestion{c}%
The \lstinline{graft} function takes two trees and attaches copies of the second
tree to each leaf of the first tree:
\begin{lstlisting}
    def graft : btree → btree → btree
    | btree.empty      u := u
    | (btree.node l r) u := btree.node (graft l u) (graft r u)
\end{lstlisting}

Give a proof by induction of the lemma \lstinline{height_graft}, showing that
the height of a grafted tree is the sum of the heights of the original trees.
For each case, clearly indicate the inductive hypotheses and the goal to be
proved.
You can refer to the following two lemmas without proving them:
\begin{lstlisting}
    #check max_add_add_left  -- ∀a b c : ℕ, max (a + b) (a + c) = a + max b c
    #check max_add_add_right -- ∀a b c : ℕ, max (a + b) (c + b) = max a c + b
\end{lstlisting}

\begin{lstlisting}
    lemma height_graft :
      ∀t u : btree, height (graft t u) = height t + height u
\end{lstlisting}

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

Case \li{empty}: The goal is
\li|height (graft btree.empty u) = height btree.empty + height u|.

The left-hand side simplifies as follows: \\
\li|height (graft btree.empty u)| \\
\li|= height u| by definition of \li|graft|

The right-hand side simplifies as follows: \\
\li|height btree.empty + height u| \\
\li|= 0 + height u| by definition of \li|height| \\
\li|= height u| by arithmetic

The two sides are equal.

Case \li{node}. The goal is
\li|height (graft (btree.node l r) u) = height (btree.node l r) + height u|.
The induction hypotheses are
\li|∀u, height (graft l u) = height l + height u| and
\li|∀u, height (graft r u) = height r + height u|.

The left-hand side simplifies as follows: \\
\li|height (graft (btree.node l r) u)| \\
\li|= height (btree.node (graft l u) (graft r u))| by definition of \li|graft| \\
\li|= 1 + max (height (graft l u)) (height (graft r u))| by definition of \li|height| \\
\li|= 1 + max (height l + height u) (height r + height u)| by induction hypotheses \\
\li|= 1 + max (height l) (height r) + height u| by \li|max_add_add_right|

The right-hand side simplifies as follows: \\
\li|height (btree.node l r) + height u| \\
\li|1 + max (height l) (height r) + height u| by definition of \li|height|

The two sides are equal.
\end{answer}

\newpage

\question{2}{Repeating strings}{4+3}

\subquestion{a}%
Complete the Lean definition of an inductive predicate \lstinline{is_repeat} on
two strings \lstinline{xs} and \lstinline{ys}, stating that \lstinline{ys} is
the string \lstinline{xs} concatenated with itself one or more times:

\begin{lstlisting}
    inductive is_repeat : list char → list char → Prop
\end{lstlisting}

Examples of strings where this relation holds:
\begin{lstlisting}
    is_repeat "exams" "exams"
    is_repeat "love" "lovelove"
    is_repeat "abab" "abababababab"
\end{lstlisting}
Examples of strings where this relation does not hold:
\begin{lstlisting}
    ¬ is_repeat "abc" ""
    ¬ is_repeat "lovelove" "love"
    ¬ is_repeat "aaa" "aaaa"
    ¬ is_repeat "abc" "dabcabcd"
\end{lstlisting}
(For convenience, we identify strings with lists of characters.)

Your definition should consider two cases: \lstinline{ys} repeats \lstinline{xs} one time and \lstinline{ys} repeats \lstinline{xs} more than one time.

\begin{answer}
\begin{lstlisting}
    | once : ∀xs, is_repeat xs xs
    | many : ∀xs ys, is_repeat xs ys → is_repeat xs (xs ++ ys)
\end{lstlisting}
or
\begin{lstlisting}
    | once : ∀xs, is_repeat xs xs
    | many : ∀xs ys, is_repeat xs ys → is_repeat xs (ys ++ xs)
\end{lstlisting}
\end{answer}

\subquestion{b}%
Give a short proof of the proposition \lstinline{is_repeat "a" "aaa"}:
\begin{lstlisting}
    lemma a_aaa : is_repeat "a" "aaa"
\end{lstlisting}

\begin{answer}
Apply \li{is_repeat.many} twice, then apply \li{is_repeat.once}.
\end{answer}

\newpage
\question{3}{The \textsc{IFFY} language}{6+9+6}

The \textsc{IFFY} programming language is similar to the \textsc{WHILE}
language, but its \lstinline{if} statement does not work quite right. It has the
following kinds of statements:
\begin{itemize}
  \item \lstinline{skip} does nothing;
  \item \lstinline{x := a} assigns \lstinline{a} to the variable \lstinline{x};
  \item \lstinline{S ; T} executes the statements of \lstinline{S} followed by the statements of \lstinline{T};
  \item \lstinline{iffy b then S} does nothing if the Boolean \lstinline{b} is false. If \lstinline{b} is true, it nondeterministically chooses between executing the statement \lstinline{S} or doing nothing.
\end{itemize}

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

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

\subquestion{a}%
The big-step semantics of the \textsc{IFFY} language relates a program
\lstinline{S : stmt} and an input state \lstinline{s :} \li{string → ℤ} to an
output state \lstinline{t : string → ℤ}. Complete the following big-step
semantics by giving the derivation rules for the \lstinline{iffy} statement:

\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}
\begin{lstlisting}
           (S, s) ⟹ t
    ------------------------ If-Exec   if b is true
    (iffy b then S, s) ⟹ t

    ------------------------ If-Skip
    (iffy b then S, s) ⟹ s
\end{lstlisting}
\end{answer}

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

\begin{lstlisting}
    inductive big_step : (stmt × (string → ℤ)) → (string → ℤ) → Prop
    | skip {s} : big_step (stmt.skip, s) s
\end{lstlisting}

\begin{answer}
\begin{lstlisting}
  | assign {x a s} : big_step (assign x a, s) (λy, if x = y then a else s y)
  | seq {S₁ S₂ s t u} : big_step (S₁, s) t → big_step (S₂, t) u →
      big_step (S₁ ;; S₂, s) u
  | if_exec {S s t} : big_step (S, s) t → big_step (iffy tt S, s) t
  | if_skip {b S s} : big_step (iffy b S, s) s
\end{lstlisting}
\end{answer}

\subquestion{c}%
Give a derivation tree in the big-step semantics for an execution of the program
\lstinline{P} defined below, such that the variable \lstinline{x} gets
assigned the value \lstinline{1}. Clearly indicate the name of each rule.

\begin{lstlisting}
    def P : stmt :=
    assign "x" 0 ;; iffy true (assign "x" 1)
\end{lstlisting}

\begin{answer}
{\footnotesize
\begin{lstlisting}
                                          ------------------------------------- Assign
                                          ((assign "x" 1), s[x:=0]) ⟹ s[x:=1]
----------------------------- Assign   --------------------------------------------- If-Exec
(assign "x" 0, s) ⟹ s[x:=0]           (iffy b (assign "x" 1), s[x:=0]) ⟹ s[x:=1]
------------------------------------------------------------------------------------ Seq
       (assign "x" 0 ;; iffy b (assign "x" 1), s) ⟹ s[x:=1]
\end{lstlisting}
}
\end{answer}

\newpage

\question{4}{Logic}{6+6+5}

\subquestion{a}%
Give a detailed proof of the following lemma. Make sure to
emphasize and clearly label every introduction or elimination rule.
\begin{lstlisting}
    lemma about_exists_and_or {α : Type} {p q : α → Prop} :
      (∃x, p x ∨ q x) → (∃x, p x) ∨ (∃x, q x) :=
\end{lstlisting}

\begin{answer}
Assume \li{h : ∃ x, p x ∨ q x}. \\
Perform $\exists$-elimination on \li{h}, giving a witness \li{w} and
the property \li{hpq : p w ∨ q w}. \\
Perform or elimination on \li{hpq}. This gives two cases.

Case \li{hp : p w}: Perform $\exists$-introduction with the witness \li{w},
giving \li{∃x, p x}. \\
Then perform left $\lor$-introduction to get \li|(∃x, p x) ∨ (∃x, q x)|.

Case \li{hq : p w}: Similar to \li{hp}. Perform $\exists$-introduction with the
witness \li{w}, giving \li{∃x, q x}. \\
Then perform right $\lor$-introduction to get \li|(∃x, p x) ∨ (∃x, q x)|.
\end{answer}

\subquestion{b}%
Let \lstinline{R : ℤ → ℤ → Prop} be a predicate on two integers
that satisfies the following three introduction rules:
\begin{center}
\begin{tabular}{@{}r@{}l@{}}
\lstinline|R.refl| & \lstinline| : ∀a, R a a| \\
\lstinline|R.symm| & \lstinline| : R ?a ?b → R ?b ?a| \\
\lstinline|R.trans| & \lstinline| : R ?a ?b → R ?b ?c → R ?a ?c| \\
\end{tabular}
\end{center}

Give a detailed proof of the following theorem.
Clearly indicate when you use the rules \lstinline{R.refl}, \lstinline{R.symm}, or \lstinline{R.trans}:

\begin{lstlisting}
    theorem euclid : ∀a b c : ℤ, R a b → R a c → R b c
\end{lstlisting}

\begin{answer}
Fix \li{a}, \li{b}, \li{c}. \\
Assume \li{hab : R a b} and \li{hac : R a c}. \\
By \li{R.symm} on \li{hab}, we get \li{hba : R b a}. \\
By \li{R.trans} on \li{hba} and \li{hac}, we get the desired conclusion
\li{R b c}.
\end{answer}

\subquestion{c}%
One of the following two lemma statements is correct.
Indicate which is the correct lemma and give a detailed proof of that statement.
Make sure to emphasize and clearly label every introduction or elimination rule.

\begin{lstlisting}
    lemma or_of_and {p q : Prop} (h : p ∧ q) : p ∨ q

    lemma and_of_or {p q : Prop} (h : p ∨ q) : p ∧ q
\end{lstlisting}

\begin{answer}
\li{or_of_and} is correct. By left $\land$-elimination, we get \li{hp : p}.
By left $\lor$-introduction, we get the desired conclusion, \li{p ∨ q}.
\end{answer}

\newpage

\question{5}{Monads}{7+5+4+3}

\subquestion{a}%
Complete the following recursive Lean definition taking a list of functions and a list of arguments.
It applies the first function to the first argument, the second function to the second argument, and so on, stopping when either list runs out.
\begin{lstlisting}
    def list.pairwise {α β : Type} : list (α → β) → list α → list β
\end{lstlisting}
For example, \lstinline{list.pairwise [(λx, x + 1), (λx, x * 2)] [1, 3, 10] = [2, 6]}.

\begin{answer}
\begin{lstlisting}
    | []        _         := []
    | _         []        := []
    | (f :: fs) (x :: xs) := f x :: list.pairwise fs xs
\end{lstlisting}
\end{answer}

\subquestion{b}%
Let \lstinline{m} be a monad. Recall that a monad \lstinline{m} has two operations:
\begin{itemize}
  \item \lstinline!pure {α} : α → m α!
  \item \lstinline!bind {α β} : m α → (α → m β) → m β!
\end{itemize}

Complete the following definition of the operation \lstinline{ap mf mx} that applies its first boxed argument to the second boxed argument, putting the result in a box:
\begin{lstlisting}
    def ap {α β : Type} (mf : m (α → β)) (mx : m α) : m β
\end{lstlisting}

\begin{answer}
\begin{lstlisting}
    do f ← mf,
       x ← mx,
       pure (f x)
\end{lstlisting}
\end{answer}

\subquestion{c}%
The operations \lstinline{pure} and \lstinline{bind} on \li{list} are defined as follows:
\begin{lstlisting}
    pure x = [x]

    bind []        f = []
    bind (x :: xs) f = f x ++ bind xs f
\end{lstlisting}

What are the values returned by the following two calls to \lstinline{list.length}?
\begin{itemize}
  \item \lstinline{list.length (list.pairwise [(λx, x + 1), (λx, x - 1)] [10])}
  \item \lstinline{list.length (ap [(λx, x + 1), (λx, x - 1)] [10])}
\end{itemize}

\begin{answer}
\li|list.pairwise [(λx, x + 1) (λx, x - 1)] [10] = [10 + 1] = [11]|
has length 1.

\li|ap [(λx, x + 1) (λx, x - 1)] [10] = [(λx, x + 1) (λx, x - 1)] >>= λf, [10] >>= λx, [f x] = ([10] >>= λx, [x + 1]) ++ ([10] >>= λx, [x - 1]) = [11] ++ [9] = [11, 9]|
has length 2.
\end{answer}

\subquestion{d}%
Does applying \lstinline{ap} to two lists always give the same result as
\lstinline{list.pairwise} on those lists? Briefly explain your answer.

\begin{answer}
No. For exaple, the lengths are different in the previous subquestion.
\end{answer}

\newpage

\question{6}{Mathematics in Lean}{5+5+2}

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

\begin{answer}
\li|Type| \\
\li|ℕ| \\
\li|Type| \\
\li|Type 1| \\
\li|Type|
\end{answer}

\subquestion{b}%
The type class \lstinline{monoid} of monoids 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}

The type of Booleans can be viewed as a monoid, with \lstinline{tt : bool} as
\lstinline{one} and the ``and'' operator \lstinline{&&} as \lstinline{mul}.
Complete the following instantiation of \lstinline{bool} as a monoid by
providing a suitable definition of
the five fields of the monoid. For each of the three properties, state the
property to prove and very briefly explain why it holds.
\begin{lstlisting}
    instance bool.monoid : monoid bool :=
    { ... }
\end{lstlisting}

\begin{answer}
\begin{lstlisting}
    { mul := (&&),
      one := tt,
      mul_assoc :=
        We must show ∀a b c : bool, (a && b) && c = a && (b && c),
        i.e, associativity of conjunction, obvious (by truth table of &&)
      mul_one :=
        We must show ∀a : bool, a && tt = a, obvious (by truth table of &&)
      one_mul :=
        We must show ∀ a : bool, tt && a = a, obvious (by truth table of &&) }
\end{lstlisting}
\end{answer}

\subquestion{c}%
The \li{mathlib} linters reject the following proof. Briefly point out at least one improvement you would make.
\begin{lstlisting}
    lemma mul_left_comm {α : Type} [field α]
      (x y z : α) (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) :
      x * (y * z) = y * (x * z) :=
    have hxy : x * y ≠ 0,
      from mul_ne_zero hx hy,
    calc  x * (y * z)
        = (x * y) * z : by rw mul_assoc
    ... = (y * x) * z : by rw mul_comm x y
    ... = y * (x * z) : by rw mul_assoc
\end{lstlisting}

\begin{answer}
Possible answers:
\begin{itemize}
\item \li{field α} can become \li{comm_monoid} or \li{comm_semigroup}
\item the \li{have hxy} is unnecessary
\item the hypothesis \li{hx}, \li{hy}, and \li{hz} can be deleted
\end{itemize}
\end{answer}

\vfill

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

\end{document}
