From 618450ebbd0c2c49d7f53f12e3d66021c7b1dae1 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Sun, 3 Dec 2023 23:39:26 +0100
Subject: Non-uniqueness of proofs.

---
 transp-inf110-02-typage.tex | 58 ++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 57 insertions(+), 1 deletion(-)

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
@@ -2253,11 +2253,67 @@ fun u -> (match (pi1 u) with Inj1 v -> Inj1 v\\
 {\color{purple}- : ('a, 'b) sum * ('a, 'c) sum -> ('a, 'b * 'c) sum = <fun>}
 }
 
+\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}
-- 
cgit v1.2.3