derniers changements du rapport et catch de Not_found

RapportPresentation/ex-presentation.tex

@@ -92,6 +92,8 @@
 
   \lstinline{Qed}
 
+  \lstinline{Check}
+
   Tactiques:
 
   \lstinline{exact}
@@ -166,7 +168,7 @@
 
 \begin{frame}{Fiabilité}
   \begin{itemize}
-    \item Comment être sûrs de nos preuves
+    \item Comment être sûrs de nos preuves ?
     \pause
     \item Envoyer nos termes de preuves à \textbf{\color{blue}{Coq}}.
   \end{itemize}

RapportPresentation/ex-rapport.tex

@@ -100,8 +100,7 @@ Le code est structuré de la manière suivante~:
 
 \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}.
+	qui implémente l'algorithme de vérification de type.
 \item \lstinline{hlam.ml} qui décrit les~$\lambda$-termes creux,
 	utilisés dans les preuves.
 \item \lstinline{proof.ml} qui définit la structure d'une preuve
@@ -152,7 +151,9 @@ déterministe avec les règles rappelées dans
 le livre de S. Mimram~\cite{SMIM} et \textit{très} brièvement dans le livre de
 Landin~\cite{PJL700}.
 
-
+L'implémentation du~\textit{OU} et du~\textit{ET} est incomplète.
+Nous n'avons pas eu le temps d'implémenter les déconstructeurs associés
+(les projecteurs et le \verb|match|).
 
 \section{Preuves}
 \label{s:proof}
@@ -173,9 +174,11 @@ Compléter la preuve correspond
 
 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 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)
+    \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
@@ -190,8 +193,14 @@ 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|Undo| pour annuler la dernière tactique.
+	Son implémentation est très brutale, on se contente de maintenir une pile des états
+	du terme de preuve. Appliquer cette tactique revient à dépiler l'état courant et à
+	revenir au précédent. L'implémentation pourrait être plus judicieuse.
     \item \verb|Qed| pour clore la preuve d'un but
+	\item \verb|Check| construit le fichier \lstinline{checker.v} qui contient
+	le but courant ainsi qu'un \lstinline{exact} du terme de preuve.
+	Ce fichier est envoyé au top-level de Coq afin d'être vérifié.
     \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
@@ -209,6 +218,11 @@ Voici les commandes et tactiques implémentées:
 		rien ne se passe.
 \end{itemize}
 
+
+Là encore, il manque la tactique~\lstinline|destruct|.
+
+On peut prouver~\lstinline{A -> A /\ A} mais pas l'implication inverse.
+
 \section{Conlusion}
 Nous avons présenté notre assistant de preuve \textbf{Pieuvre}.
 Il permet de prouver des prédicats logiques simples.
@@ -225,8 +239,13 @@ 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.
+Ainsi, on propose de sauvegarder les termes de preuves
+puis de les envoyer à Coq pour valider la preuve.
+Cette approche est assez satisfaisante dans la mesure où
+la construction du terme de preuve repose uniquement sur les tactiques
+et pas sur notre implémentation du~$\lambda$-calcul.
+Ainsi, on peut supposer qu'on n'a jamais de faux-positif:
+si Check valide notre preuve, c'est quelle est valide.
 
 
 \section{Répartition du travail}

typing.ml

@@ -5,7 +5,10 @@ exception Could_not_infer
 
 let rec typecheck (g : gam) (e : lam) (expected_t : ty) : bool =
   match e with
-  Var x -> (List.assoc x g) = expected_t
+  Var x ->
+    begin try (List.assoc x g) = expected_t
+    with Not_found -> false
+    end
   | Fun ((x, actual_t1), e) ->
     begin match expected_t with
     Arr (expected_t1, expected_t2) ->
@@ -52,13 +55,13 @@ and typeinfer (g : gam) (e : lam) : ty =
     Arr (t1, t2) ->
       if typecheck g e2 t1
       then t2
-      else  raise Could_not_infer
-    | _ ->  raise Could_not_infer
+      else raise Could_not_infer
+    | _ -> raise Could_not_infer
     end
   | Exf (e, t) ->
     if typecheck g e t
     then Bot
-    else  raise Could_not_infer
+    else raise Could_not_infer
   | Pair (e1, e2) ->
     And (
       typeinfer g e1,
@@ -69,14 +72,14 @@ and typeinfer (g : gam) (e : lam) : ty =
     Or (t_l, _) ->
       if typecheck g e t_l
       then t
-      else  raise Could_not_infer
-    | _ ->  raise Could_not_infer
+      else raise Could_not_infer
+    | _ -> raise Could_not_infer
     end
   | Right (e, t) ->
     begin match t with
     Or (_, t_r) ->
       if typecheck g e t_r
       then t
-      else  raise Could_not_infer
-    | _ ->  raise Could_not_infer
+      else raise Could_not_infer
+    | _ -> raise Could_not_infer
     end