%%% TODO: Temporary
%\def\inclloesung{}

\documentclass[11pt]{article}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%
%%% Hinweise zur Verwendung:
%%%
%%%  1. Datei kompilieren und das PDF durchlesen. Die enthaltenen Aufgaben erklären die Verwendung.
%%%
%%%  2. Wenn es nicht kompiliert: TeX-Live-Pakete nachinstallieren,
%%%     alle benötigten Pakete sind in TeX-Live enthalten, aber nicht alle werden
%%%     von jeder Distribution standardmässig installiert, z.b. "totcount" und "multido"
%%%
%%%  3. Nicht vergessen alle Zeilen mit "%TODO" Marker zu bearbeiten.
%%%
%%%  4. Alle Aufgaben mit "aufgaben" environment erstellen, dieses hat 2 Argumente: Name und Punktzahl.
%%%
%%%  5. Erste Beispielaufgabe findet sich ab Zeile 411
%%%
%%%  6. Bewertungskasten auf der ersten Seite wird automatisch erstellt,
%%%     dies benötigt aber 2-malige Anwendung von pdflatex.
%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%% ANZEIGE DER LÖSUNG IM PDF EIN/AUSSCHALTEN %%%
\newif\ifSol
%%%TODO DISABLE
\ifdefined\inclloesung
  \Soltrue
\else
 \Solfalse
\fi
%
% Lösungstexte werden mit den Environments "loesung" oder "loes" und den Befehlen \Loesung{} und \Loes{} erstellt, siehe Beispiele

%%% ANZEIGE DER KOMMENTARE/BEWERTUNG IM PDF EIN/AUSSCHALTEN %%%
\newif\ifComment
%%%TODO DISABLE
\Commenttrue
% \Commentfalse
%
% Kommentare werden mit dem Befehl "\KOMMENTAR{}" erstellt, siehe Beispiele
% Bewertungskriterien mit dem Environment "bewertung" erstellen

\newcommand{\AUTO}[1]{#1}
\newcommand{\MANUAL}[1]{}
\newcommand{\autoormanual}[2]{\AUTO{#1}\MANUAL{#2}}

\newcounter{lang}
\newcommand{\newL}[1]{\refstepcounter{lang}L_{\thelang}{#1}}
\newcommand{\refL}[1]{L_{\ref*{#1}}}

\newcounter{automat}
\newcommand{\newA}[1]{\refstepcounter{automat}A_{\theautomat}\label{#1}}
\newcommand{\refA}[1]{A_{\ref*{#1}}}

\newcounter{grammar}
\newcommand{\newG}[1]{\refstepcounter{grammar}G_{\thegrammar}\label{#1}}
\newcommand{\refG}[1]{G_{\ref*{#1}}}

\newcommand{\courseshorthand}{ITP}
\newcommand{\coursetitle}{Interactive Theorem Proving}

\usepackage{a4wide}
\usepackage{fancyhdr}
\usepackage[utf8]{inputenc}
\usepackage{amssymb,stmaryrd}
\usepackage{color}
% \usepackage{bcprules}
\usepackage{amsmath}
\usepackage{boxedminipage}
\usepackage{multicol}
\usepackage{calc}
\usepackage{ifthen}
\usepackage{verbatim}
\usepackage{fancyvrb}
\usepackage{listings}
\usepackage{framed}
\usepackage{graphicx}
\usepackage{prftree}
% \usepackage{dashrule}
\usepackage{totcount}
\usepackage{multido}
\usepackage{bussproofs}
\usepackage{wasysym}

\EnableBpAbbreviations
\def\ScoreOverhang{2pt}
\def\proofSkipAmount{\vskip 0pt}
\def\defaultHypSeparation{\hskip1em}

\usepackage{tikz}
\usetikzlibrary{calc,shapes,arrows.meta,arrows,decorations.markings}
\usetikzlibrary{automata}     % Import library for drawing atomata
\usetikzlibrary{positioning}  %
%%% COMMON MATH MAKROS

\usetikzlibrary{arrows}
\providecommand{\field}[1]{\mathbb{#1}}
\providecommand{\NN}{\field{N}}
\providecommand{\QQ}{\field{Q}}
\providecommand{\RR}{\field{R}}
\providecommand{\ZZ}{\field{Z}}

\newcommand{\holds}{\ensuremath{\,.\,}} % \forall x \holds z

\providecommand{\Nat}{\field{N}}

%\tikzset{/pgf/arrow keys/length=5mm}
%\tikzset{every picture/.style=semithick}
%\tikzset{/tikz/arrows = {Latex[length=3mm]}}
% XXX Aendert die Pfeilkoepfe global
\tikzset{>=Stealth}
%\tikzset{myptr/.style={decoration={markings,mark=at position 1 with %
%    {\arrow[scale=3,>=stealth]{>}}},postaction={decorate}}}
%\tikzset{>=Kite, arrowhead=5mm}
%\tikzset{every picture/.style{\arrow[scale=3,>=stealth]{>}}}
%\pgfdeclarearrow{
%
%}
%\tikzset{myptr/.style={decoration={markings,mark=at position 1 with %
%    {\arrow[scale=3,>=stealth]{>}}},postaction={decorate}}}
%\tikzset{arrows={->[scale=4,blue]}}

% XXX fuegt neue Pfeilkoepfe hinzu. Bei nicht-loop-Dingensen wird der
% alte Pfeilkopf entfernt. Bei loop-dingensen nicht, das ginge mit
% dem Code darunter. ABER: Nicht bei allen loop-Dingern wuerde ein
% neuer Pfeilkopf gezeichnet. Das sieht auch doof aus.
\tikzset{
  meinKopf/.style={
    %decoration={markings,mark=at position 1 with {\arrow[scale=1.5]{>}}},
    decoration={markings,mark=at position 1 with {\arrow[scale=1.5,>=stealth]{>}}},
    postaction={decorate}
    %shorten >=0.4pt
    }
    }

%\tikzset{every loop/.style={meinKopf}}
%\tikzset{every loop/.style={
%    decoration={markings,mark=at position 0.5 with {\arrow[scale=1.5,>=stealth]{>}}},
%    postaction={decorate,draw}
%}}

%%% JAVA Listings:
% \providecommand{\deflistings}[1]{%
%   \lstset{%
%     language=#1,%
%     basicstyle=\small\ttfamily,%
%     keywordstyle=\bfseries,%
%     identifierstyle=,%
%     commentstyle=\itshape,%
%     showstringspaces=false,%
%     extendedchars=true,%
%   }%
% }
% \deflistings{Java}
%
%% Markus, 2011-12-13: Added handling of umlauts
%% Source: http://www.artikcommunity.biz/showthread.php?t=10931382#post47117516
% \lstset{extendedchars=true,literate={ä}{{\"a}}1 {ö}{{\"o}}1 {ü}{{\"u}}1 {Ä}{{\"A}}1 {Ö}{{\"O}}1 {Ü}{{\"U}}1 {ß}{\ss}1}
%% Markus, 2011-12-13: Added handling for long source lines
%% Source: http://www.ureader.de/message/1543599.aspx
%%   Unfortunately \rotatebox seems not to work within ``prebreak''.
%%   So we save the the symbol in box in advance.
%%   However, rotatebox is not allowed in the preamble
%%   (http://newsgroups.derkeiler.com/Archive/Comp/comp.text.tex/2011-01/msg00912.html)
%%   Hence, we execute the code at the begin of the document.
%
% \AtBeginDocument{%
%   \newbox{\lstbreaksym}%
%   \savebox{\lstbreaksym}{\;\raisebox{.9ex}[0ex][0ex]{\rotatebox{180}{\ensuremath{\Rsh}}}}%
%   \lstset{
%     breakautoindent  = true,
%     breakindent      = 2em,
%     breaklines       = true,
%     postbreak        = ,
%     prebreak         = \usebox{\lstbreaksym},
%   }%
% }

\def\lstlanguagefiles{lstleanxbw.sty}
\lstset{language=leanxbw}
%\lstMakeShortInline|

\makeatletter
\renewcommand\lst@visiblespace{\ensuremath{\;}}
\newcommand\li{\lstinline[language=leanxbw,showspaces=true]}

\parindent0em
\parskip1ex plus0.25ex minus0.25ex

\setlength{\voffset}{-1.6cm}
\setlength{\textheight}{25.5cm}
\setlength{\hoffset}{-5mm}
\setlength{\textwidth}{17cm}

\pagestyle{empty}

\fancyhead{}
\fancyhead[LO]{Name:}
\fancyhead[RO,RE]{\thepage}
\fancyfoot{}

\RequirePackage{color}
\RequirePackage{boxedminipage}
\RequirePackage{ifthen}
\definecolor{ErrorRed}{rgb}{1,0.80,0.80}
\definecolor{NoteBlue}{rgb}{0.8,0.80,1.0}
\definecolor{CorrectGreen}{rgb}{0.8,1.0,0.8}
\definecolor{ExampleGrey}{rgb}{0.8,0.8,0.8}

\renewcommand*\ttdefault{txtt}
\definecolor{stephanColor}{rgb}{0.0,0.3,0.0}
\definecolor{sebastianColor}{rgb}{0.4,0.0,0.4}
\newcommand{\dscomment}[1]{%
\colorbox{NoteBlue}{
\begin{minipage}{\textwidth}
\color{blue}\textbf{DS:} #1
\end{minipage}}}
\newcommand{\sbcomment}[1]{%
\colorbox{NoteBlue}{
\begin{minipage}{\textwidth}
\color{stephanColor}\textbf{SB:} #1
\end{minipage}}}
\newcommand{\sscomment}[1]{%
\colorbox{NoteBlue}{
\begin{minipage}{\textwidth}
\color{sebastianColor}\textbf{SS:} #1
\end{minipage}}}

\newcommand{\blank}[1]{\hdashrule{#1}{1pt}{1pt 4pt}}

\newcommand{\breakpage}[1][\vfill]{% Für Seitenumbruch innerhalb einer Aufgabe

  #1

  \hspace*{-4EX}\emph{The question continues on the next page.}
  \vspace*{4EX}

    \newpage

  \hspace*{-4EX}\emph{Continuation of Question~\ref{A\arabic{aufgno}}:}
}

\newcommand{\Loesung}[1]{\colorbox{NoteBlue}{\textbf{PROPOSED SOLUTION:} \protect#1}}
\newcommand{\Loes}[1]{\colorbox{NoteBlue}{\protect#1}}
% \newcommand{\Loesung}[1]{\par\colorbox{NoteBlue}{\begin{minipage}{.94\textwidth}\textbf{L\"OSUNGSVORSCHLAG:} \protect#1\end{minipage}}}
% \newcommand{\Loes}[1]{\par\colorbox{NoteBlue}{\begin{minipage}{.94\textwidth}\protect#1\end{minipage}}}
\newcommand{\fillLoes}[2][6EX]{\hspace*{1.4EX}\makebox[0pt][l]{\rule{#1}{0.15mm}}\makebox[#1][l]{\hspace*{2EX}\Loes{~\hfill\protect#2}}}

\newcommand{\KOMMENTAR}[2][]{\colorbox{ErrorRed}{$\maltese$\begin{Large}\textbf{KOMMENTAR #1:} #2\end{Large}$\maltese$}}

% Andreas, 2011-11-30 colored boxes that split over pages
% no floats, footnotes etc allowed.
% source: http://tex.stackexchange.com/questions/10085/colored-fancy-boxes
\newenvironment{solution}{%
  \def\FrameCommand{\fboxsep=\FrameSep \fcolorbox{NoteBlue}{NoteBlue}}%
  \color{black}\MakeFramed {\FrameRestore}}%
 {\endMakeFramed}

\newenvironment{loesung}{%
    \begin{solution}%
      \textbf{PROPOSED SOLUTION:}
  }{
    \end{solution}
  }

\newenvironment{loes}{%
    \begin{solution}%
  }{
    \end{solution}
  }

\newenvironment{bewertung}{%
  \def\FrameCommand{\fboxsep=\FrameSep \fcolorbox{CorrectGreen}{CorrectGreen}}%
  \color{black}\MakeFramed {\FrameRestore}}%
 {\endMakeFramed}

\newcommand{\platz}[1]{\vspace*{#1}}
\newcommand{\nuraufgabe}[1]{#1}
\newcommand{\nurloesung}[1]{}
\ifSol
  \renewcommand{\platz}[1]{}
  \renewcommand{\nuraufgabe}[1]{}
  \renewcommand{\nurloesung}[1]{#1}
\else
  \renewenvironment{loesung}{\comment}{\endcomment\vfill}
  \renewenvironment{loes}{\comment}{\endcomment\vfill}
  \renewenvironment{bewertung}{\comment}{\endcomment\vfill}
  \renewcommand{\Loesung}[1]{}%
  \renewcommand{\Loes}[1]{}%
\fi

\ifComment
\else
  \renewenvironment{bewertung}{\comment}{\endcomment\vfill}
  \renewcommand{\KOMMENTAR}[2][]{}
\fi

\usepackage{hyperref}

%%% Automatic Numbering written by Steffen Jost (jost@tcs.ifi.lmu.de) 2012

% Pages
\newcounter{emptypages}
\setcounter{emptypages}{2} %TODO: Anzahl Leerseiten am Ende einstellen.
\regtotcounter{page}
\newcounter{adjustedpages}
\newcommand{\updatepages}{\setcounter{adjustedpages}{\totvalue{page}}\addtocounter{adjustedpages}{-\value{emptypages}}}

% Points
\newtotcounter{aufgno}
\newtotcounter{sumpunkte}
\newcounter{halfpoints}
\newcommand{\makepcounter}[1]{\newcounter{volatilepunkte#1}\newtotcounter{punkte#1}}
% \multido{\i=1+1}{20}{\makepcounter{\i}} %%% Does not work unfortunately
\makepcounter{1}
\makepcounter{2}
\makepcounter{3}
\makepcounter{4}
\makepcounter{5}
\makepcounter{6}
\makepcounter{7}
\makepcounter{8}
\makepcounter{9}
\makepcounter{10}
\makepcounter{11}
\makepcounter{12}
\makepcounter{13}
\makepcounter{14}
\makepcounter{15}
\makepcounter{16}
\makepcounter{17}
\makepcounter{18}
\makepcounter{19}
\makepcounter{20}
\makepcounter{21}
\makepcounter{22}
\makepcounter{23}
\newcommand{\setpunkte}[2]{\setcounter{punkte#1}{#2}}
\newcommand{\gettotpunkte}[1]{\total{punkte#1}}
\newcommand{\getpunkte}[1]{\arabic{volatilepunkte#1}} % \gettotpunkte{} cannot be used everywhere, hence we need to copy the values into normal counter after begin document
\newcommand{\copypunkte}[1]{\setcounter{volatilepunkte#1}{\totvalue{punkte#1}}}
\newcommand{\updatepunkte}{%
  \multido{\I=1+1}{\totvalue{aufgno}}{\copypunkte{\I}}%
  \setcounter{halfpoints}{(\totvalue{sumpunkte}+1)/2}%
}

% \newcommand{\option}{\raisebox{-1.5mm}{\Huge $\Box$}\enspace}

%%% Aufgaben
\newenvironment{aufgabe}[2]{
\refstepcounter{aufgno}%
\setpunkte{\arabic{aufgno}}{#2}
\addtocounter{sumpunkte}{#2}%
{\bf \ifSol\colorbox{NoteBlue}{Solution to Question}\else Question\fi~\arabic{aufgno} (#1): \hfill (#2 points)%
\phantomsection\addcontentsline{toc}{chapter}{A\arabic{aufgno} (#2): #1}\label{A\arabic{aufgno}}%
\\[2mm]
}
}{\newpage}

\begin{document}
\updatepunkte
\updatepages

%%% BEGIN

\vspace*{-12mm}
Institute for Informatics of the Ludwig-Maximilians-Universität München
\hspace{\fill}Summer semester 2024\\
Prof.~Dr.~Jasmin Blanchette
\hspace{\fill}{25.07.2024}\\
Xavier Généreux\\
Balazs Toth\\[-1.5em]
\begin{center}
  {\Large \Loes{Solution to the} Final Examination in the Course \\[0.4em] \bf
  Interactive Theorem Proving} \\[0.5em]
\end{center}
\vspace{2mm}

You have
%\textbf{{\total{sumpunkte}}~Minuten}
\textbf{120~minutes}
at your disposal.
Written or electronic aids are not permitted.
Carrying electronic devices, even switched off, will be considered cheating.

Write your full name and matriculation number clearly legible on this cover sheet,
as well as your name in the header on {each sheet}. Hand in all
sheets. Leave them stapled together.
Use only \textbf{pens} and \textbf{neither} the color \textbf{red nor green}.

Check that you have received all the sheets. Guidelines for writing
pen-and-paper proofs are given on \textbf{page~1}. Questions can be found on
\textbf{pages 2--\arabic{adjustedpages}}. You may use the back of the sheets for
secondary calculations. If you use the back of a sheet to answer, clearly mark
what belongs to which question and indicate in the corresponding question where
all parts of your answer can be found. Cross out everything that should not be
graded.

There are \total{aufgno} questions for a total of \total{sumpunkte}~points. The
subquestions can be completed independently of each other.

With your signature, you confirm that you are in sufficiently good health at the
beginning of the examination and that you accept this examination bindingly.

\vfill

\begin{tabular}{@{}ll@{}}
\Large \bf Last name: & \Large \bf
\\[6mm]
\Large \bf First name: & \Large \bf
\\[6mm]
\Large \bf Matriculation number: & \Large \bf
\\[6mm]
\Large \bf Program of study: & \Large \bf
\\[6mm]%
\multicolumn{2}{@{}l@{}}{\Large\bf $\Box$\enskip Please check with an X \emph{only} if the exam should be voided and}\\[1mm]
\multicolumn{2}{@{}l@{}}{\Large\bf \phantom{$\Box$\enskip}not graded.} \\[1mm]
\multicolumn{2}{@{}l@{}}{{\Large\bf \phantom{$\Box$\enskip}}\bf Bitte \emph{nur} ankreuzen, wenn die Klausur entwertet und nicht korrigiert werden soll.}
\end{tabular}
\vspace{10mm}

Hierby I confirm the correctness of the above information:
% \vspace{2cm}

\hspace{10cm} $\overline{\hspace{2cm} \mbox{Signature\strut} \hspace{2cm}}$

\vfill
Please leave the following table blank: \\[-4ex]
\let\NumberCols\empty%
\begingroup%
  \multido{\i=1+1}{\totvalue{aufgno}}{\xdef\NumberCols{\NumberCols c|}}%
\endgroup%
\let\NumberRow\empty%
\begingroup%
  \multido{\i=1+1}{\totvalue{aufgno}}{ \xdef\NumberRow{\NumberRow\i&}}%
\endgroup%
\let\PointRow\empty%
\begingroup%
  \multido{\i=1+1}{\totvalue{aufgno}}{ \xdef\PointRow{\PointRow \getpunkte{\i} &}}%
\endgroup%
\newlength{\boxwidth}
\setlength{\boxwidth}{(\linewidth - 14EM) / (\totvalue{aufgno}+6) }
\newsavebox{\emptywidth}
\sbox{\emptywidth}{\hspace{\boxwidth}}
\let\EmptyRow\empty%
\begingroup%
  \multido{\i=1+1}{\totvalue{aufgno}}{ \xdef\EmptyRow{\EmptyRow\usebox{\emptywidth}&}}%
\endgroup%
\addtolength{\boxwidth}{3mm}

\begin{center}
\begin{tabular}{|l||\NumberCols|c|c||c|}
\hline
\large Question\rule[-2ex]{0em}{6ex}  & \NumberRow $\sum$  %& \large Bonus & \large Note
\\ \hline
\large Points\rule[-2ex]{0em}{6ex}   & \PointRow  {\total{sumpunkte}} \\ \hline
\large Score\rule[-2ex]{0em}{6ex} & \EmptyRow  \hspace*{\boxwidth} \\ \hline
\end{tabular}
\end{center}
%\pagebreak %% bei Option twoside
%\quad      %% bei Oprion twoside
\vfill
\newpage

%%% END

\parindent0em
\parskip1ex plus0.25ex minus0.25ex

\newenvironment{code}{\begin{quote}\tt}{\end{quote}}

%\newcommand{\bittewenden}{\fancyfoot[R]{-- bitte wenden --}\newpage\fancyfoot{}}
\newcommand{\bittewenden}{\newpage}

\setlength{\voffset}{-1.6cm}
\setlength{\textheight}{25.5cm}
\setlength{\hoffset}{-5mm}
\setlength{\textwidth}{17cm}

\pagestyle{empty}

\fancyhead{}
\fancyhead[LO]{Name:}
\fancyhead[RO,RE]{\thepage}
\fancyfoot{}
%\cfoot{}

\setcounter{page}{1}
\pagestyle{fancy}

\renewcommand{\theenumi}{\alph{enumi}}
\renewcommand{\labelenumi}{\textbf{\theenumi)}}
\renewcommand{\theenumii}{\roman{enumii}}
% \renewcommand{\labelenumii}{\textbf{\theenumii)}}
\renewcommand{\theenumiii}{\arabic{enumiii}}
% \renewcommand{\labelenumiii}{\textbf{\theenumiii)}}

\newcommand{\ankreuzen}[1]{\ensuremath{%
    \fbox{\phantom{X}}\ifthenelse{\equal{#1}{}}{}{~~\mbox{#1}}}}
\newcommand{\ja}{\ankreuzen{ja}}
\newcommand{\nein}{\ankreuzen{nein}}
\newcommand{\linie}{\rule{\linewidth}{0.1pt}\\}
\newcommand{\richtig}{\Loes{X}\Loes{\hspace*{-4.4EX}}} %small: -4.6EX

~~

\vfill

\fbox{
\begin{minipage}{.97\textwidth}

\textbf{Guidelines for Paper Proofs}\strut

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

\medskip

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 {induction 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 mention which key lemmas they depend on.
You should be explicit whenever you use a function definition or an introduction
rule for an inductive predicate.

\end{minipage}
}

\vfill

~~

\newpage

\begin{aufgabe}{Types and Terms}{20}
\vspace*{-2em}
\begin{enumerate}

\item Recall the following simplified typing rules for Lean's dependent type theory:

\vskip\abovedisplayskip

\centerline{\prftree[r]{\textsc{Cst}\quad if \li{c} is globally declared with type~\li|\σ|}
  {\strut\text{\li{C ⊢ c : σ}}}}

\vskip2\jot

\centerline{\prftree[r]{\textsc{Var}\quad if \li{x : σ} is the rightmost occurrence of \li{x} in \li{C}}
  {\strut\text{\li{C ⊢ x : σ}}}}

\vskip2\jot

\centerline{\prftree[r]{\textsc{App}$'$}
  {\strut\text{\li{C ⊢ t : (x : σ) → τ[x]}}}
  {\strut\text{\li{C ⊢ u : σ}}}
  {\strut\text{\li{C ⊢ t u : τ[u]}}}}

\vskip2\jot

\centerline{\prftree[r]{\textsc{Fun}$'$}
  {\strut\text{\li{C, x : σ ⊢ t : τ[x]}}}
  {\strut\text{\li{C ⊢ (fun x : σ ↦ t) : (x : σ) → τ[x]}}}}

\vskip\belowdisplayskip

Let \li$a : ℕ$, \li$f : (ℕ → ℕ) → ℕ → ℕ$, \li$g : ℕ → ℕ → ℕ$, and
\li$h : (y : ℕ) → {x : ℕ // x < y}$ be globally declared constants.
What is the type of the following two Lean terms? Give in each case a typing
derivation as justification for the type.

\begin{enumerate}
\item \li{h a}\nurloesung{\hfill(6~points)}

\begin{loesung}
The type is \li${x : ℕ // x < a}$. The typing derivation is
%
\[\prftree[r]{\textsc{App}$'$}
  {
    \prftree[r]{\textsc{Cst}}
      {\strut\text{\li|\⊢ h : (y : ℕ) → \{x : ℕ // x < y\}|}}
  }
  {
    \prftree[r]{\textsc{Cst}}
      {\strut\text{\li|\⊢ a : ℕ|}}
  }
  {\strut\text{\li|\⊢ h a : \{x : ℕ // x < a\}|}}\]
\end{loesung}
\begin{bewertung}
\begin{itemize}
\item 2 points for the type
\item 4 points for the derivation tree
\end{itemize}
\end{bewertung}

\vfill

\item \li{f (fun x : ℕ ↦ g x x)}\nurloesung{\hfill(8~points)}

\begin{loesung}
The type is \li$ℕ → ℕ$. The typing derivation is
%
{\footnotesize
\[\prftree[r]{\textsc{App}$'$}
  {
    \prftree[r]{\textsc{Cst}}
      {\strut\text{\li|\⊢ f : (ℕ → ℕ) → ℕ → ℕ|}}
    \kern-6ex
  }
  {
    \prftree[r]{\textsc{Fun}$'$}
      {
        \prftree[r]{\textsc{App}$'$}
          {
            \prftree[r]{\textsc{App}$'$}
              {
                \prftree[r]{\textsc{Cst}}
                  {\strut\text{\li|x : ℕ \⊢ g : ℕ → ℕ → ℕ|}}
              }
              {
                \prftree[r]{\textsc{Var}}
                  {\strut\text{\li|x : ℕ \⊢ x : ℕ|}}
              }
              {\strut\text{\li|x : ℕ \⊢ g x : ℕ → ℕ|}}
          }
          {
                \prftree[r]{\textsc{Var}}
                  {\strut\text{\li|x : ℕ \⊢ x : ℕ|}}
          }
          {\strut\text{\kern15ex\li|x : ℕ \⊢ g x x : ℕ|\kern15ex}}
      }
      {\strut\text{\li|\⊢ (fun x : ℕ ↦ g x x) : ℕ → ℕ|}}
  }
  {\strut\text{\li|\⊢ f (fun x : ℕ ↦ g x x) : ℕ → ℕ|}}\]
}
\end{loesung}
\begin{bewertung}
\begin{itemize}
\item 2 points for the type
\item 6 points for the derivation tree
\end{itemize}
\end{bewertung}

\vfill
\end{enumerate}

\newpage

\item

Let \li|α|, \li|β|, and \li|γ| be Lean types. Give an inhabitant for each of the
following types:

\begin{itemize}
\item \li|α → α|\nurloesung{\hfill(2 points)}

\begin{loesung}
\li|fun a ↦ a|
\end{loesung}
\begin{bewertung}
\begin{itemize}
\item 1 point for \li|fun a|
\item 1 point for \li|a|
\end{itemize}
\end{bewertung}

\vfill
\item \li|(α → β) → (γ → α) → γ → β|\nurloesung{\hfill(2 points)}

\begin{loesung}
\li|fun g f c ↦ g (f c)|
\end{loesung}
\begin{bewertung}
\begin{itemize}
\item 1 point for \li|fun g f c|
\item 1 point for \li|g (f c)|
\end{itemize}
\end{bewertung}

\vfill
\item \li|(γ → (α → β) → α) → γ → β → α|\nurloesung{\hfill(2 points)}

\begin{loesung}
\li|fun h c b ↦ h c (fun a ↦ b)|
\end{loesung}
\begin{bewertung}
\begin{itemize}
\item 1 point for \li|fun h c b|
\item 1 point for \li|h c (fun a ↦ b)|
\end{itemize}
\end{bewertung}

\vfill
\end{itemize}
\end{enumerate}
\end{aufgabe}

\begin{aufgabe}{Functional Programming}{25}
\vspace*{-2em}
\begin{enumerate}
\item Consider the following Lean function definition:

\begin{lstlisting}
def surround {α : Type} (a : α) : List α → List α
  | []      => [a]
  | b :: bs => a :: b :: surround a bs
\end{lstlisting}

\begin{enumerate}
\item Compute the value of \li|surround 0 [1, 2, 3]|.%
\nurloesung{\hfill(2 points)}

\begin{loesung}
\li|[0, 1, 0, 2, 0, 3, 0]|.
\end{loesung}
\begin{bewertung}
2 points for right answer, 0 otherwise
\end{bewertung}

\vfill

\item Prove the following Lean theorem. Make sure to follow the proof guidelines
  given on page~1.\nurloesung{\\
  \noindent\hbox{}\hfill(8 points)}

\begin{lstlisting}
theorem map_surround {α β : Type} (f : α → β) (x : α) (ys : List α) :
  List.map f (surround x ys) = surround (f x) (List.map f ys)
\end{lstlisting}

\begin{loesung} ~~

The proof is by structural induction on \li|ys|.

The base case is
\begin{center}
\li|List.map f (surround x []) = surround (f x) (List.map f [])|
\end{center}
Both sides simplify to \li|[f x]| and are hence equal.

The induction step is
\begin{center}
\li|List.map f (surround x (y :: ys'))|
\li|= surround (f x) (List.map f (y :: ys'))|
\end{center}
The induction hypothesis is
\begin{center}
\li|List.map f (surround x ys') = surround (f x) (List.map f ys')|
\end{center}
The induction step simplifies to
\begin{center}
\li|[f x, f y] ++ List.map f (surround x ys')|
\li|= [f x, f y] ++ surround (f x) (List.map f ys')|
\end{center}
By the induction hypothesis, the two sides are equal.

\end{loesung}
\begin{bewertung}
\begin{itemize}
\item 1 point for ``by (structural) induction''
\item 1 point for ``on \li|ys|''
\item 1 point for statement of base case
\item 1 point for proof of base case
\item 1 point for statement of induction step
\item 1 point for statement of induction hypothesis
\item 2 points for proof of induction step (IH and \li|simp|)
\end{itemize}
\end{bewertung}

\vskip0pt plus 100fill

\newpage

\item Prove the following Lean theorem. Make sure to follow the proof guidelines
  given on page~1.\nurloesung{\\
  \noindent\hbox{}\hfill(8 points)}

\begin{lstlisting}
theorem length_surround {α : Type} (x : α) (ys : List α) :
  List.length (surround x ys) = 2 * List.length ys + 1
\end{lstlisting}

\begin{loesung} ~~

The proof is by structural induction on \li|ys|.

The base case is
\begin{center}
\li|List.length (surround x []) = 2 * List.length [] + 1|
\end{center}
Both sides simplify to \li|1| and are hence equal.

The induction step is
\begin{center}
\li|List.length (surround x (y :: ys')) = 2 * List.length (y :: ys') + 1|
\end{center}
The induction hypothesis is
\begin{center}
\li|List.length (surround x ys') = 2 * List.length ys' + 1|
\end{center}
The induction step simplifies to
\begin{center}
\li|List.length (surround x ys') + 2 = 2 * List.length ys' + 3|
\end{center}
By the induction hypothesis and some basic arithmetic reasoning, the two sides
are equal.

\end{loesung}
\begin{bewertung}
\begin{itemize}
\item 1 point for ``by (structural) induction''
\item 1 point for ``on \li|ys|''
\item 1 point for statement of base case
\item 1 point for proof of base case
\item 1 point for statement of induction step
\item 1 point for statement of induction hypothesis
\item 2 points for proof of induction step (IH and \li|arith|)
\end{itemize}
\end{bewertung}

\end{enumerate}

\newpage

\item Define a Lean function \li|suffixes| that takes a list and that returns a
list of all suffixes of that list, including the list itself, from longest to
shortest. For example, \li|suffixes [1, 2, 3]| should evaluate to
\li|[[1,| \li|2,| \li|3], [2, 3], [3], []]|.\nurloesung{\hfill(7~points)}

\begin{loesung}
\begin{lstlisting}
def suffixes {α : Type} : List α → List (List α)
  | []      => [[]]
  | x :: xs => (x :: xs) :: suffixes xs
\end{lstlisting}
\end{loesung}
\begin{bewertung}
\begin{itemize}
\item 1 point for ``\li|def suffixes {α : Type}|''
\item 1 point for type
\item 1 point for LHS of first equation
\item 1 point for RHS of first equation
\item 1 point for LHS of second equation
\item 2 points for RHS of second equation
\end{itemize}
\end{bewertung}
\end{enumerate}
\end{aufgabe}

\begin{aufgabe}{Inductive Predicates}{25}
\vspace*{-2em}
\begin{enumerate}
\item Consider the following Lean inductive predicate, which determines whether
a list has odd length:

\begin{lstlisting}
inductive OddLength {α : Type} : List α → Prop
  | singleton (x : α) :
    OddLength [x]
  | add_two (x y : α) {xs : List α} :
    OddLength xs → OddLength (x :: y :: xs)
\end{lstlisting}

For example, \li|OddLength [1, 2, 3]| holds, whereas \li|OddLength [4, 5]|
does not.

Prove the following Lean theorem about \li|OddLength|. Make sure to follow the proof guidelines given on page~1.\nurloesung{\hfill(9~points)}

\begin{lstlisting}
theorem OddLength_map {α β : Type} (f : α → β) (xs : List α)
    (hxs : OddLength xs) :
  OddLength (List.map f xs)
\end{lstlisting}

\begin{loesung}
The proof is by rule induction on \li|hxs|.

In the \li|singleton| case, the goal is
\begin{center}
\li|OddLength (List.map f [x])|
\end{center}
This simplifies to \li|OddLength [f x]|, which is provable using
\li{OddLength.singleton}.

In the \li|add_two| case, the goal is
\begin{center}
\li|OddLength xs' → OddLength (List.map f (x :: y :: xs'))|
\end{center}
The induction hypothesis is
\begin{center}
\li|OddLength (List.map f xs')|
\end{center}
The goal simplifies to
\begin{center}
\li|OddLength xs' → OddLength (f x :: f y :: List.map f xs'))|
\end{center}
We prove it using \li{OddLength.add_two} with the induction hypothesis.

\end{loesung}
\begin{bewertung}
\begin{itemize}
\item 1 point for ``by (rule) induction''
\item 1 point for ``on \li|hxs|''
\item 1 point for statement of \li|singleton| case
\item 1 point for proof of \li|singleton| case
\item 1 point for statement of \li|add_two| case
\item 1 point for statement of induction hypothesis
\item 3 points for proof of \li|add_two| case (\li|simp|, \li{add_two}, and IH)
\end{itemize}
\end{bewertung}

\newpage

\item Define an inductive predicate \li|InList| in Lean that takes a value
\li|x| of the polymorphic type \li|α| and a list \li|ys| over \li|α| as
arguments and that holds if \li|x| occurs in \li|ys|.\nurloesung{\hfill(7~points)}

\begin{loesung}
\begin{lstlisting}
inductive InList {α : Type} : α → List α → Prop
  | in_hd (x : α) (xs : List α)   : InList x (x :: xs)
  | in_tl (x y : α) (ys : List α) : InList x ys → InList x (y :: ys)
\end{lstlisting}
\end{loesung}
\begin{bewertung}
\begin{itemize}
\item 1 point for ``\li|inductive InList {α : Type}|''
\item 1 point for type
\item 1 point for LHS of first introduction rule
\item 1 point for RHS of first introduction rule
\item 1 point for LHS of second introduction rule
\item 2 points for RHS of second introduction rule
\end{itemize}
\end{bewertung}

\newpage

\item Consider the following Lean type of binary trees and a helper function
  that counts the number of nodes in a given tree:
\begin{lstlisting}
inductive Tree (α : Type) : Type
  | nil  : Tree α
  | node : α → Tree α → Tree α → Tree α

def numNodes {α : Type} : Tree α → ℕ
  | Tree.nil        => 0
  | Tree.node a l r => numNodes l + numNodes r + 1
\end{lstlisting}

Define an inductive predicate \li|RightHeavy| in Lean that takes a tree
as argument and that holds if the tree enjoys \emph{either} of the following
properties:
\begin{itemize}
\item The tree is of the form \li|Tree.nil|.
\item The tree is of the form \li|Tree.node a l r|,
  the number of nodes in \li|l| is less than or equal to the number of nodes in
  \li|r|, and both \li|l| and \li|r| recursively satisfy \li|RightHeavy|.%
\nurloesung{\\\noindent\hbox{}\hfill(9~points)}
\end{itemize}

\begin{loesung}
\begin{lstlisting}
inductive RightHeavy {α : Type} : Tree α → Prop
  | nil :
    RightHeavy Tree.nil
  | node (a : α) (l r : Tree α) :
    numNodes l ≤ numNodes r → RightHeavy l → RightHeavy r →
    RightHeavy (Tree.node a l r)
\end{lstlisting}
\end{loesung}
\begin{bewertung}
\begin{itemize}
\item 1 point for ``\li|inductive RightHeavy {α : Type}|''
\item 1 point for type
\item 1 point for LHS of first clause
\item 1 point for RHS of first clause
\item 1 point for LHS of second clause
\item 4 points for RHS of second clause
\end{itemize}
\end{bewertung}
\end{enumerate}
\end{aufgabe}

\begin{aufgabe}{Metaprogramming}{8}

Consider the following custom Lean tactic:

\begin{lstlisting}
macro "mystery" : tactic =>
  `(tactic| repeat' first
              | assumption
              | intro _
              | apply And.intro
              | apply Iff.intro)
\end{lstlisting}

\begin{enumerate}
\item Briefly explain what the \li|mystery| tactic
does. You may assume that we already know what \li|assumption|,
\li|intro|, and \li|apply| does.\nurloesung{\hfill(3~points)}

\begin{loesung}
The tactic repeatly tries to apply the first applicable tactic among four
tactics:\ \li{assumption}, \li{intro _}, \li{apply And.intro}, and
\li{apply Iff.intro}. By ``repeatedly,'' we mean that the process is repeated
for all goals and recursively for all emerging subgoals.
\end{loesung}
\begin{bewertung}
\begin{itemize}
\item 1 point for general explanation
\item 1 point for \li|repeat'|'s explanation
\item 1 point for \li|first|'s explanation
\end{itemize}
\end{bewertung}

\newpage

\item In the following Lean code fragment, the \li{mystery} tactic is applied
  to massage the goal:

\begin{lstlisting}
theorem abac (a b c : Prop) :
  a → b ∧ a ∧ ¬ c :=
  by
    mystery
\end{lstlisting}

The proof state before invoking \li|mystery| is
\begin{lstlisting}
a b c : Prop
⊢ a → b ∧ a ∧ ¬c
\end{lstlisting}
Give the proof state \emph{after} invoking \li|mystery|. Make sure to include
all subgoals.
\nurloesung{\hfill(5~points)}

\begin{loesung}
\begin{lstlisting}
a b c : Prop
ha : a
⊢ b

a b c : Prop
ha : a
hc : c
⊢ False
\end{lstlisting}
\end{loesung}
\begin{bewertung}
\begin{itemize}
\item 1 point for first subgoal's hypotheses
\item 1 point for first subgoal's target
\item 1 point for second subgoal's hypotheses
\item 1 point for second subgoal's target
\item 1 point for lack of extraneous subgoals (e.g., for \li|a|)
\end{itemize}
\end{bewertung}
\end{enumerate}
\end{aufgabe}

\begin{aufgabe}{Operational Semantics}{12}

The IF0 programming language is similar to WHILE, with two  
  differences.
  First, the \li{while}--\li{do} statement is omitted.
  Second, the \li{if}--\li{then}--\li{else} statement is replaced by
    \li{if_zero}--\li{then}--\li{else}. For example, the program
\begin{lstlisting}
if_zero m * n then
  x := 0
else
  y := 1
\end{lstlisting}
executes \li|x := 0| if the condition \li|m * n = 0| holds when entering the
construct; otherwise, it executes \li|y := 1|.

In Lean, IF0 would be modeled by the following datatype:

\begin{lstlisting}
inductive Stmt : Type where
  | skip   : Stmt
  | assign : String → (State → ℕ) → Stmt
  | seq    : Stmt → Stmt → Stmt
  | ifZero : (State → ℕ) → Stmt → Stmt → Stmt

infixr:90 "; " => Stmt.seq
\end{lstlisting}

\begin{enumerate}
\item Complete the following specification of a big-step semantics for IF0 in
  Lean by giving the missing derivation rules for \li|seq| and
  \li|if_zero|.%
  \nurloesung{\hfill(6~points)}

\vskip\abovedisplayskip

\noindent\hfill
\RL{\textsc{Skip}}
\AXC{\phantom{.}}
\UIC{\strut\li|(skip, s) ⟹ s|}
\DP
\hfill\hbox{}

\smallskip

\noindent\hfill
\AXC{\phantom{.}}
\RL{\textsc{Assign}}
\UIC{\strut\li$(x := a, s) ⟹ s[x ↦ s(a)]$}
\DP
\hfill\hbox{}

\vskip\belowdisplayskip

\begin{loesung}

\vskip\abovedisplayskip

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

\smallskip

\noindent\hfill
\AXC{\strut\li|(S, s) ⟹ t|}
\RL{\textsc{IfZero\_True}\quad if \li{s(a) = 0}}
\UIC{\strut\li|(if_zero a then S else T, s) ⟹ t|}
\DP
\hfill\hbox{}

\smallskip

\noindent\hfill
\AXC{\strut\li|(T, s) => t|}
\RL{\textsc{IfZero\_False}\quad if \li{s(a) ≠ 0}}
\UIC{\strut\li|(if_zero a then S else T, s) ⟹ t|}
\DP
\hfill\hbox{}
\end{loesung}
\begin{bewertung}
\begin{itemize}
\item 2 points for \textsc{Seq}
\begin{itemize}
\item 1 point for premises
\item 1 point for conclusion
\end{itemize} 
\item 2 points for \textsc{IfZero\_True}
\begin{itemize}
  \item 1 point for premise and side condition
  \item 1 point for conclusion
\end{itemize}
\item 2 points for \textsc{IfZero\_False}
\begin{itemize}
  \item 1 point for premise and side condition
  \item 1 point for conclusion
\end{itemize}
\end{itemize}
\end{bewertung}

\newpage

\item Complete the following Lean definition of an inductive predicate that
  encodes the big-step semantics you specified in subquestion a) above.%
  \nurloesung{\hfill(6~points)}

\begin{lstlisting}
inductive BigStep : Stmt × State → State → Prop where
  | skip (s) :
    BigStep (Stmt.skip, s) s
  | assign (x a s) :
    BigStep (Stmt.assign x a, s) (s[x ↦ a s])
\end{lstlisting}

\begin{loesung}
\begin{lstlisting}
  | seq (S T s t u) (hS : BigStep (S, s) t)
      (hT : BigStep (T, t) u) :
    BigStep (S; T, s) u
  | ifZero_true (a S T s t) (hcond : a s = 0)
      (hbody : BigStep (S, s) t) :
    BigStep (Stmt.ifZero a S T, s) t
  | ifZero_false (a S T s t) (hcond : a s ≠ 0)
      (hbody : BigStep (T, s) t) :
    BigStep (Stmt.ifZero a S T, s) t
\end{lstlisting}
\end{loesung}
\begin{bewertung}
\begin{itemize}
\item 2 points for \li|seq|
\begin{itemize}
  \item 1 point for rule name, variables, and premises
  \item 1 point for conclusion
\end{itemize}
\item 2 points for \li|ifZero_True|
\begin{itemize}
  \item 1 point for rule name, variables, and premises
  \item 1 point for conclusion
\end{itemize}
\item 2 points for \li|ifZero_False|
\begin{itemize}
  \item 1 point for rule name, variables, and premises
  \item 1 point for conclusion
\end{itemize}
\item Folgefehler are acknowledged
\end{itemize}
\end{bewertung}
\end{enumerate}
\end{aufgabe}

\begin{aufgabe}{Mathematics}{10}
\vspace*{-2em}
\begin{enumerate}
\item Let \li|σ : Type 2| and \li|τ : Type 3| be Lean types. Give the type of
  each of the following Lean terms.\nurloesung{\\
  \noindent\hbox{}\hfill(4~points)}

\begin{lstlisting}
fun x : σ ↦ x
Type 5
σ → τ
fun α : Type ↦ Option (α × α)
\end{lstlisting}

\begin{loesung} ~~ \\
\li|σ → σ| \\
\li|Type 6| (or \li|Sort 7|) \\
\li|Type 3| (or \li|Sort 4|) \\
\li|Type → Type| (or \li|Sort 1 → Sort 1|)
\end{loesung}
\begin{bewertung}
\begin{itemize}
\item 1 point per type
\end{itemize}
\end{bewertung}

\newpage

\item A \emph{bag} is a collection of elements that allows multiple (but
finitely many) occurrences of its elements. For example, the bag \li|{2, 7}| is
equal to the bag \li|{7, 2}| but different from \li|{2, 7, 7}|.

Finite bags can be defined as a quotient over lists. We start with the type
\li|List α| of finite lists and consider only the number of occurrences of
elements in the lists, ignoring the order in which elements occur. Following
this scheme, \li|[2, 7, 7]|, \li|[7, 2, 7]|, and \li|[7, 7, 2]| would be three
equally valid representations of the bag \li|{2, 7, 7}|.

The \li|List.count| function returns the number of occurrences of an element in
a list. Since it uses equality on elements of type \li|α|, it requires \li|α| to
belong to the \li|BEq| (Boolean equality) type class. For this reason, the
definitions below take \li|[BEq α]| as a type class argument.

\begin{lstlisting}
instance Bag.Setoid (α : Type) [BEq α] : Setoid (List α) :=
{ r     := fun as bs ↦ ∀x, List.count x as = List.count x bs
  iseqv :=
    { refl  := by simp
      symm  := by aesop
      trans := by aesop } }

def Bag (α : Type) [BEq α] : Type :=
  Quotient (Bag.Setoid α)

def Bag.mk {α : Type} [BEq α] : List α → Bag α :=
  Quotient.mk (Bag.Setoid α)
\end{lstlisting}

Complete the following two definitions.%
\nurloesung{\hfill(4~points)}

\begin{lstlisting}
def Bag.empty {α : Type} [BEq α] : Bag α :=

def Bag.singleton {α : Type} [BEq α] (a : α) : Bag α :=
\end{lstlisting}

\begin{loesung} ~~ \\
\verb|Bag.mk []| \\
\verb|Bag.mk [a]|
\end{loesung}
\begin{bewertung}
\begin{itemize}
\item 2 points per term
\end{itemize}
\end{bewertung}

\newpage

\item Consider the following Lean type classes:
\begin{lstlisting}
universe u

class Mul (α : Type u) : Type u where
  mul : α → α → α

infixl:70 " * " => Mul.mul

class Semigroup (α : Type u)
  extends Mul α : Type u where
  mul_assoc : ∀a b c : α, a * b * c = a * (b * c)
\end{lstlisting}
%
The \li{Semigroup} type class provides an associative binary operator called
\li{mul} abbreviated as \li|*|.

The concatenation operator \li|++| on lists is an associative binary operator.
Exploit this fact to fill in the gap in the following type class
instantiation:\nurloesung{\hfill(2~points)}

\begin{lstlisting}
instance List.Semigroup {α : Type} : Semigroup (List α) :=
  { mul       :=
    mul_assoc := by simp }
\end{lstlisting}

\begin{loesung} ~~ \\
\li|fun xs ys ↦ xs ++ ys|
\end{loesung}
\begin{bewertung}
2 points for right answer, 0 otherwise
\end{bewertung}
\end{enumerate}
\end{aufgabe}

\nuraufgabe{\multido{\i=1+1}{\value{emptypages}}{\newpage\hspace*{12mm}}}
\end{document}
