fin du rapport, sujet à modification
This commit is contained in:
Marwan
parent
00c1a116d1
commit
4996209b05
@ -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}
|
||||
|
||||
@ -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"
|
||||
|
||||
@ -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 <return> 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 <return> 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 <return> 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 <return> 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 <return> 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 <return> 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 <return> 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 <return> 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 <return> 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 <return> 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 <return> 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 <return> 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 <return> 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 <return> 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 <return> 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 <return> 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 <return> 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 <return> 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 <return> 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
|
||||
</usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi12.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/share/texmf-dist/fonts/type1/public/cm-super/sfbx1000.pfb></usr/share/texmf-dist/fonts/type1/public/cm-super/sfbx1440.pfb></usr/share/texmf-dist/fonts/type1/public/cm-super/sfrm1000.pfb></usr/share/texmf-dist/fonts/type1/public/cm-super/sfrm1200.pfb></usr/share/texmf-dist/fonts/type1/public/cm-super/sfrm1728.pfb></usr/share/texmf-dist/fonts/type1/public/cm-super/sfti1000.pfb></usr/share/texmf-dist/fonts/type1/public/cm-super/sftt0900.pfb></usr/share/texmf-dist/fonts/type1/public/cm-super/sftt1000.pfb>
|
||||
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)
|
||||
|
||||
|
||||
Binary file not shown.
Binary file not shown.
@ -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}
|
||||
|
||||
Loading…
Reference in New Issue
Block a user