From 74b4b47860513fa25387275634b85bca8eca690c Mon Sep 17 00:00:00 2001
From: Mysaa <samy.avrillon@ens-lyon.fr>
Date: Wed, 3 Aug 2022 20:54:04 +0200
Subject: [PATCH] =?UTF-8?q?D=C3=A9but=20de=20la=20nouvelle=20(j'esp=C3=A8r?=
 =?UTF-8?q?e=20bonne)=20preuve.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 RapportStage.tex | 184 ++++++++++++++++++++++++++++++++---------------
 header.tex       |   2 +-
 2 files changed, 128 insertions(+), 58 deletions(-)

diff --git a/RapportStage.tex b/RapportStage.tex
index 6c977f1..b8024f7 100644
--- a/RapportStage.tex
+++ b/RapportStage.tex
@@ -839,67 +839,137 @@
 			
 			C'est sous cette seconde forme que nous allons prouver le théorème (elle est plus \enquote{bas niveau}).
 			
-			Procédons par récurrence sur la longueur de la réduction $h\bracket{\varepsilon} \rightarrow^* \hbar\bracket{\overline{e'}}$
+			Nous allons Tout d'abord faire une récurrence sur la taille de la réduction $h\bracket{\varepsilon}\rightarrow^* \hbar\bracket{\overline{e'}}$, notée $n$.
+			
+			
+			\paragraph{Initialisation}
+				On essaie alors de montrer le résultat par induction sur $\hbar$.
+				
+				On suppose que $h\bracket{\varepsilon} = \hbar\bracket{\overline{e'}}$.
+				
+				\subparagraph{Cas $\hbar = \hole$}
+					Alors
+					\[h\bracket{\gamma} = \hbar\bracket{\overline{f'}}\quad\text{avec}\quad \overline{f'} = \left(h\bracket{\gamma}\right)\]
+					
+				\subparagraph{Cas $\hbar = \fj{new C($\overline{\hbar'}$)}$}
+					Alors, il y a deux possibilités.
+					
+					Ou bien, on a $h = \fj{x}$, et alors puisque $\varepsilon \prec \gamma$ et que $\varepsilon(\fj{x}) = \hbar\bracket{\overline{e'}}$, alors, on a que $\gamma(\fj{x})\rightarrow^*\hbar\bracket{\overline{f'}}$
+					Ou bien, on a $h = \fj{new C($\overline{h'}$)}$, et donc par induction
+					\[\overline{h'}\bracket{\gamma} \rightarrow^* \overline{\hbar'\bracket{\overline{f''}}}\]
+					
+					Et donc, en notant $\overline{f'}$ la concaténation des $\overline{\overline{f''}}$, on obtient que 
+					\[h\bracket{\gamma} \rightarrow^* \hbar\bracket{\overline{f'}}\]
+					
+			\paragraph{Hérédité}
+				
+				Notre hypothèse de récurrence, notée \textsc{(HR)} est la suivante:
+				\[\forall h \quad \varepsilon \prec \gamma \implies h\bracket{\varepsilon} \prec^{<n} h\bracket{\gamma}\]
+				
+				Nous allons continuer en faisant une induction sur $h$.
+				
+				\subparagraph{Cas $h = \fj{$h_0$.meth($\overline{h_1}$)}$}
+				
+					\underline{Cas 1} si la première réduction ne se fait pas sur la racine de $h$.
+					
+					Alors, dans l'un des $h_x\bracket{\varepsilon}$ on a que 
+					\[h_x\bracket{\varepsilon} \rightarrow e^0\]
+					
+					Il y a alors trois possibilités:
+					
+					\underline{La réduction se fait uniquement avec des nœuds de $h_x$}
+						Alors, on a $h_x \rightarrow h_x'$, et donc $h \rightarrow h'$ indépendamment du \eng{mapping} considéré et on peut appliquer \textsc{(HR)} qui nous donne que, puisque $h'\bracket{\varepsilon} \rightarrow^{n-1} \hbar\bracket{\overline{e'}}$, alors, on a 
+						\[h\bracket{\gamma} \rightarrow h'\bracket{\gamma} \rightarrow^* \hbar\bracket{\overline{f'}}\]
+						
+					\underline{La réduction se fait sur un nœud à l'interieur d'une variable $\fj{x}$ de $h_x$}
+						Alors, dans cette occurrence de la variable $\fj{x}$ dans $h_x$, nous avons une réduction de la forme suivante.
+						\[\varepsilon(\fj{x}) \rightarrow e^{\fj{x}}\]
+						Choisissons alors un nom de variable non utilisé dans $\epsilon$ et $\gamma$, ici noté $\fj{y}$, et créons $\varepsilon'$ ainsi:
+						
+						\[\varepsilon' = \left[ \begin{array}{ccc}
+							\fj{x} &\mapsto& \varepsilon(\fj{x})\\
+							\fj{y} &\mapsto& e^{\fj{x}}\\
+							v &\mapsto& \varepsilon(v)
+						\end{array} \right]
+						\quad
+						\gamma' = \left[ \begin{array}{ccc}
+							\fj{x} &\mapsto& \gamma(\fj{x})\\
+							\fj{y} &\mapsto& \gamma(\fj{x})\\
+							v &\mapsto& \gamma(v)
+						\end{array} \right]\]
+					
+						Ainsi, la réduction considérée s'exprime comme
+						\[h\bracket{\varepsilon} \rightarrow h'\bracket{\varepsilon'} \rightarrow^{n-1} \hbar\bracket{\overline{e'}}\]
+						
+						Or, nous avons aussi que $\varepsilon' \prec \gamma'$. Nous n'avons en effet que $\varepsilon(\fj{y})\prec\gamma(\fj{y})$ à vérifier, c'est à dire que $\varepsilon(\fj{x})\rightarrow e^{\fj{x}} \prec \gamma(\fj{x})$
+						
+						Cela est vrai par propriété de confluence sur l'opération de réduction. 
+						
+						\begin{tikzpicture}
+							\node (e1) at (1,1) {$\varepsilon(\fj{x})$};
+							
+							\node (e2) at (0,0) {$e^{\fj{x}}$};
+							
+							\node (e3) at (0,-1) {$\hbar\bracket{\overline{e'}}$};
+							
+							\node (e4) at (1,-2) {$\hbar\bracket{\overline{e''}}$};
+							
+							\draw[->] (e1) -- (e2);
+							\draw[->] (e2) to node[very near end, above right] {$*$} (e3);
+							
+							\draw[->,dashed] (e1) to node[very near end, above right] {$*$} (e4);
+							\draw[->,dashed] (e3) to node[very near end, above right] {$*$} (e4);
+						\end{tikzpicture}
+					
+						On peut alors appliquer que $\varepsilon \prec \gamma$.
+						
+						Nous avons toutes les conditions réunies qui nous permettent d'appliquer l'hypothèse de récurrence.
+						
+					\underline{La réduction s'est faîte entre un nœud de $h$ et un nœud de $\varepsilon$}
+						Il y a deux cas de figure pour lesquels les deux cas précédents ne sont pas adéquats. Le premier est un appel à \eng{field} de la forme $\fj{x.field}$ et le second est un appel à méthode de la forme $\fj{x.meth($\overline{h'}$)}$.
+						\marginpar{Faut-il ajouter le cas du Cast ?}
+						
+						Dans ces deux cas, nous avons nécessairement $\varepsilon(\fj{x}) = \fj{new C($\overline{e^\varepsilon}$)}$, et donc aussi $\gamma(\fj{x}) = \fj{new C($\overline{e^\gamma}$)}$ avec $\overline{e^\varepsilon} \prec \overline{e^\gamma}$, puisque $\varepsilon \prec \gamma$.
+						
+						Dans le cas de $\fj{x.field}$, on choisit un nouveau nom de variable inutilisé $\fj{y}$, et nous créons une nouvelle fois $\varepsilon'$ et $\gamma'$ ainsi.
 		
-			\paragraph{Si la réduction est de taille $0$}
-				Alors $h\bracket{\varepsilon} = \hbar\bracket{\overline{e'}}$.
-				
-				On peut alors prouver le lemme suivant par induction sur $h$:
-				\[\forall h,\hbar,\varepsilon,\gamma,\overline{e'}\qquad \left|\begin{array}{ll}\varepsilon \prec \gamma \\h\bracket{\varepsilon} = \hbar\bracket{\overline{e'}}\end{array}\right. \implies \exists \overline{f'}\quad h\bracket{\gamma} \rightarrow^* \hbar\bracket{\overline{f'}}\]
-				
-				\subparagraph{$h$ = \fj{x} (variable)}
-					Alors \[h\bracket{\varepsilon} = \varepsilon(\fj{x}) \prec \gamma(\fj{x}) = h\bracket{\gamma}\]
-				
-				\subparagraph{$h$ = \fj{new C($h'_1$,...,$h'_k$)}}
-					Dans le cas où $\hbar = \hole$, alors on a $\overline{e'} = (e_0)$.
-					Alors, en posant $\overline{f'} = (h\bracket{\gamma})$, on obtient que $\hbar\bracket{\overline{f'}} = h\bracket{\gamma}$, d'où le résultat.
+						\[\varepsilon' = \left[ \begin{array}{ccc}
+							\fj{x} &\mapsto& \varepsilon(\fj{x})\\
+							\fj{y} &\mapsto& e^\varepsilon_k\\
+							v &\mapsto& \varepsilon(v)
+						\end{array} \right]
+						\quad
+						\gamma' = \left[ \begin{array}{ccc}
+							\fj{x} &\mapsto& \gamma(\fj{x})\\
+							\fj{y} &\mapsto& e^\gamma_k\\
+							v &\mapsto& \gamma(v)
+						\end{array} \right]\]
 					
-					Sinon, c'est que $\hbar = \fj{new C($\hbar'_1$,...,$\hbar'_2$)}$.
-					
-					Or, par induction, nous avons que il existe $\overline{f_1}$, ..., $\overline{f_k}$ tels que pour tout $i$, on aie $h'_i\bracket{\gamma} \rightarrow^* \hbar'_i\bracket{\overline{f_i}}$
-					
-					Alors, avec 
-					\[\overline{f'} = \overline{f_1} \| \cdots \| \overline{f_k}\]
-					
-					On obtient bien, par congruence de la relation de réduction : \[h\bracket{\gamma} \rightarrow^* \hbar\bracket{\overline{f'}}\]
-					
-				\subparagraph{$h$ = Autre chose}
-						Alors, c'est nécessairement que $\hbar = \hole$, à cause de la première égalité.
-						
-						On peut alors faire la même preuve que dans le cas précédent.
+						Nous avons alors toujours $\varepsilon' \prec \gamma'$, mais aussi que la première réduction s'écrit 
+						\[h\bracket{\varepsilon} \rightarrow h'\bracket{\varepsilon'} \rightarrow^{n-1} \hbar\bracket{\overline{e'}}\]
+						où $h'$ est obtenu en remplaçant l'occurrence de $\fj{x.field}$ susnommée par $\fj{y}$.
 						
 						
-				\underline{Le lemme est donc démontré} et on peut utiliser ce dernier pour montrer le cas d'initialisation.
+						On peut donc appliquer l'hypothèse de récurrence. pour obtenir, puisque les \eng{class table} considérées sont les mêmes
+						\[h\bracket{\gamma} \rightarrow h'\bracket{\gamma'} \rightarrow^* \hbar\bracket{\overline{f'}}\]
+						
+						Dans le cas de $\fj{x.meth($\overline{h'}$)}$, la procédure est presque la même.
+						
+						Nous allons noter $\overline{v}$ les noms des paramètres de $\fj{C.meth}$. Nous noterons aussi $h_m$ le corps de cette méthode.
+						
+						Nous allons enfin obtenir $h_m'$ en remplacant dans $h_m$ la variable $\fj{this}$ par la variable $\fj{x}$ et les appels à chaque variable $v_k$ par l'expression à variables $h'_k$.
+						
+						Nous pouvons garder $\varepsilon$ et $\gamma$ tels qu'ils sont.
+						
+						Alors, en remplacant l'appel $\fj{x.meth($\overline{h'}$)}$ susnommé par $h_m'$ dans $h$, on obtient une nouvelle expression $h'$ telle que la réduction soit
+						\[h\bracket{\varepsilon} \rightarrow h'\bracket{\varepsilon} \rightarrow^{n-1} \hbar\bracket{\overline{e'}}\]
+						
+						Mais en ayant aussi que 
+						\[h\bracket{\gamma} \rightarrow h'\bracket{\gamma}\]
+						
+						On peut enfin appliquer l'hypothèse de récurrence de la même manière.
+						
+					\underline{Cas 2} où la première réduction se fait sur la racine de $h$.
 				
-			\paragraph{Récursivité}
-				Si le théorème est vrai pour toute réduction de taille strictement infèrieure à $n$.
 				
-				L'hypothèse est que \[h\bracket{\varepsilon} \rightarrow^n \hbar\bracket{\overline{e'}}\]
-				
-				Nous allons donc traiter les cas suivant le type de la première relation de cette chaine.
-				
-				\subparagraph{\textsc{R-Invk} sur un nœud de $h$}
-					Alors, on a que 
-					\[h\bracket{\varepsilon} = \mathfrak{h}_0\bracket{\fj{new C($\overline{h_1\bracket{\varepsilon}}$).meth($\overline{h_2\bracket{\varepsilon}}$)}} \rightarrow \mathfrak{h}_0\bracket{h_b\bracket{\varepsilon'}} = h'\bracket{\varepsilon'} \rightarrow^{<n} \hbar\bracket{\overline{e'}}\]
-					
-					\[\text{Avec}\quad \left\lbrace\begin{array}{ccl}
-						\mathfrak{h}_0& \text{est} & \text{Une expression avec un seul trou}\\
-						h_b & = & \operatorname{mbody}(\fj{C},\fj{meth})\\
-						\overline{\fj{x}} & \text{sont} & \text{Les variables de \fj{C.meth}}\\
-						h' & = & \mathfrak{h}_0\bracket{h_b}\\
-						\varepsilon' & = & \left[\begin{array}{ccc}
-							\fj{this} & \mapsto & \fj{new C($\overline{h_1\bracket{\varepsilon}}$)}\\
-							\overline{\fj{x}} & \mapsto & \overline{h_2\bracket{\varepsilon}}
-						\end{array}\right]
-					\end{array}\right.\]
-				
-					On note aussi \[\gamma' = \left[\begin{array}{ccc}
-						\fj{this} & \mapsto & \fj{new C($\overline{h_1\bracket{\gamma}}$)}\\
-						\overline{\fj{x}} & \mapsto & \overline{h_2\bracket{\gamma}}
-					\end{array}\right]\]
-				
-				Ainsi, nous avons
-				\[h\bracket{\gamma} = \mathfrak{h}_0\bracket{\fj{new C($\overline{h_1\bracket{\gamma}}$).meth($\overline{h_2\bracket{\gamma}}$)}} \rightarrow \mathfrak{h}_0\bracket{h_b\bracket{\gamma'}} = h'\bracket{\gamma'}\]
-				
-				Or, $\varepsilon' \prec \gamma'$, puisque $\varepsilon \prec \gamma$, 
 \end{document}
diff --git a/header.tex b/header.tex
index f53d548..48e27a8 100644
--- a/header.tex
+++ b/header.tex
@@ -34,7 +34,7 @@
 
 \usepackage{csquotes}
 \usepackage[lighttt]{lmodern}
-\usetikzlibrary{shapes.geometric}
+\usetikzlibrary{shapes.geometric,positioning}
 
 % Macros caractères globales
 \newcommand{\pgrph}{\P}