Nouvelle version qui ne marche pas.

RapportStage.tex

@@ -839,51 +839,67 @@
 			
 			C'est sous cette seconde forme que nous allons prouver le théorème (elle est plus \enquote{bas niveau}).
 			
-			Procédons par induction sur $h$.
-			
-			\subparagraph{$h$ = $\fj{x}$ (variable)}
-				Alors
-				\[h\bracket{\varepsilon} = \varepsilon(x
-				\fj{x}) \prec \gamma(\fj{x}) = h\bracket{\gamma}\]
-				
-			\subparagraph{$h$ = $\fj{$h_0$.meth($\overline{h'}$)}$}
-				
-				Par hypothèse d'induction, on a
-				\[h_0\bracket{\varepsilon} \prec h_0\bracket{\gamma} \quad\text{et}\quad \overline{h'}\bracket{\varepsilon}\prec\overline{h'}\bracket{\gamma}\]
-				
-				Soit $\hbar$ tel que $h\bracket{\varepsilon}\rightarrow^* \hbar\bracket{e'}$
-				
-				Le cas $\hbar = \hole$ se traite de la même manière dans tous les cas de l'induction, puisque alors, en considérant $\overline{f'} = \left(h\bracket{\gamma}\right)$, alors $h\bracket{\gamma} = \hbar\bracket{\overline{f'}}$, donc $h\bracket{\gamma}\rightarrow^* \hbar\bracket{f'}$
-				
-				Sinon, on a que $\hbar=\fj{new C($\overline{\hbar'}$)}$
-				
-				Donc, puisque la racine de l'expression $h\bracket{\varepsilon}$ passe d'un appel à méthode à un \fj{new}, c'est nécessairement qu'il y a eu une réduction \textsc{R-Invk} sur la racine, donc que 
-				\[h_0\bracket{\varepsilon} \rightarrow^* \fj{new D($\overline{h_1\bracket{\varepsilon}}$)}\]
-					
-				Et donc, par hypothèse d'induction,
-				\[h_0\bracket{\gamma} \rightarrow^* \fj{new D($\overline{h_1\bracket{\gamma}}$)}\]
-				
-				Alors, en notant $h_{\fj{meth}} = \operatorname{mbody}(\fj{D},\fj{meth})$ (c'est une expression avec des variables libres, que l'on note d'ailleurs $\overline{\fj{x}}$).
-				
-				\begin{align}
-					h\bracket{\epsilon} & \rightarrow^* & \fj{new D($\overline{h_1}\bracket{\varepsilon}$).meth(\overline{h'}\bracket{\varepsilon})} \\
-					& \rightarrow & h_{\fj{body}}\bracket{\varepsilon'}
-				\end{align}
-				et \[\varepsilon' = \left[\begin{array}{ccl}
-				\fj{this} & \mapsto & \fj{new D($\overline{h_1\bracket{\varepsilon}}$)}\\
-				\overline{\fj{x}} & \mapsto & \overline{h'}\bracket{\varepsilon}
-				\end{array}\right]\]
-			
-				De même, on a 
-				\begin{align}
-					h\bracket{\gamma} & \rightarrow^* & \fj{new D($\overline{h_1}\bracket{\gamma}$).meth(\overline{h'}\bracket{\gamma})} \\
-					& \rightarrow & h_{\fj{body}}\bracket{\vargamma'}
-				\end{align}
-				et \[\vargamma' = \left[\begin{array}{ccl}
-					\fj{this} & \mapsto & \fj{new D($\overline{h_1\bracket{\vargamma}}$)}\\
-					\overline{\fj{x}} & \mapsto & \overline{h'}\bracket{\vargamma}
-				\end{array}\right]\]
+			Procédons par récurrence sur la longueur de la réduction $h\bracket{\varepsilon} \rightarrow^* \hbar\bracket{\overline{e'}}$
 		
-			
+			\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.
+					
+					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.
+						
+						
+				\underline{Le lemme est donc démontré} et on peut utiliser ce dernier pour montrer le cas d'initialisation.
+				
+			\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}