% vim:expandtab:sts=4:sw=4
% anaseto@bardinflor.perso.aquilenet.fr, licence cc-by-sa
% dernière version sur :
% http://bardinflor.perso.aquilenet.fr/elsxutajxoj/agreg/developpements
\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{lmodern}
\usepackage{microtype}
\usepackage[french]{babel}

\usepackage{stmaryrd}
%%% outils mathématiques {{{
\usepackage{amsmath,amssymb,amsfonts,mathtools,dsfont}

%%%% ensembles
\newcommand{\ensemblenombre}[1]{\ensuremath{\mathbb{#1}} }
% complexes, entiers, rationnels, réels, etc...
\newcommand{\C}{\ensemblenombre{C}}
\newcommand{\D}{\ensemblenombre{D}}
\newcommand{\F}{\ensemblenombre{F}}
\newcommand{\K}{\ensemblenombre{K}}
\newcommand{\N}{\ensemblenombre{N}}
\newcommand{\Q}{\ensemblenombre{Q}}
\newcommand{\R}{\ensemblenombre{R}}
\newcommand{\U}{\ensemblenombre{U}}
\newcommand{\Z}{\ensemblenombre{Z}}
\renewcommand*{\P}{\ensemblenombre{P}} % L'ensemble P
\renewcommand*{\S}{\mathfrak{S}} % L'ensemble S (groupe symétrique)
\newcommand*{\A}{\mathfrak{A}} % L'ensemble A (groupe alterné)

% lettres caligrafiées
\renewcommand*{\cal}{\mathcal} % pour les A,B ronds etc..

%% restrictions
\newcommand*{\res}{\mathclose{}|\mathopen{}}

%%%%%%%%%%%% fonctions pratiques %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%% classiques
\newcommand*{\abs}[1]{\ensuremath{\left| #1 \right|}} %valeur absolue
\newcommand*{\di}{\ensuremath{\mathop{}\mathopen{}\mathrm{d}} } % le «d» de dx
\newcommand*{\implique}{\ensuremath{\Rightarrow}} % mieux \implies
\newcommand*{\mdl}[1]{\ensuremath{\left|  #1  \right|}} %module
\newcommand*{\norminf}[1]{\ensuremath{\left\| #1 \right\|_{\infty}} } %norme infinie
\newcommand*{\norm}[1]{\ensuremath{\left\| #1 \right\|}} %norme
\newcommand*{\pe}[1]{\ensuremath{\lfloor  #1  \rfloor}} %partie_entière
\newcommand*{\ps}[2]{\ensuremath{\big( #1|#2\big)}} % produit scalaire.
\newcommand*{\ssig}{\ensuremath{\Longleftrightarrow}} %si et seulement si: la grande
\newcommand*{\ssi}{\ensuremath{\Leftrightarrow}} % si et seulement si: petite flèche
\newcommand*{\vide}{\phi} % ensemble vide
\newcommand{\ind}{\mathds{1}}

%%% moins classiques
\newcommand*{\leg}[2]{\ensuremath{\left( \frac{#1}{#2} \right)}} % legendre

% dérivée partielle #1-ième de #2 par rapport à #3, pareil mais sans l'ordre. Idem pour
% les dérivées totales.
\newcommand*{\dpto}[3][ ]{\ensuremath{\frac{\partial^{#1} #2}{\partial #3^{#1} }} }
\newcommand*{\dpt}[2]{\ensuremath{\frac{\partial #1}{\partial #2}} }
\newcommand*{\dto}[3][ ]{\ensuremath{\frac{d^{#1} #2}{d^{#1} #3}} }
\newcommand*{\dt}[2]{\ensuremath{\frac{d #1}{d #2}} }

\renewcommand*{\vec}{\ensuremath{\overrightarrow}} %pour les vecteurs 

% A --> B
% x |-> y
\newcommand{\fun}[4]{%
    \begin{matrix}
        #1 & \to & #2 \
        #3 & \mapsto & #4
    \end{matrix}}
% fonction avec le nom en plus
% f: A --> B
%    x |-> y
\newcommand{\nfun}[5]{%
    \begin{matrix}
        #1\colon & #2 & \to & #3 \
           & #4 & \mapsto & #5
    \end{matrix}}

%%%%% nom de fonctions courantes %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% operators
\DeclareMathOperator{\Poin}{Poin}
\DeclareMathOperator{\tr}{tr}
\DeclareMathOperator{\im}{Im}
\DeclareMathOperator{\aut}{Aut}
\DeclareMathOperator{\argth}{Argth}
\DeclareMathOperator{\var}{Var}
\DeclareMathOperator{\argch}{Argch}
\DeclareMathOperator{\rang}{rang}
\DeclareMathOperator{\supp}{supp}
\DeclareMathOperator{\com}{com}
\DeclareMathOperator{\adh}{adh}
\DeclareMathOperator{\argsh}{Argsh}
\DeclareMathOperator{\ch}{ch}
\DeclareMathOperator{\Int}{Int}
\DeclareMathOperator{\residu}{Res}
\DeclareMathOperator{\spec}{Spec}
\DeclareMathOperator{\isom}{Isom}
\DeclareMathOperator{\diag}{diag}
\DeclareMathOperator{\gal}{Gal}
\DeclareMathOperator{\indice}{Ind}
\DeclareMathOperator{\cov}{Cov}
\DeclareMathOperator{\mat}{mat}
\DeclareMathOperator{\Ir}{Ir}
\DeclareMathOperator{\id}{id}
\DeclareMathOperator{\pgcd}{pgcd}
\DeclareMathOperator{\stab}{Stab}
\DeclareMathOperator{\sh}{sh}
\DeclareMathOperator{\vect}{Vect}
\DeclareMathOperator{\disc}{disc}
\DeclareMathOperator{\card}{Card}
\DeclareMathOperator{\ppcm}{ppcm}
\DeclareMathOperator{\conv}{Conv}
\renewcommand*{\ker}{\ensuremath{\mathrm{Ker}} } % noyau
\newcommand*{\rond}[1]{\ensuremath{\overset{\hphantom{l}\circ}{#1}} } % ex: pour l'intérieur

\renewcommand*{\th}{\ensuremath{\mathrm{th}} }

% pour «e»
\newcommand{\e}{\mathrm{e}}

%% plus joli
\renewcommand{\leq}{\leqslant}
\renewcommand{\geq}{\geqslant}

% compatibilité
\newcommand{\ensemble}[2]{{#1 \mid #2}}
% }}}

%%% Théorèmes {{{
\usepackage{amsthm}
\usepackage{ifthen}

% Styles
\newtheoremstyle{note}%
    {4pt}% space above
    {4pt}% space below
    {}% body font
    {}% indent amount
    {}% theorem head font
    {.}% punctuation after theorem head
    {.5em}% space after theorem head
    {\textsc{\thmname{#1}\thmnumber{~#2}}\thmnote{~(\textit{#3})}}

\newtheoremstyle{theorema}%
    {4pt}{4pt}{}{}{}{.}{.5em}
    {\textbf{\thmname{#1}\thmnumber{~#2}}\thmnote{~(\textit{#3})}}

% Théorèmes:
% \theoremstyle{style}
% \newtheorem{nom}[compteur]{texte}[compteur réinitialiasant]
\theoremstyle{theorema}

\newtheorem{theoreme}{Théorème}

\newtheorem{proposition}[theoreme]{Proposition}
\newtheorem{lemme}[theoreme]{Lemme}
\newtheorem{axiome}{Axiome}
\newtheorem{corollaire}[theoreme]{Corollaire}
\newtheorem{conjecture}[theoreme]{Conjecture}

\theoremstyle{note} %définitions

\newtheorem*{definition}{Définition}
\newtheorem*{exemple}{Exemple}
\newtheorem*{application}{Application}
\newtheorem*{remarque}{Remarque}
\newtheorem*{notation}{Notation}
\newtheorem*{notations}{Notations}
\newtheorem*{probleme}{Question}
\newtheorem*{rappel}{Rappel}
\newtheorem*{conclusion}{Conclusion}
\newtheorem*{resume}{Résumé}
\newtheorem*{contrexemple}{Contre-exemple}
% }}}

\title{Correction des règles de Hoare}
\author{}
\date{}
\DeclareMathOperator{\Aexpv}{Aexpv}
\DeclareMathOperator{\Aexp}{Aexp}
\DeclareMathOperator{\Var}{Var}
\DeclareMathOperator{\Av}{\cal{A}v}
\DeclareMathOperator{\Assn}{Assn}

\begin{document}

\maketitle

On ommet dans les assertions les notations pour les interprétations, ce
qui n'a aucune conséquence dans le déroulement de la preuve. Pour le
reste, la preuve est celle de \cite{WI}.

\begin{lemme}
    \label{lem:avsubts}
    Soient $a,a_0\in \Aexpv$, et $X\in \Var$. Alors pour tout état
    $\sigma$,
    \[
        \Av\llbracket a_0[a/X]\rrbracket \sigma = \Av\llbracket a_0
        \rrbracket \sigma [\Av\llbracket a \rrbracket \sigma / X]
    \]
\end{lemme}

\begin{proof}
    Induction structurelle sur $a_0$.
\end{proof}

\begin{lemme}
    \label{lem:statesubst}
    Soit $B\in \Assn$, $X\in \Var$ et $a\in \Aexp$. Alors pour tout état
    $\sigma$ :
    \[
    \sigma \models B[a/X] \text{ ssi } \sigma[\cal{A}\llbracket a
    \rrbracket \sigma / X] \models B.
    \]
\end{lemme}

\begin{proof}
    Induction structurelle sur $B$.
\end{proof}

\begin{theoreme}
    Soit un triplet de Hoare $\{A\}c\{B\}$. Alors $\vdash
    \{A\}c\{B\}$ implique $\models \{A\}c\{B\}$.
\end{theoreme}

On remarque que pour montrer le théorème, il suffit de prouver que
chaque règle de Hoare est correcte, car on peut alors déduire le
théorème par induction sur le nombre de règles dans une preuve.

\paragraph{Skip :} $\models\{A\}\bold{skip}\{A\}$ est clair.

\paragraph{Affectation :} Notons $c\equiv (\texttt{X := a})$. On a
$\sigma \models B[a/X]$ ssi $\sigma[\cal{A}\llbracket a \rrbracket
\sigma /X] \models B$ d'après le lemme \ref{lem:statesubst}, donc
$\sigma \models B[a/X] \implies C\llbracket \texttt{X := a}\rrbracket
\sigma \models B$, d'où $\models\{B[a/X]\} X := a \{B\}$.

\paragraph{Séquence :} Supposons $\models \{A\} c \{C\}$ et
$\models\{C\}c_1\{B\}$. Supposons $\sigma \models A$. Alors $C\llbracket
c_0 \rrbracket \sigma \models C$ car $\models \{A\} c_0 \{C\}$. On a
aussi $C\llbracket c_1 \rrbracket (C\llbracket c_0 \rrbracket \sigma)
\models B$ car $\models \{C\} c_1 \{B\}$. D'où $\models\{A\}
c_0\;c_1\{B\}$.

\paragraph{Conditionnelle :} Supposons $\models \{A \wedge b\} c_0
\{B\}$ et $\models \{A \wedge \neg b\} c_1 \{B\}$. Supposons $\sigma
\models A$. Ou bien $\sigma \models b$ ou bien $\sigma \models \neg b$.
Dans le premier cas $\sigma \models A \wedge b$ donc $C\llbracket c_0
\rrbracket \sigma \models B$. Dans le deuxième analoguement $C\llbracket
c_1\rrbracket \sigma \models B$ aussi, donc $\models\{A\}\text{\textbf{ if
}} b
\text{ \textbf{then} } c_0 \text{\textbf{ else }} c_1\{B\}$.

\paragraph{Boucles While :} Supposons $\models\{A\wedge b\}c\{A\}$, i.e
$A$ invariant de $w \equiv \text{\textbf{while} } b \text{ \textbf{ do
}} c$. On sait que $C\llbracket w\rrbracket = \lim_n \theta_n$ avec des
$\theta_n$ de domaine croissant, et définis de sorte que :
\[
\theta_{n+1} \colon \sigma \mapsto
\begin{cases}
    \sigma & \text{ si } \cal{B}\llbracket b \rrbracket \sigma =
    \text{ \textbf{false}}\\
    (\theta_n \circ C\llbracket c \rrbracket) \sigma & \text{ si }
    \cal{B} \llbracket b\rrbracket \sigma = \text{ \textbf{true}}.
\end{cases}
\]

Montrons par induction sur $n$, $P(n)$ : $\forall \sigma, \sigma'\in
\Sigma$,
\[
    (\theta_n(\sigma) = \sigma'\text{ et } \sigma\models A) \implies
    (\sigma' \models A \wedge \neg b)
\]
On aura alors $\sigma \models A \implies C\llbracket w\rrbracket \sigma
\models A \wedge \neg b$ pour tout $\sigma \in \Sigma$, d'où $\models
\{A\} w \{A \wedge \neg b\}$ comme voulu.

\emph{Cas $n = 0$}. Il est très vrai.
\emph{Induction.} On suppose $P(n)$ pour un $n\geq 0$. Supposons
$\theta_{n+1}\sigma = \sigma'$, et $\sigma \models A$. Deux cas sont
possibles :
\begin{enumerate}
    \item $\cal{B} \llbracket b\rrbracket \sigma = $ \textbf{true} et
    $\sigma' = (\theta_n \circ C\llbracket c \rrbracket) \sigma$;
    \item $\cal{B} \llbracket b\rrbracket \sigma = $ \textbf{false} et
    $\sigma = \sigma'$.
\end{enumerate}
Montrons que dans les deux cas $\sigma' \models A \wedge \neg b$.
\begin{enumerate}
    \item On a $\sigma \models b$ donc $\sigma \models A \wedge b$. D'où
    il existe $\sigma'' \in \Sigma$ tel que $\sigma'' = C\llbracket
    c\rrbracket \sigma$ et $\sigma' = \theta_n\sigma''$. D'où $\sigma''
    \models A$ car $\models \{A\wedge b\} c \{A\}$ (hypothèse du while).
    Par hypothèse d'induction $\sigma' \models A\wedge \neg b$.
    \item Ici $\sigma \models A \wedge \neg b$. Mais $\sigma = \sigma'$
    donc c'est fini.
\end{enumerate}

\paragraph{Conséquence :} Supposons $\models (A \implies A')$ et
$\models \{A'\} c \{B'\}$ et $\models (B' \implies B)$. Supposons
$\sigma \models A$. Alors $\sigma\models A'$, d'où $C\llbracket
c\rrbracket \sigma \models B'$ et donc $C\llbracket c \rrbracket \sigma
\models B$. D'où $\models \{A\}c\{B\}$.

\begin{thebibliography}{1}
   \bibitem{WI}
    G.Winskel, \emph{The Formal Semantics of Programming Languages}.
\end{thebibliography}

\end{document}
