Working on the conservation of eta inequality, seems feasible

just A LOT of subcases

diff --git a/macros.tex b/macros.tex
index 2ea3ddea1db6c7398c55c3d351ea1f2b0876d7ee..5e151cc18eef3e7b032943819266ef7f6a32127f 100644 (file)
--- a/macros.tex
+++ b/macros.tex
@@ -83,6 +83,8 @@
 \newcommand{\varfour}{w}\r
 \r
 \newcommand{\Red}[2]{\xrightarrow{#2}_{#1}}\r
-\newcommand{\TODO}{\textcolor{red}{TODO}}\r
+\newcommand{\TODO}{{\color{red}\textbf{TODO}}}\r
 \r
-\renewcommand{\Lam}[2]{\lambda#1.\, \{\!\!\{#2\}\!\!\}}
\ No newline at end of file
+\renewcommand{\Lam}[2]{\lambda#1.\, \{\!\!\{#2\}\!\!\}}\r
+\renewcommand{\vec}{\overrightarrow}\r
+\newcommand{\reflemma}[1]{Lemma~\ref{l:#1}}
\ No newline at end of file

diff --git a/notes.tex b/notes.tex
index c7c14bd1723e2dfd1ac624ad626216eaf958ec81..264e827a00f9dda3ab29415e7654e6a6a5778b5d 100644 (file)
--- a/notes.tex
+++ b/notes.tex
@@ -241,8 +241,8 @@
 % \end{example}\r
 \clearpage\r
 \section[Tentativi X-separability]{Tentativi $\mathbf X$--separability (July, 15$^{\mathbf{th}}\div\infty$)}\r
-\newcommand{\perm}{\pi}\r
-\newcommand{\Perm}[2]{\pi[#1,#2]}\r
+\newcommand{\perm}{p}\r
+\newcommand{\Perm}[2]{\operatorname{P}[#1,#2]}\r
 \newcommand{\xK}{\kappa}\r
 \newcommand{\xN}{n}\r
 \newcommand{\LAM}[2]{\Lambda_{#2,#1}}\r
@@ -299,7 +299,7 @@
   for every $\xK' \geq \xK{}$.\r
 \end{lemma}\r
 \r
-\begin{lemma}\r
+\begin{lemma}\label{l:k-prime-nf}\r
   Let $\tm$ a \knnf, $\var$ a variable, $i$ a natural number, and $\xK'\defeq \xK + i + 1$.\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
@@ -309,19 +309,18 @@
   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\tmtwo\sigma$ is a $\xK'$-nf.\r
+    By \ih{} each term in $\vec{(\nf{\tmtwo\sigma})}$ is a $\xK'$-nf.\r
     We conclude since by hypothesis $|\vec\vartwo|\leq\xK{}<\xK'$.\r
-\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)} \nf{\vec{(\tmtwo\sigma)}}$,\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 $|\vec\tmtwo|\leq i$:\r
-    $\tm\sigma \to^* \lambda\vec\vartwo\vec\varthree.\, \varthree\vec\alpha \vec{(\tmtwo\sigma)}\vec\varthree $ for some $\varthree\in\vec\varthree$\r
-    and $|\vec\varthree| = i + 1 - |\vec\tmtwo|$.\r
-    Conclude by \ih{} and because $|\vec\vartwo\vec\varthree| \leq \xK{} + i + 1 - |\vec\tmtwo| \leq \xK{} + i + 1 = \xK'$.\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
+    Conclude by \ih{} and because $|\vec\vartwo\vec\varthree\varthree'| \leq \xK{} + i - |\vec\tmtwo| + 1 \leq \xK{} + i + 1 = \xK'$.\r
   \end{itemize}\r
   \r
 \end{proof}\r
@@ -345,16 +344,90 @@
 %   \end{itemize}\r
 % \end{proof}\r
 \r
+\r
+\begin{lemma}\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
+\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
+  \r
+  By structural induction on $\tm$.\r
+  Let $\tm = \lambda\vec\vartwo.\, h\,\vec a$ for $|\vec\vartwo|\leq\xK$.\r
+  \TODO{}\r
+\end{proof}\r
+\r
+% TODO: $\xK$-standard proof of $\eta$.\r
+\r
 \begin{lemma}\r
-  For every \knnf{s} $\tm,\tmtwo$,\r
+  For every \knnf s $\tm$ and $\tmtwo$,\r
   every fresh variable $\var$,\r
-  $\perm\defeq\Perm{i}{i+k+1}$ permutator,\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
 \begin{proof}\r
-  The implication from left to right is trivial.\r
-  We now prove that if $\nf{\tm\Subst\var\perm}\EtaEq\nf{\tmtwo\Subst\var\perm}$\r
-  then also $\tm\EtaEq\tmtwo$.\r
+  Let $\sigma \defeq \Subst\var\perm$.\r
+  First of all, note that by \reflemma{k-prime-nf}\r
+  $\nf{\tm\sigma}$ and $\nf{\tmtwo\sigma}$ are defined and\r
+  are $\xK'$-nfs for $\xK'\defeq\xK + i + 1$.\r
+  \r
+  If $\tm\EtaEq\tmtwo$ then necessarily $\nf{\tm\sigma}\EtaEq\nf{\tmtwo\sigma}$.\r
+  Let us now assume that $\tm\EtaNeq\tmtwo$, and prove that\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
+  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
+    \item $h_1 \neq h_2$: we distinguish three subcases.\r
+    \begin{itemize}\r
+      \item $h_1,h_2\neq \var$:\r
+       it follows that $\nf{\tm\sigma} = \nf{(\lambda\vec\vartwo.\,h_1\,\vec a)\sigma} = \lambda\vec\vartwo.\,h_1\,\vec{(\nf{a\sigma})}$\r
+       and $\nf{\tmtwo\sigma} = \nf{(\lambda\vec\vartwo.\,h_2\,\vec b)\sigma} = \lambda\vec\vartwo.\,h_2\,\vec{(\nf{b\sigma})}$,\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
+      \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
+     if $h_1,h_2\neq\var$, then again $\nf{\tm\sigma} = \lambda\vec\vartwo.\,h_1\,\vec{(\nf{a\sigma})}$\r
+     and $\nf{\tmtwo\sigma} = \lambda\vec\vartwo.\,h_2\,\vec{(\nf{b\sigma})}$,\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
+     \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
+       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
+       If equal conclude, otherwise conclude by lemma above.\r
+     \end{itemize}\r
+    \item \r
+    $h_1 = h_2$ and $|\vec a| = |\vec b|$\r
+    but $a_n \EtaNeq b_n$ for some $n$.\r
+    If $h_1=h_2\neq\var$, then again\r
+    $\lambda\vec\vartwo.\,h_1\,\vec{(\nf{a\sigma})} =%\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
+    \r
+    We now consider the other subcase $h_1=h_2=\var$, and the following subsubcases:\r
+    \begin{itemize}\r
+      \item $|\vec a| = |\vec b| \leq i$: \TODO easy \r
+      \item $|\vec a| = |\vec b| > i$ and $a_i\EtaEq b_i$: \TODO ok\r
+      \item $|\vec a| = |\vec b| > i$ and $a_i\EtaNeq b_i$: \TODO\r
+       by \ih{} already $\nf{a_i\sigma\vec\alpha}\EtaNeq\nf{b_i\sigma\vec\alpha}$\r
+       and conclude by appending the $\vec a$ and $\vec b$.\r
+    \end{itemize}\r
+  \end{itemize}\r
 \end{proof}\r
 \r
 \end{document}\r