From: acondolu <andrea.condoluci@unibo.it>
Date: Sat, 28 Jul 2018 08:25:01 +0000 (+0200)
Subject: One more lemma
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ce17a6ffcfd4bcacb390948283478e59c1af1dd8;p=fireball-separation.git

One more lemma
---

diff --git a/notes.tex b/notes.tex
index c4e4cfd..81c9280 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{}$.
@@ -314,7 +301,7 @@
     \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?}).
+     $\nf{(\tmtwo_i\sigma\vec\alpha)}$ is inert.
      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|$:
@@ -325,6 +312,19 @@
   
 \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$,
@@ -349,26 +349,35 @@
   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}
+  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}
+  \TODO{}
+\end{proof}
+
+\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 +389,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 +401,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|$: