Rework the introduction to quantifiers (work in progress!).

1 files changed, 162 insertions, 23 deletions

diff --git a/transp-inf110-03-quantif.tex b/transp-inf110-03-quantif.tex
index 0ef600c..b16fb58 100644
--- a/transp-inf110-03-quantif.tex
+++ b/transp-inf110-03-quantif.tex
@@ -93,9 +93,11 @@ connecteurs propositionnels $\Rightarrow,\land,\lor,\top,\bot$.
 mathématiques au-delà de ces connecteurs : les
 \textbf{quantificateurs} $\forall,\exists$, qui :
 \begin{itemize}
-\item prennent une formule $P(v)$ dépendant d'une variable $v$ libre,
-\item lient cette variable pour former une nouvelle formule $\forall
-  v. P(v)$ ou $\exists v. P(v)$.
+\item prennent une formule $P(v)$ dépendant d'une variable $v$ libre
+  {\footnotesize (de type $I$)},
+\item lient cette variable, pour former une nouvelle formule :
+  $\forall (v:I). P(v)$ ou $\exists (v:I). P(v)$
+  {\footnotesize (parfois juste $\forall v. P(v)$ et $\exists v. P(v)$)}.
 \end{itemize}
 
 \medskip
@@ -113,7 +115,7 @@ comme des « $\land$ et $\lor$ en famille », c'est-à-dire que :
 
 \itempoint Il existe de \alert{nombreux systèmes logiques} différant
 notamment en \alert{ce qu'on a le droit de quantifier} (qui sont les
-$v$ ici ? quel est leur domaine ?).
+$v$ ici ? quel est leur domaine $I$ ?).
 
 \smallskip
 
@@ -137,10 +139,10 @@ maintenant les quantificateurs :
   de transformer un témoignage de $P$ en un témoignage de $Q$,}
 \item {\color{darkgray} un témoignage de $\top$ est trivial,} \quad
   \itempoint {\color{darkgray} un témoignage de $\bot$ n'existe pas,}
-\item un témoignage de $\forall x.P(x)$ est un moyen
+\item un témoignage de $\forall v.P(v)$ est un moyen
   de transformer un $x$ quelconque en un témoignage de $P(x)$,
-\item un témoignage de $\exists x.P(x)$ est la donnée d'un certain
-  $x_0$ et d'un témoignage de $P(x_0)$.
+\item un témoignage de $\exists v.P(v)$ est la donnée d'un certain
+  $t_0$ et d'un témoignage de $P(t_0)$.
 \end{itemize}
 
 \end{frame}
@@ -170,16 +172,17 @@ prendre le produit.
 
 \medskip
 
-\itempoint Une preuve de $\forall v.P(v)$ correspondra à un terme de
-forme $\lambda(v:{?}).\,(\cdots)$, où le type de $(\cdots)$ correspond
-à $P(v)$.
+\itempoint Une preuve de $\forall (v:I).P(v)$ correspondra à un terme
+de forme $\lambda(v:I).\,(\cdots)$, où le type de $(\cdots)$
+correspond à $P(v)$.
 
 \medskip
 
-\itempoint Remarquer que $\forall v.P$, si $P$ ne dépend pas de $v$,
-« ressemble » à $I \Rightarrow P$ de la même manière que $\prod_{i\in
-  I} S = S^I$ (ensemblistement ou numériquement).  {\footnotesize (Les
-  détails dépendent de la nature de la quantification.)}
+\itempoint Remarquer que $\forall (v:I).P$, si $P$ ne dépend pas de
+$v$, « ressemble » à $I \Rightarrow P$ de la même manière que
+$\prod_{i\in I} S = S^I$ (ensemblistement ou numériquement).
+           {\footnotesize (Les détails dépendent de la nature de la
+             quantification.)}
 
 \end{frame}
 %
@@ -195,22 +198,22 @@ forme $\lambda(v:{?}).\,(\cdots)$, où le type de $(\cdots)$ correspond
 \medskip
 
 \itempoint De façon analogue, la \alert{quantification existentielle}
-$\exists v. P(v)$ {\footnotesize (« la donnée d'un $v_0$ et d'un
-  témoignage de $P(v_0)$ »)}, qui est une sorte de \emph{disjonction
+$\exists v. P(v)$ {\footnotesize (« la donnée d'un $t_0$ et d'un
+  témoignage de $P(t_0)$ »)}, qui est une sorte de \emph{disjonction
 en famille} $\bigvee_v P(v)$, correspondra au \alert{type somme en
-  famille} $\sum_v \sigma(v)$ {\footnotesize (« donnée d'un $v_0$ et
-  d'une valeur de type $\sigma(v_0)$ »)}.
+  famille} $\sum_v \sigma(v)$ {\footnotesize (« donnée d'un $t_0$ et
+  d'une valeur de type $\sigma(t_0)$ »)}.
 
 \medskip
 
-\itempoint Une preuve de $\exists v.P(v)$ correspondra à un terme de
-forme $\langle v_0, \cdots\rangle$, où le type de $(\cdots)$
-correspond à $P(v_0)$.  {\footnotesize (De nouveau, il faut des
+\itempoint Une preuve de $\exists (v:I).P(v)$ correspondra à un terme de
+forme $\langle t_0, \cdots\rangle$, où le type de $(\cdots)$
+correspond à $P(t_0)$.  {\footnotesize (De nouveau, il faut des
   « familles de types ».)}
 
 \medskip
 
-\itempoint Remarquer que $\exists v.P$, si $P$ ne dépend pas de $v$,
+\itempoint Remarquer que $\exists (v:I).P$, si $P$ ne dépend pas de $v$,
 « ressemble » à $I \times P$ de la même manière que $\sum_{i\in I} S =
 I\times S$.  {\footnotesize (Les détails dépendent de la nature de la
   quantification.)}
@@ -219,13 +222,149 @@ I\times S$.  {\footnotesize (Les détails dépendent de la nature de la
 
 \itempoint Mais Curry-Howard atteint ses limites : il n'est pas dit
 que d'une preuve de $\exists v.P(v)$ on \alert{puisse extraire} le
-$v_0$ correspondant dans autre chose qu'une preuve.  {\footnotesize
+$t_0$ correspondant dans autre chose qu'une preuve.  {\footnotesize
   (Les détails dépendent du système logique précis considéré {\tiny et
     si Martin-Löf est dans la salle}.)}
 
 \end{frame}
 %
 \begin{frame}
+\frametitle{Règles d'introduction et d'élimination de $\forall$}
+
+{\footnotesize\textcolor{orange}{Les règles ci-dessous (et
+    transp. suivant) sont \alert{incomplètes} : il manque des
+    explications sur le type $I$ sur lequel on quantifie et comment on
+    peut en former des « termes ».}\par}
+
+\medskip
+
+\itempoint \underline{Introduction du $\forall$ :} pour montrer
+$\forall (v:I).\, Q$, on s'arrange (quitte à renommer la variable
+liée) pour que $v:I$ soit « frais », c'est-à-dire qu'il n'apparaisse
+(libre) dans \alert{aucune hypothèse} en cours : si on montre $Q$ sur
+ce $v$ « arbitraire », on peut conclure $\forall (v:I).\, Q$.
+
+\smallskip
+
+{\footnotesize (Rédaction : « soit $v$ arbitraire (…) on a $Q(v)$ ;
+  donc $\forall (v:I).\, Q(v)$ ».)\par}
+
+\medskip
+
+\textcolor{teal}{Ceci donnera un $\lambda$-terme noté
+  $\lambda(v:I).(\cdots)$ comme l'ouverture d'une hypothèse.}
+
+\bigskip
+
+\itempoint \underline{Élimination du $\forall$ :} pour utiliser
+$\forall (v:I). Q$, on peut l'appliquer à un $t$ quelconque (un
+\alert{terme} de type $I$).
+
+\smallskip
+
+{\footnotesize (Rédaction : « on a $\forall (v:I). Q(v)$ et $t$ de
+  type $I$ ; en particulier, on a $Q(t)$ ».)\par}
+
+\medskip
+
+\textcolor{teal}{Ceci donnera un $\lambda$-terme noté $ft$ comme
+  l'application d'une implication.}
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Règles d'introduction et d'élimination de $\exists$}
+
+\itempoint \underline{Introduction du $\exists$ :} pour montrer
+$\exists (v:I). Q$, on peut le montrer sur un terme $t$ quelconque de
+type $I$.
+
+\smallskip
+
+{\footnotesize (Rédaction : « pour ce $t$ de type $I$ on a $Q(t)$ ; en
+  particulier, on a $\exists (v:I). Q(v)$ ».)\par}
+
+\medskip
+
+\textcolor{teal}{Ceci donnera un $\lambda$-terme noté $\langle
+  t,\cdots\rangle$ comme pour une conjonction.}
+
+\bigskip
+
+\itempoint \underline{Élimination du $\exists$ :} pour utiliser
+$\exists (v:I). P(v)$ pour montrer une conclusion $Q$, on s'arrange
+(quitte à renommer la variable liée) pour que $v$ soit « frais »,
+c'est-à-dire qu'il n'apparaisse (libre) dans \alert{aucune hypothèse}
+en cours \alert{ni dans la conclusion} $Q$ : si on montre $Q$ à partir
+de $P$ sur ce $v$ « arbitraire », on peut conclure $Q$ à partir de
+$\exists v. P$.
+
+\smallskip
+
+{\footnotesize (Rédaction : « on a $\exists (v:I). P(v)$ : soit $v$
+  arbitraire tel que $P(v)$ : (…) on a $Q$ ; donc $Q$ ».)\par}
+
+\medskip
+
+\textcolor{teal}{Ceci donnera un $\lambda$-terme noté
+  $(\texttt{match~}\cdots\texttt{~with~}\langle v,h\rangle \mapsto
+  \cdots)$.}
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Aperçu d'ensemble des règles de la déduction naturelle}
+
+\begin{tabular}{c|c|c}
+&Intro&Élim\\\hline
+$\Rightarrow$
+&\scalebox{0.65}{$\inferrule{\Gamma,{\color{mydarkgreen}P}\vdash Q}{\Gamma\vdash P\Rightarrow Q}$}
+&\scalebox{0.65}{$\inferrule{\Gamma\vdash P\Rightarrow Q\\\Gamma\vdash P}{\Gamma\vdash Q}$}
+\\\hline
+$\land$
+&\scalebox{0.65}{$\inferrule{\Gamma\vdash Q_1\\\Gamma\vdash Q_2}{\Gamma\vdash Q_1\land Q_2}$}
+&\scalebox{0.65}{$\inferrule{\Gamma\vdash Q_1\land Q_2}{\Gamma\vdash Q_1}$}
+\quad\scalebox{0.65}{$\inferrule{\Gamma\vdash Q_1\land Q_2}{\Gamma\vdash Q_2}$}
+\\\hline
+$\lor$
+&\scalebox{0.65}{$\inferrule{\Gamma\vdash Q_1}{\Gamma\vdash Q_1\lor Q_2}$}
+\quad\scalebox{0.65}{$\inferrule{\Gamma\vdash Q_2}{\Gamma\vdash Q_1\lor Q_2}$}
+&\scalebox{0.65}{$\inferrule{\Gamma\vdash P_1\lor P_2\\\Gamma,{\color{mydarkgreen}P_1}\vdash Q\\\Gamma,{\color{mydarkgreen}P_2}\vdash Q}{\Gamma\vdash Q}$}
+\\\hline
+$\top$
+&\scalebox{0.65}{$\inferrule{\strut}{\Gamma\vdash \top}$}
+&\scalebox{0.65}{(néant)}
+\\\hline
+$\bot$
+&\scalebox{0.65}{(néant)}
+&\scalebox{0.65}{$\inferrule{\Gamma\vdash \bot}{\Gamma\vdash Q}$
+(ou pour la logique classique : $\inferrule{\Gamma,\neg Q\vdash \bot}{\Gamma\vdash Q}$)}
+\\\hline
+$\forall$
+&$\inferrule{\Gamma, {\color{mydarkgreen}v:I}\vdash Q}{\Gamma\vdash \forall (v:I).\, Q}$ ($v$ \alert{frais})
+&$\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash \forall (v:I).\, Q}{\Gamma\vdash Q[v\backslash t]}$
+\\\hline
+$\exists$
+&$\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash Q[v\backslash t]}{\Gamma\vdash \exists (v:I).\, Q}$
+&$\inferrule{\Gamma\vdash \exists (v:I). P\\\Gamma, {\color{mydarkgreen}v:I}, {\color{mydarkgreen}P}\vdash Q}{\Gamma\vdash Q}$
+($v$ \alert{frais})
+\\
+\end{tabular}
+
+\smallskip
+
+\itempoint « $v$ frais » = « $v$ n'apparaît nulle part ailleurs »
+(cf. transp. précédents).
+
+\smallskip
+
+\itempoint Le contexte $\Gamma$ peut contenir des formules
+(hypothèses) et des variables d'« individus » (avec leur type,
+p.ex. $v:I$).
+
+\end{frame}
+%
+\begin{frame}
 \frametitle{Le problème du $\exists$ et des types sommes}
 
 Doit-on croire à ceci (pour $U$ et $V$ deux types) ?