with $|\vec\var| = i$ and $|\vec\alpha| = j$.\r
\end{definition}\r
\r
-{\color{yellow}\begin{definition}[Good permutation]\r
- Let $\tm$ a \knnf.\r
- $\Perm i j$ is \emph{good} for $\tm$ if\r
- $i<\Args\tm$ and $j \geq \xK + i + 1$.\r
-\end{definition}}\r
-\r
-% \begin{lemma}\r
-% Let $\tm$ in nf.\r
-% Let $\vec\alpha$ fresh variables.\r
-% If $|\vec\alpha|\geq \lams\tm$,\r
-% then the normal form of $\tm\,\vec\alpha$ is inert.\r
-% \end{lemma}\r
-\r
\begin{lemma}[Monotonicity]\label{l:k-nf-mono}\r
If $\tm$ is a \knnf{}, then it is also a $\xK'$-nf\r
for every $\xK' \geq \xK{}$.\r
Then for every $j \geq \xK'$, $\nf{\tm\Subst\var{\Perm i j}}$ is defined and it is a $\xK'$-nf.\r
\end{lemma}\r
\begin{proof}\r
- By (course-of-value) structural induction on $\tm$.\r
- Let $\tm=\lambda\vec\vartwo.\,\varthree\,\vec\tmtwo$ and $\sigma\defeq\Subst\var{\Perm i j}$.\r
+ By induction on $|\tm|$.\r
+ Let $\tm=\lambda\vec\vartwo.\,\head\,\vec\args$ and $\sigma\defeq\Subst\var{\Perm i j}$.\r
By cases:\r
\begin{itemize}\r
- \item Case $\varthree\neq\var$: $\nf{(\lambda\vec\vartwo.\,\varthree\,\vec\tmtwo)\sigma} = \lambda\vec\vartwo.\,\varthree\,\vec{(\nf{\tmtwo\sigma})}$.\r
- By \ih{} each term in $\vec{(\nf{\tmtwo\sigma})}$ is a $\xK'$-nf.\r
+ \item Case $\head\neq\var$: $\nf{\tm\sigma} = \lambda\vec\vartwo.\,\head\,\vec{(\nf{\args\sigma})}$.\r
+ By \ih{} each term in $\vec{(\nf{\args\sigma})}$ is a $\xK'$-nf.\r
We conclude since by hypothesis $|\vec\vartwo|\leq\xK{}<\xK'$.\r
- \item Case $\varthree=\var$ and $i<|\vec\tmtwo|$:\r
- $\tm\sigma \to^* \lambda\vec\vartwo.\, (\tmtwo_i\sigma)\vec\alpha \vec{(\tmtwo\sigma)} $.\r
- Now, by \ih{} $\nf{\tmtwo_i\sigma}$ is a $\xK'$-nf, and since $|\vec\alpha|\geq\xK'$,\r
- $\nf{(\tmtwo_i\sigma\vec\alpha)}$ is inert (\textcolor{red}{Serve lemma?}).\r
- Therefore $\nf\tm = \lambda\vec\vartwo.\,\nf{(\tmtwo_i\sigma\vec\alpha)} \vec{(\nf{\tmtwo\sigma})}$,\r
- and again by \ih{} it is also a $\xK'$-nf.\r
- \item Case $\varthree=\var$ and $i \geq |\vec\tmtwo|$:\r
- $\tm\sigma \to^* \lambda\vec\vartwo\vec\varthree\varthree'.\, \varthree'\vec\alpha \vec{(\tmtwo\sigma)}\vec\varthree $ for \r
- $|\vec\varthree| = i - |\vec\tmtwo|$.\r
+ \item Case $\head=\var$ and $|\vec\args| \leq i$:\r
+ $\tm\sigma \to^* \lambda\vec\vartwo\vec\varthree\varthree'.\, \varthree'\vec\alpha \vec{(\args\sigma)}\vec\varthree $ for \r
+ $|\vec\varthree| = i - |\vec\args|$.\r
Conclude by \ih{} and because $|\vec\vartwo\vec\varthree\varthree'| \leq \xK{} + i - |\vec\tmtwo| + 1 \leq \xK{} + i + 1 = \xK'$.\r
+ \item Case $\head=\var$ and $i<|\vec\args|$:\r
+ $\tm\sigma \to^* \lambda\vec\vartwo.\, (\args_i\sigma)\vec\alpha \vec{(\args\sigma)} $.\r
+ Now, by \ih{} $\nf{\args_i\sigma}$ is a $\xK'$-nf, and since $|\vec\alpha|\geq\xK'$,\r
+ $\nf{(\args_i\sigma\vec\alpha)}$ is inert.\r
+ Therefore $\nf\tm = \lambda\vec\vartwo.\,\nf{(\args_i\sigma\vec\alpha)} \vec{(\nf{\args\sigma})}$,\r
+ and again by \ih{} it is also a $\xK'$-nf.\r
\end{itemize}\r
\r
\end{proof}\r
\r
+\begin{lemma}[Admissible]\r
+ Let $\tm$ an inert \knnf.\r
+ If $i<\Args\tm$ and $j \geq \xK + i + 1$\r
+ then $\nf{\tm\Subst{\HeadOf\tm}{\Perm i j}}$\r
+ is inert.\r
+\end{lemma}\r
+\begin{proof}\r
+ Let $\tm = \var\,\vec a$, $\perm \defeq \Perm i j$, and $\sigma\defeq\Subst\var\perm$.\r
+ Then $\nf{\tm\Subst\var\perm} = \nf{(a_i\sigma\,\vec\alpha\,\vec {(a\sigma)})}$.\r
+ By \reflemma{k-prime-nf} $\nf{a_i\sigma}$ is a $\xK'$-nf with $\xK'\defeq \xK+i+1$.\r
+ Therefore $\nf{(a_i\sigma\vec\alpha)}$ is inert because $|\vec\alpha|=j\geq\xK'$.\r
+\end{proof}\r
+\r
% \begin{lemma}\r
% Let $\tm$ a \knnf, and $\Head\tm=\var$.\r
% If $i<\Args\tm$ and $j \geq \xK + i + 1$,\r
% \end{proof}\r
\r
\r
-\begin{lemma}\r
+\begin{lemma}\label{l:aux1}\r
For every \knnf s $\tm$,\r
every fresh variable $\var$,\r
every $\perm\defeq\Perm{i}{j}$ permutator with $j>\xK+i+1$:\r
- $\nf{\tm\Subst\var\perm\vec\alpha} \EtaNeq \alpha_j$.\r
+ $\nf{(\tm\Subst\var\perm\vec\alpha)} = \tmtwo \, \alpha_j$\r
+ for some inert $\tmtwo$.\r
\end{lemma}\r
\begin{proof}\r
First of all note that by \reflemma{k-prime-nf}\r
$\nf{\tm\Subst\var\perm}$ is a $\xK'$-nf for $\xK' \defeq \xK+i+1$, therefore\r
- $\nf{\tm\Subst\var\perm\vec\alpha}$ is inert because $|\vec\alpha|>\xK'$ by hypothesis.\r
+ $\nf{(\tm\Subst\var\perm\vec\alpha)}$ is inert because $|\vec\alpha|>\xK'$ by hypothesis.\r
\r
- By structural induction on $\tm$.\r
- Let $\tm = \lambda\vec\vartwo.\, h\,\vec a$ for $|\vec\vartwo|\leq\xK$.\r
- \TODO{}\r
+ More precisely, $\nf{(\tm\Subst\var\perm\,\alpha_1\cdots\alpha_{\xK'})}$ is inert,\r
+ 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$,\r
+ and we conclude.\r
\end{proof}\r
\r
-% TODO: $\xK$-standard proof of $\eta$.\r
+\begin{lemma}\label{l:aux2}\r
+ For every \knnf s $\tm$,\r
+ every fresh variable $\var$,\r
+ every $\perm\defeq\Perm{i}{j}$ permutator with $j>\xK+i+1$:\r
+ $\nf{(\tm\Subst\var\perm)} \EtaNeq \alpha_j$.\r
+\end{lemma}\r
+\begin{proof}\r
+ By induction on $|\tm|$.\r
+ Let $\tm = \lambda\vec\vartwo.\,h\,\vec a$ and $\sigma\defeq\Subst\var\perm$:\r
+ \begin{itemize}\r
+ \item If $h \neq \var$, then $\nf{\tm\sigma} = \lambda\vec\vartwo.\,h\,\vec {(\nf {a\sigma})}$,\r
+ and we conclude since $h\neq \alpha_j$ by the hypothesis that $\alpha_j$ is\r
+ a fresh variable.\r
+ \item If $h=\var$ and $|\vec a| \leq i$, then\r
+ $\tm\sigma \to^* \lambda\vec\vartwo\vec\varthree\varthree'.\, \varthree'\vec\alpha \vec{(\args\sigma)}\vec\varthree $,\r
+ and we conclude since the head $\varthree'$ is a bound variable,\r
+ while $\alpha_j$ is free.\r
+ \item If $h=\var$ and $|\vec a| > i$, then\r
+ $\tm\sigma \to^* \lambda\vec\vartwo.\, (\args_i\sigma)\vec\alpha \vec{(\args\sigma)} $.\r
+ $\nf{(\args_i\sigma\,\vec\alpha)} = \tmtwo\,\alpha_j$ by \reflemma{aux1}\r
+ for some inert $\tmtwo$. Clearly $\tmtwo\,\alpha_j \EtaNeq \alpha_j$.\r
+ \end{itemize}\r
+\end{proof}\r
\r
-\begin{lemma}\r
+\begin{theorem}\r
For every \knnf s $\tm$ and $\tmtwo$,\r
every fresh variable $\var$,\r
$\perm\defeq\Perm{i}{j}$ permutator with $j>\xK+i+1$,\r
$\tm\EtaEq\tmtwo$ iff $\nf{\tm\Subst\var\perm}\EtaEq\nf{\tmtwo\Subst\var\perm}$.\r
-\end{lemma}\r
+\end{theorem}\r
\begin{proof}\r
Let $\sigma \defeq \Subst\var\perm$.\r
First of all, note that by \reflemma{k-prime-nf}\r
$\nf{\tm\sigma}\EtaNeq\nf{\tmtwo\sigma}$.\r
Let $\tm \EtaEq \lambda\vec\vartwo.\, h_1\,\vec a$ and \r
$\tmtwo \EtaEq \lambda\vec\vartwo.\, h_2\,\vec b$,\r
- with $|\vec\vartwo| = \xK$.\r
+ with $|\vec a|,|\vec b| > i$ {\color{red}[Capire perche' si puo' $\eta$-espandere qui]}.\r
By (course-of-value) induction on the size of $\tm$ and $\tmtwo$,\r
and by cases on the definition of eta-difference:\r
\begin{itemize}\r
and therefore $\nf{\tm\sigma} \EtaNeq \nf{\tmtwo\sigma}$ because\r
their head variables are different.\r
\item $h_1=\var$ and $h_2\neq \var$: \TODO\r
+ $\nf{\tmtwo\sigma} = \nf{(\lambda\vec\vartwo.\,h_2\,\vec b)\sigma} = \lambda\vec\vartwo.\,h_2\,\vec{(\nf{b\sigma})}$\r
\item $h_1\neq\var$ and $h_2=\var$: symmetric to the case above.\r
\end{itemize}\r
\item $h_1 = h_2$ and $|\vec a| \neq |\vec b|$:\r
and we conclude because the two terms have a different number of arguments.\r
\r
We now consider the other subcase $h_1=h_2=\var$, and the following subsubcases:\r
+ {\color{red}[Usare \reflemma{aux2} nei punti seguenti]}\r
\begin{itemize}\r
- \item Both $|\vec a|,|\vec b|\leq i$: \TODO\r
- \item w.l.o.g. $|\vec a|>i$ and $|\vec b|\leq i$: use boh \TODO\r
- \item Both $|\vec a|,|\vec b|> i$: \TODO use the lemma above\r
+ \item $|\vec a|,|\vec b|\leq i$: \TODO\r
+ \item $|\vec a|>i$ and $|\vec b|\leq i$: use boh \TODO\r
+ \item $|\vec a|\leq i$ and $|\vec b|> i$: symmetric to the case above.\r
+ \item $|\vec a|,|\vec b|> i$: \TODO use the lemma above\r
plus another one. Reason on the numebr of arguments\r
$\Args{\nf{a_i\sigma\vec\alpha}}$ vs \r
$\Args{\nf{b_i\sigma\vec\alpha}}$.\r
\lambda\vec\vartwo.\,h_2\,\vec{(\nf{b\sigma})}$,\r
and we conclude by \ih{} since $a_n \EtaNeq b_n$ implies that \r
$\nf{a_n\sigma} \EtaNeq \nf{b_n\sigma}$.\r
- {\color{red}[Can we use the \ih{} here?]}\r
+ {\color{red}[Capire se possiamo davvero usare l'\ih{} qui]}\r
\r
We now consider the other subcase $h_1=h_2=\var$, and the following subsubcases:\r
\begin{itemize}\r
projects / fireball-separation.git / blobdiff