289 lines
8.9 KiB
TeX
289 lines
8.9 KiB
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}
|