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

Resit Exam \\
14 February 2023, 18:45--21:30, NU-3B19 \\
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}{Connectives and quantifiers}{6+6}

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 existential
quantification and conjunction. Make sure to emphasize and clearly label every
step corresponding to the introduction or elimination of a connective or
quantifier.

\begin{lstlisting}
    lemma about_exists_and_and {α : Type} (p q : α → Prop) :
      (∃x, p x ∧ q x) → (∃x, p x)
\end{lstlisting}

\begin{answer}
Assume \li{hex : ∃x, p x ∧ q x}. \\
By \li{∃}-elimination, we obtain a witness \li{x}
such that \li{hand : p x ∧ q x}. \\
From \li{hand}, we obtain \li{hpx : p x} by \li{∧}-left-elimination. \\
From \li{hpx}, we obtain \li{∃x, p x} by \li{∃}-introduction with the witness
\li{x}, as desired. QED
\end{answer}

\subquestion{b}%
Let |p| be a unary predicate over |ℕ|. The set of propositions

\begin{lstlisting}
    {(∀x, p x), (∃y, ¬ p y)}
\end{lstlisting}
%
is inconsistent. Show this by proving the following implication. In your proof,
identify clearly which values are supplied for the universal quantifier.

\begin{lstlisting}
    lemma inconsistent_predicate {p : ℕ → Prop} :
      (∀x, p x) → (∃y, ¬ p y) → false
\end{lstlisting}

\begin{answer}
Assume \li{hall : ∀x, p x}. \\
Assume \li{hexn : ∃y, ¬ p y}. \\
Performing \li{∃}-elimination on \li{hexn} yields a witness \li{y}
such that \li{hnpy : ¬ p y}. \\
From \li{hall}, we obtain \li{hpy : p y} by \li{∀}-elimination (by instantiation
of \li{x} with \li{y}). \\
From \li{hnpy} and \li{hpy}, we derive \li{false}, as desired. QED
\end{answer}

\newpage
\question{2}{Terms of the \li|λ|-calculus}{6+6+8}

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

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

where

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

\subquestion{a}%
Implement the Lean function

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

that returns the set of all variables that occur freely or bound within a
term. For example:

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

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

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

\subquestion{b}%
Implement the Lean function

\begin{lstlisting}
    def bound_vars : term → set string
\end{lstlisting}

that returns the set of all \emph{bound} variables within a term. A
variable is bound if it is bound by a \li|λ|-abstraction. For example:

\begin{lstlisting}
    bound_vars (term.var x) = {}
    bound_vars (term.abs x (term.var y)) = {x}
    bound_vars (term.abs y (term.app (term.var x) (term.var y))) = {y}
\end{lstlisting}

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

\subquestion{c}%
Prove that \li|vars| is never empty:

\begin{lstlisting}
    lemma vars_nonempty (t : term) :
      vars t ≠ ∅
\end{lstlisting}

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

Case \li{t = term.var x}. \\
The goal is \li{vars (term.var x) ≠ ∅}.

By definition of \li{vars}, the left-hand side of the goal is
\li|vars (term.var x) = {x}|, which is clearly not empty.

Case \li{t = term.abs x t}. \\
The goal is \li{vars (term.abs x t) ≠ ∅}. \\
The induction hypothesis is \li{vars t ≠ ∅}.

By definition of \li{vars}, the left-hand side of the goal is
\li|vars (term.abs x t) = {x} ∪ vars t|, which is clearly not empty.

Case \li{t = term.app t t'}. \\
The goal is \li{vars (term.app t t') ≠ ∅}. \\
The induction hypotheses are \li{vars t ≠ ∅} and \li{vars t' ≠ ∅}.

By definition of \li{vars}, the left-hand side of the goal is
\li|vars (term.app t t') = vars t ∪ vars t'|. By the first induction hypothesis,
\li{vars t} is nonempty; hence \li{vars t ∪ vars t'} is nonempty. QED
\end{answer}

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

Consider the STRINGY programming language, which comprises five kinds of
statements:

\begin{itemize}
\item \li|skip| does nothing;
\item \li|print s| outputs the string \li|s|;
\item \li|seq S T| executes |S| then |T|;
\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
    | skip   : stmt
    | print  : string → stmt
    | seq    : stmt → stmt → stmt
    | choice : stmt → stmt → stmt
    | repeat : stmt → stmt
\end{lstlisting}

\subquestion{a}%
The small-step semantics for the STRINGY language relates
an initial configuration |(S : stmt,| |s : string)| to a possible next configuration
|(S' : stmt, s' : string)|. Notice that strings capture the program's state,
in much the same way as |state| in the WHILE language.

Complete the following specification of a small-step semantics for the language
by giving the missing derivation rules for the |choice| and |repeat| statements.
Notice that |print| appends the new output to any earlier output (using |++|).

\vskip\abovedisplayskip

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

\smallskip

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

\vskip\belowdisplayskip

\begin{answer}
\noindent\hfill
\AXC{\phantom{.}}
\RL{\textsc{Choice-Left}}
\UIC{\strut\li|(choice S T, s) ⇒ (S, s)|}
\DP
\hfill\hbox{}

\smallskip

\noindent\hfill
\AXC{\phantom{.}}
\RL{\textsc{Choice-Right}}
\UIC{\strut\li|(choice S T, s) ⇒ (T, s)|}
\DP
\hfill\hbox{}

\smallskip

\noindent\hfill
\AXC{\phantom{.}}
\RL{\textsc{Repeat-Base}}
\UIC{\strut\li|(repeat S, s) ⇒ (skip, s)|}
\DP
\hfill\hbox{}

\smallskip

\noindent\hfill
\AXC{\phantom{.}}
\RL{\textsc{Repeat-Step}}
\UIC{\strut\li|(repeat S, s) ⇒ (seq S (repeat S), s)|}
\DP
\hfill\hbox{}
\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 : (stmt × string) → (stmt × string) → Prop
    | print {s s'} :
      small_step (stmt.print s', s) (stmt.skip, s ++ s')
    | seq_step {s s' S S' T} :
      small_step (S, s) (S', s') →
      small_step (stmt.seq S T, s) (stmt.seq S' T, s')
    | seq_skip {s T} :
      small_step (stmt.seq stmt.skip T, s) (T, s)
    ...
\end{lstlisting}

\begin{answer}
\begin{lstlisting}
| choice_left {s S T} :
  small_step (stmt.choice S T, s) (S, s)
| choice_right {s S T} :
  small_step (stmt.choice S T, s) (T, s)
| repeat_base {s S} :
  small_step (stmt.repeat S, s) (stmt.skip, s)
| repeat_step {s S} :
  small_step (stmt.repeat S, s) (stmt.seq S (stmt.repeat S), s)
\end{lstlisting}
\end{answer}

\newpage
\question{4}{A monad for sticky errors}{9+6}

Error handling can clutter programs. ``Sticky errors'' are an idiom that can be
used to reduce clutter. With sticky errors, a global error flag is initialized
to false and is changed to true as soon as an error has occurred. From then
on, it remains true, even if some operations succeed---errors are ``sticky.''
At the end of the program, we can check the flag to see if an error has
occurred. Using this idiom, we can concentrate the error handling at the end of
the program and write the rest of the program optimistically, without worrying
about errors. Schematically:

\begin{lstlisting}
    do_something();
    do_something_else();
    if (error_flag)
      print "There was an error";
\end{lstlisting}

In Lean, we model the state of such a program as a pair |(α, bool)|, where
|α| is the result of the program and |bool| indicates whether an error has
occurred so far. To increase readability, we introduce aliases for pair
constructs:

\begin{lstlisting}
    def sticky (α : Type) : Type := (α × bool)
    def sticky.value {α : Type} : sticky α → α := prod.fst
    def sticky.is_error {α : Type} : sticky α → bool := prod.snd
\end{lstlisting}

To make it convenient to write programs with sticky errors, we implement the
monad operators |pure| and |bind| as follows:

\begin{lstlisting}
    def sticky.pure {α : Type} : α → sticky α :=
    λa, (a, ff)

    def sticky.bind {α β : Type} : sticky α → (α → sticky β) → sticky β :=
    λma f,
      let mb := f (sticky.value ma) in
        (sticky.value mb,
         sticky.is_error ma || sticky.is_error mb)
\end{lstlisting}

For example, the command
\li|#reduce sticky.bind (3, tt) (λn, (7 * n, ff))|
prints the |sticky| value \hbox{|(21, tt)|.}

Recall that |tt| and |ff| are the truth values of type |bool|, and
\li$||$ denotes ``or.''

\subquestion{a}%
Assume |ma >>= f| is syntactic sugar for
|sticky.bind ma f|. Prove the first monad law, shown below. 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 pairs and Booleans. In particular, you
may use the lemma stating that \li{(prod.fst p, prod.snd p) = p} for every pair
\li{p}.

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

\begin{answer}

\phantom{\li{=} }\li{sticky.pure a >>= f} \\
\li{= (a, ff) >>= f}\qquad (by definition of \li{sticky.pure}) \\
\li{= let mb := f a in (sticky.value mb, ff || sticky.is_error mb)} \\
\noindent\hbox{}\qquad
  (by definition of \li{sticky.bind}) \\
\li{= (sticky.value (f a), ff || sticky.is_error (f a))}\qquad
  (by inlining of \li{let}) \\
\li{= (sticky.value (f a), sticky.is_error (f a))}\qquad
  (by basic property of Booleans) \\
\li{= (prod.fst (f a), prod.snd (f a))}\qquad
  (by definition of \li{sticky.value} and \li{sticky.is_error}) \\
\li{= f a}\qquad
  (by lemma \li{(prod.fst p, prod.snd p) = p})
\end{answer}

\subquestion{b}%
Commutative monads are monads for which we can reorder actions
that do not depend on each other. For sticky errors, the property can be stated
as follows:

\begin{lstlisting}
    lemma sticky.bind_comm {α β γ δ : Type} (ma : sticky α) (f : α → sticky β)
        (g : α → sticky γ) (h : α → β → γ → sticky δ) :
      (ma >>= λa, f a >>= λb, g a >>= λc, h a b c) =
      (ma >>= λa, g a >>= λc, f a >>= λb, h a b c)
\end{lstlisting}

Is |sticky| a commutative monad? If yes, provide a justification (as text or
in the form of a brief proof sketch). If no, provide a counterexample (i.e.,
concrete values for |ma|, |f|, |g|, and |h| above and the result of evaluating
both sides of the equality).

\begin{answer}
Yes, |sticky| is a commutative monad. The ``value'' components of the two
computations are the same if we execute \li{f} or \li{g} first. It is only the
``error'' components that are a source of worry, but for both computations, the
error flag is set at the end if and only if one of \li{f}, \li{g}, or \li{h} has
set it, regardless of the order in which \li{f} and \li{g} are executed.
\end{answer}

\newpage
\question{5}{The stringy language revisited}{6+6}

Recall the STRINGY language from Question 3. Based on the small-step semantics
we specified in Question 3, we can define a big-step semantics (and the usual
syntactic sugar) as follows:

\begin{lstlisting}
    infixr ` ⇒ ` := small_step                -- introduces the ⇒ syntax
    infixr ` ⇒* ` : 100 := star small_step    -- introduces the ⇒* syntax

    def big_step : stmt × string → string → Prop :=
    λSs t, Ss ⇒* (stmt.skip, t)

    infixr ` ⟹ ` : 110 := big_step           -- introduces the ⟹ syntax
\end{lstlisting}

Based on the big-step semantics, we can in turn define a Hoare logic (and the
usual syntactic sugar):

\begin{lstlisting}
    def partial_hoare (P : string → Prop) (S : stmt)
      (Q : string → Prop) : Prop :=
    ∀s t, P s → (S, s) ⟹ t → Q t

    -- introduces the {* P *} S {* Q *} syntax
    notation `{* ` P : 1 ` *} ` S : 1 ` {* ` Q : 1 ` *}` := partial_hoare P S Q
\end{lstlisting}

Notice that |string| takes the place of |state|: Our notion of state consists of
a single string, which grows with each |print| statement.

\subquestion{a}%
Extend the following specification of the Hoare logic rules for
STRINGY by giving the Hoare rules for the |skip| and |seq| statements.
(We will return to the |print| statement in Subquestion 5b.)

\vskip\abovedisplayskip

\noindent\hfill
\AXC{\strut\texttt{\{P\} S \{Q\}}}
  \AXC{\strut\texttt{\{P\} T \{Q\}}}
\RL{\textsc{Choice}}
\BIC{\strut\texttt{\{P\} choice S T \{Q\}}}
\DP
\qquad
\AXC{\strut\texttt{\{I\} S \{I\}}}
\RL{\textsc{Repeat}}
\UIC{\strut\texttt{\{I\} repeat S \{I\}}}
\DP
\hfill\hbox{}

\vskip\belowdisplayskip

\begin{answer}
\noindent\hfill
\AXC{\strut}
\RL{\textsc{Skip}}
\UIC{\strut\texttt{\{Q\} skip \{Q\}}}
\DP
\qquad
\AXC{\strut\texttt{\{P\} S \{Q\}}}
  \AXC{\strut\texttt{\{Q\} T \{R\}}}
\RL{\textsc{Seq}}
\BIC{\strut\texttt{\{P\} S; T \{R\}}}
\DP
\hfill\hbox{}
\end{answer}

\subquestion{b}%
Which of the following Hoare rule, if any, is correct for the |print|
statement? Justify your answer.

\vskip\abovedisplayskip

\noindent\hfill
\AXC{\phantom{.}}
\RL{\textsc{Print-1}}
\UIC{\strut\texttt{\{Q\} print s' \{Q\}}}
\DP
\hfill\hbox{}

\smallskip

\noindent\hfill
\AXC{\phantom{.}}
\RL{\textsc{Print-2}}
\UIC{\strut\texttt{\{Q\} print s' \{$\lambda$s, Q (s ++ s')\}}}
\DP
\hfill\hbox{}

\smallskip

\noindent\hfill
\AXC{\phantom{.}}
\RL{\textsc{Print-3}}
\UIC{\strut\texttt{\{$\lambda$s, Q (s ++ s')\} print s' \{Q\}}}
\DP
\hfill\hbox{}

\vskip\belowdisplayskip

(Note that we mix Lean and informal notations above.)

\begin{answer}
Rule \textsc{Print-3} is correct. If we start in a state \li{s} that satisfies
\li{Q (s ++ s')} and we extend \li{s} with \li{s'}, we end up in a state \li{s}
such that \li{Q s}. This is analogous to the assignment rule of the WHILE
language, with the assignment \li{s := s ++ s'}.
\end{answer}

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

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

\begin{lstlisting}
    (3 : ℕ)    ℕ    ℕ → ℕ    list    Type 3
\end{lstlisting}

\begin{answer}
\begin{lstlisting}
ℕ
Type
Type
Type → Type (or Type u → Type u)
Type 4
\end{lstlisting}
\end{answer}

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

Natural numbers can be viewed as a monoid, with |0| as |one| and addition |+| as
|mul|. (The names |one| and |mul| are admittedly confusing in this setting.)
Complete the following instantiation of |ℕ| 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] def nat.monoid : monoid nat :=
    {  ⋯  }
\end{lstlisting}

\begin{answer}
\begin{lstlisting}
mul       := (+),
one       := 0,
mul_assoc := ∀a b c : α, (a + b) + c = a + (b + c),
  -- by associativity of + on natural numbers
one_mul   := ∀a : α, 0 + a = a,
  -- because 0 is neutral element for + on natural numbers
mul_one   := ∀a : α, a + 0 = a
  -- because 0 is neutral element for + on natural numbers
\end{lstlisting}
\end{answer}

\subquestion{c}%
The type class \li|group| of groups is defined as follows in Lean:

\begin{lstlisting}
    @[class] structure 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 |nat| be instantiated as a group, using the same definition for
|mul| and |one| as in Subquestion 6b? Briefly explain your answer.

\begin{answer}
No, because natural numbers other than |0| admit no inverse. For example, there
is no natural number \li{inv 7} such that \li{(inv 7) + 7 = 0}.
\end{answer}

\vfill

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

\end{document}
