diff options
| -rw-r--r-- | exercices-inf110.tex | 155 |
1 files changed, 145 insertions, 10 deletions
diff --git a/exercices-inf110.tex b/exercices-inf110.tex index d3c885c..44f9c50 100644 --- a/exercices-inf110.tex +++ b/exercices-inf110.tex @@ -963,8 +963,7 @@ Autrement dit : En Python, avec de petites variations : -{\tt -\noindent +{\tt\noindent def ackermann\_small(m,n,k):\\ \strut\quad \# Returns A(m,n,k) value if m<=1 or n<=1 or k<=2\\ \strut\quad if k==0: return m+n\\ @@ -1952,7 +1951,7 @@ A)$. En Coq, cette preuve s'écrit : -{\tt +{\tt\noindent Parameter A B C : Prop.\\ Theorem thm : A\textbackslash /B -> ((A->B)->B) /\textbackslash\ ((B->A)->A).\\ Proof. intro H. destruct H. split. intro H1. apply H1. exact H. @@ -1993,12 +1992,12 @@ intuitionniste. \textit{(Cette question est sans doute plus facile à traiter en utilisant l'une quelconque des sémantiques vues en cours pour le calcul propositionnel intuitionniste.)} -\textbf{(3)} Montrer qu'il revient au même, en calcul propositionnel -intuitionniste, de postuler $P \lor \neg P$ pour \emph{toute} -proposition $P$, ou bien de postuler $\neg\neg Q \Rightarrow Q$ pour -\emph{toute} proposition $Q$. (Pour le sens qui ne découle pas -immédiatement de (1), on pourra démontrer la proposition $\neg\neg (P -\lor \neg P)$ sans hypothèse.) +\textbf{(3)} Montrer qu'il revient pourtant au même, en calcul +propositionnel intuitionniste, de postuler $P \lor \neg P$ pour +\emph{toute} proposition $P$, ou bien de postuler $\neg\neg Q +\Rightarrow Q$ pour \emph{toute} proposition $Q$. (Pour le sens qui +ne découle pas immédiatement de (1), on pourra démontrer la +proposition $\neg\neg (P \lor \neg P)$ sans hypothèse.) \begin{corrige} \textbf{(1)} Voici une démonstration écrite en informellement en @@ -2013,7 +2012,7 @@ $(A \lor \neg A) \Rightarrow (\neg\neg A \Rightarrow A)$. » En Coq, cette preuve s'écrit : -{\tt +{\tt\noindent Parameter A : Prop.\\ Theorem thm : (A\textbackslash /\textasciitilde A) -> (\textasciitilde\textasciitilde A->A).\\ Proof. intro H. destruct H. split. intro H2. exact H. @@ -2214,6 +2213,142 @@ $\neg\neg(P \lor \neg P)$ (sans hypothèse). Si on postule $\neg\neg Q \lor \neg P$ pour conclure $P \lor \neg P$. \end{corrige} +% + +\exercice\label{exercise-negneg-conjunction}\ (${\star}{\star}$)\par\nobreak + +Montrer $\neg\neg A \land \neg\neg B \Rightarrow \neg\neg (A\land B)$ +en calcul propositionnel intuitionniste. On écrira la preuve très +soigneusement et on en donnera un $\lambda$-terme. + +\begin{corrige} +Voici une preuve écrite informellement en langage naturel : + +Supposons $\neg\neg A\land\neg\neg B$ (donc à la fois $\neg\neg A$ et +$\neg\neg B$), et on veut montrer $\neg\neg (A\land B)$. Pour ça, +supposons $\neg (A\land B)$ et on veut arriver à une contradiction. +Supposons provisoirement qu'on ait $A$. Si de plus on a $B$, alors on +a $A\land B$, ce qui contredit $\neg (A\land B)$ : ceci montre $\neg +B$ (toujours sous l'hypothèse $A$ !) ; mais commme on a $\neg\neg B$, +on a une contradiction. On a donc prouvé $\neg A$ ; mais comme on a +$\neg\neg A$, on a une contradiction. + +La revoici écrite dans le style « drapeau » : +\bgroup\normalsize +\begin{footnotesize} +\begin{flagderiv}[exercise-negneg-conjunction-proof] +\assume{mainhyp}{\neg\neg A\land\neg\neg B}{} +\assume{khyp}{\neg (A\land B)}{} +\step{nna}{\neg\neg A}{$\land$Élim$_1$ sur \ref{mainhyp}} +\assume{ahyp}{A}{} +\step{nnb}{\neg\neg B}{$\land$Élim$_2$ sur \ref{mainhyp}} +\assume{bhyp}{B}{} +\step{conj}{A\land B}{$\land$Int sur \ref{ahyp}, \ref{bhyp}} +\step{contrb}{\bot}{$\Rightarrow$Élim sur \ref{khyp} et \ref{conj}} +\conclude{negb}{\neg B}{$\Rightarrow$Int de \ref{bhyp} dans \ref{contrb}} +\step{contra}{\bot}{$\Rightarrow$Élim sur \ref{nnb} et \ref{negb}} +\conclude{nega}{\neg A}{$\Rightarrow$Int de \ref{ahyp} dans \ref{contra}} +\step{contr}{\bot}{$\Rightarrow$Élim sur \ref{nna} et \ref{nega}} +\conclude{negk}{\neg\neg (A\land B)}{$\Rightarrow$Int de \ref{khyp} dans \ref{contr}} +\conclude{mainconc}{\neg\neg A\land\neg\neg B \Rightarrow \neg\neg (A\land B)}{$\Rightarrow$Int de \ref{mainhyp} dans \ref{negk}} +\end{flagderiv} +\end{footnotesize} +\egroup + +En Coq, cette preuve s'écrit : + +{\tt\noindent +Parameter A : Prop. Parameter B : Prop.\\ +Theorem thm : \textasciitilde\textasciitilde A /\textbackslash\ \textasciitilde\textasciitilde B -> \textasciitilde\textasciitilde(A/\textbackslash B).\\ +Proof. intro H. intro K. destruct H as [H1w H2w]. +apply H1w. intro H1. apply H2w. intro H2. +apply K. split. exact H1. exact H2. Qed. +\par} + +En voici un $\lambda$-terme de preuve : +\[ +\lambda(h:\neg\neg +A\land\neg\neg B). \penalty0\, \lambda(k:\neg(A\land B)). \penalty0\, +(\pi_1 h) \penalty0 (\lambda(h_1:a). \penalty500\, (\pi_2 h) +\penalty1000 (\lambda(h_2:B). \penalty1500\, k\langle h_1, +h_2\rangle)) +\] +(ou en syntaxe Coq : \texttt{fun (H : + \textasciitilde\ \textasciitilde\ A + /\textbackslash\ \textasciitilde\ \textasciitilde\ B) (K : + \textasciitilde\ (A /\textbackslash\ B)) => match H with conj H1w + H2w => H1w (fun H1 : A => H2w (fun H2 : B => K (conj H1 H2))) end} ; +la forme est un peu différente parce que Coq utilise un \texttt{match} +pour déstructurer une conjonction alors que nous avons utilisé $\pi_1$ +et $\pi_2$, mais une fois noté que $\pi_1 h$ et $\pi_2 h$ +correspondent à \texttt{H1w} et \texttt{H2w} c'est bien +essentiellement le même terme). +\end{corrige} + +% + +\exercice\ (${\star}{\star}{\star}$)\par\nobreak + +Montrer qu'il revient pourtant au même, en calcul propositionnel +intuitionniste, de postuler $\neg P \lor \neg\neg P$ pour \emph{toute} +proposition $P$ (« loi faible du tiers exclu »), ou bien de postuler +$\neg (Q\land R) \Rightarrow \neg Q \lor \neg R$ pour \emph{toutes} +propositions $Q,R$ (« quatrième loi de De Morgan »). On pourra +prendre connaissance de la conclusion de +l'exercice \ref{exercise-negneg-conjunction}. + +Expliquer pourquoi $\neg (A\land B) \Rightarrow \neg A \lor \neg B$ +n'est pas démontrable en calcul propositionnel intuitionniste. + +\begin{corrige} +Montrons d'abord que si on postule $\neg P \lor \neg\neg P$ pour toute +proposition $P$, on peut en déduire $\neg (Q\land R) \Rightarrow \neg +Q \lor \neg R$ pour toutes propositions $Q,R$. Soient donc $Q,R$ deux +propositions quelconques (ou variables propositionnelles, si on +préfère), et on veut prouver $\neg (Q\land R) \Rightarrow \neg Q \lor +\neg R$. Supposons $\neg (Q\land R)$ et on veut prouver $\neg Q \lor +\neg R$. Appliquons notre postulat $\neg P \lor \neg\neg P$ avec $P$ +valant $Q$ puis $R$ successivement : on a $\neg Q \lor \neg\neg Q$ et +$\neg R \lor \neg\neg R$ ; par la loi d'élimination du $\lor$, ceci +nous permet de raisonner par cas (dans chaque cas, on cherche à +prouver $\neg Q \lor \neg R$) : dans le cas où $\neg Q$, ainsi que +dans le cas où $\neg R$, on a évidemment $\neg Q \lor \neg R$ ; il +reste donc à traiter le cas où $\neg\neg Q$ et $\neg\neg R$. Or +$\neg\neg A \land \neg\neg B \Rightarrow \neg\neg (A\land B)$ est +démontrable en calcul propositionnel intuitionniste +(exercice \ref{exercise-negneg-conjunction}). Donc on peut affirmer +$\neg\neg (Q\land R)$, ce qui contredit $\neg (Q\land R)$, et une +contradiction permet de tirer n'importe quelle conclusion, notamment +$\neg Q \lor \neg R$. Bref, dans chacun des cas on a bien prouvé +$\neg Q \lor \neg R$. On peut maintenant décharger la supposition +$\neg (Q\land R)$ et affirmer que $\neg (Q\land R) \Rightarrow \neg Q +\lor \neg R$ comme on voulait. + +Réciproquement, montrons que si on postule $\neg (Q\land R) +\Rightarrow \neg Q \lor \neg R$ pour toutes propositions $Q,R$, on +peut en déduire $\neg P \lor \neg\neg P$ pour toute proposition $P$. +Soit donc $P$ une proposition quelconque (ou variable +propositionnelle, si on préfère), et on veut prouver $\neg P \lor +\neg\neg P$. Appliquons notre postulat $\neg (Q\land R) \Rightarrow +\neg Q \lor \neg R$ avec $Q$ valant $P$ et $R$ valant $\neg P$ : il +nous donne $\neg (P\land \neg P) \Rightarrow \neg P \lor \neg\neg P$. +Or $\neg (P\land \neg P)$ est évident (une preuve en est donnée par le +$\lambda$-terme $\lambda(h:P\land\neg P). \penalty0\, (\pi_2 h)(\pi_1 +h)$), donc on a bien $\neg P \lor \neg\neg P$ comme ou voulait. + +Si $\neg (A\land B) \Rightarrow \neg A \lor \neg B$ était démontrable +en calcul propositionnel intuitionniste, on pourrait remplacer les +variables propositionnelles $A,B$ par des propositions $Q,R$ +quelconques. Notamment, d'après ce qu'on vient de voir au paragraphe +précédent, on pourrait démontrer $\neg P \lor \neg\neg P$ pour $P$ une +proposition quelconque. Mais $\neg C \lor \neg\neg C$ n'est +certainement pas prouvable en calcul propositionnel intuitionniste : +car s'il l'était, par la propriété de la disjonction, $\neg C$ ou bien +$\neg\neg C$ le serait, ce qui n'est pas le cas (même classiquement, +on ne peut pas prouver $\neg C$ seul, ni $\neg\neg C$ seul, qui peut +prendre l'une ou l'autre valeur de vérité). +\end{corrige} + % % |