From: acondolu <andrea.condoluci@unibo.it>
Date: Sat, 28 Jul 2018 11:33:15 +0000 (+0200)
Subject: Proved another lemma (aux1 + aux2)
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a7a2c1856a363d14919592eec69c3d0e50dc883f;p=fireball-separation.git

Proved another lemma (aux1 + aux2)
---

diff --git a/macros.tex b/macros.tex
index 5e151cc..4c30e15 100644
--- a/macros.tex
+++ b/macros.tex
@@ -87,4 +87,6 @@
 
 \renewcommand{\Lam}[2]{\lambda#1.\, \{\!\!\{#2\}\!\!\}}
 \renewcommand{\vec}{\overrightarrow}
-\newcommand{\reflemma}[1]{Lemma~\ref{l:#1}}
\ No newline at end of file
+\newcommand{\reflemma}[1]{Lemma~\ref{l:#1}}
+\newcommand{\head}{h}
+\newcommand{\args}{a}
diff --git a/notes.tex b/notes.tex
index 81c9280..3dd97d1 100644
--- a/notes.tex
+++ b/notes.tex
@@ -291,23 +291,23 @@
   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.
-     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}
@@ -345,7 +345,7 @@
 % \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$:
@@ -362,14 +362,28 @@
   and we conclude.
 \end{proof}
 
-\begin{lemma}
+\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}
-  \TODO{}
+  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{theorem}
@@ -410,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