Yet another presentation of natural deduction proofs (flag presentation).

1 files changed, 38 insertions, 2 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 3746973..fdb603d 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -8,7 +8,6 @@
 \usepackage{lmodern}
 \DeclareUnicodeCharacter{00A0}{~}
 \DeclareUnicodeCharacter{2026}{...}
-\DeclareUnicodeCharacter{1E25}{\d{h}}
 % Beamer theme:
 \usetheme{Goettingen}
 %\usecolortheme{albatross}
@@ -22,6 +21,7 @@
 %
 \usepackage{mathrsfs}
 \usepackage{mathpartir}
+\usepackage{flagderiv}
 %
 \usepackage{graphicx}
 \usepackage{tikz}
@@ -31,6 +31,7 @@
 \renewcommand{\thefootnote}{\textdagger}
 \newcommand{\dbllangle}{\mathopen{\langle\!\langle}}
 \newcommand{\dblrangle}{\mathclose{\rangle\!\rangle}}
+\setlength{\derivskip}{4pt}
 %
 %
 %
@@ -1425,7 +1426,8 @@ $\bot$
 
 On peut aussi n'écrire que les conclusions (partie droite du
 signe $\vdash$), à condition d'indiquer pour chaque hypothèse
-déchargée à quel endroit elle l'a été :
+déchargée à quel endroit elle l'a été (ceci sacrifie de la lisibilité
+pour un gain de place) :
 
 \bigskip
 
@@ -1467,4 +1469,38 @@ déchargée à quel endroit elle l'a été :
 
 \end{frame}
 %
+\begin{frame}
+\frametitle{Encore une présentation différente}
+
+Présentation « drapeau », plus proche de l'écriture naturelle, commode
+à vérifier :
+
+{\footnotesize
+\begin{flagderiv}[example-proof1]
+\assume{conj}{A\land B}{}
+\step{partb}{B}{$\land$Élim$_2$ sur \ref{conj}}
+\step{parta}{A}{$\land$Élim$_1$ sur \ref{conj}}
+\step{newconj}{B\land A}{$\land$Int sur \ref{partb}, \ref{parta}}
+\conclude{}{A\land B \Rightarrow B\land A}{$\Rightarrow$Int de \ref{conj} dans \ref{newconj}}
+\end{flagderiv}
+\par}
+
+\vskip-2ex
+
+{\footnotesize
+\begin{flagderiv}[example-proof2]
+\assume{disj}{A\lor B}{}
+\assume{parta}{A}{}
+\step{fromparta}{B\lor A}{$\lor$Int$_2$ sur \ref{parta}}
+\done
+\assume{partb}{B}{}
+\step{frompartb}{B\lor A}{$\lor$Int$_1$ sur \ref{partb}}
+\done
+\step{newdisj}{B\lor A}{$\lor$Élim sur \ref{disj} de \ref{parta} dans \ref{fromparta} et de \ref{partb} dans \ref{frompartb}}
+\conclude{}{A\lor B \Rightarrow B\lor A}{$\Rightarrow$Int de \ref{disj} dans \ref{newdisj}}
+\end{flagderiv}
+\par}
+
+\end{frame}
+%
 \end{document}