\documentclass[12pt]{article}

\usepackage{a4}
\usepackage[latin1]{inputenc}
\usepackage[francais]{babel}
\usepackage[all]{xy}
\usepackage{amsfonts,amsmath,amsthm,amssymb,stmaryrd}

\newcommand{\R}{\mathbb{R}}
\newcommand{\N}{\mathbb{N}}

\title{Magistère d'Informatique et Modélisation}
\author{Devoir de logique}

\date{3 octobre 2001}

\begin{document}
\maketitle 
\thispagestyle{empty}

\textbf{Avant-propos:} Les étudiants choisiront un seul des exercices
suivants.  Ils pourront s'assembler en groupes dont la taille est
indiquée au début de chaque exercice.

\subsection*{Problème de Post} 

\noindent \textbf{\emph{Taille du groupe:}} jusqu'à 4.

\noindent \textbf{\emph{A rendre le}} 19 décembre 2001.

Écrivez un programme qui permet de trouver la plus petite solution
d'un problème de correspondance de Post et permet ensuite de trouver des
problèmes avec des très grandes plus petites solutions sur le modèle
du concours proposé par le site \emph{PCP at home}.  Le travail sera
jugé sur l'organisation et la (les) méthode(s) employées et la qualité
du compte-rendu.  Si de plus vous avez vraiment réussi à vous placer
dans la liste proposée par \emph{PCP at home}, ça n'en sera que mieux.

\noindent \textbf{Note importante:}  vous pouvez utilisez les cycles de
vos ordinateurs personnels et \underline{très} raisonnablement les
moyens de l'École, mais en aucun cas vous ne pouvez utilisez
illégalement ces moyens.  Si vous avez vraiment besoin de puissance de
calcul, consultez-moi.



\subsection*{Preuve en COQ}

\noindent \textbf{\emph{Taille du groupe:}} jusqu'à 4.

\noindent \textbf{\emph{A rendre le}} 24 octobre 2001.

En ajoutant une constante \texttt{False} qui satisfait
\begin{center}
  \texttt{(p:proposition) (theorem False => p)},
\end{center}
démontrez en \textsc{Coq} 
\begin{verbatim}
 (p,q:proposition) 
    (theorem (((p => False) => False) => p) => ((p => q) => p) => p).
\end{verbatim}
Le résultat sera envoyé par courrier électronique à
\textsf{Pierre.Lescanne@ens-lyon.fr} sous forme d'un fichier
exécutable commenté.

\newpage
\subsection*{Fonctions convexes}

\noindent \textbf{\emph{Taille du groupe:}} 2.

\noindent \textbf{\emph{A rendre le}} 17 octobre 2001.

Une fonction $f : \R \rightarrow  \R$ est convexe si 
\[(\forall x_1\in\R)(\forall x_2\in\R)\ \  f\left(\frac{x_1+x_2}{2}\right) \le
\frac{f(x_1)+f(x_2)}{2}.\] 
\begin{enumerate}
\item Montrez que pour tout $n\in\N^+$ et  $x_1\in\R,..., x_n\in\R$,
\[f\left(\frac{x_1+....+x_n}{n}\right) \le
\frac{f(x_1)+...+f(x_n)}{n}.\] \textsf{Indication:} On montrera entre
autres que si l'inégalité est satisfaite pour $n+1$ nombres alors elle
est satisfaite pour $n$ nombres.

\item Énoncez la règle d'induction utilisée sur le modèle de
  $\mathit{Ind_C}$ ci-dessous.

\item Prouvez la l'équivalence de cette règle d'induction avec la
  règle
\[\mathit{Ind_C}: (\forall P)\ ([P(0) \vee (\forall n) P(n)
\Rightarrow P(n+1)] \Rightarrow (\forall k) P(k)).\]

\end{enumerate}



\end{document}
% LocalWords:  PCP at False theorem consultez-moi
