From 877a92cbab58c072e915ce82ce83758152a5b0a1 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Mon, 22 Jan 2024 12:49:02 +0100
Subject: Improve that last exercise.

---
 controle-20240126.tex | 28 +++++++++++++++++++++++++---
 1 file changed, 25 insertions(+), 3 deletions(-)

diff --git a/controle-20240126.tex b/controle-20240126.tex
index b48ed48..343c58c 100644
--- a/controle-20240126.tex
+++ b/controle-20240126.tex
@@ -113,6 +113,8 @@ Git: \input{vcline.tex}
 
 \exercice
 
+(Dans cet exercice, on ne demande pas de justifier les réponses.)
+
 \textbf{(1)} En calcul propositionnel intuitionniste, quelle est la
 conclusion de la démonstration représentée par le $\lambda$-terme
 suivant ?  (Ou si on préfère : quel est le type de ce terme du
@@ -127,14 +129,25 @@ $\lambda$-calcul simplement typé enrichi de types produits ?)
 \textbf{(2)} En logique du premier ordre, quelle est la conclusion de
 la démonstration représentée par le $\lambda$-terme suivant ?
 \[
+\lambda(p: C\land\forall x. B(x))).\,
+\lambda(x:I).\,
+\langle (\pi_1 p),\,(\pi_2 p)x\rangle
+\]
+(Ici, $C$ est une variable de relation nullaire, c'est-à-dire une
+variable propositionnelle, $B$ est une variable de relation unaire, et
+$I$ est le symbole du type des individus.)
+
+\textbf{(3)} En logique du premier ordre, quelle est la conclusion de
+la démonstration représentée par le $\lambda$-terme suivant ?
+\[
 \lambda(p: \exists x.(A\Rightarrow B(x))).\,
 \lambda(h:A).\,
 (\texttt{match~}p\texttt{~with~}\langle x,j\rangle
 \mapsto \langle x,jh\rangle)
 \]
 (Ici, $A$ est une variable de relation nullaire, c'est-à-dire une
-variable propositionnelle, $B$ est une variable de relation unaire, et
-$x$ est une variable d'individu.)
+variable propositionnelle, et $B$ est une variable de relation
+unaire.)
 
 \begin{corrige}
 \textbf{(1)} Dans le contexte où $p$ a type $C\land(A\Rightarrow B)$
@@ -145,7 +158,15 @@ l'expression dans son ensemble a type $C\land(A\Rightarrow B)
 \Rightarrow (A \Rightarrow C\land B)$, i.e., elle représente une
 preuve de cette affirmation.
 
-\textbf{(2)} On se place dans le contexte où $p$ a type $\exists
+\textbf{(2)} On se place dans le contexte où $p$ a type $C\land
+\forall x. B(x)$ et $x$ est un individu.  Alors $\pi_1 p$ a type $C$
+et $\pi_2 p$ a type $\forall z. B(z)$, si bien que $(\pi_2 p)x$ a type
+$B(x)$, et $\langle (\pi_1 p),\,(\pi_2 p)x\rangle$ a type $C\land
+B(x)$, donc l'expression dans son ensemble a type $(C\land \forall
+x. B(x)) \Rightarrow \forall x. (C\land B(x))$, i.e., elle représente
+une preuve de cette affirmation.
+
+\textbf{(3)} On se place dans le contexte où $p$ a type $\exists
 x.(A\Rightarrow B(x))$ et $h$ a type $A$.  Le \texttt{match} va
 déstructurer $p$ en un $x$ individu et un $j$ de type $A\Rightarrow
 B(x)$.  Alors $jh$ a type $B(x)$, et $\langle x,jh\rangle$ a type
@@ -155,6 +176,7 @@ x. B(x))$, i.e., elle représente une preuve de cette affirmation.
 \end{corrige}
 
 
+
 %
 %
 %
-- 
cgit v1.2.3