%% /home/plescann/MIM-1/LOGIQUE/LAMBDA/transp.tex

%% Time-stamp: <modifié par Pierre Lescanne le 20 Jan 2003 à 10h07>

\documentclass[%
  slidesonly,%  Pour sortir les transparents seuls
  semrot,%      Permettre des rotations eventuelles
  semhelv,%    Helvetica
  a4%           A4 paper
  ]{seminar}

\usepackage{fancybox}
\usepackage[francais]{babel}
\usepackage[latin1]{inputenc}
\usepackage{color}
%\usepackage{stmaryrd,amssymb}
%\usepackage[dvips]{graphicx}
%\usepackage{amsmath}            % nice mathematics
\usepackage[all]{xy}
\usepackage{qsymbols}
\usepackage{prooftree}

%% Time-stamping  
%% compute the time in hours and minutes; 
 \newcount\timehh\newcount\timemm \timehh=\time 
 \divide\timehh by 60 \timemm=\time
 \count255=\timehh\multiply\count255 by -60 \advance\timemm by \count255
 \newcommand{\timestamp}
 { {\protect\small\sl\today\ -- 
 \ifnum\timehh<10 0\fi\number\timehh\,h\,
   \ifnum\timemm<10 0\fi\number\timemm}}
                                          % avec dvips

\def\printlandscape{\special{landscape}}    % pour sortir en landscape
                                            % avec dvips

\slidesmag{5}
\articlemag{1}

\rotateheaderstrue       % si tu combines slide et slide*


\title{\color{red}{\textit{Lambda-calcul simplement typé}}}

\author{}

\date{}

\pagestyle{}

\slidestyle{empty}

\slideframe{}   

\input{mes_couleurs}

\newcommand{\Ra}{\ensuremath{\Rightarrow}}
\newcommand{\fleche}{\rightarrow}
\newcommand{\et}{\mathop{\&}}
\newcommand{\sh}{\mathop{|}}
\newcommand{\eqa}{\mathop{\equiv_\alpha}}
\newcommand{\Y}{\mathsf{Y}}
\newcommand{\ali}{\newline\hspace*{20pt}}
\renewcommand{\phi}{\varphi}
%% <...> are angle brackets.
\mathcode`\<=\string"4268 \mathcode`\>=\string"5269 %



\newcommand{\inferTwoLabel}[4]{
{#1} \quad 
 \bl{\begin{array}{c}
   #2 \hspace{2em} #3\\
   \hline \noalign{\vskip 1pt}#4
  \end{array}}}

\newcommand{\leafLabel}[2]{
 {#1} \quad
  \bl{\begin{array}{c}
  #2
  \end{array}}}

\newcommand{\inferLabel}[3]{
    {#1} \quad 
    \bl{\begin{array}{c}
      #2\\
      \hline \noalign{\vskip 1pt}#3
    \end{array}
  }}

 \newcommand{\inferTwo}[3]{\bl{
 \begin{array}{c}
   #1 \hspace{2em} #2\\
   \hline \noalign{\vskip 1pt}#3
  \end{array}}}

 \newcommand{\infer}[2]{\bl{
 \begin{array}{c}
   #1\\
   \hline \noalign{\vskip 1pt}#2
  \end{array}}}
    
\newenvironment{displaymathbleu}%
  {\begin{displaymath}\color{blue}}
  {\end{displaymath}}

\newenvironment{eqnarraybleu}%
  {\begin{color}{blue}\begin{eqnarray*}}
  {\end{eqnarray*}\end{color}}

%% ==============================================================
%%                   Reductions and other relations
%% ==============================================================

\newcommand{\ra}{\xymatrix{\ar@{>}[r] &}}
\newcommand{\ranorm}{\xymatrix{\ar@{>>|}[r] &}}
\newcommand{\rara}{\xymatrix{\ar@{>>}[r] &}}
\newcommand{\longequiv}{\xymatrix{\ar@3{-}[r] &}}

%%%%%%%%%%%%%%%%%%%% iteration of arrows  %%%%%%%%%%%%%%%%%%%%
\newcommand{\rastar}{\rasup{*}}
\newcommand{\raplus}{\rasup{+}}

%%%%%%%%%%%%%%%%%%%% fleches avec souscrit et superscrit %%%%%%%%%%%%%
% par exemple -- B, p --> s'ecrit \rasub{B,p}

\newcommand{\rasub}[1]{\xymatrix{\ar@{>}[r]_{#1} &}}
\newcommand{\ranormsub}[1]{\xymatrix{\ar@{>>|}[r]_{#1} &}}
\newcommand{\rarasub}[1]{\xymatrix{\ar@{>>}[r]_{#1} &}}
\newcommand{\rasup}[1]{\xymatrix{\ar@{>}[r]^{#1} &}}
\newcommand{\rarasup}[1]{\xymatrix{\ar@{>>}[r]^{#1} &}}
\newcommand{\rasupsub}[2]{\xymatrix{\ar@{>}[r]^{#1}_{#2} &}}
\newcommand{\rarasupsub}[2]{\xymatrix{\ar@{>>}[r]^{#1}_{#2} &}}
\newcommand{\conv}[1]{\xymatrix{\ar@{<<->>}[r]_{#1} &}}

%%%%%%%%%%%%%%%%%%%% Les fleches %%%%%%%%%%%%%

\newcommand{\rabeta}{\rasub{\beta}}
\newcommand{\rarabeta}{\rarasub{\beta}}
\newcommand{\raR}{\rasub{R}}
\newcommand{\raraR}{\rarasub{R}}
\newcommand{\plusararR}{\xymatrix{&\ar@{>>}[l]^{R}_+}}
\newcommand{\plusraraR}{\rarasupsub{+}{R}}
\newcommand{\rapar}{\xymatrix @ -1.5pc {\ar@{>}[rr]&||&}}
\newcommand{\rarapar}{\xymatrix @ -1.5pc {\ar@{>>}[rr]&||&}}

%%%%%%%%%%%%%%%%%% Headings %%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\heading}[1]{%
{\color{vertfonce}\bf\large #1}{\color{yellow}\\\rule{\textwidth}{2pt}}
}

\newcommand{\subheading}[1]{%
  \begin{center}
    \color{green}{\bf\Ovalbox{#1}}
  \end{center}}

\begin{document}

%------------------------------------------------------
\begin{slide}
  \maketitle \addtocounter{slide}{-1} \slidepagestyle{empty}


\vfill 

\hfill\textit{\footnotesize version du \timestamp}

\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Le paradoxe du barbier} %
  \bleu{\Omega `= (`l x . x x) (`l x . x x)} et \bleu{\Y `= `l f . (`l
    x f (x x))~(`l x f (x x)) } contiennent des termes qui
  s'appliquent à eux-mêmes.

Le \rouge{paradoxe du barbier} est:

\begin{quotation}
  \verdir{Le barbier rase tous ceux qui ne se rasent pas eux-mêmes. \ali
    {\color{mauve} Qui rase le barbier} ?}
\end{quotation}

Pour éviter les paradoxes, on cherche à éviter de tels termes.

On va donc \rouge{typer} les termes.

Typer est aussi bien pour la programmation.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les objectifs du typage}%
Le typage a donc deux objectifs:
\begin{itemize}
\item préserver la correction, \verdir{rien de mauvais ne peut arriver},
\item préserver la terminaison, \verdir{toutes les réductions se terminent}. 
\end{itemize}
\vspace*{8pt}
En $\lambda$-calcul la \rouge{terminaison} s'appelle la \rouge{normalisation forte}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les environnements} 

Il faut typer les variables libres, il faut donc faire des \rouge{hypothèses
sur les types} de ces variables.

D'où la notion d'\rouge{environnement}.

Un environnement est un ensemble d'association de types à des variables.

\begin{displaymathbleu}
  \label{eq:env}
  \Gamma \equiv x_1:\sigma_1,...,x_n:\sigma_n
\end{displaymathbleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les types} 
Un \rouge{jugement} est l'affirmation du type \bleu{\sigma} d'un terme
\bleu{M} sous un certain environnement \bleu{\Gamma}:
\bl{
\begin{displaymath}
  \label{eq:jug}
  \Gamma \vdash M:\sigma
\end{displaymath}}
Les types sont
\begin{itemize}
\item soit des types de base \bleu{o},
\item soit des types applications \bleu{\sigma \fleche \tau}.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les règles} 
\[\leafLabel{\mbox{(Var)}}{\Gamma, x:\sigma \vdash x:\sigma}\]

\[\inferLabel{\mbox{(Abs)}}{\Gamma, x:\sigma \vdash
  M:\tau}{\Gamma\vdash \lambda x . M:\sigma\fleche\tau}\]

\[\inferTwoLabel{\mbox{(App)}}{\Gamma\vdash
  M:\sigma\fleche\tau}{\Gamma\vdash N:\sigma}{\Gamma\vdash M N :
  \tau}\]

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Exercices} 
Typez les termes 

\bleu{B\equiv \lambda x y z. x (y z)}, 

\bleu{I \equiv \lambda x. x},

\bleu{C\equiv \lambda x y z. x z y}, 

\bleu{K \equiv \lambda x y . x}, 

\bleu{S \equiv \lambda x y z . x z (y z)}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Exercices (suite)} 

\vspace*{20pt}

\begin{enumerate}
\item Typez \bleu{I I \equiv (\lambda x. x)(\lambda x. x)}.

  
\item 
  Typez \bleu{\textbf{2}\textbf{2} \equiv (\lambda f x. f(f x))
    (\lambda f x. f(f x))}.

\item A-t-on le même type pour \bleu{I} (resp. \bleu{\textbf{2}}) dans 
  chaque cas?
\end{enumerate}

\verdir{Conclusion :}  Le système de \rouge{types simples} n'est pas assez général.  Il
ne permet d'affecter un type unique à chaque terme.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\framebox{\parbox{8.5cm}{Si \bleu{\Gamma, x:\sigma \vdash M:\tau} et
    \bleu{\Gamma\vdash N:\sigma} alors \bleu{\Gamma\vdash
      M[x:=N]:\tau}}}

\rouge{Démonstration :}  Par induction sur \bleu{M}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\framebox{\parbox{8.5cm}{Si \bleu{\Gamma, x:\sigma \vdash M:\tau} et
    \bleu{\Gamma\vdash N:\sigma} alors \bleu{\Gamma\vdash
      M[x:=N]:\tau}}}

\rouge{Démonstration :}  Par induction sur \bleu{M}.

\rouge{$\bullet$} Si \bleu{M \equiv y} alors \bleu{\Gamma} contient
\bleu{y:\tau} et \bleu{M[x:=N]\equiv M\equiv y} donc le résultat
qui   est \bleu{\Gamma\vdash y:\tau} est clair.

\rouge{$\bullet$} Si \bleu{M \equiv x} alors \bleu{\tau=\sigma} et \bleu{M[x:=N]\equiv
    N} et le résultat est l'une des hypothèses.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\framebox{\parbox{8.5cm}{Si \bleu{\Gamma, x:\sigma \vdash M:\tau} et
    \bleu{\Gamma\vdash N:\sigma} alors \bleu{\Gamma\vdash
      M[x:=N]:\tau}}}

\rouge{Démonstration :}  Par induction sur \bleu{M}.

 \rouge{$\bullet$}  Si \bleu{M \equiv P~Q} alors par (App) pour un certain \bleu{\tau'}, on a
 \begin{itemize}
 \item \bleu{\Gamma, x:\sigma \vdash P:\tau'\rightarrow \tau} duquel
   on tire par induction \bleu{\Gamma\vdash P[x:=N]:\tau'\rightarrow
     \tau}
 \item et \bleu{\Gamma, x:\sigma \vdash Q:\tau'} duquel on tire par
   induction \bleu{\Gamma\vdash Q[x:=N]:\tau'}.
\end{itemize}
Donc par (App) \bleu{\Gamma\vdash
      (P~Q)[x:=N]:\tau} puisque \bleu{(P~Q)[x:=N]\equiv P[x:=N]~Q[x:=N]}.

\rouge{$\bullet$} Le cas \bleu{M \equiv \lambda x.P} est similaire.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Réduction du sujet} 
\rouge{Lemme} \verdir{Réduction du sujet}

La $\beta$-réduction préserve le type.

\framebox{\parbox{7.5cm}{Si \bleu{\Gamma \vdash M:\sigma} et si
    \bleu{M\rabeta N} alors \bleu{\Gamma \vdash N:\sigma}.}}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\framebox{\parbox{7.5cm}{Si \bleu{\Gamma \vdash M:\sigma} et si
    \bleu{M\rabeta N} alors \bleu{\Gamma \vdash N:\sigma}.}}

\rouge{Démonstration :}  Par induction sur la définition de
\bleu{M\rabeta N}.  
\begin{itemize}
\item \rouge{$M\equiv (\lambda x.M_1) M_2$} \\\bleu{\Gamma\vdash
    (\lambda x .M_1) M_2:\sigma} vient de \bleu{\Gamma, x:\tau
    \vdash M_1:\sigma} et de \bleu{\Gamma \vdash M_2:\tau}.\\
D'autre part \bleu{N\equiv M_1[x:=M_2]}\\ or d'après le lemme
\bleu{\Gamma\vdash M_1[x:=M_2]:\sigma}.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\framebox{\parbox{7.5cm}{Si \bleu{\Gamma \vdash M:\sigma} et si
    \bleu{M\rabeta N} alors \bleu{\Gamma \vdash N:\sigma}.}}

\rouge{Démonstration :}  Par induction sur la définition de
\bleu{M\rabeta N}.  
\begin{itemize}
\item \rouge{$M\equiv (\lambda x.M_1) M_2$} \\\bleu{\Gamma\vdash
    (\lambda x .M_1) M_2:\sigma} vient de \bleu{\Gamma, x:\tau
    \vdash M_1:\sigma} et de \bleu{\Gamma \vdash M_2:\tau}.\\
D'autre part \bleu{N\equiv M_1[x:=M_2]}\\ or d'après le lemme
\bleu{\Gamma\vdash M_1[x:=M_2]:\sigma}.
\item \rouge{$M\equiv M_1 M_2$} avec  \rouge{$N\equiv N_1 M_2$} et
  \rouge{$M_1\rabeta N_1$}.\\
\bleu{\Gamma\vdash M} vient de \bleu{\Gamma\vdash
  M_1:\tau\fleche\sigma} et \bleu{\Gamma\vdash M_2:\tau}, \\par
induction  \bleu{\Gamma\vdash
  N_1:\tau\fleche\sigma} et donc \bleu{\Gamma\vdash N_1 M_2:\sigma}.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\framebox{\parbox{7.5cm}{Si \bleu{\Gamma \vdash M:\sigma} et si
    \bleu{M\rabeta N} alors \bleu{\Gamma \vdash N:\sigma}.}}

\rouge{Démonstration :}  Par induction sur la définition de
\bleu{M\rabeta N}.  
\begin{itemize}
\item \rouge{$M\equiv (\lambda x .M_1) M_2$} \\\bleu{\Gamma\vdash
    (\lambda x .M_1) M_2:\sigma} vient de \bleu{\Gamma, x:\tau
    \vdash M_1:\sigma} et de \bleu{\Gamma \vdash M_2:\tau}.\\
D'autre part \bleu{N\equiv M_1[x:=M_2]}\\ or d'après le lemme
\bleu{\Gamma\vdash M_1[x:=M_2]:\sigma}.
\item \rouge{$M\equiv M_1 M_2$} avec  \rouge{$N\equiv N_1 M_2$} et
  \rouge{$M_1\rabeta N_1$}.\\
\bleu{\Gamma\vdash M} vient de \bleu{\Gamma\vdash
  M_1:\tau\fleche\sigma} et \bleu{\Gamma\vdash M_2:\tau}, \\par
induction  \bleu{\Gamma\vdash
  N_1:\tau\fleche\sigma} et donc \bleu{\Gamma\vdash N_1 M_2:\sigma}.
\item \rouge{Les autres cas sont similaires.}
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Commentaires}
\begin{itemize}
\item Si un terme est d'un certain type, \rouge{il n'en sortira pas} par
  $\beta$-réduction. 
\item Si un terme a une forme normale et s'il a un type, alors \rouge{sa
  forme normale a ce type}.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}

\vspace*{60pt}

  \begin{center}
    {\Large \bf \color{mauve}{\textit{La correspondance de Curry-Howard}}}
\end{center}
\vfill
\begin{quote}
  La mathématique c'est l'art de donner le même nom à des choses
  différentes.    \rightline{\rouge{Henri Poincaré}}
\end{quote}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{La correspondance de Curry-Howard} 


\begin{small}
\begin{math}
\begin{array}{c @{\qquad} |  @{\qquad} c}
\leafLabel{\mbox{\verdir{(Var)}}}{\Gamma,\rouge{ x:}~\sigma \vdash \rouge{x:}~\sigma} & \bl{\Gamma, p \vdash p}\\

\inferLabel{\mbox{\verdir{(Abs)}}}{\Gamma, \rouge{x:}~\sigma \vdash
 \rouge{M:}~\tau}{\Gamma\vdash \rouge{\lambda x . M:}~\sigma\fleche\tau} 
& \inferLabel{\verdir{\Ra I}}{\Gamma, p \vdash q}{\Gamma\vdash p\Ra q} \\

\inferTwoLabel{\mbox{\verdir{(App)}}}{\Gamma\vdash
 \rouge{M:}~\sigma\fleche\tau}{\Gamma\vdash \rouge{N:}~\sigma}{\Gamma\vdash \rouge{M N :}~
  \tau} & \inferTwoLabel{\verdir{\Ra E}}{\Gamma\vdash p\Ra q}{\Gamma\vdash
  p}{\Gamma\vdash q} \\
\end{array}
\end{math}
\end{small}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La correspondance de Curry-Howard}
Dans \bleu{\Gamma\vdash \rouge{M:}~\sigma}, 
\begin{itemize}
\item  \rouge{M:} est une \rouge{annotation} qui est le \rouge{«terme de preuve»},

\item \bleu{\sigma} peut-être vu comme un \rouge{type} ou comme une \rouge{proposition}.
\end{itemize}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La preuve de B}
 \begin{scriptsize}
\bl{\[%
\newcommand{\IIII}%
{\inferTwoLabel{\Ra E}%
{(p \Ra q),\ (r \Ra p), r \vdash p\Ra q}%
{\mathcal{\verdir{D}}}{(p \Ra q),\ (r \Ra p), r \vdash q}}
%
\newcommand{\III}%
{\infer{\IIII}{(p \Ra q),\ (r \Ra p) \vdash r \Ra q}}
%
\newcommand{\II}%
{\infer{\III}{(p \Ra q) \vdash (r \Ra p) \Ra r \Ra q}}
%
\newcommand{\IO}%
{\infer{\II}{\vdash(p \Ra q) \Ra (r \Ra p) \Ra r \Ra q}}
%
\IO
\]}
\end{scriptsize}
où $\mathcal{\verdir{D}}$ est
\begin{scriptsize}
\bl{\[%
\newcommand{\V}%
{\inferTwoLabel{\Ra E}%
{(p \Ra q),\ (r \Ra p), r \vdash r \Ra p}%
{(p \Ra q),\ (r \Ra p), r \vdash r}
{(p \Ra q),\ (r \Ra p), r \vdash p}}
%
\V
\]}
\end{scriptsize}
\vfill
\end{slide}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La preuve de B annotée}
 \begin{scriptsize}
\bl{\[%
\newcommand{\IIII}%
{\inferTwoLabel{\Ra E}%
{ \rouge{x:~} (p \Ra q),\ \rouge{y:~} (r \Ra p), \rouge{z:~} r \vdash \rouge{x:~} p\Ra q}%
{\mathcal{\verdir{D}}}{\rouge{x:~} (p \Ra q),\ \rouge{y:~} (r \Ra p), \rouge{z:~} r \vdash \rouge{x~(y~z):~}q}}
%
\newcommand{\III}%
{\infer{\IIII}{\rouge{x:~} (p \Ra q),\ \rouge{y:~} (r \Ra p) \vdash \rouge{\lambda z .x~(y~z) :~}r \Ra q}}
%
\newcommand{\II}%
{\infer{\III}{\rouge{x:~} (p \Ra q) \vdash \rouge{\lambda y z .x~(y~z) :~}(r \Ra p) \Ra r \Ra q}}
%
\newcommand{\IO}%
{\infer{\II}{\vdash\rouge{\lambda x y z .x~(y~z) :~} (p \Ra q) \Ra (r \Ra p) \Ra r \Ra q}}
%
\IO
\]}
\end{scriptsize}
où $\mathcal{\verdir{D}}$ est
\begin{scriptsize}
\bl{\[%
\newcommand{\V}%
{\inferTwoLabel{\Ra E}%
{\rouge{x:~} (p \Ra q),\ \rouge{y:~}(r \Ra p), \rouge{z:~}r \vdash \rouge{y:~}r \Ra p}%
{\rouge{x:~} (p \Ra q),\ \rouge{y:~}(r \Ra p), \rouge{z:~}r \vdash \rouge{z:~}r}
{\rouge{x:~} (p \Ra q),\ \rouge{y:~}(r \Ra p), \rouge{z:~}r \vdash \rouge{y~z:~}p}}
%
\V
\]}
\end{scriptsize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La preuve de B annotée}
 \begin{scriptsize}
\bl{\[%
\newcommand{\IIII}%
{\inferTwoLabel{\Ra E}%
{ \rouge{x:~} (p \Ra q),\ \rouge{y:~} (r \Ra p), \rouge{z:~} r \vdash \rouge{x:~} p\Ra q}%
{\mathcal{\verdir{D}}}{\rouge{x:~} (p \Ra q),\ \rouge{y:~} (r \Ra p), \rouge{z:~} r \vdash \rouge{x~(y~z):~}q}}
%
\newcommand{\III}%
{\infer{\IIII}{\rouge{x:~} (p \Ra q),\ \rouge{y:~} (r \Ra p) \vdash \rouge{\lambda z .x~(y~z) :~}r \Ra q}}
%
\newcommand{\II}%
{\infer{\III}{\rouge{x:~} (p \Ra q) \vdash \rouge{\lambda y z .x~(y~z) :~}(r \Ra p) \Ra r \Ra q}}
%
\newcommand{\IO}%
{\infer{\II}{\vdash\rouge{\lambda x y z .x~(y~z) :~} (p \Ra q) \Ra (r \Ra p) \Ra r \Ra q}}
%
\IO
\]}
\end{scriptsize}
où $\mathcal{\verdir{D}}$ est
\begin{scriptsize}
\bl{\[%
\newcommand{\V}%
{\inferTwoLabel{\Ra E}%
{\rouge{x:~} (p \Ra q),\ \rouge{y:~}(r \Ra p), \rouge{z:~}r \vdash \rouge{y:~}r \Ra p}%
{\rouge{x:~} (p \Ra q),\ \rouge{y:~}(r \Ra p), \rouge{z:~}r \vdash \rouge{z:~}r}
{\rouge{x:~} (p \Ra q),\ \rouge{y:~}(r \Ra p), \rouge{z:~}r \vdash \rouge{y~z:~}p}}
%
\V
\]}
\end{scriptsize}
La preuve du lemme \bleu{B} est le terme \rouge{$B$}!
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Simplification de preuves}
La preuve
\begin{footnotesize}
\begin{displaymathbleu}
  \prooftree %
     \prooftree % -
          \prooftree % --
          (p "=>" p), q "|-" p "=>" p %
          \justifies (p "=>" p) "|-" q "=>" p "=>" p %
          \using \rouge{(\Ra I)}
          \endprooftree % --
     \justifies "|-" (p "=>" p) "=>" q "=>" p "=>" p \using
      \rouge{(\Ra I)}
      \endprooftree % -
      \quad
      \prooftree % -
      p "|-" p \justifies "|-" p "=>" p \using \rouge{(\Ra I)}
      \endprooftree % -
      \justifies "|-" q "=>" p "=>" p \using \rouge{(\Ra E)}
  \endprooftree %
\end{displaymathbleu}
\end{footnotesize}
peut être réduite
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Simplification de preuves}
En effet, on fait une introduction immédiatement suivie d'une
élimination :
\begin{footnotesize}
\begin{displaymathbleu}
  \prooftree %
     \prooftree % -
          \prooftree % --
          (p "=>" p), q "|-" p "=>" p %
          \justifies  (p "=>" p) "|-" {\color{mauve} q "=>" p "=>" p} %
          \using \rouge{(\Ra I)}
          \endprooftree % --
     \justifies "|-" (p "=>" p) "=>" q "=>" p "=>" p \using
      \rouge{(\Ra I)}
      \endprooftree % -
      \quad
      \prooftree % -
      p "|-" p \justifies "|-" p "=>" p \using \rouge{(\Ra I)}
      \endprooftree % -
      \justifies "|-" {\color{mauve} q "=>" p "=>" p} %
      \using \rouge{(\Ra E)}
  \endprooftree %
\end{displaymathbleu}
\end{footnotesize}
On peut obtenir une preuve de \bleu{"|-" q "=>" p "=>" p} à partir de
la preuve de \bleu{(p "=>" p) "|-" q "=>" p "=>" p}. 

Pour cela, il suffit de remplacer chaque occurrence de l'utilisation de
l'hypothèse \bleu{(p "=>" p)} par sa preuve.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Simplification de preuves}
En utilisant cette remarque
\begin{footnotesize}
\begin{displaymathbleu}
  \prooftree %
     \prooftree % -
          \prooftree % --
          (p "=>" p), q "|-" p "=>" p %
          \justifies (p "=>" p) "|-"  {\color{mauve} q "=>" p "=>" p} %
          \using \rouge{(\Ra I)}
          \endprooftree % --
     \justifies "|-" (p "=>" p) "=>" q "=>" p "=>" p \using
      \rouge{(\Ra I)}
      \endprooftree % -
      \quad
      \prooftree % -
      p "|-" p \justifies "|-" p "=>" p \using \rouge{(\Ra I)}
      \endprooftree % -
      \justifies "|-" {\color{mauve} q "=>" p "=>" p} %
      \using \rouge{(\Ra E)}
  \endprooftree %
\end{displaymathbleu}
\end{footnotesize}
donne
\begin{footnotesize}
\begin{displaymathbleu}
  \prooftree %
      \prooftree % -
      q, p "|-" p 
      \justifies q "|-" p "=>" p %
      \using \rouge{(\Ra I)}
      \endprooftree % -
      \justifies "|-" q "=>" p "=>" p %
      \using \rouge{(\Ra I)}
  \endprooftree %
\end{displaymathbleu}
\end{footnotesize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Simplification de preuves}
Donc avec les annotations par les termes de preuve
\begin{footnotesize}
\begin{displaymathbleu}
  \prooftree %
     \prooftree % -
          \prooftree % --
          \rouge{x :}~ (p "=>" p), \rouge{y :}~ q "|-" p "=>" p %
          \justifies \rouge{x :}~ (p "=>" p) "|-"  \rouge{`l y. x :}~q "=>" p "=>" p %
          \using \verdir{(Abs)}
          \endprooftree % --
     \justifies "|-" \rouge{`l x y. x :}~ (p "=>" p) "=>" q "=>" p "=>" p %
     \using \verdir{(Abs)}
      \endprooftree % -
      \quad
      \prooftree % -
       \rouge{z :}~  p "|-" \rouge{z :}~ p %
      \justifies "|-" \rouge{`l z . z : } p "=>" p \using \verdir{(Abs)}
      \endprooftree % -
      \justifies  "|-" \rouge{(`l x y. x)~ (`l z . z) :}~ q "=>" p "=>" p %
      \using \verdir{(App)}
  \endprooftree %
\end{displaymathbleu}
\end{footnotesize}
donne
\begin{footnotesize}
\begin{displaymathbleu}
  \prooftree %
      \prooftree % -
      \rouge{y :}~q, \rouge{z :}~p "|-" p 
      \justifies \rouge{y :}~q "|-" \rouge{`l z . z :}~p "=>" p %
      \using \verdir{(Abs)}
      \endprooftree % -
      \justifies "|-" \rouge{`l y z . z :}~q "=>" p "=>" p %
      \using \verdir{(Abs)}
  \endprooftree %
\end{displaymathbleu}
\end{footnotesize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Simplification de preuves}
Donc avec les annotations par les termes de preuve
\begin{footnotesize}
\begin{displaymathbleu}
  \prooftree %
     \prooftree % -
          \prooftree % --
          \rouge{x :}~ (p "=>" p), \rouge{y :}~ q "|-" p "=>" p %
          \justifies \rouge{x :}~ (p "=>" p) "|-"  \rouge{`l y. x :}~q "=>" p "=>" p %
          \using \verdir{(Abs)}
          \endprooftree % --
     \justifies "|-" \rouge{`l x y. x :}~ (p "=>" p) "=>" q "=>" p "=>" p %
     \using \verdir{(Abs)}
      \endprooftree % -
      \quad
      \prooftree % -
       \rouge{z :}~  p "|-" \rouge{z :}~ p %
      \justifies "|-" \rouge{`l z . z : } p "=>" p \using \verdir{(Abs)}
      \endprooftree % -
      \justifies  "|-" \rouge{(`l x y. x)~ (`l z . z) :}~ q "=>" p "=>" p %
      \using \verdir{(App)}
  \endprooftree %
\end{displaymathbleu}
\end{footnotesize}
donne
\begin{footnotesize}
\begin{displaymathbleu}
  \prooftree %
      \prooftree % -
      \rouge{y :}~q, \rouge{z :}~p "|-" p 
      \justifies \rouge{y :}~q "|-" \rouge{`l z . z :}~p "=>" p %
      \using \verdir{(Abs)}
      \endprooftree % -
      \justifies "|-" {\color{mauve} (`l y. x)[x:= `l z . z]} `= \rouge{`l y z . z :}~q "=>" p "=>" p %
      \using \verdir{(Abs)}
  \endprooftree %
\end{displaymathbleu}
\end{footnotesize}
La $`b$-réduction correspond à la simplification des preuves.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Simplification de preuves}
\begin{displaymathbleu}
  \prooftree
      \prooftree
          \prooftree
          {\cal D}
          \justifies  `f, `G "|-"  `j 
          \endprooftree
      \justifies `G "|-"  `f "=>" `j %
      \using \rouge{("=>" I)} %
      \endprooftree
      \quad 
      \prooftree 
      {\cal D'}
      \justifies `G "|-" `f
      \endprooftree
      \justifies `G "|-" `j 
      \using \rouge{("=>" E)}
  \endprooftree
\end{displaymathbleu}
se transforme en
\begin{displaymathbleu}
      \prooftree %
      {\cal D''} 
        \justifies `G "|-" `j %
    \endprooftree %
\end{displaymathbleu}
\bleu{\cal D''} est la preuve \bleu{\cal D} dans laquelle toutes les
utilisations de l'hypothèse \bleu{`f} sont remplacées par la preuve
\bleu{\cal D} de \bleu{`f}.  %
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Simplification de preuves}
\begin{displaymathbleu}
  \prooftree
      \prooftree
          \prooftree
          {\cal D}
          \justifies  \rouge{x :}~`f, `G "|-"  \rouge{M :}~`j 
          \endprooftree
      \justifies `G "|-"  \rouge{(`l x . M) :}~`f "=>" `j %
      \using \verdir{(Abs)} %
      \endprooftree
      \quad 
      \prooftree 
      {\cal D'}
      \justifies `G "|-" \rouge{N :}~`f
      \endprooftree
      \justifies `G "|-" \rouge{(`l x . M)~N :}~`j 
      \using \verdir{(App)}
  \endprooftree
\end{displaymathbleu}
se transforme en
\begin{displaymathbleu}
      \prooftree %
      {\cal D''} 
        \justifies `G "|-" \rouge{M[x:=N] :}~`j %
    \endprooftree %
\end{displaymathbleu}
\bleu{\cal D''} est la preuve \bleu{\cal D} (qui se note \rouge{$M$})
dans laquelle toutes les utilisations de l'hypothèse \bleu{\rouge{x
    :}~`f} sont remplacées par la preuve
\bleu{\cal D} de~\bleu{`f} (qui se note \rouge{$N$}).  %
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La correspondance complète de Curry-Howard}
On obtient le tableau de correspondance:

\vspace*{5pt}

\begin{Large}
\begin{center}
\begin{tabular}{c @{\qquad} |  @{\qquad} c}
\verdir{types} & \verdir{propositions}\\
\verdir{termes} & \verdir{preuves}\\
\verdir{réduction} & \verdir{simplification des preuves}
\end{tabular}
\end{center}
\end{Large}
\vfill
\end{slide}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large \bf \color{mauve}{\textit{Forte normalisation}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Terminaision de la simplification ?}
Est-ce que le processus de simplification de preuves se \rouge{termine}?

Autrement dit est-ce que ce processsus est vraiment un processsus de
simplifiction.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Normalisation forte}
\rouge{Définition :}   Un terme \bleu{M} est \verdir{fortement normalisable} si
toute suite de réductions \bleu{M \rabeta M_1 \rabeta ...\rabeta M_n
  ...} est finie.

\vspace{10pt}

\rouge{Théorème :} Si \bleu{\Gamma \vdash M: \tau} alors \bleu{M} est
\verdir{fortement normalisable}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Normalisation forte (démonstration), 1$^{\textrm{er}}$ lemme} 
  \framebox{\parbox{9.5cm}{\rouge{Lemme:} Si \bleu{A}, \bleu{B} et
      \bleu{\vec{C}} \verdir{sont fortement normalisables} \ali et
      \bleu{A B \vec{C}} \verdir{n'est pas fortement normalisable} \ali
      alors il y a un \bleu{D} tel que
\begin{enumerate}
\item \bleu{A\rarabeta \lambda x. D}
\item \bleu{D[x:=B] \vec{C}} \verdir{n'est pas fortement normalisable}.
\end{enumerate}}}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Normalisation forte (démonstration), 1$^{\textrm{er}}$ lemme} 
  \framebox{\parbox{2cm}{\rouge{Démonstration:}}}

Puisque \bleu{A}, \bleu{B} et
      \bleu{\vec{C}} \verdir{sont fortement normalisables}, la réduction
      infinie qui part de \bleu{A B \vec{C}} est de la forme 
\bl{\[A B \vec{C}\rarabeta (\lambda x.D) B_1 \vec{C_1} \rabeta
D[x:=B_1]\vec{C_1} \rarabeta ...\]}

Mézalors le résultat vient immédiatement du fait que 
\bl{
\[D[x:=B] \vec{C} \rarabeta D[x:=B_1]\vec{C_1}.\]
}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Normalisation forte (démonstration), 1$^{\textrm{er}}$
    lemme} 
Remettons le lemme à l'endroit.

  \framebox{\parbox{9.5cm}{\rouge{Lemme:} Si \bleu{A}, \bleu{B} et
      \bleu{\vec{C}} \verdir{sont fortement normalisables} \ali
      et s'il y a un \bleu{D} tel que
\begin{enumerate}
\item \bleu{A\rarabeta \lambda x. D}
\item \bleu{D[x:=B] \vec{C}} \verdir{est fortement normalisable}.
\end{enumerate}
alors \bleu{A B \vec{C}} \verdir{est fortement normalisable} 
}}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Normalisation forte (démonstration), 2$^{\textrm{ème}}$ lemme} 
  \framebox{\parbox{7cm}{\rouge{Lemme:} 
Si \bleu{M}\rouge{et} \bleu{P} sont \verdir{typés}
\ali et si  \bleu{M}  et \bleu{P} sont \verdir{fortement normalisables},
\ali alors \bleu{M[x:=P]} est \verdir{fortement normalisable}.
}}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Normalisation forte (démonstration), 2$^{\textrm{ème}}$ lemme} 
  \framebox{\parbox{2cm}{\rouge{Démonstration:}}}

Par induction sur le triplet \bleu{(type(P), h(M), taille(M))}, où
\begin{itemize}
\item[\rouge{$\bullet$}] où \bleu{type(P)} est la complexité du type de \bleu{P},
\item[\rouge{$\bullet$}]  \bleu{h(M)} (ou hauteur) est la longueur de la plus longue
  réduction qui commence en~\bleu{M},
\item[\rouge{$\bullet$}]   \bleu{taille(M)} est la taille de \bleu{M}.
\end{itemize}

 \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Normalisation forte (démonstration), 2$^{\textrm{ème}}$ lemme}
  \begin{itemize}
  \item \rouge{$M = \lambda y . N$} , clairement \bleu{h(M) = h(N)},
  mais \bleu{taille(M) > taille(N)}.  On applique l'induction.%
  
  Donc \bleu{N[x:=P]} est fortement normalisable, donc
  \bleu{M[x:=P] `=`l N[x:=P]} est fortement normalisable.
  
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Normalisation forte (démonstration), 2$^{\textrm{ème}}$ lemme}
  \begin{itemize}
  \item \rouge{$y \vec{R}$}, les réductions ont lieu dans les
    \bleu{R_i}, donc clairement \bleu{h(M) \ge h(R_i)}, et
    \bleu{taille(M) > taille(R_i)}.  

    On applique l'induction à chacun
    des \bleu{R_i}, on conclut que chaque \bleu{R_i[x:=P]} est
    fortement normalisable, donc \bleu{y ... R_i[x:=P]...} est
    fortement normalisable, mais comme %
    \begin{displaymathbleu}
      y ... R_i[x:=P]... `= (y \vec{R})[x:=P].
\end{displaymathbleu}
    Par conséquent, \bleu{(y \vec{R})[x:=P]} est aussi fortement
    normalisable
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
 \heading{Normalisation forte (démonstration), 2$^{\textrm{ème}}$ lemme}
   \begin{itemize}
  \item \rouge{$M = (\lambda y . L) Q \vec{R}$} 
 
Par induction, \bleu{L[x:=P]}, \bleu{Q[x:=P]} et \bleu{\vec{R}[x:=P]}
sont fortement normalisables.

Posons \bleu{D} \rouge{$\equiv$} \bleu{L[y:=Q]\ \vec{R}}.

Si on veut utiliser le lemme précédent, il suffit de montrer que
\bleu{L[x:=P][y:=Q[x:=P]]\ \vec{R}[x:=P]} \rouge{$\equiv$} \bleu{D[x:=P]}
\ali est fortement
normalisable .

Or \bleu{h(D) < h(M)} donc par induction \bleu{D[x:=P]} est fortement
normalisable.  On peut appliquer le lemme.

Et donc par le lemme, \bleu{M[x:=P]} est fortement
normalisable.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
 \heading{Normalisation forte (démonstration), 2$^{\textrm{ème}}$ lemme}
   \begin{itemize}
  \item \rouge{$M = x L \vec{Q}$} 
    
    On veut démontrer que \bleu{P~ L[x:=P]~ \vec{Q}[x:=P]} est fortement
    normalisable.

    Par induction, \bleu{L' \equiv L[x:=P]} et \bleu{\vec{Q'} \equiv
      \vec{Q}[x:=P]} sont fortement normalisables.

    
    Si on veut utiliser le lemme précédent, il suffit de montrer que si
    \bleu{P\rarabeta \lambda y. P_1} alors \bleu{M'} \rouge{$\equiv$}
    \bleu{P_1[y:=L']\vec{Q'}} est fortement normalisable.

    Remarquons que cela nous indique que  \bleu{type(x) =
      type(P) = type(`l y. P_1) = `s "->" `t}.
  \end{itemize}    
  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
 \heading{Normalisation forte (démonstration), 2$^{\textrm{ème}}$ lemme}
   \begin{itemize}
  \item \rouge{$M = x L \vec{Q}$ (suite)} 
    
    Puisque \bleu{`s = type(L)= type(L')<type(P)}, on peut appliquer
    l'hypothèse d'induction et donc \bleu{P_1[y:=L']} est fortement
    normalisable.
    
    Parce que \bleu{`t = type(P_1[y:=L'])<type(P)}, on conclut par
    induction, que \bl{ \(M' {\color{red}\equiv} (z
      \vec{Q'})[z:=P_1[y:=L']]\) } est fortement normalisable
  
  Ainsi on peut appliquer le deuxième lemme et conclure que
  \bleu{M[x:=P]} est fortement normalisable.
\end{itemize}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Normalisation forte (démonstration)} 
  \framebox{\parbox{8cm}{\rouge{Théorème :} Si \bleu{\Gamma \vdash M:
        \tau} alors \bleu{M} est \verdir{fortement normalisable}. }}
  
  Le théorème est prouvé par induction structurelle sur le terme dont
  on cherche à prouver la normalisation forte.
\begin{itemize}
\item \rouge{Le terme est une variable ou une abstraction} c'est clair.
\item \rouge{Le terme est une application} \bleu{P\ Q}
  \ali alors on utilise une \verdir{astuce} en disant que 
  \begin{displaymathbleu}
    P\ Q \quad \rouge{\equiv} \quad (z Q)[z:=P]
  \end{displaymathbleu}
  ça devient évident par le 2$^{\textrm{ème}}$ lemme dont les
  hypothèses proviennent de l'induction structurelle.  %
 
  \begin{footnotesize}
    En effet si \bleu{Q} est fortement normalisable alors \bleu{z~Q}
    est fortement normalisable.
\end{footnotesize}
\end{itemize}

\vfill
\end{slide}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large \bf \color{mauve}{\textit{Les autres connecteurs}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
 \heading{Le  $\&$ et le produit cartésien}
 Le \bleu{\&} s'interprète bien calculatoirement en ajoutant des
 opérateurs de \rouge{produit cartésien}.
 \begin{description}
 \item[\rouge{Le constructeur de paires : }] \bleu{<\_,\_>},
 \item[\rouge{Les destructeurs ou projections :}] \bleu{`p^1} et
   \bleu{`p^2}.
 \end{description}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
 \heading{Le  $\&$ et le produit cartésien}
Les règles de typage
\begin{displaymathbleu}
  \prooftree
  `G "|-" M : `s `* `t
  \justifies `G "|-" `p^1~M: `s
  \endprooftree
  \qquad \qquad
  \prooftree
  `G "|-" M : `s `* `t
  \justifies `G "|-" `p^2~M: `t
  \endprooftree
\end{displaymathbleu}
\begin{displaymathbleu}
  \prooftree
  `G "|-" M : `s \qquad `G "|-" N : `t
  \justifies `G "|-" <M, N> : `s `* `t
 \endprooftree
\end{displaymathbleu}
correspond clairement à \rouge{deux règles d'éliminations} du \bleu{\&}
et à \rouge{la règle d'introduction} du \bleu{\&}.  
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
 \heading{Le  $\&$ et le produit cartésien}
On a deux règles de réduction
\begin{eqnarraybleu}
  `p^1~<M,N> & "->" & M\\
  `p^2~<M,N> & "->" & N
\end{eqnarraybleu}
qui correspondent à la simplication de preuve:
\begin{displaymathbleu}
  \prooftree
  \prooftree
  \prooftree
  \mathcal{D}
  \justifies `G "|-" M : `s 
  \endprooftree
  \qquad `G "|-" N: `t 
  \justifies `G "|-" <M,N>: `s `* `t
  \endprooftree
  \justifies `G "|-" `p^1<M,N>: `s 
  \endprooftree
  \qquad  "->"\qquad %
    \prooftree
     \mathcal{D}
     \justifies `G "|-" M : `s
    \endprooftree 
 \end{displaymathbleu}
et la simplification symétrique.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
 \heading{Le  $\vee$ et la somme}
Le \bleu{\vee} s'interprète comme la structure de données
\rouge{somme}.
\begin{description}
\item[\rouge{Les deux constructeurs :}] \bleu{\textsf{in}_1} et \bleu{\textsf{in}_2},
\item[\rouge{Le destructeur ou discriminateur :}] \bleu{\rouge{case} \quad
    \rouge{of}~\quad \rouge{in} \quad \rouge{or} \quad.}%
\ali un peu le \textbf{match} de CAML.
\end{description}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
 \heading{Le  $\vee$ et la somme}
Les règles de typage sont
\begin{displaymathbleu}
  \prooftree
  `G "|-" M : `s 
  \justifies`G "|-" \textsf{in}_1~M : `s \vee `t
  \endprooftree
  \qquad \qquad
  \prooftree
   `G "|-" M : `t
  \justifies`G "|-" \textsf{in}_2~M : `s \vee `t
  \endprooftree
\end{displaymathbleu}
\begin{displaymathbleu}
  \prooftree
  `G "|-" M : `s \qquad `G, x : `s "|-" P : `r \qquad `G, x : `t "|-" Q : `r 
  \justifies `G "|-" \rouge{case}~M~ \rouge{of}~x~\rouge{in}~ P~\rouge{or}~ Q : `r
  \endprooftree
\end{displaymathbleu}
Elles correspondent aux règles d'introduction du \bleu{\vee} et à la
règle d'élimination du \bleu{\vee}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
 \heading{Le  $\vee$ et la somme}
On a les règles de réduction
\begin{eqnarraybleu}
  \rouge{case}~(\textsf{in}_1~M)~\rouge{of}~x~ \rouge{in}~ P~\rouge{or}~ Q
  &"->"& P[x:=M]\\ 
  \rouge{case}~(\textsf{in}_2~M)~\rouge{of}~x~ \rouge{in}~ P~\rouge{or}~ Q
  &"->"& Q[x:=M] 
\end{eqnarraybleu} 
qui correspond à la simplication de preuve.
\begin{scriptsize}
\begin{displaymathbleu}
  \prooftree %
  \prooftree % -
  \prooftree % --
  \mathcal{D}' \justifies `G "|-" M : s
  \endprooftree % --
  \justifies `G "|-" \textsf{in}_1~M : s \vee `t
  \endprooftree % -
  \quad 
   \prooftree % ---
   \mathcal{D} 
   \justifies `G, x : `s "|-" P : `r 
   \endprooftree % ---
  \quad `G, x : `t "|-" Q : `r
  \justifies  \rouge{case}~M~\rouge{of}~x~\rouge{in}~ P~\rouge{or}~ Q : `r%
  \endprooftree %
 \qquad  "->"\qquad %
 \prooftree 
 \mathcal{D}\{\mathcal{D}' / `G, x:`s "|-" x:`s\}
 \justifies `G "|-" P : `r 
\endprooftree
\end{displaymathbleu}
\end{scriptsize}
\vfill
\end{slide}
%------------------------------------------------------
\end{document}
