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

Final Exam \\
Tuesday 21 December 2021, 08:30--11:15, RAI blok 09 \\
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}{Connectives and quantifiers}{6+9}

The following two subquestions are about basic mastery of logic. Please provide
highly detailed proofs.

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

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

\begin{answer}
Assume \li|∀x, p x| and \li|∀x, q x|. Fix \li|a|. To prove \li|p a ∨ q a|, by
the left introduction rule of \li|∨|, it suffices to prove \li|p a|. This
corresponds to \li|∀x, p x| instantiated with \li|a|.
\end{answer}

\subquestion{b}%
Prove the following one-point rule for existential quantification. 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}
By \li|↔|-introduction, it suffices to show \\
(1) \li|(∃x : α, x = t ∧ p x) → p t| and \\
(2) \li|p t → (∃x : α, x = t ∧ p x)|.

Let's start with (2). Assume \li|p t|. With the \li|∃|-introduction rule, instantiate
\li|x| with \li|t|, and then we must prove \li|t = t ∧ p t|. By \li|∧|-introduction, it
suffices to prove \li|t = t| and \li|p t|. The first formula is an instance of
reflexivity of \li|=| and the second formula corresponds to an assumption.

For (1), we assume \li|∃x : α, x = t ∧ p x| and show \li|p t|. From the
assumption, by \li|∃|-elimination there exists a witness \li|y| such that
\li|y = t| and \li|p y|. Using \li|y = t|, we rewrite \li|p y| into \li|p t|, as desired.
\end{answer}

\newpage
\question{2}{Lambda-terms}{5+5+7}

Consider the following inductive type representing untyped \li|λ|-terms:

\begin{lstlisting}
    inductive lam : Type
    | var : string → lam
    | abs : string → lam → lam
    | app : lam → lam → lam
\end{lstlisting}

where

\begin{itemize}
\item \li|lam.var x| represents the variable \li|x|;
\item \li|lam.abs x t| represents the \li|λ|-abstraction \li|λx, t|;
\item \li|lam.app t t'| represents the application \li|t t'|.
\end{itemize}

\subquestion{a}%
Implement the Lean function

\begin{lstlisting}
    def vars : lam → set string
\end{lstlisting}

that returns the set of all variables that occur freely or bound within a
\li|λ|-term. For example:

\begin{lstlisting}
    vars (lam.var x) = {x}
    vars (lam.abs x (lam.var y)) = {x, y}
\end{lstlisting}

You may assume that the type constructor \li|set| supports the familiar set
operations.

\begin{answer}
\begin{lstlisting}
    | (lam.var x)    := {x}
    | (lam.abs x t)  := {x} ∪ vars t
    | (lam.app t t') := vars t ∪ vars t'
\end{lstlisting}
\end{answer}

\subquestion{b}%
Implement the Lean function

\begin{lstlisting}
    def free_vars : lam → set string
\end{lstlisting}

that returns the set of all \emph{free} variables within a \li|λ|-term. A
variable is free if it occurs outside the scope of any binder ranging over it.
For example:

\begin{lstlisting}
    free_vars (lam.var x) = {x}
    free_vars (lam.abs x (lam.var y)) = {y}
    free_vars (lam.abs x (lam.app (lam.var x) (lam.var y))) = {y}
\end{lstlisting}

\begin{answer}
\begin{lstlisting}
    | (lam.var x)    := {x}
    | (lam.abs x t)  := free_vars t \ {x}
    | (lam.app t t') := free_vars t ∪ free_vars t'
\end{lstlisting}
\end{answer}

\subquestion{c}%
Prove that \li|free_vars| is a subset of \li|vars|. Note that \li|A ⊆ B| is
defined as \li|∀a, a ∈ A → a ∈ B|.

\begin{lstlisting}
    lemma free_vars_subset_vars (t : lam) :
      free_vars t ⊆ vars t
\end{lstlisting}

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

Case \li{var}:
The goal is \li{free_vars (lam.var x) ⊆ vars (lam.var x)}.
By definition, both sides simplify to \li|{x}|. Clearly,
\li|{x} ⊆ {x}|.

Case \li{abs}: The goal is
\li|free_vars (lam.abs x t) ⊆ vars (lam.abs x t)|.
The induction hypothesis is
\li|free_vars t ⊆ vars t|.
Simplifying the goal using the definitions above, we get
\li|free_vars t \ {x} ⊆ {x} ∪ vars t|. Clearly, by basic properties of set
operations, a sufficient condition for this to hold is if
\li|free_vars t ⊆ vars t|, and this is the induction hypothesis.

Case \li{app}: The goal is
\li|free_vars (lam.app t t') ⊆ vars (lam.app t t')|.
The induction hypotheses are
\li|free_vars t ⊆ vars t| and \li|free_vars t' ⊆ vars t'|.
Simplifying the goal using the definitions above, we get
\li|free_vars t ∪ free_vars t' ⊆ vars t ∪ vars t'|.
Clearly, by basic properties of set operations, this follows from the induction
hypotheses.
\end{answer}

\newpage
\question{3}{A loopy language}{8+8}

Consider the LOOPY programming language, which comprises three kinds of
statements:

\begin{itemize}
\item \li|output s| prints the string \li|s|;
\item \li|choice S T| nondeterministically executes either \li|S| or \li|T|;
\item \li|repeat S| executes \li|S| a nondeterministic number of times,
  printing the concatenation (\li|++|) of zero or more strings.
\end{itemize}

In Lean, we can model the language's abstract syntax as follows:

\begin{lstlisting}
    inductive stmt : Type
    | output : string → stmt
    | choice : stmt → stmt → stmt
    | repeat : stmt → stmt
\end{lstlisting}

\subquestion{a}%
The big-step semantics for the LOOPY language relates programs \li|S : stmt|
to possible outputs \li|s : string|.

Complete the following specification of a big-step semantics for the language by
giving the missing derivation rules for \li|choice| and \li|repeat|.

\vskip\abovedisplayskip

\noindent\hfill
\AXC{\phantom{.}}
\RL{\textsc{Output}}
\UIC{\strut\li|output s ⟹ s|}
\DP
\hfill\hbox{}

\vskip\belowdisplayskip

\begin{answer}
\begin{lstlisting}
    S ⟹ s
    ---------------- ChoiceLeft
    choice S T ⟹ s

    T ⟹ s
    ---------------- ChoiceRight
    choice S T ⟹ s

    --------------- RepeatBase
    repeat S ⟹ ""

    S ⟹ s    repeat S ⟹ t
    ------------------------- RepeatStep
    repeat S ⟹ s ++ t
\end{lstlisting}
\end{answer}

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

\begin{lstlisting}
    inductive big_step : stmt → string → Prop
    | output {s} : big_step (stmt.output s) s
\end{lstlisting}

\begin{answer}
\begin{lstlisting}
    | choice_left {S T s} : big_step S s → big_step (stmt.choice S T) s
    | choice_right {S T s} : big_step T s → big_step (stmt.choice S T) s
    | repeat_base {S} : big_step (stmt.repeat S) ""
    | repeat_step {S s s'} :
      big_step S s → big_step (stmt.repeat S) s' →
      big_step (stmt.repeat S) (s ++ s')
\end{lstlisting}
\end{answer}

\newpage
\question{4}{The list monad}{6+9}

The list monad is a monad that stores a list of values of type \li|α|. It
corresponds to the Lean type constructor \li|list|.

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

\begin{lstlisting}
    def list.pure {α : Type} : α → list α

    def list.bind {α β : Type} : list α → (α → list β) → list β
\end{lstlisting}

\li|pure| should create a singleton list. \li|bind| should apply its second
argument to all the elements of the first argument and concatenate the resulting
lists. Examples:

\begin{lstlisting}
    list.pure 7 = [7]
    list.bind [1, 2, 3] (λx, [x, 10 * x]) = [1, 10, 2, 20, 3, 30]
\end{lstlisting}

You may assume the following operator and functions are available, among others:

\begin{itemize}
\item \li|++| concatenates two lists;
\item \li|list.map| applies its first argument elementwise to its second argument;
\item \li|list.flatten| transforms a list of list into a flattened list formed
  by concatenating all the lists together.
\end{itemize}

\begin{answer}
\begin{lstlisting}
    λa, [a]

    λas f, list.flatten (list.map f as)
\end{lstlisting}
\end{answer}

\subquestion{b}%
Assume \li|ma >>= f| is syntactic sugar for \li|list.bind ma f|. Prove the first
two monad laws:

\begin{lstlisting}
    lemma list.pure_bind {α β : Type} (a : α) (f : α → list β) :
      (list.pure a >>= f) = f a

    lemma list.bind_pure {α : Type} (ma : list α) :
      (ma >>= list.pure) = ma
\end{lstlisting}

Your proofs should be step by step, with at most one rewrite rule or definition
expansion per step, so that we can clearly see what happens.

You may assume reasonable lemmas about \li|list.map| and \li|list.flatten|.
Please state them.

\begin{answer}
For the first property: \\
\li{(list.pure a >>= f)} \\
\li{= ([a] >>= f)} by definition of \li{list.pure} \\
\li{= list.flatten (list.map f [a])} by definition of \li{list.bind} \\
\li{= list.flatten [f a]} by property of \li{list.map} \\
\li{= f a} by property of \li{list.flatten}

For the second property:
\li{(ma >>= list.pure)} \\
\li{= list.flatten (list.map list.pure ma)} by definition of \li{list.bind} \\
\li{= list.flatten (list.map (λa, [a]) ma)} by definition of \li{list.pure} \\
\li{= list.flatten (list.map (λa, [a]) ma)} by definition of \li{list.pure} \\
\li{= ma} by property \li{list.flatten (list.map (λa, [a]) as) = as}, provable by induction
\end{answer}

\newpage
\question{5}{The loopy language revisited}{4+4+6}

\subquestion{a}%
Implement the following \li|repeat| function in Lean. It takes a number \li|n|
and a string \li|s| and returns the string obtained by concatenating \li|n|
copies of \li|s|.

\begin{lstlisting}
    def repeat : ℕ → string → string
\end{lstlisting}

\begin{answer}
\begin{lstlisting}
    | 0       _ := ""
    | (n + 1) s := s ++ repeat n s
\end{lstlisting}
\end{answer}

\subquestion{b}%
In mathematics, the Kleene star operator takes a string set \li|A| and returns
the set of all the strings that are obtained by concatenating strings from
\li|A| zero or more times. A natural way to model this in Lean is using an
inductive predicate. Complete the following definition with the necessary
introduction rules so that \li|kleene_star A s| is true if and only if string
\li|s| is in the Kleene star of set \li|A|:

\begin{lstlisting}
    inductive kleene_star (A : set string) : string → Prop
\end{lstlisting}

\begin{answer}
\begin{lstlisting}
    | empty : kleene_star ""
    | step {s t} : s ∈ A → kleene_star t → kleene_star (s ++ t)
\end{lstlisting}
\end{answer}

\subquestion{c}%
Use the Kleene star to complete the following definition of the denotational
semantics of the LOOPY language from question~3. The denotation of a LOOPY
program should be the set of all strings it can output.

\begin{lstlisting}
    def denote : stmt → set string
    | (stmt.output s) := {s}
\end{lstlisting}

Recall that the Lean syntax for set comprehensions is \li${x | φ x}$, where
\li|φ x| denotes some condition on~\li|x|.

\begin{answer}
\begin{lstlisting}
    | (stmt.choice S T) := denote S ∪ denote T
    | (stmt.repeat S)   := {s | kleene_star (denote S) s}
\end{lstlisting}
\end{answer}

\newpage
\question{6}{Types and type classes}{4+5+4}

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

\begin{lstlisting}
    [1, 2, (3 : ℤ)]    list ℕ    list    Sort 1
\end{lstlisting}

\begin{answer}
\li{list ℤ} \\
\li{Type} \\
\li{Type → Type} (or \li{Type u → Type u}) \\
\li{Sort 2}
\end{answer}

\subquestion{b}
The type class \li|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}

A list can be viewed as a monoid, with the empty list \li|[]| as \li|one| and
list concatenation \li|++| as \li|mul|. Complete the following instantiation of
\li|list α| 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 string.monoid {α : Type} : monoid (list α) :=
    {  ⋯  }
\end{lstlisting}

\begin{answer}
\begin{lstlisting}
    { mul := (++),
      one := [],
      mul_assoc :=
        the property is (a ++ b) ++ c = a ++ (b ++ c),
        i.e. associativity of append on lists, which holds
        (it can be proved by induction),
      mul_one :=
        the property is [] ++ a = a, which clearly holds
        (it is the first case of the definition of ++),
      one_mul :=
        the property is a ++ [] = a, which clearly holds
        (it can be proved by induction) }
\end{lstlisting}
\end{answer}

\subquestion{c}%
The type class \li|group| of groups 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|list α| be instantiated as a group, using the same definition
for \li|mul| and \li|one| as in question 6b? Briefly explain your answer.

\begin{answer}
No, this cannot be done, because there is no inverse \li{xs} for \li{[a]} such
that \li{[a] ++ xs = []}.
\end{answer}

\vfill

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

\end{document}
