Commit 8345d236 authored by Samuel Ben Hamou's avatar Samuel Ben Hamou
Browse files

Modification mise en page rapport.

parent 042fecc2
......@@ -81,32 +81,35 @@
\newtheorem{pb}[theorem]{Problème}
\usepackage{titlesec}
\titleformat*{\section}{\bf\Large\sffamily}
\titleformat*{\subsection}{\bf\large\sffamily}
\titleformat*{\subsubsection}{\bf\sffamily}
\titleformat*{\section}{\center\bf\Large\sffamily}
\titleformat*{\subsection}{\center\bf\large\sffamily}
\titleformat*{\subsubsection}{\center\bf\sffamily}
\setcounter{tocdepth}{2}
\title{Extensions d'un cours de logique du premier ordre certifié en Coq}
\author{Samuel Ben Hamou}
\date{\today}
\begin{document}
\begin{center}
\vspace*{2em}
\includegraphics[scale=0.45]{logo_ens.png} \hspace*{1cm} \includegraphics[scale=0.1]{logo-irif.png} \\
%\begin{center}
%\vspace*{1em}
\vspace*{6em}
{\LARGE Rapport de stage} \\ \vspace{2em}
{\huge Extensions d'un cours de logique du premier ordre certifié en Coq} \\ \vspace{4em}
%\vspace*{2em}
\includegraphics[scale=0.45]{logo_ens.png} %\hspace*{1cm}
\hfill \includegraphics[scale=0.1]{logo-irif.png} \\
\begin{center}
\vspace*{0.5em}
%\vspace*{6em}
{\LARGE Rapport de stage} \\ \vspace{1em}
{\huge Extensions d'un cours de logique du premier ordre certifié en Coq} \\ \vspace{1.5em}
{\Large Stage effectué du 1 juin au 17 juillet 2020} \\ \vspace{6em}
{\Large Stage effectué du 1 juin au 17 juillet 2020} \\ \vspace{2.5em}
{\Large Samuel Ben Hamou} \\ \smallskip
{\large \'Ecole Normale Supérieure Paris-Saclay} \\
{\large 1ère année, Département Informatique} \\ \vspace{4em}
{\large 1ère année, Département Informatique} \\ \vspace{1.5em}
{\Large Sous la supervision de Pierre Letouzey} \\ \smallskip
{\large IRIF, INRIA et CNRS} \vspace{4em}
{\large IRIF, INRIA et CNRS} \vspace{1.5em}
\end{center}
......@@ -121,17 +124,15 @@ Dans un premier temps, il a fallu se familiariser avec les outils du stage : à
\end{itemize}
\end{abstract}
\newpage
\renewcommand{\contentsname}{\centerline{Table des matières}}
\renewcommand{\contentsname}{\centerline{Table des matières} \vspace*{-2em}}
\tableofcontents
\newpage
% QUES meilleur nom ?
\section{Introduction}
\section*{Introduction}
\subsection{Contexte pratique du stage}
\subsection*{Contexte pratique du stage}
Ce stage a été effectué sous la direction de Pierre Letouzey, maître de conférence à l'Université Paris-Diderot, et membre du groupe $\pi r^2$ de l'IRIF. Compte tenu du contexte sanitaire, la majeur partie des échange a eu lieu par visio-conférence et par mail, à un rythme assez soutenu. J'ai cependant pu me rendre physiquement à l'IRIF afin de discuter dans la vraie vie avec avec mon maître de stage.
......@@ -141,7 +142,7 @@ Il n'en demeure pas moins que le stage a pu se dérouler sans trop d'embûches,
Le dépôt du projet se trouve dans la branche \og Stage \fg{} à l'adresse suivante : \url{https://gitlab.math.univ-paris-diderot.fr/letouzey/natded}.
\subsection{Motivations}
\subsection*{Motivations}
Le but du stage a été d'enrichir l'encodage de \verb+NatDed+ déjà existant, tout en gardant en tête la vocation pédagogique du projet, puisqu'il s'agit d'illustrer un cours de logique de M1 \cite{poly}.
......@@ -149,7 +150,7 @@ Le but du stage a été d'enrichir l'encodage de \verb+NatDed+ déjà existant,
Par la suite, il a été à propos d'ajouter d'autres aspects de la logique à cet encodage, tels que le $\lambda$-calcul et la théorie des ensembles, qui sont tous deux des point abordés dans le cours donné par Pierre Letouzey. En effet, le $\lambda$-calcul est un élément essentiel de la construction des assistants de preuve tels que Coq.
\subsection{Encodage existant et état de l'art}
\subsection*{Encodage existant et état de l'art}
L'encodage \verb+NatDed+ existait déjà avant le stage. \`A ce moment là, il contenait déjà un système de déduction naturelle avec des séquents, ainsi qu'un grand nombre de lemmes et résultats utiles, y compris sur la méta-théorie. Deux méthodes sont possibles pour établir une preuve dans cette encodage : une méthode constructive, reposant sur le prédicat \verb+Pr+ dont la définition est donnée en annexe \ref{pr}, qui permet de construire une preuve pas à pas, mais n'est pas forcément pratique à utiliser pour démontrer des résultats méta-théoriques. L'autre méthode, \verb+Valid+, permet de vérifier qu'une dérivation est bien formée (cela implique donc de fournir directement une dérivation complète, ce qui alourdi considérablement le style des preuves). Le choix qui a été fait pour stage est d'utiliser \verb+Pr+ systématiquement.
......@@ -163,17 +164,17 @@ A priori, il s'agit du premier codage Coq de la déduction naturelle qui allie l
\item \emph{Pédagogie} : avec un peu de patience -- et, je l'espère, en s'aidant du travail effectué pendant le stage -- on peut utiliser ce codage pour illustrer un cours sur la théorie de la démonstration, ou bien justifier que l'on peut admettre un certain nombre de résultats longs à démontrer en exhibant une preuve (plus ou moins lisible à l'\oe il nu) dans ce système.
\end{itemize}
\subsection{Mise en place de l'environnement de travail}
\subsection*{Mise en place de l'environnement de travail}
Avant de se lancer dans le stage à proprement parler, il a fallu consacrer une petite semaine à l'acquisition de réflexes de travail, à la fois sur le support (GitLab) et sur l'encodage lui-même.
\subsubsection{Dépôt Git}
\subsubsection*{Dépôt Git}
La première journée du stage a été passée à appréhender un outil nouveau pour manipuler de gros projets de code : GitLab. \`A ce titre, et pour me fixer les idées, j'ai rédigé la cheatsheet présentée en \ref{gitsheet}.
L'usage de Git a été d'un grand recours, notamment lorsque nous voulions discuter d'un morceau de preuve en visio-conférence, car chacun pouvait travailler et mettre à jour le dépôt de son côté, la fusion se faisant ensuite aisément grâce à la commande \verb+git pull+.
\subsubsection{Premières preuves}
\subsubsection*{Premières preuves}
Afin de me faire la main sur un encodage déjà très évolué, j'ai tenté de démontrer les petits résultats classiques suivants :
\begin{itemize}
......@@ -550,9 +551,9 @@ Pour ce faire, il a suffit d'exhiber le $\lambda$-terme témoin $\lambda x \cdot
%%%
% QUES meilleur nom ?
\section{Conclusion}
\section*{Conclusion}
\subsection{Apports mutuels du stage}
\subsection*{Apports mutuels du stage}
Ce stage m'a permis d'avoir un premier aperçu, quelque peu biaisé du fait des conditions sanitaires, de ce à quoi peut ressembler le quotidien d'un chercheur. J'ai notamment pu découvrir la suprême frustration que constitue le fait d'achopper pendant plusieurs jours sur un problème, qui se trouve ensuite balayé d'un revers de main par quelqu'un d'autre -- en l'occurrence Pierre Letouzey -- soit car cette personne est plus coutumière des outils utilisés, soit tout simplement parce qu'elle trouve la bonne idée qui nous échappait depuis le début. J'ai aussi eu la joie de découvrir la satisfaction que procure un travail qui avance à bon rythme et qui prend une tournure plus intéressante que prévu, satisfaction qui efface sans nul doute l'amertume de des échecs passés.
......@@ -565,7 +566,7 @@ De mon côté, j'espère avoir contribué à rendre le projet \verb+NatDed+ plus
J'espère aussi que mon travail aura permis à Pierre Letouzey de mieux cerner les limites du projet, et que cela l'aidera s'il souhaite poursuivre son travail sur \verb+NatDed+.
\subsection{Prolongements envisageables}
\subsection*{Prolongements envisageables}
Le sujet du stage était volontairement long, et plusieurs points n'ont pas pu être abordés. De plus, au cours du stage, plusieurs perspectives non explorées ont été évoquées, voici donc une liste non-exhaustive de prolongements envisageables de ce stage.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment