diff --git a/RapportPresentation/ex-rapport.aux b/RapportPresentation/ex-rapport.aux index 80a291e..c951a3d 100644 --- a/RapportPresentation/ex-rapport.aux +++ b/RapportPresentation/ex-rapport.aux @@ -12,12 +12,15 @@ \@writefile{toc}{\contentsline {section}{\numberline {3}Organisation du code}{1}{}\protected@file@percent } \newlabel{s:orga}{{3}{1}{}{}{}} \citation{SelingerNotes} +\@writefile{toc}{\contentsline {section}{\numberline {4}$\lambda $-calcul simplement typé}{2}{}\protected@file@percent } +\newlabel{s:stlc}{{4}{2}{}{}{}} +\@writefile{toc}{\contentsline {section}{\numberline {5}Preuves}{3}{}\protected@file@percent } +\newlabel{s:proof}{{5}{3}{}{}{}} +\@writefile{toc}{\contentsline {section}{\numberline {6}Tactiques}{3}{}\protected@file@percent } +\newlabel{s:tactic}{{6}{3}{}{}{}} +\@writefile{toc}{\contentsline {section}{\numberline {7}Conlusion}{3}{}\protected@file@percent } \bibstyle{plain} \bibdata{ex-biblio} \bibcite{SelingerNotes}{1} -\@writefile{toc}{\contentsline {section}{\numberline {4}$\lambda $-calcul simplement typé}{2}{}\protected@file@percent } -\newlabel{s:stlc}{{4}{2}{}{}{}} -\@writefile{toc}{\contentsline {section}{\numberline {5}Preuves}{2}{}\protected@file@percent } -\newlabel{s:proof}{{5}{2}{}{}{}} -\@writefile{toc}{\contentsline {section}{\numberline {6}Vérification des preuves}{2}{}\protected@file@percent } -\gdef \@abspage@last{3} +\@writefile{toc}{\contentsline {section}{\numberline {8}Répartition du travail}{4}{}\protected@file@percent } +\gdef \@abspage@last{4} diff --git a/RapportPresentation/ex-rapport.fdb_latexmk b/RapportPresentation/ex-rapport.fdb_latexmk index 0aa3b92..1c558c3 100644 --- a/RapportPresentation/ex-rapport.fdb_latexmk +++ b/RapportPresentation/ex-rapport.fdb_latexmk @@ -1,13 +1,13 @@ # Fdb version 4 -["bibtex ex-rapport"] 1715673124.42722 "ex-rapport.aux" "ex-rapport.bbl" "ex-rapport" 1715675326.19747 0 - "./ex-biblio.bib" 1715672341.14715 878 b24a3ee5eaad1f378a00844cfb93a00b "" +["bibtex ex-rapport"] 1715699264.87395 "ex-rapport.aux" "ex-rapport.bbl" "ex-rapport" 1715705388.52522 0 + "./ex-biblio.bib" 1715679705.69998 878 b24a3ee5eaad1f378a00844cfb93a00b "" "/usr/share/texmf-dist/bibtex/bst/base/plain.bst" 1713199481 20613 bd3fbfa9f64872b81ac57a0dd2ed855f "" - "ex-rapport.aux" 1715675325.91528 1056 73909169f0984220be1f002f5c1fdca4 "pdflatex" + "ex-rapport.aux" 1715705388.22718 1282 9f68572beef99d3d362ece324dcd844f "pdflatex" (generated) "ex-rapport.bbl" "ex-rapport.blg" (rewritten before read) -["pdflatex"] 1715675325.3409 "ex-rapport.tex" "ex-rapport.pdf" "ex-rapport" 1715675326.19786 2 +["pdflatex"] 1715705387.64229 "ex-rapport.tex" "ex-rapport.pdf" "ex-rapport" 1715705388.5256 2 "/usr/share/texmf-dist/fonts/enc/dvips/cm-super/cm-super-t1.enc" 1713199481 2971 def0b6c1f0b107b3b936def894055589 "" "/usr/share/texmf-dist/fonts/map/fontname/texfonts.map" 1713199481 3524 cb3e574dea2d1052e39280babc910dc8 "" "/usr/share/texmf-dist/fonts/tfm/jknappen/ec/ecbx1000.tfm" 1713199481 3584 2d666ecf6d466d8b007246bc2f94d9da "" @@ -76,9 +76,9 @@ "/usr/share/texmf-dist/web2c/texmf.cnf" 1713199481 41588 b43d3e860a4f94167ee1e725ff526a72 "" "/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map" 1715669800.4283 5312086 49e033e8d3948bcca48e0612d8828e70 "" "/var/lib/texmf/web2c/pdftex/pdflatex.fmt" 1715669744 7119913 84688908edcaa506b571016b2546b806 "" - "ex-rapport.aux" 1715675325.91528 1056 73909169f0984220be1f002f5c1fdca4 "pdflatex" - "ex-rapport.bbl" 1715673124.50549 167 f13b79c5d213ac0741acd90cb6ff3d89 "bibtex ex-rapport" - "ex-rapport.tex" 1715675323.56847 4800 822b40565accad567b431e11f1652783 "" + "ex-rapport.aux" 1715705388.22718 1282 9f68572beef99d3d362ece324dcd844f "pdflatex" + "ex-rapport.bbl" 1715699264.97094 167 f13b79c5d213ac0741acd90cb6ff3d89 "bibtex ex-rapport" + "ex-rapport.tex" 1715705386.27388 9099 54e3d582f6b866f34c22f8c59a54fe57 "" (generated) "ex-rapport.aux" "ex-rapport.log" diff --git a/RapportPresentation/ex-rapport.log b/RapportPresentation/ex-rapport.log index 637ba3e..f0afd92 100644 --- a/RapportPresentation/ex-rapport.log +++ b/RapportPresentation/ex-rapport.log @@ -1,4 +1,4 @@ -This is pdfTeX, Version 3.141592653-2.6-1.40.26 (TeX Live 2024/Arch Linux) (preloaded format=pdflatex 2024.5.14) 14 MAY 2024 10:28 +This is pdfTeX, Version 3.141592653-2.6-1.40.26 (TeX Live 2024/Arch Linux) (preloaded format=pdflatex 2024.5.14) 14 MAY 2024 18:49 entering extended mode restricted \write18 enabled. file:line:error style messages enabled. @@ -228,185 +228,297 @@ LaTeX Font Info: ... okay on input line 49. LaTeX Info: Redefining \degres on input line 49. LaTeX Info: Redefining \up on input line 49. \c@lstlisting=\count298 -LaTeX Font Info: Trying to load font information for T1+cmtt on input line 70. +LaTeX Font Info: Trying to load font information for T1+cmtt on input line 71. (/usr/share/texmf-dist/tex/latex/base/t1cmtt.fd File: t1cmtt.fd 2023/04/13 v2.5m Standard LaTeX font definitions ) [1 {/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}{/usr/share/texmf-dist/fonts/enc/dvips/cm-super/cm-super-t1.enc}] LaTeX Font Info: Font shape `T1/cmtt/bx/n' in size <9> not available -(Font) Font shape `T1/cmtt/m/n' tried instead on input line 129. +(Font) Font shape `T1/cmtt/m/n' tried instead on input line 130. -LaTeX Font Warning: Command \small invalid in math mode on input line 151. +LaTeX Font Warning: Command \small invalid in math mode on input line 155. -./ex-rapport.tex:151: LaTeX Error: Command \ttfamily invalid in math mode. +./ex-rapport.tex:155: LaTeX Error: Command \ttfamily invalid in math mode. See the LaTeX manual or LaTeX Companion for explanation. Type H for immediate help. ... -l.151 {\Gamma \vdash \lstinline{x : A}} +l.155 {\Gamma \vdash \lstinline{x : A}} Please use the math alphabet \mathtt instead of the \ttfamilyFB command. -LaTeX Font Warning: Command \small invalid in math mode on input line 151. +LaTeX Font Warning: Command \small invalid in math mode on input line 155. -./ex-rapport.tex:151: LaTeX Error: Command \ttfamily invalid in math mode. +./ex-rapport.tex:155: LaTeX Error: Command \ttfamily invalid in math mode. See the LaTeX manual or LaTeX Companion for explanation. Type H for immediate help. ... -l.151 {\Gamma \vdash \lstinline{x : A}} +l.155 {\Gamma \vdash \lstinline{x : A}} Please use the math alphabet \mathtt instead of the \ttfamilyFB command. -LaTeX Font Warning: Command \small invalid in math mode on input line 157. +LaTeX Font Warning: Command \small invalid in math mode on input line 161. -./ex-rapport.tex:157: LaTeX Error: Command \ttfamily invalid in math mode. +./ex-rapport.tex:161: LaTeX Error: Command \ttfamily invalid in math mode. See the LaTeX manual or LaTeX Companion for explanation. Type H for immediate help. ... -l.157 ...sh \lstinline{fun (x : A) => M : A -> B}} +l.161 ...sh \lstinline{fun (x : A) => M : A -> B}} Please use the math alphabet \mathtt instead of the \ttfamilyFB command. -LaTeX Font Warning: Command \small invalid in math mode on input line 157. +LaTeX Font Warning: Command \small invalid in math mode on input line 161. -./ex-rapport.tex:157: LaTeX Error: Command \ttfamily invalid in math mode. +./ex-rapport.tex:161: LaTeX Error: Command \ttfamily invalid in math mode. See the LaTeX manual or LaTeX Companion for explanation. Type H for immediate help. ... -l.157 ...sh \lstinline{fun (x : A) => M : A -> B}} +l.161 ...sh \lstinline{fun (x : A) => M : A -> B}} Please use the math alphabet \mathtt instead of the \ttfamilyFB command. -./ex-rapport.tex:157: LaTeX Error: Command \bfseries invalid in math mode. +LaTeX Font Warning: Command \small invalid in math mode on input line 161. + + +./ex-rapport.tex:161: LaTeX Error: Command \ttfamily invalid in math mode. See the LaTeX manual or LaTeX Companion for explanation. Type H for immediate help. ... -l.157 ...sh \lstinline{fun (x : A) => M : A -> B}} +l.161 ...sh \lstinline{fun (x : A) => M : A -> B}} + +Please use the math alphabet \mathtt instead of the \ttfamilyFB command. + + +./ex-rapport.tex:161: LaTeX Error: Command \bfseries invalid in math mode. + +See the LaTeX manual or LaTeX Companion for explanation. +Type H for immediate help. + ... + +l.161 ...sh \lstinline{fun (x : A) => M : A -> B}} Please use the math alphabet \mathbf instead of the \bfseries command. -LaTeX Font Warning: Command \small invalid in math mode on input line 163. +LaTeX Font Warning: Command \small invalid in math mode on input line 167. -./ex-rapport.tex:163: LaTeX Error: Command \ttfamily invalid in math mode. +./ex-rapport.tex:167: LaTeX Error: Command \ttfamily invalid in math mode. See the LaTeX manual or LaTeX Companion for explanation. Type H for immediate help. ... -l.163 ...a \vdash \lstinline{M N} : \lstinline{B}} +l.167 ...a \vdash \lstinline{M N} : \lstinline{B}} Please use the math alphabet \mathtt instead of the \ttfamilyFB command. -LaTeX Font Warning: Command \small invalid in math mode on input line 163. +LaTeX Font Warning: Command \small invalid in math mode on input line 167. -./ex-rapport.tex:163: LaTeX Error: Command \ttfamily invalid in math mode. +./ex-rapport.tex:167: LaTeX Error: Command \ttfamily invalid in math mode. See the LaTeX manual or LaTeX Companion for explanation. Type H for immediate help. ... -l.163 ...a \vdash \lstinline{M N} : \lstinline{B}} +l.167 ...a \vdash \lstinline{M N} : \lstinline{B}} Please use the math alphabet \mathtt instead of the \ttfamilyFB command. -LaTeX Font Warning: Command \small invalid in math mode on input line 163. +LaTeX Font Warning: Command \small invalid in math mode on input line 167. -./ex-rapport.tex:163: LaTeX Error: Command \ttfamily invalid in math mode. +./ex-rapport.tex:167: LaTeX Error: Command \ttfamily invalid in math mode. See the LaTeX manual or LaTeX Companion for explanation. Type H for immediate help. ... -l.163 ...a \vdash \lstinline{M N} : \lstinline{B}} +l.167 ...a \vdash \lstinline{M N} : \lstinline{B}} Please use the math alphabet \mathtt instead of the \ttfamilyFB command. -LaTeX Font Warning: Command \small invalid in math mode on input line 163. +LaTeX Font Warning: Command \small invalid in math mode on input line 167. -./ex-rapport.tex:163: LaTeX Error: Command \ttfamily invalid in math mode. +./ex-rapport.tex:167: LaTeX Error: Command \ttfamily invalid in math mode. See the LaTeX manual or LaTeX Companion for explanation. Type H for immediate help. ... -l.163 ...a \vdash \lstinline{M N} : \lstinline{B}} +l.167 ...a \vdash \lstinline{M N} : \lstinline{B}} Please use the math alphabet \mathtt instead of the \ttfamilyFB command. -LaTeX Font Warning: Command \small invalid in math mode on input line 169. +LaTeX Font Warning: Command \small invalid in math mode on input line 173. -./ex-rapport.tex:169: LaTeX Error: Command \ttfamily invalid in math mode. +./ex-rapport.tex:173: LaTeX Error: Command \ttfamily invalid in math mode. See the LaTeX manual or LaTeX Companion for explanation. Type H for immediate help. ... -l.169 {\Gamma \vdash \lstinline{exf (M : A) : A}} +l.173 {\Gamma \vdash \lstinline{exf (M : A) : A}} Please use the math alphabet \mathtt instead of the \ttfamilyFB command. -LaTeX Font Warning: Command \small invalid in math mode on input line 169. +LaTeX Font Warning: Command \small invalid in math mode on input line 173. -./ex-rapport.tex:169: LaTeX Error: Command \ttfamily invalid in math mode. +./ex-rapport.tex:173: LaTeX Error: Command \ttfamily invalid in math mode. See the LaTeX manual or LaTeX Companion for explanation. Type H for immediate help. ... -l.169 {\Gamma \vdash \lstinline{exf (M : A) : A}} +l.173 {\Gamma \vdash \lstinline{exf (M : A) : A}} Please use the math alphabet \mathtt instead of the \ttfamilyFB command. -(./ex-rapport.bbl [2]) [3] (./ex-rapport.aux) + +LaTeX Font Warning: Command \small invalid in math mode on input line 180. + + +./ex-rapport.tex:180: LaTeX Error: Command \ttfamily invalid in math mode. + +See the LaTeX manual or LaTeX Companion for explanation. +Type H for immediate help. + ... + +l.180 ...amma \vdash \lstinline{(M, N) : A /\\ B}} + +Please use the math alphabet \mathtt instead of the \ttfamilyFB command. + + +LaTeX Font Warning: Command \small invalid in math mode on input line 180. + + +./ex-rapport.tex:180: LaTeX Error: Command \ttfamily invalid in math mode. + +See the LaTeX manual or LaTeX Companion for explanation. +Type H for immediate help. + ... + +l.180 ...amma \vdash \lstinline{(M, N) : A /\\ B}} + +Please use the math alphabet \mathtt instead of the \ttfamilyFB command. + + +LaTeX Font Warning: Command \small invalid in math mode on input line 180. + + +./ex-rapport.tex:180: LaTeX Error: Command \ttfamily invalid in math mode. + +See the LaTeX manual or LaTeX Companion for explanation. +Type H for immediate help. + ... + +l.180 ...amma \vdash \lstinline{(M, N) : A /\\ B}} + +Please use the math alphabet \mathtt instead of the \ttfamilyFB command. + + +LaTeX Font Warning: Command \small invalid in math mode on input line 186. + + +./ex-rapport.tex:186: LaTeX Error: Command \ttfamily invalid in math mode. + +See the LaTeX manual or LaTeX Companion for explanation. +Type H for immediate help. + ... + +l.186 ...ash \lstinline{l(M : A \\/ B) : A \\/ B}} + +Please use the math alphabet \mathtt instead of the \ttfamilyFB command. + + +LaTeX Font Warning: Command \small invalid in math mode on input line 186. + + +./ex-rapport.tex:186: LaTeX Error: Command \ttfamily invalid in math mode. + +See the LaTeX manual or LaTeX Companion for explanation. +Type H for immediate help. + ... + +l.186 ...ash \lstinline{l(M : A \\/ B) : A \\/ B}} + +Please use the math alphabet \mathtt instead of the \ttfamilyFB command. + + +LaTeX Font Warning: Command \small invalid in math mode on input line 190. + + +./ex-rapport.tex:190: LaTeX Error: Command \ttfamily invalid in math mode. + +See the LaTeX manual or LaTeX Companion for explanation. +Type H for immediate help. + ... + +l.190 ...ash \lstinline{r(M : A \\/ B) : A \\/ B}} + +Please use the math alphabet \mathtt instead of the \ttfamilyFB command. + + +LaTeX Font Warning: Command \small invalid in math mode on input line 190. + + +./ex-rapport.tex:190: LaTeX Error: Command \ttfamily invalid in math mode. + +See the LaTeX manual or LaTeX Companion for explanation. +Type H for immediate help. + ... + +l.190 ...ash \lstinline{r(M : A \\/ B) : A \\/ B}} + +Please use the math alphabet \mathtt instead of the \ttfamilyFB command. + +[2] [3] (./ex-rapport.bbl) [4] (./ex-rapport.aux) *********** LaTeX2e <2023-11-01> patch level 1 L3 programming layer <2024-02-20> *********** ) Here is how much of TeX's memory you used: - 6176 strings out of 476047 - 90478 string characters out of 5792626 - 1979187 words of memory out of 5000000 - 28259 multiletter control sequences out of 15000+600000 + 6181 strings out of 476047 + 90507 string characters out of 5792626 + 2030187 words of memory out of 5000000 + 28264 multiletter control sequences out of 15000+600000 569761 words of font info for 64 fonts, out of 8000000 for 9000 14 hyphenation exceptions out of 8191 - 56i,8n,65p,214b,1232s stack positions out of 10000i,1000n,20000p,200000b,200000s + 56i,8n,65p,231b,1232s stack positions out of 10000i,1000n,20000p,200000b,200000s -Output written on ex-rapport.pdf (3 pages, 185810 bytes). +Output written on ex-rapport.pdf (4 pages, 195685 bytes). PDF statistics: - 75 PDF objects out of 1000 (max. 8388607) - 45 compressed objects within 1 object stream + 78 PDF objects out of 1000 (max. 8388607) + 47 compressed objects within 1 object stream 0 named destinations out of 1000 (max. 500000) 1 words of extra memory for PDF output out of 10000 (max. 10000000) diff --git a/RapportPresentation/ex-rapport.pdf b/RapportPresentation/ex-rapport.pdf index c37ea8f..87192c5 100644 Binary files a/RapportPresentation/ex-rapport.pdf and b/RapportPresentation/ex-rapport.pdf differ diff --git a/RapportPresentation/ex-rapport.synctex.gz b/RapportPresentation/ex-rapport.synctex.gz index 1876d87..3b36ae5 100644 Binary files a/RapportPresentation/ex-rapport.synctex.gz and b/RapportPresentation/ex-rapport.synctex.gz differ diff --git a/RapportPresentation/ex-rapport.tex b/RapportPresentation/ex-rapport.tex index 3aac58d..76f7387 100644 --- a/RapportPresentation/ex-rapport.tex +++ b/RapportPresentation/ex-rapport.tex @@ -61,9 +61,10 @@ 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~\ref{s:stlc} notre implémentation -du $\lambda$-calcul simplement typé puis \ref{s:proof} -notre implémentation des preuves. +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} @@ -129,6 +130,9 @@ pour les types et pour les termes: \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 @@ -139,12 +143,12 @@ $\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. Tous les termes sont alors -typables avec les règles bidirectionnelles suivantes: +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: -\TODO{règles de typage} - \[ \dfrac {\lstinline{x : A} \in \Gamma} @@ -153,13 +157,13 @@ typables avec les règles bidirectionnelles suivantes: \[ \dfrac - {\Gamma \vdash \lstinline{M : B}} + {\Gamma, \lstinline{x : A} \vdash \lstinline{M : B}} {\Gamma \vdash \lstinline{fun (x : A) => M : A -> B}} \] \[ - \dfrac{\Gamma \vdash M : \lstinline{A -> B} - \quad \Gamma \vdash N : \lstinline{A}} + \dfrac{\Gamma \vdash \lstinline{M : A -> B} + \quad \Gamma \vdash \lstinline{N : A}} {\Gamma \vdash \lstinline{M N} : \lstinline{B}} \] @@ -169,17 +173,116 @@ typables avec les règles bidirectionnelles suivantes: {\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} -\TODO{Augustin} +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. -\section{Vérification des preuves} -\TODO{parler de la vérification de preuve, -quelles difficultés ? quelles certitudes ?} +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}