From 1f69892ba027a5808f31c6e1ac89f0f34083af24 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Mon, 8 Jan 2024 14:20:38 +0100
Subject: Add minor clarifications here and there.

---
 transp-inf110-03-quantif.tex | 26 +++++++++++++++++---------
 1 file changed, 17 insertions(+), 9 deletions(-)

diff --git a/transp-inf110-03-quantif.tex b/transp-inf110-03-quantif.tex
index 78b6e27..beaac0b 100644
--- a/transp-inf110-03-quantif.tex
+++ b/transp-inf110-03-quantif.tex
@@ -162,7 +162,7 @@ $\forall v. P(v)$ {\footnotesize (« une façon de transformer $v$ en un
   témoignage de $P(v)$ »)}, qui est une sorte de \emph{conjonction en
 famille} $\bigwedge_v P(v)$, correspondra au \alert{type produit en
   famille} $\prod_v \sigma(v)$ {\footnotesize (« fonction renvoyant
-  une valeur de $\sigma(v)$ pour chaque $v$ »)}.
+  pour chaque $v$ une valeur de $\sigma(v)$ »)}.
 
 \medskip
 
@@ -232,7 +232,7 @@ $t_0$ correspondant dans autre chose qu'une preuve.  {\footnotesize
 \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
+    transp. suivants) 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}
 
@@ -383,6 +383,8 @@ ces notations pour $\forall, \exists$ :
 si $s$ désigne une preuve de $Q$ faisant intervenir $v$ variable libre
 de type $I$, on notera $\lambda(v:I).\,s$ la preuve de
 $\forall(v:I).\,Q$ obtenue par introduction du $\forall$.
+{\footnotesize (\textbf{N.B.} $v$ peut apparaître dans $Q$ mais pas
+  dans $\Gamma$.)}
 \[
 \inferrule{\Gamma, v:I\vdash s:Q}{\Gamma\vdash \lambda(v:I).\,s\;:\;\forall (v:I).\, Q}
 \]
@@ -394,6 +396,9 @@ $f$ désigne une preuve de $\forall(v:I).\,Q$ et $t$ un terme de
 type $I$, on notera $ft$ la preuve de $Q[v\backslash t]$ {\footnotesize
   (c'est-à-dire $Q$ avec $v$ remplacé par $t$)} obtenue par
 élimination du $\forall$ sur ce terme.
+
+{\footnotesize (\textbf{N.B.} on n'explique pas comment le « terme »
+  $t$ est formé.)}
 \[
 \inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash f \;:\; \forall (v:I).\, Q}{\Gamma\vdash ft \;:\; Q[v\backslash t]}
 \]
@@ -401,8 +406,8 @@ type $I$, on notera $ft$ la preuve de $Q[v\backslash t]$ {\footnotesize
 \medskip
 
 \itempoint Ceci est conforme à l'idée de BHK : une preuve de
-$\forall(v:I).\, Q(v)$ prend un $t$ de type $I$ et renvoie une preuve
-de $Q(t)$.
+$\forall(v:I).\, Q(v)$ prend un $x$ de type $I$ et renvoie une preuve
+de $Q(x)$.
 
 \end{frame}
 %
@@ -421,11 +426,14 @@ du $\exists$.
 \medskip
 
 \itempoint \textcolor{blue}{\underline{Élimination du $\exists$ :}} si
-$z$ désigne une preuve de $\exists(v:I).\,P$ et $s$ une preuve de $Q$
-faisant intervenir $v$ variable libre de type $I$ et $h$ hypothèse
-supposant $P$ (pour ce $v$-là, donc), on notera
-$(\texttt{match~}z\texttt{~with~}\langle v,h\rangle \mapsto s)$ la
-preuve de $Q$ obtenue par élimination du $\exists$.
+$z$ désigne une preuve de $\exists(v:I).\,P$ et $s$ une preuve,
+faisant intervenir $v$ variable libre de type $I$, de $Q$ qui ne fait
+pas intervenir $v$, et $h$ hypothèse supposant $P$ (pour ce $v$-là,
+donc), on notera $(\texttt{match~}z\texttt{~with~}\langle v,h\rangle
+\mapsto s)$ la preuve de $Q$ obtenue par élimination du $\exists$.
+
+{\footnotesize (\textbf{N.B.} $v$ peut apparaître dans $s$ mais pas
+  dans $\Gamma$ ni $Q$.)}
 \[
 \inferrule{\Gamma\vdash z \;:\; \exists (v:I).\, P\\\Gamma,\, v:I,\, h:P\vdash Q}{\Gamma\vdash (\texttt{match~}z\texttt{~with~}\langle v,h\rangle \mapsto s) \;:\; Q}
 \]
-- 
cgit v1.2.3