fpropworld.tex

\subsection{Function World}
Ce monde nous introduit un outil fondamental de Lean : les fonctions. 
Un élément important à remarquer est qu'en Lean, toutes les fonctions sont curryfiées.


\subsubsection{Niveau 6}
Voici un exemple de niveau de ce monde, le niveau 6, qui demande de créer une fonction de fonctions assez fastidieuse, et qui utilise le fait que ces fonctions sont curryfiées. 
L'énoncé se formule comme ceci : 

\begin{align*}
        & (P, Q, R : \Type) : \\ & (P \to (Q \to R)) \to ((P \to Q) \to (P \to R))
\end{align*}

La preuve est de fait succinte : 
\begin{minted}[mathescape,linenos,numbersep=5pt,frame=lines,framesep=2mm,breaklines, escapeinside = ||]{lean}
intros f g p, -- On introduit les différents éléments/fonctions pour créer la fonction demandée 
apply f p, -- On modifie le but à l'aide de la fonction curryfiée 
exact g p, -- On trouve le résultat demandé 
\end{minted}
Ce qui conclut la preuve.

\subsection{Proposition World}
Dans ce monde on aborde un aspect fondamental de l'assistant de preuves Lean : une preuve est composée d'implications, et c'est ici que les fonctions prennent toute leur importance : pour montrer que A implique B, il suffit de créer une fonction de A vers B, soit un élément de type $A \to B$.
\subsubsection{Niveau 1}
Pour illustrer ce point, voici un exemple simple, le tout premier niveau de Proposition World. 

\mintinline[breaklines]{lean}|lemma : (P,Q : Prop) (p : P) (h : P → Q) : Q|

Donc, en français, on dispose d'une preuve de P, et d'une fonction de P dans Q (i-e d'un élément de type $P \to Q$), trouvons un élément de type Q (montrons que Q est vrai). 
Ce qui se résout tout aussi succintement : 

\mint{lean}|exact h(p),| 

\subsubsection{Niveau 8}
Un autre niveau intéressant est le niveau 8, qui propose une preuve du lemme suivant, une implication de l'équivalence entre une proposition et sa contraposée (si cela a du sens) : 

\begin{minted}[mathescape,linenos,numbersep=5pt,frame=lines,framesep=2mm,breaklines, escapeinside = ||]{lean}
lemma : |($P \to Q) \to (\lnot Q \to \lnot P)$|. 

-- En Lean, on demande donc de créer une fonction qui prend une preuve que $P \to Q$ et renvoie une preuve de $\lnot Q \to \lnot P$.
intro f, -- On dispose d'une preuve de $P\to Q$ 
-- Lean nous demande alors de créer un élément de type $\lnot Q \to \lnot P$, qui serait l'image de la fonction qu'il nous est demandé de créer.
repeat{rw not_iff_imp_false}, -- On retranscrit la définition de $\lnot P$ :  $\lnot P \equiv P \to false$.
-- Le but est alors réécrit en $(Q \to false) \to P \to false$, ce qui revient à créer une fonction curryfiée des éléments de type $(Q \to false) \times P$ vers les preuves de $false$. On réapplique la même technique d'introduire un élément de chacun des ensembles de départ : 
intros h p,
-- On dispose alors d'un élément p de P, d'une fonction f de P dans Q et d'une fonction h de Q dans $false$, et il nous faut créer une preuve de $false$, qui est facilement trouvable avec : 
exact h(f(p)), -- Ce qui conclut la preuve. 
\end{minted}


\subsection{Advanced Proposition World}
\subsubsection{Niveau 8}
Dans ce monde on démontre à l'aide de fonctions et de nouvelles méthodes les règles de base de la manipulation de consjonctions et disjonctions logiques. Un exemple combinant la plupart des nouvelles méthodes est le Lemme suivant : 


\begin{minted}[mathescape,numbersep=5pt,frame=lines,framesep=2mm,breaklines, escapeinside = ||]{lean}
lemma : (P,Q,R : Prop) : |$P \land (Q \lor R) \leftrightarrow (P \land Q) \lor (P \land R)$|
\end{minted}

Ici on ne démontrera que l'implication directe, l'implication réciproque se faisant de façon similaire.
Pour séparer les implications, une technique existe : \texttt{split}, qui permet de montrer d'abord l'implication directe puis l'implication réciproque. A noter que cette technique permet aussi de séparer le but en plusieurs buts lorsqu'on a à montrer une conjonction de propositions.
Pour gérer les disjonctions de propositions, la technique \texttt{cases} existe et permet, par exemple, quand on sait que $P\lor Q$, dans un premier temps supposer P puis supposer Q. Cette technique permet aussi de séparer les conjonctions connues en plusieurs nouvelles données : si l'on a un élément pq de $P\land Q$, \texttt{cases pq with p q} nous renvoie deux éléments p et q de P et Q respectivement.
Finalement, lorsqu'on doit montrer une disjonction de propositions, il suffit d'en montrer une, et les techniques \texttt{left} et \texttt{right} nous permettent de choisir la proposition à démontrer.
La preuve est donc la suivante : 
\begin{minted}[mathescape,linenos,numbersep=5pt,frame=lines,framesep=2mm,breaklines, escapeinside = ||]{lean}
intro h,     -- h de type $P \land (Q \lor R)$
cases h with p qor,     -- p de type P , qor de type $Q \lor R$
cases qor with q r,     -- On sépare en deux cas en fonction de la disjonction :

-- Premier cas : q de type Q
left,    -- On choisit de montrer $P \land Q$
split,     -- On sépare en deux buts
exact p,
exact q,

-- Deuxième cas : r de type R
right,      -- On choisit de montrer $P \land R$
split,     -- On sépare en deux buts
exact p,
exact r, -- Ce qui conclut la preuve de l'implication directe.
\end{minted}