Add various missing bits to answer key.

1 files changed, 120 insertions, 6 deletions

diff --git a/controle-20240126.tex b/controle-20240126.tex
index 0e3c269..fa0ed60 100644
--- a/controle-20240126.tex
+++ b/controle-20240126.tex
@@ -106,7 +106,7 @@ et $3$ points par exercice et environ $0.75$ points par question du
 problème.
 
 \ifcorrige
-Ce corrigé comporte \textcolor{red}{à remplir} pages (page de garde incluse).
+Ce corrigé comporte 13 pages (page de garde incluse).
 \else
 Cet énoncé comporte 7 pages (page de garde incluse).
 \fi
@@ -202,11 +202,50 @@ que programme (i.e., le comportement du programme associé à la preuve
 par la correspondance de Curry-Howard).
 
 \begin{corrige}
-\textcolor{red}{Corrigé de cet exercice à écrire.  Ce qui suit est un
-  résumé.}  Le $\lambda$-terme est $\lambda(x:A).\,
-\lambda(k:A\Rightarrow B).\, k x$, et le programme transforme $x$ en
-la fonction qui applique une fonction $k$ à $x$, ou, ce qui revient au
-même, il prend successivement $x$ et $k$ et applique $k$ à $x$.
+Voici une preuve complète écrite dans le style « drapeau » :
+\bgroup\normalsize
+\begin{footnotesize}
+\begin{flagderiv}[exercice-2-proof]
+\assume{hypa}{A}{}
+\assume{hypaib}{A\Rightarrow B}{}
+\step{concb}{B}{$\Rightarrow$Élim sur \ref{hypaib} et \ref{hypa}}
+\conclude{subconc}{(A\Rightarrow B) \Rightarrow B}{$\Rightarrow$Int de \ref{hypaib} dans \ref{concb}}
+\conclude{mainconc}{A\Rightarrow (A\Rightarrow B) \Rightarrow B}{$\Rightarrow$Int de \ref{hypaib} dans \ref{subconc}}
+\end{flagderiv}
+\end{footnotesize}
+\egroup
+
+La voici écrite sous forme d'arbre de preuve :
+\begin{footnotesize}
+\[
+\inferrule*[left={$\Rightarrow$Int}]{
+\inferrule*[Left={$\Rightarrow$Int}]{
+\inferrule*[Left={$\Rightarrow$Élim}]{
+\inferrule*[Left={Ax}]{ }{A,\; A\Rightarrow B \vdash A\Rightarrow B}\\
+\inferrule*[Right={Ax}]{ }{A,\; A\Rightarrow B \vdash A}
+}{A, A\Rightarrow B \vdash B}
+}{A \vdash (A\Rightarrow B) \Rightarrow B}
+}{\vdash A\Rightarrow (A\Rightarrow B) \Rightarrow B}
+\]
+\end{footnotesize}
+ou, si on veut donner des noms aux hypothèses et marquer tous les
+termes de preuve intermédiaires :
+\begin{footnotesize}
+\[
+\inferrule*[left={$\Rightarrow$Int}]{
+\inferrule*[Left={$\Rightarrow$Int}]{
+\inferrule*[Left={$\Rightarrow$Élim}]{
+\inferrule*[Left={Ax}]{ }{x:A,\; k:A\Rightarrow B\; \vdash\; k:A\Rightarrow B}\\
+\inferrule*[Right={Ax}]{ }{x:A,\; k:A\Rightarrow B\; \vdash\; x:A}
+}{x:A,\; k:A\Rightarrow B\; \vdash\; kx:B}
+}{x:A \; \vdash \; \lambda(k:A\Rightarrow B).\,kx\; :\; (A\Rightarrow B) \Rightarrow B}
+}{\vdash\; \lambda(x:A).\, \lambda(k:A\Rightarrow B).\,kx\; :\;  A\Rightarrow (A\Rightarrow B) \Rightarrow B}
+\]
+\end{footnotesize}
+Le $\lambda$-terme est donc $\lambda(x:A).\, \lambda(k:A\Rightarrow
+B).\, k x$, et le programme transforme $x$ en la fonction qui applique
+une fonction $k$ à $x$, ou, ce qui revient au même, il prend
+successivement $x$ et $k$ et applique $k$ à $x$.
 \end{corrige}
 
 
@@ -442,6 +481,81 @@ formule proposée avait été démontrable, on aurait trouvé tout
 $\mathbb{R}^2$ (par \emph{correction} de la sémantique des ouverts) :
 ce n'est pas le cas, donc la formule n'est pas démontrable.
 
+\begin{center}
+\lineskip=1explus5ex
+\begin{tabular}{c}
+\begin{tikzpicture}
+\begin{scope}
+\clip (-1.5,-1.5) -- (1.5,-1.5) -- (1.5,1.5) -- (-1.5,1.5) -- cycle;
+\fill[gray] (1.5,1.5) -- (1.5,0) -- (0,0) -- (-0.866,1.5) -- cycle;
+\end{scope}
+\draw[->] (-1.55,0)--(1.55,0) node[right]{$x$};
+\draw[->] (0,-1.55)--(0,1.55) node[above]{$y$};
+\end{tikzpicture}
+\\ $U$
+\end{tabular}
+\penalty0
+\begin{tabular}{c}
+\begin{tikzpicture}
+\begin{scope}
+\clip (-1.5,-1.5) -- (1.5,-1.5) -- (1.5,1.5) -- (-1.5,1.5) -- cycle;
+\fill[gray] (-1.5,1.5) -- (-0.866,1.5) -- (0,0) -- (-0.866,-1.5) -- (-1.5,-1.5) -- cycle;
+\end{scope}
+\draw[->] (-1.55,0)--(1.55,0) node[right]{$x$};
+\draw[->] (0,-1.55)--(0,1.55) node[above]{$y$};
+\end{tikzpicture}
+\\ $V$
+\end{tabular}
+\penalty0
+\begin{tabular}{c}
+\begin{tikzpicture}
+\begin{scope}
+\clip (-1.5,-1.5) -- (1.5,-1.5) -- (1.5,1.5) -- (-1.5,1.5) -- cycle;
+\fill[gray] (1.5,-1.5) -- (-0.866,-1.5) -- (0,0) -- (1.5,0) -- cycle;
+\end{scope}
+\draw[->] (-1.55,0)--(1.55,0) node[right]{$x$};
+\draw[->] (0,-1.55)--(0,1.55) node[above]{$y$};
+\end{tikzpicture}
+\\ $W$
+\end{tabular}
+\penalty-1000
+\begin{tabular}{c}
+\begin{tikzpicture}
+\begin{scope}
+\clip (-1.5,-1.5) -- (1.5,-1.5) -- (1.5,1.5) -- (-1.5,1.5) -- cycle;
+\fill[gray] (-1.5,1.5) -- (-0.866,1.5) -- (0,0) -- (1.5,0) -- (1.5,-1.5) -- (-1.5,-1.5) -- cycle;
+\end{scope}
+\draw[->] (-1.55,0)--(1.55,0) node[right]{$x$};
+\draw[->] (0,-1.55)--(0,1.55) node[above]{$y$};
+\end{tikzpicture}
+\\ $\dottedneg U$
+\end{tabular}
+\penalty0
+\begin{tabular}{c}
+\begin{tikzpicture}
+\begin{scope}
+\clip (-1.5,-1.5) -- (1.5,-1.5) -- (1.5,1.5) -- (-1.5,1.5) -- cycle;
+\fill[gray] (1.5,-1.5) -- (-0.866,-1.5) -- (0,0) -- (-0.866,1.5) -- (1.5,1.5) -- cycle;
+\end{scope}
+\draw[->] (-1.55,0)--(1.55,0) node[right]{$x$};
+\draw[->] (0,-1.55)--(0,1.55) node[above]{$y$};
+\end{tikzpicture}
+\\ $\dottedneg V$
+\end{tabular}
+\penalty0
+\begin{tabular}{c}
+\begin{tikzpicture}
+\begin{scope}
+\clip (-1.5,-1.5) -- (1.5,-1.5) -- (1.5,1.5) -- (-1.5,1.5) -- cycle;
+\fill[gray] (1.5,1.5) -- (1.5,0) -- (0,0) -- (-0.866,-1.5) -- (-1.5,-1.5) -- (-1.5,1.5) -- cycle;
+\end{scope}
+\draw[->] (-1.55,0)--(1.55,0) node[right]{$x$};
+\draw[->] (0,-1.55)--(0,1.55) node[above]{$y$};
+\end{tikzpicture}
+\\ $\dottedneg W$
+\end{tabular}
+\end{center}
+
 \emph{Sémantique de la réalisabilité :} Supposons qu'il existe un
 \emph{même} programme $e$ qui réalise la formule qu'on considère
 quelles que soient les parties $P,Q,R \subseteq \mathbb{N}$ mises à la