Non-uniqueness of proofs.

1 files changed, 57 insertions, 1 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 50a442d..5083da9 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -2255,9 +2255,65 @@ fun u -> (match (pi1 u) with Inj1 v -> Inj1 v\\
 
 \end{frame}
 %
+\begin{frame}
+\frametitle{Les preuves ne sont pas uniques}
+
+{\footnotesize La question de l'égalité est compliquée, on ne
+  l'abordera guère.\par}
+
+\itempoint Une même proposition peut avoir des preuves
+(fonctionnellement) \alert{différentes}.
+
+\medskip
+
+Par exemple, les entiers de Church typés :
+\begin{itemize}
+\item $\overline{0}_{\alpha} :=
+  \lambda(f:\alpha\to\alpha).\lambda(x:\alpha).x$
+\item $\overline{1}_{\alpha} :=
+  \lambda(f:\alpha\to\alpha).\lambda(x:\alpha).fx$
+\item $\overline{2}_{\alpha} :=
+  \lambda(f:\alpha\to\alpha).\lambda(x:\alpha).f(fx)$ etc.
+\end{itemize}
+tous de type $(\alpha\to\alpha)\to(\alpha\to\alpha)$ prouvent tous
+$(A\Rightarrow A)\Rightarrow(A\Rightarrow A)$.
+
+\medskip
+
+{\footnotesize
+
+($\overline{0}$) : « [\textbf{(1)} Supposons $A\Rightarrow A$.
+    [\textbf{(2)} Supposons $A$.]  \textbf{(3)} On a $A\Rightarrow A$
+    par $\Rightarrow$Int de (2) dans (2).]  \textbf{(4)} On a
+  $(A\Rightarrow A)\Rightarrow(A\Rightarrow A)$ par $\Rightarrow$Int
+  de (1) dans (3). »
+
+\medskip
+
+($\overline{1}$) : « [\textbf{(1)} Supposons $A\Rightarrow A$.
+  [\textbf{(2)} Supposons $A$.  \textbf{(3)} On a $A$ par
+    $\Rightarrow$Élim sur (1) et (2).]  \textbf{(4)} On a
+  $A\Rightarrow A$ par $\Rightarrow$Int de (2) dans (3).]
+\textbf{(5)} On a $(A\Rightarrow A)\Rightarrow(A\Rightarrow A)$ par
+$\Rightarrow$Int de (1) dans (4). »
+
+\medskip
+
+($\overline{2}$) : « [\textbf{(1)} Supposons $A\Rightarrow A$.
+  [\textbf{(2)} Supposons $A$.  \textbf{(3)} On a $A$ par
+    $\Rightarrow$Élim sur (1) et (2).  \textbf{(4)} On a $A$ par
+    $\Rightarrow$Élim sur (1) et (3).]  \textbf{(5)} On a
+  $A\Rightarrow A$ par $\Rightarrow$Int de (2) dans (4).]
+\textbf{(6)} On a $(A\Rightarrow A)\Rightarrow(A\Rightarrow A)$ par
+$\Rightarrow$Int de (1) dans (5). »
+
+\par}
+
+\end{frame}
+%
 % TODO:
 % - substitution des variables propositionnelles par des formules
 % - substitution d'équivalences
-% - Kriple
+% - Kripke
 %
 \end{document}