Almost complete proof of Lemma 2

*** Passo su carta a cercare prova di Lemma 3 ***

diff --git a/macros.tex b/macros.tex
index b9ac79db7aa8a76f8fc98d17e807f0a5a6c616af..2ea3ddea1db6c7398c55c3d351ea1f2b0876d7ee 100644 (file)
--- a/macros.tex
+++ b/macros.tex
@@ -1,3 +1,8 @@
+\usepackage{blindtext}\r
+\usepackage{enumerate}\r
+\usepackage{hyperref, bookmark}\r
+\usepackage{amsmath, amsfonts, amssymb, amsthm}\r
+\usepackage{xcolor}\r
 \usepackage{bussproofs}\r
 \r
 \theoremstyle{plain}\r
@@ -78,3 +83,6 @@
 \newcommand{\varfour}{w}\r
 \r
 \newcommand{\Red}[2]{\xrightarrow{#2}_{#1}}\r
+\newcommand{\TODO}{\textcolor{red}{TODO}}\r
+\r
+\renewcommand{\Lam}[2]{\lambda#1.\, \{\!\!\{#2\}\!\!\}}
\ No newline at end of file

diff --git a/notes.tex b/notes.tex
index 142ea4dfab5ea2181b134f19829434398608d0ac..c7c14bd1723e2dfd1ac624ad626216eaf958ec81 100644 (file)
--- a/notes.tex
+++ b/notes.tex
@@ -1,16 +1,8 @@
 \documentclass[12pt]{article}\r
-\usepackage{blindtext}\r
-\usepackage{enumerate}\r
-\usepackage{hyperref, bookmark}\r
-\usepackage{amsmath, amsfonts, amssymb, amsthm}\r
-\usepackage{xcolor}\r
-\r
 \title{Strong Separation}\r
 % \author{---}\r
 \date{\vspace{-2em}\today{}}\r
-\r
 \input{macros}\r
-\renewcommand{\Lam}[2]{\lambda#1.\, \{\!\!\{#2\}\!\!\}}\r
 \r
 \begin{document}\r
 \r
@@ -248,32 +240,39 @@
 %\r
 % \end{example}\r
 \clearpage\r
-\section{Tentativi $\mathbf X$--separability (July, 15$^{\mathbf{th}}\div\infty$)}\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{\xK}{\kappa}\r
 \newcommand{\xN}{n}\r
 \newcommand{\LAM}[2]{\Lambda_{#2,#1}}\r
 \newcommand{\LAMNK}{\LAM\xN\xK}\r
-\newcommand{\Apply}[2]{(#1\mapsto#2)}\r
-\newcommand{\kn}{$(\kappa,n)$}\r
-\newcommand{\knnf}{\kn{}-nf}\r
+% \newcommand{\kn}{$(\kappa,n)$}\r
+\newcommand{\knnf}{$\xK{}$-nf}\r
 \newcommand{\Lams}[1]{\operatorname{lams}(#1)}\r
 \newcommand{\Args}[1]{\operatorname{args}(#1)}\r
 \newcommand{\Head}[1]{\operatorname{head}(#1)}\r
+\newcommand{\nf}[1]{#1{\downarrow}}\r
+\newcommand{\Nat}{\mathbb{N}}\r
 \begin{definition}[$\Lams\cdot,\Args\cdot,\Head\cdot$]\r
   \[\Lams{\lambda\vec\var.\,\vartwo\,\vec\tm} \defeq |\vec\var| \]\r
   \[\Args{\lambda\vec\var.\,\vartwo\,\vec\tm} \defeq |\vec\tm| \]\r
   \[\Head{\lambda\vec\var.\,\vartwo\,\vec\tm} \defeq \vartwo \]\r
 \end{definition}\r
 \r
-\begin{definition}[\kn{}-normal forms]\r
+\begin{definition}[$\xK$-normal forms]\r
   First recall that terms in normal form have the shape\r
   $\lambda\vec\var.\,\vartwo\,\vec\tm$, where the terms $\vec\tm$ are in normal form too.\r
   \r
-  We define inductively the set of \knnf s (for $\xK,\xN$ natural numbers):\r
+  We define inductively the set of \knnf s (where $\xK$ is a natural number):\r
   $\lambda\vec\var.\,\vartwo\,\vec\tm$ is a \knnf{} iff \r
-  $|\vec\var|\leq\xK$, $|\vec\tm|\leq\xN$, and every term in $\vec\tm$ is a \knnf{}.\r
+  $|\vec\var|\leq\xK$%\r
+  %, $|\vec\tm|\leq\xN$\r
+  , and every term in $\vec\tm$ is a \knnf{} as well.\r
+\end{definition}\r
+\r
+\begin{definition}[Normal form $\nf\cdot$]\r
+  \r
 \end{definition}\r
 \r
 \begin{definition}[Permutator $\Perm\cdot\cdot$]~\r
@@ -282,39 +281,80 @@
   with $|\vec\var| = i$ and $|\vec\alpha| = j$.\r
 \end{definition}\r
 \r
-\begin{definition}{$\Apply\cdot\cdot$}\r
-  We denote by $\tmtwo\Apply\var\tm$ the normal form of $\tmtwo\Subst\var\tm$ in normal form --\r
-  if it has one.\r
-\end{definition}\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
+\end{lemma}\r
 \r
 \begin{lemma}\r
-  Let $\tm$ a \knnf, and $\Head\tm=\var$.\r
-  If $A\leq \Args\tm$ and $B \geq \xK + A + 1$,\r
-  let $\tmtwo\defeq\tm\Apply\var{\Perm{A}{B}}$ in:\r
-  $\Lams\tm=\Lams\tmtwo$ and $\tmtwo\in\LAM ? ?$\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
 \begin{proof}\r
-  By induction on the normal form structure of $\tm$.\r
-  Let $\tm=\lambda\vec\var.\,\vartwo\,\vec\tmtwo$:\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 cases:\r
   \begin{itemize}\r
-    \item if $\vartwo=\var$, then\r
-    $\tm\Apply\var\perm = \lambda\var_1\ldots\var_{???}.\,\var\,\vec\tmthree$\r
-    \item if $\vartwo\neq\var$, then $\tm\Apply\var\perm = \lambda\vec\var.\,\vartwo\,\vec\tmthree$\r
-    where $\vec\tmthree\defeq \vec\tmtwo\Apply\var\perm$.\r
-    Conclude by inductive hypothesis.\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
+    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
+     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
   \end{itemize}\r
+  \r
 \end{proof}\r
-\begin{corollary}\r
-  Let $\tm \defeq \var\,f_1\cdots f_m$ a \knnf.\r
-  If $A\leq m$ and $B \geq A + \xK$,\r
-  then $\tm\Apply\var{\Perm{A}{B}}$ is an inert.\r
-\end{corollary}\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
+%   then $\tmtwo\defeq\nf{\tm\Subst\var{\Perm i j}}$ is defined;\r
+%   $\Lams\tm=\Lams{\tmtwo}$; $\tmtwo$ is a $(j,\xN + j)$-nf.\r
+% \end{lemma}\r
+% \begin{proof}\color{red}\TODO{}\r
+%   By induction on the normal form structure of $\tm$:\r
+%   let $\tm=\lambda\vec\var.\,\vartwo\,\vec\tmtwo$.\r
+%   By \ih{}, $\nf{\tmtwo\Subst\var\perm}$ are $(j,\xN+j)$-nfs.\r
+%   \begin{itemize}\r
+%     \item if $\vartwo=\var$, then\r
+%     $\nf{\tm\Subst\var\perm} = \lambda\var_1\ldots\var_{???}.\,\var\,\vec\tmthree$\r
+%     \item if $\vartwo\neq\var$, then $\nf{\tm\Subst\var\perm} = \lambda\vec\var.\,\vartwo\,\vec\tmthree$\r
+%     where $\vec\tmthree\defeq \nf{\vec\tmtwo\Subst\var\perm}$.\r
+%     Conclude by inductive hypothesis.\r
+%   \end{itemize}\r
+% \end{proof}\r
 \r
 \begin{lemma}\r
-  For every $\tm,\tmtwo$ be \knnf{s},\r
+  For every \knnf{s} $\tm,\tmtwo$,\r
   every fresh variable $\var$,\r
   $\perm\defeq\Perm{i}{i+k+1}$ permutator,\r
-  $\tm\EtaEq\tmtwo$ iff $\tm\Apply\var\perm\EtaEq\tmtwo\Apply\var\perm$.\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
+\end{proof}\r
 \r
 \end{document}\r