X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=notes.tex;h=3dd97d13033ed783b6287ff312fb9ba330de46e4;hb=a7a2c1856a363d14919592eec69c3d0e50dc883f;hp=c4e4cfdfa015e5296236c1ca136055b46a685691;hpb=0fd76d8a70c67669bae7798495d33dad55bc3c6f;p=fireball-separation.git

diff --git a/notes.tex b/notes.tex
index c4e4cfd..3dd97d1 100644
--- a/notes.tex
+++ b/notes.tex
@@ -281,19 +281,6 @@
   with $|\vec\var| = i$ and $|\vec\alpha| = j$.
 \end{definition}
 
-{\color{yellow}\begin{definition}[Good permutation]
-  Let $\tm$ a \knnf.
-  $\Perm i j$ is \emph{good} for $\tm$ if
-  $i<\Args\tm$ and $j \geq \xK + i + 1$.
-\end{definition}}
-
-% \begin{lemma}
-%   Let $\tm$ in nf.
-%   Let $\vec\alpha$ fresh variables.
-%   If $|\vec\alpha|\geq \lams\tm$,
-%   then the normal form of $\tm\,\vec\alpha$ is inert.
-% \end{lemma}
-
 \begin{lemma}[Monotonicity]\label{l:k-nf-mono}
   If $\tm$ is a \knnf{}, then it is also a $\xK'$-nf
   for every $\xK' \geq \xK{}$.
@@ -304,27 +291,40 @@
   Then for every $j \geq \xK'$, $\nf{\tm\Subst\var{\Perm i j}}$ is defined and it is a $\xK'$-nf.
 \end{lemma}
 \begin{proof}
-  By (course-of-value) structural induction on $\tm$.
-  Let $\tm=\lambda\vec\vartwo.\,\varthree\,\vec\tmtwo$ and $\sigma\defeq\Subst\var{\Perm i j}$.
+  By induction on $|\tm|$.
+  Let $\tm=\lambda\vec\vartwo.\,\head\,\vec\args$ and $\sigma\defeq\Subst\var{\Perm i j}$.
   By cases:
   \begin{itemize}
-    \item Case $\varthree\neq\var$: $\nf{(\lambda\vec\vartwo.\,\varthree\,\vec\tmtwo)\sigma} = \lambda\vec\vartwo.\,\varthree\,\vec{(\nf{\tmtwo\sigma})}$.
-    By \ih{} each term in $\vec{(\nf{\tmtwo\sigma})}$ is a $\xK'$-nf.
+    \item Case $\head\neq\var$: $\nf{\tm\sigma} = \lambda\vec\vartwo.\,\head\,\vec{(\nf{\args\sigma})}$.
+    By \ih{} each term in $\vec{(\nf{\args\sigma})}$ is a $\xK'$-nf.
     We conclude since by hypothesis $|\vec\vartwo|\leq\xK{}<\xK'$.
-    \item Case $\varthree=\var$ and $i<|\vec\tmtwo|$:
-     $\tm\sigma \to^* \lambda\vec\vartwo.\, (\tmtwo_i\sigma)\vec\alpha \vec{(\tmtwo\sigma)} $.
-     Now, by \ih{} $\nf{\tmtwo_i\sigma}$ is a $\xK'$-nf, and since $|\vec\alpha|\geq\xK'$,
-     $\nf{(\tmtwo_i\sigma\vec\alpha)}$ is inert (\textcolor{red}{Serve lemma?}).
-     Therefore $\nf\tm = \lambda\vec\vartwo.\,\nf{(\tmtwo_i\sigma\vec\alpha)} \vec{(\nf{\tmtwo\sigma})}$,
-     and again by \ih{} it is also a $\xK'$-nf.
-    \item Case $\varthree=\var$ and $i \geq |\vec\tmtwo|$:
-    $\tm\sigma \to^* \lambda\vec\vartwo\vec\varthree\varthree'.\, \varthree'\vec\alpha \vec{(\tmtwo\sigma)}\vec\varthree $ for 
-    $|\vec\varthree| = i - |\vec\tmtwo|$.
+    \item Case $\head=\var$ and $|\vec\args| \leq i$:
+    $\tm\sigma \to^* \lambda\vec\vartwo\vec\varthree\varthree'.\, \varthree'\vec\alpha \vec{(\args\sigma)}\vec\varthree $ for 
+    $|\vec\varthree| = i - |\vec\args|$.
     Conclude by \ih{} and because $|\vec\vartwo\vec\varthree\varthree'| \leq \xK{} + i - |\vec\tmtwo| + 1 \leq \xK{} + i + 1 = \xK'$.
+    \item Case $\head=\var$ and $i<|\vec\args|$:
+     $\tm\sigma \to^* \lambda\vec\vartwo.\, (\args_i\sigma)\vec\alpha \vec{(\args\sigma)} $.
+     Now, by \ih{} $\nf{\args_i\sigma}$ is a $\xK'$-nf, and since $|\vec\alpha|\geq\xK'$,
+     $\nf{(\args_i\sigma\vec\alpha)}$ is inert.
+     Therefore $\nf\tm = \lambda\vec\vartwo.\,\nf{(\args_i\sigma\vec\alpha)} \vec{(\nf{\args\sigma})}$,
+     and again by \ih{} it is also a $\xK'$-nf.
   \end{itemize}
   
 \end{proof}
 
+\begin{lemma}[Admissible]
+  Let $\tm$ an inert \knnf.
+  If $i<\Args\tm$ and $j \geq \xK + i + 1$
+  then $\nf{\tm\Subst{\HeadOf\tm}{\Perm i j}}$
+  is inert.
+\end{lemma}
+\begin{proof}
+  Let $\tm = \var\,\vec a$, $\perm \defeq \Perm i j$, and $\sigma\defeq\Subst\var\perm$.
+  Then $\nf{\tm\Subst\var\perm} = \nf{(a_i\sigma\,\vec\alpha\,\vec {(a\sigma)})}$.
+  By \reflemma{k-prime-nf} $\nf{a_i\sigma}$ is a $\xK'$-nf with $\xK'\defeq \xK+i+1$.
+  Therefore $\nf{(a_i\sigma\vec\alpha)}$ is inert because $|\vec\alpha|=j\geq\xK'$.
+\end{proof}
+
 % \begin{lemma}
 %   Let $\tm$ a \knnf, and $\Head\tm=\var$.
 %   If $i<\Args\tm$ and $j \geq \xK + i + 1$,
@@ -345,30 +345,53 @@
 % \end{proof}
 
 
-\begin{lemma}
+\begin{lemma}\label{l:aux1}
   For every \knnf s $\tm$,
   every fresh variable $\var$,
   every $\perm\defeq\Perm{i}{j}$ permutator with $j>\xK+i+1$:
-  $\nf{\tm\Subst\var\perm\vec\alpha} \EtaNeq \alpha_j$.
+  $\nf{(\tm\Subst\var\perm\vec\alpha)} = \tmtwo \, \alpha_j$
+  for some inert $\tmtwo$.
 \end{lemma}
 \begin{proof}
   First of all note that by \reflemma{k-prime-nf}
   $\nf{\tm\Subst\var\perm}$ is a $\xK'$-nf for $\xK' \defeq \xK+i+1$, therefore
-  $\nf{\tm\Subst\var\perm\vec\alpha}$ is inert because $|\vec\alpha|>\xK'$ by hypothesis.
+  $\nf{(\tm\Subst\var\perm\vec\alpha)}$ is inert because $|\vec\alpha|>\xK'$ by hypothesis.
   
-  By structural induction on $\tm$.
-  Let $\tm = \lambda\vec\vartwo.\, h\,\vec a$ for $|\vec\vartwo|\leq\xK$.
-  \TODO{}
+  More precisely, $\nf{(\tm\Subst\var\perm\,\alpha_1\cdots\alpha_{\xK'})}$ is inert,
+  and therefore $\nf{(\tm\Subst\var\perm\vec\alpha)} = \nf{(\tm\Subst\var\perm\,\alpha_1\cdots\alpha_{\xK'})}\,\alpha_{\xK'+1}\cdots\alpha_j$,
+  and we conclude.
 \end{proof}
 
-% TODO: $\xK$-standard proof of $\eta$.
+\begin{lemma}\label{l:aux2}
+  For every \knnf s $\tm$,
+  every fresh variable $\var$,
+  every $\perm\defeq\Perm{i}{j}$ permutator with $j>\xK+i+1$:
+  $\nf{(\tm\Subst\var\perm)} \EtaNeq \alpha_j$.
+\end{lemma}
+\begin{proof}
+  By induction on $|\tm|$.
+  Let $\tm = \lambda\vec\vartwo.\,h\,\vec a$ and $\sigma\defeq\Subst\var\perm$:
+  \begin{itemize}
+    \item If $h \neq \var$, then $\nf{\tm\sigma} = \lambda\vec\vartwo.\,h\,\vec {(\nf {a\sigma})}$,
+    and we conclude since $h\neq \alpha_j$ by the hypothesis that $\alpha_j$ is
+    a fresh variable.
+    \item If $h=\var$ and $|\vec a| \leq i$, then
+    $\tm\sigma \to^* \lambda\vec\vartwo\vec\varthree\varthree'.\, \varthree'\vec\alpha \vec{(\args\sigma)}\vec\varthree $,
+    and we conclude since the head $\varthree'$ is a bound variable,
+    while $\alpha_j$ is free.
+    \item If $h=\var$ and $|\vec a| > i$, then
+    $\tm\sigma \to^* \lambda\vec\vartwo.\, (\args_i\sigma)\vec\alpha \vec{(\args\sigma)} $.
+    $\nf{(\args_i\sigma\,\vec\alpha)} = \tmtwo\,\alpha_j$ by \reflemma{aux1}
+    for some inert $\tmtwo$. Clearly $\tmtwo\,\alpha_j \EtaNeq \alpha_j$.
+  \end{itemize}
+\end{proof}
 
-\begin{lemma}
+\begin{theorem}
   For every \knnf s $\tm$ and $\tmtwo$,
   every fresh variable $\var$,
   $\perm\defeq\Perm{i}{j}$ permutator with $j>\xK+i+1$,
   $\tm\EtaEq\tmtwo$ iff $\nf{\tm\Subst\var\perm}\EtaEq\nf{\tmtwo\Subst\var\perm}$.
-\end{lemma}
+\end{theorem}
 \begin{proof}
   Let $\sigma \defeq \Subst\var\perm$.
   First of all, note that by \reflemma{k-prime-nf}
@@ -380,7 +403,7 @@
   $\nf{\tm\sigma}\EtaNeq\nf{\tmtwo\sigma}$.
   Let $\tm \EtaEq \lambda\vec\vartwo.\, h_1\,\vec a$ and 
   $\tmtwo \EtaEq \lambda\vec\vartwo.\, h_2\,\vec b$,
-  with $|\vec\vartwo| = \xK$ {\color{red}[Capire perche' si puo' $\xK$-$\eta$-espandere qui]}.
+  with $|\vec a|,|\vec b| > i$ {\color{red}[Capire perche' si puo' $\eta$-espandere qui]}.
   By (course-of-value) induction on the size of $\tm$ and $\tmtwo$,
   and by cases on the definition of eta-difference:
   \begin{itemize}
@@ -392,6 +415,7 @@
        and therefore $\nf{\tm\sigma} \EtaNeq \nf{\tmtwo\sigma}$ because
        their head variables are different.
       \item $h_1=\var$ and $h_2\neq \var$: \TODO
+       $\nf{\tmtwo\sigma} = \nf{(\lambda\vec\vartwo.\,h_2\,\vec b)\sigma} = \lambda\vec\vartwo.\,h_2\,\vec{(\nf{b\sigma})}$
       \item $h_1\neq\var$ and $h_2=\var$: symmetric to the case above.
     \end{itemize}
     \item $h_1 = h_2$ and $|\vec a| \neq |\vec b|$:
@@ -400,6 +424,7 @@
      and we conclude because the two terms have a different number of arguments.
      
      We now consider the other subcase $h_1=h_2=\var$, and the following subsubcases:
+     {\color{red}[Usare \reflemma{aux2} nei punti seguenti]}
      \begin{itemize}
        \item $|\vec a|,|\vec b|\leq i$: \TODO
        \item $|\vec a|>i$ and $|\vec b|\leq i$: use boh \TODO