1 files changed, 58 insertions, 0 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index fdb603d..0142fef 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -1503,4 +1503,62 @@ Présentation « drapeau », plus proche de l'écriture naturelle, commode
 
 \end{frame}
 %
+\begin{frame}
+\frametitle{Quelques tautologies du calcul propositionnel intuitionniste}
+
+\itempoint Lorsque $\vdash P$ (sans hypothèse), on dit que $P$ est
+\textbf{valide} dans le calcul propositionnel intuitionniste, ou est
+une \textbf{tautologie} de celui-ci.
+
+\medskip
+
+{\footnotesize
+
+Quelques tautologies importantes (« $P\Leftrightarrow Q$ » abrège
+« $P \Rightarrow Q$ et $Q \Rightarrow P$ ») :
+
+\begin{tabular}{|c|c|}
+\hline
+$A\Rightarrow B\Rightarrow A$&$(A\Rightarrow B\Rightarrow C)
+\Rightarrow (A\Rightarrow B)\Rightarrow A\Rightarrow C$\\
+\hline
+$A\land B \Rightarrow A$\quad\quad\quad$A\land B \Rightarrow B$&$A\Rightarrow A\lor B$\quad\quad\quad$B \Rightarrow A\lor B$\\
+\hline
+$A\Rightarrow B\Rightarrow A\land B$&$(A\Rightarrow C)\Rightarrow(B\Rightarrow C)\Rightarrow A\lor B\Rightarrow C$\\
+\hline
+$A\land B \Leftrightarrow B\land A$&$A\lor B \Leftrightarrow B\lor A$\\
+\hline
+$(A\land B)\land C \Leftrightarrow A\land(B\land C)$&$(A\lor B)\lor C \Leftrightarrow A\lor(B\lor C)$\\
+\hline
+$(A\Rightarrow B)\land (A\Rightarrow C) \Leftrightarrow (A\Rightarrow B\land C)$
+&$(A\Rightarrow C)\land (B\Rightarrow C) \Leftrightarrow (A\lor B \Rightarrow C)$\\
+\hline
+$(A\Rightarrow B)\lor (A\Rightarrow C) \mathrel{\color{red}\Rightarrow} (A\Rightarrow B\lor C)$
+&$(A\Rightarrow C)\lor (B\Rightarrow C) \mathrel{\color{red}\Rightarrow} (A\land B \Rightarrow C)$\\
+\hline
+$A\land(B\lor C) \Leftrightarrow (A\land B)\lor (A\land C)$
+&$A\lor(B\land C) \mathrel{\color{olive}\Leftrightarrow} (A\lor B)\land (A\lor C)$\\
+\hline
+$\top$&$\bot \Rightarrow C$\\
+\hline
+$\top\land A \Leftrightarrow A$&$\bot \land A \Leftrightarrow \bot$\\
+\hline
+$\top\lor A \Leftrightarrow \top$&$\bot \lor A \Leftrightarrow A$\\
+\hline
+$\neg A \land \neg B \Leftrightarrow \neg(A\lor B)$&$\neg A \lor \neg B \mathrel{\color{red}\Rightarrow} \neg(A\land B)$\\
+\hline
+$A \mathrel{\color{red}\Rightarrow} \neg\neg A$&$(\neg\neg A\Rightarrow \neg\neg B) \Leftrightarrow \neg\neg (A\Rightarrow B)$\\
+\hline
+$(\neg\neg A\land \neg\neg B) \Leftrightarrow \neg\neg (A\land B)$
+&$(\neg\neg A\lor \neg\neg B) \mathrel{\color{red}\Rightarrow} \neg\neg (A\lor B)$\\
+\hline
+$(A\Rightarrow B) \mathrel{\color{red}\Rightarrow} (\neg B\Rightarrow \neg A)$
+&$\neg A \Leftrightarrow \neg\neg\neg A$\\
+\hline
+\end{tabular}
+
+\par}
+
+\end{frame}
+%
 \end{document}