%%% 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}{09.10.2024}\\
Xavier Généreux\\
Balazs Toth\\[-1.5em]
\begin{center}
  {\Large \Loes{Solution to the} Second 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$Vector : (α : Type) → ℕ → Type$ be a type constructor.
Let \li$a : ℕ$, \li$g : ℕ → ℕ → ℚ$, and
\li$f : (x : ℕ) → Vector ℕ x$ 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{f a}\nurloesung{\hfill(6~points)}

\begin{loesung}
The type is \li$Vector ℕ a$. The typing derivation is
%
\[\prftree[r]{\textsc{App}$'$}
  {
    \prftree[r]{\textsc{Cst}}
      {\strut\text{\li|\⊢ f : (x : ℕ) → Vector ℕ x|}}
  }
  {
    \prftree[r]{\textsc{Cst}}
      {\strut\text{\li|\⊢ a : ℕ|}}
  }
  {\strut\text{\li|\⊢ f a : Vector ℕ 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{fun x ↦ g x x}\nurloesung{\hfill(8~points)}

\begin{loesung}
The type is \li$ℕ → ℚ$. The typing derivation is
%
\[\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) : ℕ → ℚ|}}\]
\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 ↦ 0|
\end{loesung}
\begin{bewertung}
\begin{itemize}
\item 1 point for \li|fun a|
\item 1 point for \li|0|
\end{itemize}
\end{bewertung}

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

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

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

\begin{loesung}
\li|fun f b c ↦ f (fun a ↦ a) c|
\end{loesung}
\begin{bewertung}
\begin{itemize}
\item 1 point for \li|fun f b c |
\item 1 point for \li|f (fun a ↦ a) c|
\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 [1, 2, 3]|. (There is no need to provide
intermediate steps.)%
\nurloesung{\\ \hfill(2 points)}

\begin{loesung}
\li|[1, 1, 2, 2, 3, 3]|.
\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 stutter_append {α : Type} (xs ys : List α) :
  stutter (xs ++ ys) = stutter xs ++ stutter ys
\end{lstlisting}

\begin{loesung} ~~

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

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

The induction step is
\begin{center}
\li|stutter (x :: xs' ++ ys) = stutter (x :: xs') ++ stutter ys|
\end{center}
The induction hypothesis is
\begin{center}
\li|stutter (xs' ++ ys) = stutter xs' ++ stutter ys|
\end{center}

The goal's left-hand side can be rewritten to \li|stutter (x :: (xs' ++ ys))|
using basic list properties. By definition of \li|stutter|, this is equal to
\li|x :: x :: stutter (xs' ++ ys)|. By the induction hypothesis, this is equal
to \li|x :: x :: (stutter xs' ++ stutter ys)|. By definition of \li|stutter|,
the goal's right-hand side simplifies to the same term. 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}

\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_stutter {α : Type} (xs : List α) :
  List.length (stutter xs) = 2 * List.length xs
\end{lstlisting}

\begin{loesung} ~~

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

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

The induction step is
\begin{center}
\li|List.length (stutter (x :: xs')) = 2 * List.length (x :: xs')|
\end{center}
The induction hypothesis is
\begin{center}
\li|List.length (stutter xs') = 2 * List.length xs'|
\end{center}
The induction step simplifies to
\begin{center}
\li|List.length (stutter xs') + 2 = 2 * List.length xs' + 2|
\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|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|arith|)
\end{itemize}
\end{bewertung}

\end{enumerate}

\newpage

\item Define a Lean function \li|separate| that takes a term and a list and
that returns a list where the term is inserted between each pair of adjacent
elements of the list. For example, \li|separate 0| \li|[1, 2, 3]| should evaluate to \li|[1, 0, 2, 0, 3]|.\nurloesung{\hfill(7~points)}

\begin{loesung}
\begin{lstlisting}
def separate {α : Type} (a : α) : List α → List α
  | []              => []
  | [b]             => [b]
  | b₁ :: b₂ :: bs' => [b₁, a] ++ separate a (b₂ :: bs')
\end{lstlisting}
\end{loesung}
\begin{bewertung}
\begin{itemize}
\item 1 point for ``\li|def separate {α : Type} (a : α)|''
\item 1 point for type
\item 1 point for first equation
\item 1 point for second equation
\item 1 point for LHS of third equation
\item 2 points for RHS of third equation
\end{itemize}
\end{bewertung}
\end{enumerate}
\end{aufgabe}

\begin{aufgabe}{Inductive Predicates}{25}
\vspace*{-2em}
\begin{enumerate}
\item A binary tree is \emph{linear} if all its nodes have at most one
child. Consider the following Lean inductive predicate, which determines
whether a binary tree is linear:

\begin{lstlisting}
inductive Linear {α : Type} : Tree α → Prop
  | nil :
    Linear Tree.nil
  | left (a : α) (l : Tree α) (hl : Linear l) :
    Linear (Tree.node a l Tree.nil)
  | right (a : α) (r : Tree α) (hr : Linear r) :
    Linear (Tree.node a Tree.nil r)
\end{lstlisting}

Recall the \li|mirror| function on binary trees:
\begin{lstlisting}
def mirror {α : Type} : Tree α → Tree α
  | Tree.nil        => Tree.nil
  | Tree.node a l r => Tree.node a (mirror r) (mirror l)
\end{lstlisting}


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

\begin{lstlisting}
theorem Linear_mirror {α : Type} (t : Tree α) (ht : Linear t) :
  Linear (mirror t)
\end{lstlisting}

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

In the \li|nil| case, the goal is
\begin{center}
\li|Linear (mirror Tree.nil)|
\end{center}
This simplifies to \li|Linear Tree.nil|, which is provable using
\li{Linear.nil}.

In the \li|left| case, the goal is
\begin{center}
\li|Linear (mirror (Tree.node a l Tree.nil))|
\end{center}
The induction hypothesis is
\begin{center}
\li|Linear (mirror l)|
\end{center}
The goal simplifies to
\begin{center}
\li|Linear (Tree.node a Tree.nil (mirror l))|
\end{center}
We prove it using \li{Linear.right _ _ ih}, where \li{ih} is the induction hypothesis.

The \li{right} case is analogous.

\end{loesung}
\begin{bewertung}
\begin{itemize}
\item 1 point for ``by (rule) induction''
\item 1 point for ``on \li|ht|''
\item 1 point for statement of \li|nil| case
\item 1 point for proof of \li|nil| case
\item 1 point for statement of \li|left| or \li|right| case
\item 1 point for the statement of the \li|left| or \li|right| induction hypothesis
\item 3 points for the proofs of \li|left| or \li{right} case
  (IH, \li{simp}, and \li{Linear.left/right})
\end{itemize}
\end{bewertung}

\newpage

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

\begin{loesung}
\begin{lstlisting}
inductive Prefix {α : Type} : List α → List α → Prop
  | nil (as : List α) :
    Prefix [] as
  | cons (a : α) (as bs : List α) (hp : Prefix as bs) :
    Prefix (a :: as) (a :: bs)\end{lstlisting}
\end{loesung}
\begin{bewertung}
\begin{itemize}
\item 1 point for ``\li|inductive Prefix {α : 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|ListOver| in Lean that takes a set over
a polymorphic type \li|α| and a list over \li|α| as arguments and that holds if
all the elements of the list belong to the set. For example,
\li|ListOver {4, 7} [7, 4, 7]| should hold, whereas \li|ListOver {7} [6]| should
not hold. You may use the predicate \li|∈| to test for set membership.
\nurloesung{\noindent\hbox{}\hfill(8~points)}

\begin{loesung}
\begin{lstlisting}
inductive ListOver {α : Type} (A : Set α) : List α → Prop
  | nil :
    ListOver A []
  | cons (a : α) (as : List α) (ha : a ∈ A) (has : ListOver A as) :
    ListOver A (a :: as)
\end{lstlisting}
\end{loesung}
\begin{bewertung}
\begin{itemize}
\item 1 point for ``\li|inductive ListOver {α : Type} (A : Set α)|''
\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}{Effectful Programming}{8}

The writer monad is a monad that stores a list of messages to be output to the
console in addition to a value of type \li|α|. In Lean, the writer monad could
be defined as follows:

\begin{lstlisting}
def Writer (α : Type) := α × List String

def Writer.pure {α : Type} (a : α) : Writer α :=
  (a, [])

def Writer.bind {α β : Type} (w : Writer α) (f : α → Writer β) : Writer β :=
  match w with
  | (a, msgs) =>
    match f a with
    | (b, msgs') => (b, msgs ++ msgs')

instance Writer.Pure : Pure Writer :=
  { pure := Writer.pure }

instance Writer.Bind : Bind Writer :=
  { bind := Writer.bind }
\end{lstlisting}
In the definition of \li|Writer.bind|, the purpose of \li|match| is to unfold
the \li|Writer| tuple. It can be useful to have an equivalent representation
using \li|Prod.fst| and \li|Prod.snd|:
\begin{lstlisting}
lemma Writer.bind_prod {α β : Type} (w : Writer α) (f : α → Writer β) :
  w >>= f = (Prod.fst (f (Prod.fst w)), Prod.snd w ++ Prod.snd (f (Prod.fst w))) :=
  by rfl
\end{lstlisting}

\begin{enumerate}
\item In addition to \li|pure| and \li|bind|, the writer monad should offer the
possibility to output messages and to retrieve the list of output messages.
Implement the following two Lean functions:%
\nurloesung{\\ ~ \hfill(3~points)}

\begin{lstlisting}
def Writer.getOutput {α : Type} (w : Writer α) : List String :=





def Writer.output {α : Type} (w : Writer α) (msg : String) : Writer α :=
\end{lstlisting}

\begin{loesung}
\begin{lstlisting}
def Writer.getOutput {α : Type} (w : Writer α) : List String :=
  match w with
  | (a, msgs) => msgs

def Writer.output {α : Type} (w : Writer α) (msg : String) : Writer α :=
  match w with
  | (a, msgs) => (a, msgs ++ [msg])
\end{lstlisting}

\end{loesung}
\begin{bewertung}
\begin{itemize}
\item 1 point for \li|Writer.getOutput|'s body
\item 2 points for \li|Writer.output|'s body
\end{itemize}
\end{bewertung}

\newpage

\item Prove the following law about writer monads. Make sure to follow the proof
guidelines given on page~1. In addition, give detailed steps when unfolding the
definition of monad operators.

Hint: The \li{Writer.bind_prod} lemma presented above may be useful.
\nurloesung{\hfill(5~points)}

\begin{lstlisting}
theorem pure_bind {α β : Type} (a : α) (f : α → Writer β) :
  (pure a >>= f) = f a := 
\end{lstlisting}

\begin{loesung}
Unfolding the \li{bind} operator using \li{Writer.bind_prod} reveals
\begin{lstlisting}
 f a = (Prod.fst (f (Prod.fst (pure a))), Prod.snd (pure a)
       ++ Prod.snd (f (Prod.fst (pure a)))) 
\end{lstlisting}
Since \li|pure a = (a, [])|, we have \li|Prod.fst (pure a) = a| and \li|Prod.snd (pure a) = []|.

This means that
\begin{lstlisting}
f a = (Prod.fst (f a), [] ++ Prod.snd (f a)) 
\end{lstlisting}
which are of course equal since \li|[]| is the identity of append.
\end{loesung}
\begin{bewertung}
\begin{itemize}
\item 2 points for unfolding \li|bind| correctly
\item 1 point for \li|Prod.fst (pure a) = a| 
\item 1 point for \li|Prod.snd (pure a) = []|
\item 1 point for \li|[]| is the identity of append. 
\end{itemize}
\end{bewertung}

%\begin{lstlisting}
%theorem pure_bind {α β : Type} (a : α) (f : α → Writer β) :
 % (pure a >>= f) = f a :=

%theorem bind_pure {α : Type} (w : Writer α) :
%  (w >>= pure) = w
%\end{lstlisting}

%\begin{loesung}
%\begin{itemize}
%\item For the first theorem, the equality simplifies to:
%\begin{lstlisting}
%(match f a with  | (b, msgs') => (b, msgs')) = f a
%\end{lstlisting}
%which is of course equal since \li|match| maps \li|f a| to itself. Note that \li|rfl| alone closes this goal.

%\item For the second theorem, the equality simplifies to:
%\begin{lstlisting}
%(match w with | (a, msgs) => (a, msgs)) = w
%\end{lstlisting}
%which is again equal for the same reason as above. This time, \li|rfl| doesn't close the goal before the simplification using:
%\li|Writer.pure, Writer.Pure, Writer.bind|, and \li|Writer.Bind|.
%\end{itemize}
%\end{loesung}
%\begin{bewertung}
%\begin{itemize}
%\item 2 points for the proof of the first theorem
%\item 2 points for the simplification the equation in the second theorem
%\item 1 point for \li|rfl| in the second theorem 
%\end{itemize}
%\end{bewertung}
\end{enumerate}
\end{aufgabe}

\begin{aufgabe}{Denotational Semantics}{12}
The IF language consists of all the same constructs as the WHILE language
except that it does not include a \li|while| loop:
\begin{lstlisting}
inductive Stmt : Type where
  | skip       : Stmt
  | assign     : String → (State → ℕ) → Stmt
  | seq        : Stmt → Stmt → Stmt
  | ifThenElse : (State → Prop) → Stmt → Stmt → Stmt
\end{lstlisting}
The denotational semantics of the IF language is given below:

\begin{lstlisting}
def denote : Stmt → Set (State × State) 
  | Stmt.skip             => Id
  | Stmt.assign x a       =>
    {st | Prod.snd st = (Prod.fst st)[x ↦ a (Prod.fst st)]} 
  | Stmt.seq S T          => denote S ◯ denote T
  | Stmt.ifThenElse B S T => (denote S ⇃ B) ∪ (denote T ⇃ (fun s ↦ ¬ B s))
\end{lstlisting}
where
\begin{lstlisting}
Id      := {ab | Prod.snd ab = Prod.fst ab}
r ⇃ P   := {ab | ab ∈ r ∧ P (Prod.fst ab)}
r₁ ◯ r₂ := {ac | ∃b, (Prod.fst ac, b) ∈ r₁ ∧ (b, Prod.snd ac) ∈ r₂}
\end{lstlisting}
We also define \li|⟦ ⟧| as syntactic sugar for \li|denote|.

\begin{enumerate}
\item Prove the following equality:
\begin{lstlisting}
⟦Stmt.ifThenElse (fun s ↦ s "x" > 0)
   (Stmt.assign "x" (fun s ↦ s "x" + 1))
   Stmt.skip⟧
=
⟦Stmt.ifThenElse (fun s ↦ s "x" = 0)
   Stmt.skip
   (Stmt.assign "x" (fun s ↦ s "x" + 1))⟧
\end{lstlisting}
Recall that program variables range over natural
numbers.\nurloesung{\hfill(6~points)}

\begin{loesung}
First, on the LHS of the equality, we unfold the semantics of the \li|if|
statements:

\begin{lstlisting}
(⟦Stmt.assign "x" (fun s ↦ s "x" + 1)⟧ ⇃ (fun s => s "x" > 0))
∪ (⟦Stmt.skip⟧ ⇃ (fun s => ¬ s "x" > 0))
\end{lstlisting}

Now consider the RHS:

\begin{lstlisting}
(⟦Stmt.skip⟧ ⇃ (fun s => s "x" = 0))
∪ (⟦Stmt.assign "x" (fun s ↦ s "x" + 1)⟧ ⇃ (fun s => ¬ s "x" = 0))
\end{lstlisting}

Noting that union commutes and that \li|¬ n = 0| is equivalent to \li|n > 0| for natural numbers \li|n|, we conclude that the two sides are equal.
\end{loesung}
\begin{bewertung}
\begin{itemize}
\item 2 points for unfolding the semantics of \li|if| on the LHS
\item 2 points for unfolding the semantics of \li|if| on the RHS
\item 1 point for converting between \li|¬ n > 0| and \li|n = 0|
\item 1 point for commutativity of union
\end{itemize}
\end{bewertung}

\newpage

\item
The \li|denote| function uses tuples in
\li{Set (State × State)}. It is called a \emph{relational} denotational semantics,
and the tuples relate prestates to poststates.
Instead, since the IF language is deterministic and terminating, we could have
defined the semantics as a function from prestates to poststates. Complete the
following definition of a \emph{functional} version of \li{denote}. (The
definition uses the \li|Classical.propDecidable| attribute to enable
noncomputable decidability on every \li|Prop|.)%
\nurloesung{\hfill(6~points)}

\begin{lstlisting}
attribute [instance 0] Classical.propDecidable

noncomputable def denote : Stmt → State → State 
| Stmt.skip             => fun s ↦ s
| Stmt.assign x a       => 
| Stmt.seq S T          => 
| Stmt.ifThenElse B S T =>
\end{lstlisting}

\begin{loesung}
\begin{lstlisting}
noncomputable def denote : Stmt → State → State 
| Stmt.skip             => fun s ↦ s
| Stmt.assign x a       => fun s ↦ s[x ↦ a s]
| Stmt.seq S T          => denote T ∘ denote S
| Stmt.ifThenElse B S T => fun s ↦ if B s then denote S s else denote T s
\end{lstlisting}
\end{loesung}
\begin{bewertung}
\begin{itemize}
\item 2 points for second RHS
\item 2 points for third RHS
\item 2 points for fourth RHS
\end{itemize}
\end{bewertung}
\end{enumerate}
\end{aufgabe}

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

\begin{lstlisting}
fun x : σ ↦ x
τ → σ
Sort 4
σ → τ
\end{lstlisting}

\begin{loesung} ~~ \\
\li|σ → σ| \\
\li|Prop| (or \li|Sort 0|) \\
\li|Type 4| (or \li|Sort 5|) \\
\li|Type| (or \li|Sort 1|)
\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     : ∀a b c, mul (mul a b) c = mul a (mul b c)
  add_assoc     : 
  left_distrib  : ∀a b c, mul a (add b c) = add (mul a b) (mul a c)
  right_distrib : 
  zero_add      : ∀a, add zero a = a
  add_zero      : ∀a, add a zero = a
  zero_mul      :
  mul_zero      : 
  add_comm      : 
\end{lstlisting}
\nurloesung{\hfill(6~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{zero}
\item 1 point for the \li{add_assoc} statement
\item 1 point for the \li{right_distrib} statement
\item 1 point for the \li{zero_mul} statement
\item 1 point for the \li{mul_zero} statement
\item 1 point for the \li{add_comm} statement

\end{itemize}
\end{bewertung}
\end{enumerate}
\end{aufgabe}

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