\begin{slide}
  \pagestyle{empty}
  \begin{center}
    ~\\[1em]
    \bleu{\rule{\linewidth}{0.1em}} 
    \\[0.5em]
    \bleu{\bf\Large Induction sur les listes}\\
    \bleu{\rule{\linewidth}{0.1em}} \\[1.5em]
    \end{center}%\addtocounter{slide}{-1}
\end{slide}


\begin{slide}\titre{Planning}
  \begin{itemize}
  \item \'Equations r\'ecursives sur les listes
  \item Complexit\'e de fonctions sur les listes
    \begin{itemize}
    \item Tri par insertion
    \item Tri rapide
    \end{itemize}
  \item Preuve de propri\'et\'es par r\'ecurrence sur les listes
  \end{itemize}
\end{slide}


\begin{slide}\titre{\'Equations r\'ecursives sur les listes}


M\^eme \'equation que sur les entiers~: 


\[\azul{f}(l)=\rosa{g}(l,\azul{f}(\rouge{h}(l)))\]

\adviwait
\vsp

On pourra utiliser un type abstrait. 
\end{slide}

\begin{slide}\titre{Le type abstrait \rouge{{\tt 'a liste}}}
{\small 
\begin{tabular}{l}
\rouge{Domaine~:}\\
{\tt 'a liste} \\
\rouge{Op\'erations de construction~:}\\
{\tt nil}~: {\tt 'a liste}\\
{\tt cons}~: {\tt 'a} $\times$ {\tt 'a liste} $\rew$  {\tt 'a liste}\\
\rouge{Op\'erations de test} (une ou deux) ~: \\
{\tt liste\_vide}~: {\tt 'a liste} $\rew$ bool\'een\\
{\tt liste\_non\_vide}~: {\tt 'a liste} $\rew$ bool\'een\\
\rouge{Op\'erations d'acc\`es~:}\\
{\tt premier}~: $\{ l \in $ {\tt 'a liste} $\mid$
{\tt non\_vide}(l) $\} \rew$ {\tt 'a}  \\
{\tt reste}~:  $\{ l \in $ {\tt 'a liste} $\mid$
{\tt non\_vide}(l) $\} \rew$ {\tt 'a liste} \\
\end{tabular} 
}
\end{slide}

\begin{slide}\titre{Exemple I~: la longueur d'une liste} 

\rouge{Probl\`eme~:} d\'efinir une fonction qui calcule la longueur 
d'une liste. 

\adviwait
\vsp

\rouge{D\'eclaration du type~:}
\begin{center}
\azul{{\tt longueur}}: {\tt 'a liste} $\rightarrow$ {\tt entier}
\end{center} 

\adviwait
\vsp

\rouge{\'Equation r\'ecursive~:}

\[\azul{{\tt longueur}}(l)=\rosa{g}(l,\azul{{\tt longueur}}(\rouge{h}(l)))\]

\end{slide}

\begin{slide}
On pose 
\[  \rouge{h}(l) = {\tt reste}(l) \hsep \rosa{g}(l,k)= 1 + k \]  
\adviwait
Cas particulier~:
\adviwait
\[ l={\tt nil} ~~ ({\tt reste}({\tt nil}) \mbox{ n'est pas d\'efini}). \] 
Ceci donne~:
\[ \begin{array}{llll}
    \azul{{\tt longueur}}(l) & = & 0 \\
                             &   & \mbox{ si } {\tt liste\_vide}(l)\\
    \azul{{\tt longueur}}(l) & = & 1 + \azul{{\tt longueur}}(
    {\tt reste}(l)) \\ 
                             &   & \mbox{ si }  {\tt liste\_non\_vide}(l)\\
    \end{array} \] 
\end{slide}

\begin{slide}
En OCAML~:
\begin{verbatim}
# let rec longueur l = match l with 
    []   -> 0 
  | p::r -> 1 + longueur r;;
val longueur : 'a list -> int = <fun>
\end{verbatim}
\end{slide}


\begin{slide}\titre{Exemple II~: inversion d'une liste}

\rouge{Probl\`eme~:} d\'efinir une fonction qui construit la liste 
inverse d'une liste. 

\adviwait
\vsp

\rouge{D\'eclaration du type~:}
\begin{center}
\azul{{\tt inv\_seq}}: {\tt 'a liste} $\rightarrow$ {\tt 'a liste}
\end{center} 
\adviwait
\rouge{\'Equation r\'ecursive~:}
\[ \azul{{\tt inv\_seq}}(l) = \rosa{g}(l,\azul{{\tt
    inv\_seq}}(\rouge{h}(l))) \]

\end{slide}

\begin{slide}
On pose~:
\[ \rouge{h}(y)= {\tt reste}(y) \hsep \rosa{g}(l,z)= {\tt ajout\_fin}({\tt premier}(l), z)\]
\adviwait

Cas particulier~: 
\[ l={\tt nil} ~~ ({\tt premier}({\tt nil}) \mbox{ et } {\tt reste}({\tt nil})
\mbox{ ne sont pas d\'efinis}). \] 

\end{slide}

\begin{slide}\titre{}
Ceci donne~:

\[ \begin{array}{lll}
   \azul{{\tt inv\_seq}}(l) & = & l \\
                            &   & \mbox{ si } {\tt liste\_vide}(l)\\ 
   \azul{{\tt inv\_seq}}(l) & = & {\tt ajout\_fin}({\tt premier}(l), \azul{{\tt
    inv\_seq}}({\tt reste}(l)) ) \\
                            & & \mbox{ si } {\tt  liste\_non\_vide}(l)\\
   \end{array} \]
\adviwait
En OCAML~: 
\begin{verbatim}
# let rec ajout_fin(e,l) = match l with
      []    -> [e]
    | p:: r -> p:: ajout_fin(e,r);;
val ajout_fin : 'a * 'a list -> 'a list = <fun>

# let rec inv_seq l = match l with
      []   -> []
    | p::r -> ajout_fin(p,inv_seq r);;
val inv_seq : 'a list -> 'a list = <fun>
\end{verbatim}

\end{slide}


\begin{slide}\titre{\'Equations sur les listes avec
    plusieurs arguments}
  
M\^eme \'equation que sur les entiers~: 
\[ \azul{f}(y,x)=\rosa{g}(y,x,\azul{f}(\rouge{h}(y),\rouge{i}(x)))\] 


\end{slide}


\begin{slide}\titre{Exemple I~: la concatenation}
 
  \rouge{Probl\`eme~:} d\'efinir une fonction qui concat\`ene
  deux listes. 

\adviwait
\vsp

\rouge{D\'eclaration du type~:}
\begin{center}
\azul{{\tt concat}}: {\tt 'a liste} $\times$ {\tt 'a liste} $\rightarrow$ {\tt 'a liste}
\end{center} 
\rouge{\'Equation r\'ecursive~:}
\[ \azul{{\tt concat}}(y,x)=\rosa{g}(y,x,\azul{{\tt concat}}(\rouge{h}(y),\rouge{i}(x)))\] 
\adviwait
On pose~:

\[ \rouge{h}(y)= {\tt reste}(y) \hsep \hsep \rouge{i}(x) = x \]

\[ \rosa{g}(y,x,z)= \left \{ \begin{array}{ll}
         x           & \mbox{ si } {\tt liste\_vide}(y)\\
         {\tt cons}({\tt premier}(y),z) & \mbox{ si } {\tt liste\_non\_vide}(y)\\
         \end{array} \right. \] 
\end{slide}



\begin{slide}
Ceci donne~:

\[  \begin{array}{lll}
   \azul{{\tt concat}}(l,x) & = & x \\
                            &   & \mbox{ si } {\tt liste\_vide}(l)\\ 
   \azul{{\tt concat}}(l,x) & = & {\tt cons}({\tt premier}(l), \azul{{\tt
    concat}}({\tt reste}(l),x) ) \\
                            & & \mbox{ si } {\tt  liste\_non\_vide}(l)\\
   \end{array} \]
En OCAML~:
\begin{verbatim}
# let rec concat(l1,l2) = match l1 with
      []   -> l2
   | p:: r -> p:: concat(r,l2);;
val concat : 'a list * 'a list -> 'a list = <fun>
\end{verbatim}

\end{slide}

\begin{slide}\titre{Exemple II~: ajout fin} 
  
\rouge{Probl\`eme~:} d\'efinir une fonction qui ajoute un 
\'el\'ement \`a la fin d'une liste. 

\adviwait
\vsp

\rouge{D\'eclaration du type~:}
\begin{center}
\azul{{\tt ajout\_fin}}: {\tt 'a liste} $\times$ {\tt 'a} $\rightarrow$ {\tt 'a liste}
\end{center} 
\adviwait

On cherche~:

\[ \azul{{\tt ajout\_fin}}(y,e)=\rosa{g}(y,e,\azul{{\tt  ajout\_fin}}(\rouge{h}(y),\rouge{i}(e)))\] 

\end{slide}
\begin{slide}
On pose~:

\[ \rouge{h}(y)= {\tt reste}(y) \hsep \hsep \rouge{i}(e) = e \]
\[ \rosa{g}(y,e,z)= \left \{ \begin{array}{ll}
         {\tt cons}(e,{\tt nil})           & \mbox{ si } {\tt liste\_vide}(y)\\
         {\tt cons}({\tt premier}(y),z) & \mbox{ si } {\tt liste\_non\_vide}(y)\\
         \end{array} \right. \] 

\adviwait
\vsp
Cas particulier~: 

\[ l={\tt nil} ~~ ({\tt reste}({\tt nil}) \mbox{ n'est pas d\'efini}). \] 

\end{slide}

\begin{slide}


Ceci donne~:

\[ \begin{array}{lll}
   \azul{{\tt ajout\_fin}}(l,e) & = & {\tt cons}(e,{\tt nil})  \\
                                &   & \mbox{ si } {\tt liste\_vide}(l)\\\\ 
   \azul{{\tt ajout\_fin}}(l,e) & = & 
       {\tt cons}({\tt premier}(l),\azul{{\tt ajout\_fin}}({\tt reste}(l), e)) \\
                            & & \mbox{ si } {\tt  liste\_non\_vide}(l)\\
   \end{array} \]

En OCAML~:
\begin{verbatim}
# let rec ajout_fin(l,e) = match l with
      []   -> [e]
   | p:: r -> p::ajout_fin(r,e);;
val ajout_fin : 'a list * 'a -> 'a list = <fun>
\end{verbatim}
\end{slide}


\begin{slide}\titre{Notions de complexit\'e}

Permet de mesurer la consommation  des ressources
lorsqu'on ex\'ecute un algorithme~:  

\begin{itemize}

    \item le \rouge{co\^ut en temps} (\textit{i.e.} le nombre d'op\'erations n\'ecessaires)

    \item le \rouge{co\^ut en espace} (\textit{i.e.} la quantit\'e de m\'emoire n\'ecessaire)

\end{itemize}

\vsp

Ce deux crit\`eres ne sont pas totalement ind\'ependants.
\end{slide}


\begin{slide}\titre{Principes de base}
  
  \begin{itemize}
  \item Mesurer la complexit\'e en \rouge{fonction de la taille des donn\'ees} de
    l'algorithme.
  \item Evaluer le c\^out \rouge{exact} est difficile.
  \item Certaines op\'erations sont \rouge{n\'egligeables} par rapport au co\^ut
      total.
  \item On s'int\'eresse
aux op\'erations dont le nombre \'evolue de fa\c{c}on significative lorsque la taille des donn\'ees varie.
Si $f$ est une fonction caract\'erisant le co\^ut d'un algorithme en
fonction de la taille $n$ des donn\'ees, on s'int\'eresse \`a la fa\c{c}on dont
cro\^{\i}t $f(n)$ lorsque $n$ cro\^{\i}t. Plus pr\'ecis\'ement, on cherche
g\'en\'eralement \`a montrer que $f(n)$ ne croit pas plus vite qu'une autre
fonction $g(n)$.

\end{itemize}
\end{slide}


\begin{slide}\titre{Ordres de grandeur}
\begin{tabular}[t]{|l|c|}
\hline
{\bf Croissance} & {\bf Ordre de grandeur} \\
\hline \hline
linéaire      & $O(n)$\\
quadratique   & $O(n^2)$\\
polynomiale   & $O(n^p)$\\
exponentielle & $O(p^n)$\\
logarithmique & $O(log(n))$\\
\hline
\end{tabular}
\end{slide}

\ignore{
\begin{slide}\titre{Exemple}
\begin{tabular}[t]{|c||c|c|c|c|c|c|c|}
\hline
taille&\multicolumn{7}{|c|}{Complexité}\\
\cline{2-8}&  $1$   &  $log_2(n)$ & $n$ & $n.log_2(n)$ & $n^2$ & $n^3$  & $2^n$\\
\hline
\hline
$n = 10^2$ & $1 \mu s$ & $6,6 \mu s$  & $0,1 ms$ & $0,6 ms$ & $10 ms$ & $1 s$     & $4.
10^{16} a$\\
$n = 10^3$ & $1 \mu s$ & $9,9 \mu s$  & $  1 ms$ & $9,9 ms$ & $1 s$   & $16,6 mn$ & $\i
nfty$\\
$n = 10^4$ & $1 \mu s$ & $13,3 \mu s$ & $10 ms$  & $0,1 s $ & $100 s$ & $11,5 j$  & $\i
nfty$\\
$n = 10^5$ & $1 \mu s$ & $16,6 \mu s$ & $0,1 s$  & $1,6 s $ & $2,7 h$ & $31,7 a$  & $\i
nfty$\\
$n = 10^6$ & $1 \mu s$ & $19,9 \mu s$ & $1 s$    & $19,9 s$ & $11,5 j$ & $31700 a$  & $
\infty$\\
\hline
\end{tabular}
\end{slide}
}




\begin{slide}\titre{Complexit\'e sur les listes~: probl\`eme du tri}

  \rouge{Probl\`eme~:}  d\'efinir  une fonction  qui  associe \`a  une
  liste d'\'el\'ements la liste form\'ee des m\^emes \'el\'ements mais
  tri\'es par ordre croissant.

\adviwait
\vsp

\rouge{D\'eclaration du type~:}
\begin{center}
\azul{{\tt tri}}: {\tt 'a liste} $\rightarrow$ {\tt 'a liste} 
\end{center} 

\adviwait
\vsp
\rouge{Hypoth\`ese de travail~:}
On dispose d'une fonction permettant de comparer deux
\'el\'ements quelconques  de type  {\tt 'a}.
\end{slide}

\begin{slide}\titre{M\'ethode par insertion}
  
\rouge{Id\'ee~:} On ram\`ene le probl\`eme ${\tt tri}(l)$ au probl\`eme
${\tt tri}({\tt reste}(l))$.

\rouge{\'Equation r\'ecursive~:}

\[\azul{{\tt tri\_ins}}(l)=\rosa{g}(l,\azul{{\tt tri\_ins}}(\rouge{h}(l)))\]

On pose 
\[  \rouge{h}(l) = {\tt reste}(l) \hsep \rosa{g}(l,z)= {\tt insertion}({\tt premier}(l),z) \]  

\adviwait

Cas particulier~:

\[ l={\tt nil} ~~ ({\tt reste}({\tt nil}) \mbox{ n'est pas d\'efini}). \] 
\end{slide}

\begin{slide}
Ceci donne~:
\[ \begin{array}{llll}
    \azul{{\tt tri\_ins}}(l) & = & l \\
                         &   & \mbox{ si } {\tt liste\_vide}(l)\\
    \azul{{\tt tri\_ins}}(l) & = & {\tt insertion}({\tt premier}(l),\azul{{\tt tri\_ins}}({\tt reste}(l)))\\ 
                         &   & \mbox{ si }  {\tt liste\_non\_vide}(l)\\
    \end{array} \] 

En OCAML~:
\begin{verbatim}
# let rec tri_ins l = match l with
      []   -> []
   | p:: r -> insertion(tri_ins r,p);;
val tri_ins : 'a list -> 'a list = <fun>
\end{verbatim}
\end{slide}

\begin{slide}\titre{Insertion d'un \'el\'ement dans une liste}
   \rouge{Probl\`eme~:}  d\'efinir  une fonction  qui 
   permet d'ins\'erer un \'el\'ement ``au bon
     endroit'' d'une liste d'\'el\'ements 
  tri\'es par ordre croissant.

\adviwait
\vsp

\rouge{D\'eclaration du type~:}
\begin{center}
\azul{{\tt insertion}}: {\tt 'a liste} $\times$ {\tt 'a} $\rightarrow$ {\tt 'a liste} 
\end{center} 
\adviwait

\rouge{\'Equation r\'ecursive~:}

\[\azul{{\tt  insertion}}(l,e)=\rosa{g}(l,e,\azul{{\tt insertion}}(\rouge{h}(l),\rouge{i}(e)))\]

\end{slide}

\begin{slide}
On pose~:

\[\rouge{h}(l) = {\tt reste}(l) \hsep \rouge{i}(e) = e\] 

\[ \rosa{g}(l,e,z)= \left \{ \begin{array}{ll}
         {\tt cons}~(e,{\tt nil})           & \mbox{ si } {\tt liste\_vide}(l)\\
         {\tt si}~ e \leq {\tt premier}(l) \\
          ~~~{\tt alors}~~{\tt cons}(e,y)   \\
          ~~~{\tt sinon}~~{\tt cons}({\tt premier}(l),z)  & \mbox{ si } {\tt liste\_non\_vide}(l)\\
         \end{array} \right. \] 
\end{slide}

\begin{slide}
Ceci donne~:

\[ \begin{array}{llll}
    \azul{{\tt insertion}}(l,e) & = & {\tt cons}~(e,{\tt nil})  \\
                                &   & \mbox{ si } {\tt liste\_vide}(l)\\
    \azul{{\tt insertion}}(l,e) & = & {\tt si}~ e \leq {\tt premier}(l) \\
        &   & ~~~~~{\tt alors}~~{\tt cons}(e,l) \\
        &   & ~~~~~{\tt sinon}~~{\tt cons}({\tt  premier}(l),\azul{{\tt
                                insertion}}({\tt reste}(l),e))  \\ 
                                &   & \mbox{ si } {\tt non\_liste\_vide}(l)\\    
    \end{array}  \]
\end{slide}
\begin{slide}
En OCAML~:
\begin{verbatim}
# let rec insertion(l,e) = match l with
      []    -> [e]
    | p:: r -> if e <= p 
                  then e::l
                  else p::insertion(r,e);;         
val insertion : 'a list * 'a -> 'a list = <fun>
\end{verbatim}
\end{slide}

\begin{slide}\titre{Complexit\'e du tri par insertion}

Pour trier une liste de $n$ \'el\'elements on doit~:

\begin{itemize}
\item Trier une liste de $n-1$ \'el\'elements
\item Ins\'erer un \'el\'ement dans une s\'equence tri\'ee  de $n-1$ \'el\'ements
\end{itemize}

C'est \`a dire


\begin{itemize}
\item Trier une liste de $n-2$ \'el\'elements
\item Ins\'erer un \'el\'ement dans une s\'equence tri\'ee  de $n-2$ \'el\'ements
\item Ins\'erer un \'el\'ement dans une s\'equence tri\'ee  de $n-1$ \'el\'ements
\end{itemize}


\end{slide}
\begin{slide}
C'est \`a dire
\begin{itemize}
\item Ins\'erer un \'el\'ement dans une s\'equence tri\'ee  de $1$ \'el\'ement
\item Ins\'erer un \'el\'ement dans une s\'equence tri\'ee  de $2$ \'el\'ements
\item \ldots
\item Ins\'erer un \'el\'ement dans une s\'equence tri\'ee  de $n-2$ \'el\'ements
\item Ins\'erer un \'el\'ement dans une s\'equence tri\'ee  de $n-1$ \'el\'ements
\end{itemize}
\end{slide}

\begin{slide}\titre{Complexit\'e de l'insertion d'un \'el\'ement dans
    une liste de $n$  \'el\'ements }
  \begin{itemize}
  \item \rouge{Meilleur cas~:} $1$ comparaison 
  \item  \rouge{Meilleur cas~:} $n$ comparaisons
  \end{itemize}
\end{slide}


\begin{slide}\titre{Co\^ut du tri par insertion d'une liste de $n$ \'el\'ements} 
\begin{itemize}
\item \rouge{Meilleur cas~:}  $1 + 1 + 1 + 1 + \ldots + 1$ ($n-1$ fois)\\
   donc un co\^ut en $O(n)$
 \item \rouge{Cas le pire~:} $(n-1) + (n-2)+ \ldots + 1$, soit : $\frac{n(n-1)}{2}$\\
   donc un co\^ut en $O(n^2)$
\end{itemize}
\end{slide}


\begin{slide}\titre{M\'ethode rapide}

\rouge{Id\'ee~:} On ram\`ene le probl\`eme ${\tt tri}(l)$
au probl\`eme ${\tt tri}(l')$ avec $l'$ une sous-liste de 
$l$ qui n'est pas forcement ${\tt reste}(l)$. 

\adviwait
\rouge{Comment?} On partage la liste $l$ en deux sous-listes
$l_1$ et $l_2$  par rapport \`a un
\rouge{pivot} $e$ de $l$ de telle sorte que 

\[ \forall x \in l_1~~~ x \leq e \hsep \mbox{ et }
    \hsep \forall y \in l_2~~~ e > y\]
\adviwait

La \rouge{m\'ethode}  satisfait  l'\'equation

\[ {\tt tri\_rap}(l) = 
   {\tt concat}({\tt tri\_rap}(l_1),{\tt cons}(e,{\tt tri\_rap}(l_2)))\]
\end{slide}


\begin{slide}\titre{Le partage d'une liste selon un pivot}
  
\rouge{Probl\`eme~:} d\'efinir une fonction qui associe \`a une liste
$l$ et \`a un \'el\'ement $e$ deux listes $l_1$ et $l_2$ t.q. 
$\forall x \in l_1~~ x \leq e \mbox{ et }
     \forall y \in l_2~~ e > y$. 

\adviwait
\vsp
\rouge{D\'eclaration du type~:}
\begin{center}
\azul{{\tt partage}}: {\tt 'a liste} $\times$ {\tt 'a} $\rightarrow$ 
{\tt 'a liste} $\times$ {\tt 'a liste}
\end{center} 

\adviwait
\vsp
\rouge{\'Equation r\'ecursive~:}

\[\azul{{\tt partage}}(l,e)=\rosa{g}(l,e,\azul{{\tt partage}}(\rouge{h}(l),e))\]

\end{slide}

\begin{slide}
On pose~:

\[ \rouge{h}(l) = {\tt reste}(l)\]  et

\[  \begin{array}{ll}
    \rosa{g}(l,e,(z_1,z_2))=  & 
                       {\tt si } ~ {\tt premier}(l) \leq e\\
                           &  ~~~ {\tt alors}~ ({\tt cons}({\tt
                           premier}(l),z_1),z_2) \\ 
                           &   ~~~ {\tt sinon} ~(z_1,{\tt cons}({\tt
                           premier}(l),z_2)) 
    \end{array}\]  
\adviwait
Cas particulier~:
\adviwait
\[ l={\tt nil} ~~ ({\tt premier}({\tt nil}) \mbox{ n'est pas
  d\'efini}). \] 
Ceci donne~:
\[ \begin{array}{llll}
   \azul{{\tt partage}}(l,e) & = & ({\tt nil},{\tt nil}) \\
                           &   & \mbox{ si } {\tt liste\_vide}(l)\\
   \azul{{\tt partage}}(l,e) & = & {\tt soit}~(s_1,s_2) = {\tt
                           partage}({\tt reste}(l),e)~{\tt dans} \\
                             && {\tt si } ~ {\tt premier}(l) \leq e\\
                             && ~~~ {\tt alors}~ ({\tt cons}({\tt
                           premier}(l),s_1),s_2) \\ 
                            && ~~~ {\tt sinon} ~(s_1,{\tt cons}({\tt
                           premier}(l),s_2)) \\ 
                           &   & \mbox{ si } {\tt liste\_non\_vide}(l)\\
   \end{array} \] 
\end{slide}
\begin{slide}
En OCAML~:
\begin{verbatim}
# let rec partage(l,e) = match l with
      []    -> ([],[])
    | p::r  -> let (s1,s2)=partage(r,e) in 
                   if p<=e 
                      then (p::s1,s2) 
                      else (s1,p::s2);;   
val partage : 'a list * 'a -> 'a list * 'a list = <fun>
\end{verbatim}
\end{slide}


\begin{slide}\titre{}
En OCAML~:
\begin{verbatim}
# let rec tri_rap(l)= match l with
      []   -> []
    | p::r -> let (s1,s2) = partage(r,p) in
                  concat(tri_rap(s1), p::tri_rap(s2));;
val tri_rap : 'a list -> 'a list = <fun>
\end{verbatim}
\end{slide}

\begin{slide}\titre{Complexit\'e du tri par insertion}

Pour trier une liste de $n$ \'el\'elements on doit~:
\begin{enumerate}
\item Partager une liste de $n-1$ \'el\'elements en deux sous-listes
      $(s_1,s_2)$ ($n-1$ comparaisons).
\item Trier la liste $s_1$.
\item Trier la liste $s_2$.
\end{enumerate}
\adviwait
\vsp
\rouge{Mais quelles sont les longueurs de $s_1$ et de $s_2$?}
\end{slide}


\begin{slide}\titre{Cas le meilleur}
\`A chaque \'etape $s_1$ et $s_2$ ont la \rouge{m\^eme} longueur.  

\rouge{Exemple~:}
\begin{enumerate}
\item \azul{{\tt tri\_rap[4;2;6;3;5;1;7]}} provoque deux appels
      \begin{enumerate}
      \item \azul{{\tt tri\_rap[2;3;1]}} provoque deux appels
             \begin{enumerate}
             \item \azul{{\tt tri\_rap[1]}} provoque deux appels \azul{{\tt tri\_rap[]}}
             \item \azul{{\tt tri\_rap[3]}} provoque deux appels \azul{{\tt tri\_rap[]}}
             \end{enumerate}
             
      \item \azul{{\tt tri\_rap[6;5;7]}} provoque deux appels
             \begin{enumerate}
             \item \azul{{\tt tri\_rap[5]}} provoque deux appels \azul{{\tt tri\_rap[]}}
             \item \azul{{\tt tri\_rap[7]}} provoque deux appels \azul{{\tt tri\_rap[]}}
             \end{enumerate}
      \end{enumerate}
\end{enumerate}
\end{slide}


\begin{slide}\titre{}
Le nombre de comparaisons est~:


\[(n-1) + 2 \times  [\frac{(n-1)}{2} -1] + 4 \times [\frac{n-1}{4} -1] + \ldots \]

La profondeur de l'arbre est de l'ordre de $log_2(n)$.

La complexité dans le meilleur des cas est donc  $O(n \times log_2(n))$.


\end{slide}
\begin{slide}\titre{Cas le pire}
\`A chaque \'etape l'une des listes $s_1$ ou $s_2$ est vide. 

\rouge{Exemple~:}

\begin{tabular}{l}
\azul{{\tt tri\_rap[1;2;3;4;5]}} provoque deux appels \\
1) \azul{{\tt tri\_rap[]}}   \\
2) \azul{{\tt tri\_rap[2;3;4;5]}} provoque deux appels \\
~~2.1) \azul{{\tt tri\_rap[]}}   \\
~~2.2) \azul{{\tt tri\_rap[3;4;5]}} provoque deux appels \\
~~~~        2.2.1) \azul{{\tt tri\_rap[]}}   \\
~~~~        2.2.2) \azul{{\tt tri\_rap[4;5]}} provoque deux appels \\
~~~~~~~               2.2.2.1) \azul{{\tt tri\_rap[]}}   \\
~~~~~~~               2.2.2.2) \azul{{\tt tri\_rap[5]}} provoque deux appels \\ 
~~~~~~~~~~~                         2.2.2.2.1) \azul{{\tt tri\_rap[]}}   \\
~~~~~~~~~~~                         2.2.2.2.2) \azul{{\tt tri\_rap[]}}   \\
\end{tabular}
\end{slide}

\begin{slide}\titre{}
Le nombre de comparaisons est~:

\[(n-1) + (n-2) + \ldots + 1 = \frac{n \times (n-1)}{2}\]

La complexité au pire est donc en $O(n^2)$.

\end{slide}


\begin{slide}\titre{Preuves de propri\'et\'es par r\'ecurrence}
  
\begin{itemize}
\item On utilise la d\'efinition inductive de l'ensemble de listes
\item On utilise la d\'efinition r\'ecursive d'une ou plusieures
  fonctions et/ou propri\'et\'es. 
\end{itemize}
\end{slide}


\begin{slide}\titre{Exemple I}
Propri\'et\'e \`a d\'emontrer~: \azul{pour toute liste $l,~ {\tt concat}(l,{\tt nil}) = l$} 

Preuve~: par induction sur $l$. 

\begin{itemize}
\item Cas de base~: \azul{$l = {\tt nil}$}.

      \[ {\tt concat}({\tt nil},{\tt nil}) = {\tt nil} \]


\item Cas inductif~:  \azul{$l = {\tt cons}(p,r)$}. 

      \[ \begin{array}{lll}
          {\tt concat}(l,{\tt nil}) & = \\
          {\tt concat}({\tt cons}(p,r),{\tt nil}) & = \\
          {\tt cons}(p,{\tt concat}(r,{\tt nil})) & =_{h.r} \\
          {\tt cons}(p,r) & = l \\
           \end{array} \]
\end{itemize}
\end{slide}

\begin{slide}\titre{Exemple II}
Propri\'et\'e \`a d\'emontrer~: 
\azul{pour tout \'el\'ement $e$ et toute liste $l_1,l_2$}

\[ \azul{{\tt ajout\_fin}(e,{\tt concat}(l_1,l_2)) = 
   {\tt concat}(l_1,{\tt ajout\_fin}(e,l_2))} \]
\adviwait

Preuve~: par induction sur $l_1$. 

\begin{itemize}
\item Cas de base~:  \azul{$l_1 = {\tt nil}$}.
      
      \[ \begin{array}{lll}
          {\tt ajout\_fin}(e,{\tt concat}(l_1,l_2)) & = \\
          {\tt ajout\_fin}(e,{\tt concat}({\tt nil},l_2)) & = \\
          {\tt ajout\_fin}(e,l_2) & = \\
          {\tt concat}({\tt nil},{\tt ajout\_fin}(e,l_2)& = \\
          {\tt concat}(l_1,{\tt ajout\_fin}(e,l_2)) 
          \end{array} \] 

\item Cas inductif~:  \azul{$l_1 = {\tt cons}(p,r)$}. 

      \[ \begin{array}{lll}
          {\tt ajout\_fin}(e,{\tt concat}(l_1,l_2)) & = \\
          {\tt ajout\_fin}(e,{\tt concat}({\tt cons}(p,r),l_2)) & = \\
          {\tt ajout\_fin}(e,{\tt cons}(p,{\tt concat}(r,l_2))) & = \\
          {\tt cons}(p,{\tt ajout\_fin}(e,{\tt concat}(r,l_2))) & =_{h.r} \\
          {\tt cons}(p,{\tt concat}(r,{\tt ajout\_fin}(e,l_2))) & = \\
          {\tt concat}({\tt cons}(p,r),{\tt ajout\_fin}(e,l_2)) & = \\
          {\tt concat}(l_1,{\tt ajout\_fin}(e,l_2)) 
          \end{array} \] 

\end{itemize}
\end{slide}

\begin{slide}\titre{Exemple III}
  
Propri\'et\'e \`a d\'emontrer~: \azul{pour tout \'el\'ement $e$ et
  toute liste $l_1,l_2$}
\[  \azul{{\tt inv\_seq}({\tt concat}(l_1,l_2)) = 
   {\tt concat}({\tt inv\_seq}(l_2),{\tt inv\_seq}(l_1))} \]

\adviwait

Preuve~: par induction sur $l_1$. 

\begin{itemize}
\item Cas de base~:  \azul{$l_1 = {\tt nil}$}.


\[ \begin{array}{ll}
   {\tt inv\_seq}({\tt concat}(l_1,l_2)) & = \\
   {\tt inv\_seq}({\tt concat}({\tt nil},l_2)) & = \\
   {\tt inv\_seq}(l_2) & =_{\mbox{{\scriptsize Exemple I}}} \\
   {\tt concat}({\tt inv\_seq}(l_2),{\tt nil}) & = \\
   {\tt concat}({\tt inv\_seq}(l_2),{\tt inv\_seq}({\tt nil})) & = \\
   {\tt concat}({\tt inv\_seq}(l_2),{\tt inv\_seq}(l_1))  
   \end{array}\] 

\item Cas inductif~:  \azul{$l_1 = {\tt cons}(p,r)$}.

\[ \begin{array}{ll}
   {\tt inv\_seq}({\tt concat}(l_1,l_2)) & = \\
   {\tt inv\_seq}({\tt concat}({\tt cons}(p,r),l_2)) & = \\
   {\tt inv\_seq}({\tt cons}(p,{\tt concat}(r,l_2))) & = \\
   {\tt ajout\_fin}(p,{\tt inv\_seq}({\tt concat}(r,l_2))) & =_{h.r}
   \\
   {\tt ajout\_fin}(p,{\tt concat}({\tt inv\_seq}(l_2),{\tt
   inv\_seq}(r))) & =_{\mbox{{\scriptsize Exemple II}}}\\
   {\tt concat}({\tt inv\_seq}(l_2),{\tt ajout\_fin}(p,{\tt inv\_seq}(r))) & = \\
   {\tt concat}({\tt inv\_seq}(l_2),{\tt inv\_seq}({\tt cons}(p,r))) & = \\
   {\tt concat}({\tt inv\_seq}(l_2),{\tt inv\_seq}(l_1)) \\
   \end{array}\] 

\end{itemize}

\end{slide}
%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "slides"
%%% End: 
