%%% 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}{14.10.2024}\\
Xavier Généreux\\
Balazs Toth\\[-1.5em]
\begin{center}
  {\Large \Loes{Solution to the} Third 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 turned 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}}.
There are \total{aufgno} questions for a total of \total{sumpunkte}~points.

You may use the back of the sheets for auxiliary calculations. If you use the
back for actual answers, 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.
%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 < 5}$ 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 < 5}$. The typing derivation is
%
\[\prftree[r]{\textsc{App}$'$}
  {
    \prftree[r]{\textsc{Cst}}
      {\strut\text{\li|\⊢ h : (y : ℕ) → \{x : ℕ // x < 5\}|}}
  }
  {
    \prftree[r]{\textsc{Cst}}
      {\strut\text{\li|\⊢ a : ℕ|}}
  }
  {\strut\text{\li|\⊢ h a : \{x : ℕ // x < 5\}|}}\]
\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{fun x ↦ f g x}\nurloesung{\hfill(8~points)}

\begin{loesung}
The type is \li$ℕ → ℕ$. The typing derivation is
%
{%\footnotesize
\[\prftree[r]{\textsc{Fun}$'$}
  {
      \prftree[r]{\textsc{App}$'$}
      {
          \prftree[r]{\textsc{App}$'$}
          {
              \prftree[r]{\textsc{Cst}}
              { \strut\text{\li|x : ℕ \⊢ f : (ℕ → ℕ) → ℕ → ℕ|} }
          }
          {
              \prftree[r]{\textsc{Cst}}
              { \strut\text{\li|x : ℕ \⊢ g : ℕ → ℕ|} }
          }
          { \strut\text{\li|x : ℕ \⊢ f g : ℕ → ℕ|} }
      }
      {
        \prftree[r]{\textsc{Var}}
        { \strut\text{\li|x : ℕ \⊢ x : ℕ|} }
      }
      { \strut\text{\li|x : ℕ \⊢ f g x : ℕ|} }
  }
  { \strut\text{\li|\⊢ fun x ↦ f g 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 b ↦ b|
\end{loesung}
\begin{bewertung}
\begin{itemize}
\item 1 point for \li|fun a b ↦|
\item 1 point for \li|b|
\end{itemize}
\end{bewertung}

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

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

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

\begin{loesung}
\li|fun h c b ↦ h (fun a a' ↦ b)|
\end{loesung}
\begin{bewertung}
\begin{itemize}
\item 1 point for \li|fun h c b|
\item 1 point for \li|h (fun a 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 stutter {α : Type} : List α → List α
  | []      => []
  | a :: as => a :: a :: stutter as
\end{lstlisting}

\begin{enumerate}
\item Give the value of \li|stutter [4, 3, 2]|.
(There is no need to provide intermediate steps.)%
\nurloesung{\\ \hfill(2 points)}

\begin{loesung}
\li|[4, 4, 3, 3, 2, 2]|.
\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_stutter {α β : Type} (f : α → β) (ys : List α) :
  List.map f (stutter ys) = stutter (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 (stutter []) = stutter (List.map f [])|
\end{center}
Both sides simplify to \li|[]| and are hence equal.

The induction step is
\begin{center}
\li|List.map f (stutter (y :: ys'))|
\li|= stutter (List.map f (y :: ys'))|
\end{center}
The induction hypothesis is
\begin{center}
\li|List.map f (stutter ys') = stutter (List.map f ys')|
\end{center}
The induction step simplifies to
\begin{center}
\li|[f y, f y] ++ List.map f (stutter ys') = [f y, f y] ++ stutter (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 stutter_snoc {α : Type} (xs : List α) (y : α) :
  stutter (xs ++ [y]) = stutter xs ++ [y, y] :=
\end{lstlisting}

\begin{loesung} ~~

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

The base case is
\begin{center}
\li|stutter ([] ++ [y]) = stutter [] ++ [y, y]|
\end{center}
Both sides simplify to \li|[y, y]| and are hence equal.

The induction step is
\begin{center}
\li|stutter ((x :: xs') ++ [y]) = stutter (x :: xs') ++ [y, y]|
\end{center}
The induction hypothesis is
\begin{center}
\li|stutter (xs' ++ [y]) = stutter xs' ++ [y, y]|
\end{center}
The induction step simplifies to
\begin{center}
\li|[x, x] ++ stutter (xs' ++ [y]) = [x, x] ++ stutter xs' ++ [y, y]|
\end{center}
(up to associativity of \li|++|). 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|xs|''
\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}

\end{enumerate}

\newpage

\item Define a Lean function \li|singletonify| that takes a list
$\verb|[|x_1,\dots, x_n\verb|]|$ and that returns a list of singletons
$\verb|[[|x_1\verb|]|,\dots, \verb|[|x_n\verb|]]|$.
For example, \li|singletonify [1, 2, 3, 5, 7]| should evaluate to
\li|[[1], [2], [3], [5], [7]]|.\nurloesung{\hfill(7~points)}

\begin{loesung}
\begin{lstlisting}
def singletonify {α : Type} : List α → List (List α)
  | []      => []
  | x :: xs => [x] :: singletonify xs
\end{lstlisting}
\end{loesung}
\begin{bewertung}
\begin{itemize}
\item 1 point for ``\li|def singletonify {α : 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 Recall the \li|stutter| function from Question~2:
\begin{lstlisting}
def stutter {α : Type} : List α → List α
  | []      => []
  | a :: as => a :: a :: stutter as
\end{lstlisting}

Now consider the following Lean inductive predicate, which holds when
a list has even length:

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

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

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

\begin{lstlisting}
theorem EvenLength_stutter {α β : Type} (xs : List α)
    (hxs : EvenLength xs) :
  EvenLength (stutter xs)
\end{lstlisting}

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

In the \li|nil| case, the goal is
\begin{center}
\li|EvenLength (stutter [])|
\end{center}
This simplifies to \li|EvenLength []|, which is provable using
\li{EvenLength.nil}.

In the \li|add_two| case, the goal is
\begin{center}
\li|EvenLength xs' → EvenLength (stutter (x :: y :: xs'))|
\end{center}
The induction hypothesis is
\begin{center}
\li|EvenLength (stutter xs')|
\end{center}
The goal simplifies to
\begin{center}
\li|EvenLength xs' → EvenLength (x :: x :: y :: y :: stutter xs')|
\end{center}
We prove it using \li{EvenLength.add_two} \emph{twice} 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 4 points for proof of \li|add_two| case (\li{simp}, \li{add_two},
\li{add_two}, and IH)
\end{itemize}
\end{bewertung}

\newpage

\item Define an inductive predicate \li{Suffix} in Lean that takes two lists over a polymorphic
type \li|α| as arguments and that holds when the first list is a suffix of the
second. For exemple, \li{Suffix [1,} \li{2] [1, 2]} and \li{Suffix [2, 4] [1, 2, 4]} should hold.
\nurloesung{\hfill(8~points)}

\begin{loesung}
\begin{lstlisting}
inductive Suffix {α : Type} : List α → List α → Prop where
  | nil (as : List α) :
    Suffix [] as
  | snoc (a : α) (as bs : List α) (hp : Suffix as bs) :
    Suffix (as ++ [a]) (bs ++ [a])
\end{lstlisting}
\end{loesung}
\begin{bewertung}
\begin{itemize}
\item 1 point for ``\li|inductive Suffix {α : 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 2 points for LHS of second introduction rule
\item 2 points for RHS of second introduction rule
\end{itemize}
\end{bewertung}

\newpage

\item Define an inductive predicate \li|EvenPalindrome| in Lean that takes a list over a polymorphic type \li|α| as argument and that holds if
the list is a palindrome (i.e., if it equals its reverse) and has even length.
For example, \li|EvenPalindrome [1, 2, 2, 1]| should hold, whereas
\li|EvenPalindrome| \li|[1, 3, 1]| and \li|EvenPalindrome [1, 3, 7]| should not
hold.
\nurloesung{\noindent\hbox{}\hfill(8~points)}

\begin{loesung}
\begin{lstlisting}
inductive EvenPalindrome {α : Type} : List α → Prop where
  | nil :
    EvenPalindrome []
  | sandwich (x : α) (xs : List α) (hxs : EvenPalindrome xs) :
    EvenPalindrome ([x] ++ xs ++ [x])
\end{lstlisting}
\end{loesung}
\begin{bewertung}
\begin{itemize}
\item 1 point for ``\li|inductive EvenPalindrome {α : 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 2 points for LHS of second introduction rule
\item 2 points for RHS of second introduction rule
\end{itemize}
\end{bewertung}
\end{enumerate}
\end{aufgabe}

\begin{aufgabe}{Metaprogramming}{8}

Consider the following custom Lean tactic:

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

\begin{enumerate}
\item Briefly explain what the \li|enigma| 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 five
tactics:\ \li{assumption}, \li{intro _}, \li{apply True.intro},
\li{apply And.intro}, and \li{apply} \li{Iff.}\allowbreak\hbox{\li{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{enigma} tactic is applied
  to transform the goal:

\begin{lstlisting}
theorem abbatf (a b : Prop) :
  a → b → b ∧ a ∧ True ∧ False :=
  by
    enigma
\end{lstlisting}

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

\begin{loesung}
\begin{lstlisting}
a b : Prop
a_1 : a
a_2 : b
⊢ False
\end{lstlisting}
\end{loesung}
\begin{bewertung}
\begin{itemize}
\item 3 points for \li|a| and \li|b| hypotheses
\item 2 points for \li|False|
\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 is  modeled by the following inductive type:

\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 small-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
\AXC{\phantom{.}}
\RL{\textsc{Assign}}
\UIC{\strut\li$(x := a, s) ⇒ (skip, s[x ↦ s(a)])$}
\DP
\hfill\hbox{}

\vskip\belowdisplayskip

\noindent\hfill
\AXC{\phantom{.}}
\RL{\textsc{SeqSkip}}
\UIC{\strut\li$(Stmt.skip; T, s) ⇒ (T, s)$}
\DP
\hfill\hbox{}

\vskip\belowdisplayskip

\begin{loesung}

\vskip\abovedisplayskip

\noindent\hfill
\AXC{\li|(S, s) ⇒ (S', s')|}
\RL{\textsc{SeqStep}}
\UIC{\strut\li|(S; T, s) ⇒ (S'; T, s')|}
\DP
\hfill\hbox{}

\smallskip

\noindent\hfill
\AXC{\phantom{.}}
\RL{\textsc{IfZeroTrue}\quad if \li{s(a) = 0}}
\UIC{\strut\li|(if_zero a then S else T, s) ⇒ (S, s)|}
\DP
\hfill\hbox{}

\smallskip

\noindent\hfill
\AXC{\phantom{.}}
\RL{\textsc{IfZeroFalse}\quad if \li{s(a) ≠ 0}}
\UIC{\strut\li|(if_zero a then S else T, s) ⇒ (T, s)|}
\DP
\hfill\hbox{}
\end{loesung}
\begin{bewertung}
\begin{itemize}
\item 2 points for \textsc{SeqStep}
\begin{itemize}
\item 1 point for premises
\item 1 point for conclusion
\end{itemize} 
\item 2 points for \textsc{IfZeroTrue}
\begin{itemize}
  \item 1 point for side condition
  \item 1 point for conclusion
\end{itemize}
\item 2 points for \textsc{IfZeroFalse}
\begin{itemize}
  \item 1 point for 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 small-step semantics you specified in subquestion a) above.%
  \nurloesung{\hfill(6~points)}

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

\begin{loesung}
\begin{lstlisting}
  | seq_step (S S' T s s') (hS : SmallStep (S, s) (S', s')) :
    SmallStep (S; T, s) (S'; T, s')
  | ifZero_true (a S T s) (hcond : a s = 0) :
    SmallStep (Stmt.ifZero a S T, s) (S, s)
  | ifZero_false (a S T s) (hcond : a s ≠ 0) :
    SmallStep (Stmt.ifZero a S T, s) (T, s)
\end{lstlisting}
\end{loesung}
\begin{bewertung}
\begin{itemize}
\item 2 points for \li|seq_step|
\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 4| and \li|τ : Type 2| be Lean types. Give the type of
  each of the following Lean terms.\nurloesung{\\
  \noindent\hbox{}\hfill(5~points)}

\begin{lstlisting}
fun (x : σ) (y : σ) ↦ x
Sort 5
fun α : Type ↦ List (ℕ × α)
σ → τ
τ → σ
\end{lstlisting}

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

\newpage

\item We call a \li{NonUnitalSemiring} a type with addition, multiplication,
and a 0 element and where addition is commutative and associative,
multiplication is associative and left and right distributive over addition,
and 0 is the additive identity.

Complete the following \li{class} declaration of \li{NonUnitalSemiring}:

\begin{lstlisting}
universe u

class NonUnitalSemiring (α : Type u) : Type u where
  add           : α → α → α
  mul           :
  zero          : α
  mul_assoc     :
  add_assoc     : ∀a b c, add (add a b) c = add a (add b c)
  left_distrib  :
  right_distrib : ∀a b c, mul (add a b) c = add (mul a c) (mul b c)
  zero_add      : ∀a, add zero a = a
  add_zero      :
  zero_mul      :
  mul_zero      : ∀a, mul a zero = zero
  add_comm      : ∀a b, add a b = add b a
\end{lstlisting}
\nurloesung{\hfill(5~points)}

\begin{loesung} ~~ \\
\begin{lstlisting}
class NonUnitalSemiring (α : Type u) : Type u where
  add           : α → α → α
  mul           : α → α → α
  zero          : α
  mul_assoc     : ∀a b c, mul (mul a b) c = mul a (mul b c)
  add_assoc     : ∀a b c, add (add a b) c = add a (add b c)
  left_distrib  : ∀a b c, mul a (add b c) = add (mul a b) (mul a c)
  right_distrib : ∀a b c, mul (add a b) c = add (mul a c) (mul b c)
  zero_add      : ∀a, add zero a = a
  add_zero      : ∀a, add a zero = a
  zero_mul      : ∀a, mul zero a = zero
  mul_zero      : ∀a, mul a zero = zero
  add_comm      : ∀a b, add a b = add b a
\end{lstlisting} 
\end{loesung}
\begin{bewertung}
\begin{itemize}
\item 1 point for \li{mull}
\item 1 point for the \li{mul_assoc} statement
\item 1 point for the \li{left_distrib} statement
\item 1 point for the \li{add_zero} statement
\item 1 point for the \li{zero_mul} statement
\end{itemize}
\end{bewertung}
\end{enumerate}
\end{aufgabe}

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