pieuvre/RapportPresentation/ex-rapport.tex

\documentclass{article}

\usepackage[T1]{fontenc}
\usepackage{xcolor}
\usepackage[french]{babel}
\usepackage{syntax}
\usepackage{listings}
\usepackage{amsmath}
\lstset{
 language=caml,
 columns=[c]fixed,
 basicstyle=\small\ttfamily,
 keywordstyle=\bfseries,
 upquote=true,
 commentstyle=,
 breaklines=true,
 showstringspaces=false}
%% installer texlive-lang-french pour cela

% ci-dessous: commenté car non offert sur les machines libre-service.
% décommentez si vous le souhaitez.
%\usepackage[french]{babel}

% pour compiler: 

% faire    pdflatex ex-rapport
% (si les references aux numeros de parties apparaissent comme des
% "?", recompiler une fois)

% la compilation de la bibliographie est davantage une "incantation":
% faire     bibtex ex-biblio
% puis      pdflatex ex-rapport (un nombre premier de fois)


% vous pouvez ensuite ouvrir le fichier ex-rapport.pdf




% elements du titre
\title{Pieuvre: le mini assitant de preuve}
\author{Marwan et Augustin}
\date{}

% definition de quelques macros, pour les maths
\newcommand{\litt}{\alpha}
\newcommand{\non}[1]{\overline{#1}}
\newcommand{\TODO}[1]{\textbf{\color{red}#1}}
\begin{document}

\maketitle

\section{Présentation}

Nous avons programmé \textbf{Pieuvre}, un assistant de preuve
pour la logique intuitionniste en \textbf{OCaml}.
Il permet, à l'aide d'une boucle interactive, de prouver des
prédicats simples.

Nous indiquons dans la partie~\ref{s:opt} comment compiler,
lancer et utiliser notre programme.
Nous exposons ensuite à la partie~\ref{s:orga} comment notre
programme est structuré.
Nous présentons enfin dans la partie~\ref{s:stlc} notre
implémentation du $\lambda$-calcul simplement typé puis dans
les parties~\ref{s:proof} et~\ref{s:tactic} notre
implémentation des preuves et des tactiques.

\section{Compiler et exécuter}
\label{s:opt}
Pour compiler : \lstinline{make pieuvre}

Pour exécuter \textbf{Pieuvre} et entrer dans la boucle
interactive de l'assistant de preuve, il suffit d'entrer la
commande \lstinline{./pieuvre}.
Sinon, on peut spécifier un des modes suivants:
\begin{itemize}
	\item \texttt{-alpha}

		qui vérifie l'$\alpha$-équivalence
		de deux $\lambda$-termes séparés par \lstinline{&}.

	\item \texttt{-reduce}

		qui affiche les $\beta$-réduction
		successives du $\lambda$-terme.
\end{itemize}
\section{Organisation du code}
\label{s:orga}

Le code est structuré de la manière suivante~:
\begin{itemize}
\item \lstinline{parser.mly} et \lstinline{lexel.mll}
	qui définissent l'analyse
	syntaxique du $\lambda$-calcul simplément typé
	ainsi que des tactiques.

\item \lstinline{lam.ml} qui contient notre implémentation
	du $\lambda$-calcul simplement typé.

\item \lstinline{types.ml} qui contient la définition
	des \lstinline{types} et \lstinline{typing.ml}
	qui implémente l'algorithme de typage bidirectionnel
	défini dans la partie~\ref{s:stlc}.
\item \lstinline{proof.ml} qui définit la structure d'une preuve
	et implémente les tactiques.

\item \lstinline{main.ml} le point d'entrée de notre programme
	qui fait l'interface avec l'utilisateur.
\end{itemize}

\section{$\lambda$-calcul simplement typé}
\label{s:stlc}
Avant de pouvoir réaliser des preuves, il faut pouvoir les encoder.
On utilise le $\lambda$-calcul simplement typé.
Dans notre programme, on utilise la syntaxe suivante
pour les types et pour les termes:


\begin{grammar}
	<A, B> ::= \lstinline{X}
	\alt \lstinline{A -> B}
	\alt \lstinline{A /\ B}
	\alt \lstinline{A \/ B}
	\alt \lstinline{false}
\end{grammar}

\begin{grammar}
	<M, N> ::= x
	  \alt \lstinline{fun (x : A)  => M}
	  \alt \lstinline{M N}
	  \alt \lstinline{exf (M : A)}
	  \alt \lstinline{l(M : A \/ B)}
	  \alt \lstinline{r(M : A \/ B)}
	  \alt \lstinline{(M, N)}
\end{grammar}
Les termes ainsi définis se réduisent à l'aide des règles de
$\beta$-réduction rappelées dans les notes de
Selinger~\cite{SelingerNotes}.
Avant d'être $\beta$-réduit par \lstinline{betastep},
les termes sont d'abord
$\alpha$-convertis avec \lstinline{alpha_convert} afin d'éviter
les problèmes de substitution.

On remarque que l'on impose d'annoter le type de l'argument
d'une $\lambda$-abstraction, des constructeurs de termes somme
et produit.
On peut alors vérifier le type de tous les termes de manière
déterministe avec les règles de typage suivantes:


\[
	\dfrac
	{\lstinline{x : A} \in \Gamma}
	{\Gamma \vdash \lstinline{x : A}}
\]

\[
	\dfrac
	{\Gamma, \lstinline{x : A} \vdash \lstinline{M : B}}
	{\Gamma \vdash \lstinline{fun (x : A) => M : A -> B}}
\]

\[
	\dfrac{\Gamma \vdash \lstinline{M : A -> B}
	\quad \Gamma \vdash \lstinline{N : A}}
	{\Gamma \vdash \lstinline{M N} : \lstinline{B}}
\]

\[
	\dfrac
	{\Gamma \vdash \lstinline{M : false}}
	{\Gamma \vdash \lstinline{exf (M : A) : A}}
\]

\[
	\dfrac
	{\Gamma \vdash \lstinline{M : A}
	\quad \Gamma \vdash \lstinline{N : B}}
	{\Gamma \vdash \lstinline{(M, N) : A /\\ B}}
\]

\[
	\dfrac
	{\Gamma \vdash \lstinline{M : A}}
	{\Gamma \vdash \lstinline{l(M : A \\/ B) : A \\/ B}}
	\quad \quad
	\dfrac
	{\Gamma \vdash \lstinline{M : B}}
	{\Gamma \vdash \lstinline{r(M : A \\/ B) : A \\/ B}}
\]

\section{Preuves}
\label{s:proof}

Pour construire la preuve d'une proposition,
on se base sur la correspondance de
Curry-Howard :
ainsi, construire une preuve correspond à créer
un~$\lambda$-terme dont le type correspond à la proposition.

Les~$\lambda$-termes de preuves sont des~$\lambda$-termes
particuliers au sens où ils sont \textbf{creux}.
Intuitivement, les~$\lambda$-termes creux, ou~\lstinline{hlam},
sont des termes avec des trous.
Compléter la preuve correspond
à remplir ces trous à l'aide de tactique.


Lorsqu'on déclare un but, on lui assigne donc :
\begin{itemize}
    \item un lambda terme creux (\verb|Ref (ref Hole)|) que l'on construit petit à petit à l'aide des tactiques.
    \item le type associé à ce que l'on souhaite prouver
    \item son contexte, c'est à dire un liste d'hypothèses (nom de l'hypothèse, type, $\lambda$-terme possiblement encore creux qui sera mis à jour facilement grâce aux \verb|ref|s)
\end{itemize}
Au moment du \verb|Qed|, ce $\lambda$-terme de preuve qui a
été gardé de côté est $\beta$-réduit puis typé contre le type
du but définit au moment de \verb|Goal|.


\section{Tactiques}
\label{s:tactic}

Dans le mode générique, le programme démarre un assistant de preuve interactif semblable à Coq.
Voici les commandes et tactiques implémentées:

\begin{itemize}
    \item \verb|Goal| pour émettre un nouveau but
    \item \verb|Undo| pour annuler la dernière tactique
    \item \verb|Qed| pour clore la preuve d'un but
    \item \verb|exact| si une hypothèse correspond parfaitement à notre but courant
    \item \verb|assumption| recherche automatique d'une hypothèse correspondant au but courant
    \item \verb|intro| pour défaire une implication
    \item \verb|intros| pour répéter \verb|intro| autant que possible
    \item \verb|cut| permet de faire une élimination
		de la coupure.
    \item \verb|apply H| où \verb|H| est une implication
		avec le but courant en conclusion permet de prouver
		directement les prémisses de l'implication.
    \item \verb|split| permet de prouver un côté puis l'autre
		d'une conjonction
    \item \verb|left| et \verb|right| permettent de choisir
		quel côté de la conjonction prouver
	\item \verb|try| pour essayer une tactique. Si elle échoue,
		rien ne se passe.
\end{itemize}

\section{Conlusion}
Nous avons présenté notre assistant de preuve \textbf{Pieuvre}.
Il permet de prouver des prédicats logiques simples.
Plusieurs extensions (et améliorations) sont envisageables.

Tout d'abord, on pourrait évidemment enrichir la grammaire
et les tactiques pour avoir un langage plus expressif.
On pourrait également laisser la possibilité à l'utilisateur
de prouver des \verb|lemmes| et des \verb|théorèmes| pour les
sauvegarder et les réutiliser plus tard.
Il faudrait alors également proposer les types dépendants.

Enfin, il faut se poser la question de la fiabilité de notre
assistant de preuve. Il serait difficile de prouver formellement
toutes les composantes du programme (la~$\beta$-réduction,
l'~$\alpha$-conversion, le \verb|typecheck|, etc.).
Ainsi, on propose de sauvegarder les termes de preuves puis de
les envoyer à Coq pour valider la preuve.

\bibliographystyle{plain}
\bibliography{ex-biblio}

\section{Répartition du travail}
\begin{itemize}
	\item parser et lexer pour le~$\lambda$-calcul et les tactiques (Marwan)
	\item exfalso et typage bidirectionnel (Marwan)
	\item $\beta$-réduction (Marwan)
	\item système de preuve (définition des \verb|hlam|,
		des contextes, des buts, etc.) (Marwan)
	\item les tactiques exact, assumption, intro, intros,
		cut, apply et try (Marwan)
	\item $\alpha$-équivalence / renommage (Augustin)
	\item fonctionnement du \verb|main| (options, arguments, etc.)
		(Augustin)
	\item boucle interactive et interface utilisateur
		(Augustin)
	\item les tactiques Goal, Qed, left, right et split (Augustin)
	\item Undo (Augustin)
\end{itemize}

\end{document}