From: acondolu Date: Fri, 27 Jul 2018 17:23:18 +0000 (+0200) Subject: Working on the conservation of eta inequality, seems feasible X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7b8e2259f217ba34f4d8871eca4fc7b79791d13a;hp=afac35ce3b2f0240a762f51c3379ff4048233a0d;p=fireball-separation.git Working on the conservation of eta inequality, seems feasible just A LOT of subcases --- diff --git a/macros.tex b/macros.tex index 2ea3dde..5e151cc 100644 --- a/macros.tex +++ b/macros.tex @@ -83,6 +83,8 @@ \newcommand{\varfour}{w} \newcommand{\Red}[2]{\xrightarrow{#2}_{#1}} -\newcommand{\TODO}{\textcolor{red}{TODO}} +\newcommand{\TODO}{{\color{red}\textbf{TODO}}} -\renewcommand{\Lam}[2]{\lambda#1.\, \{\!\!\{#2\}\!\!\}} \ No newline at end of file +\renewcommand{\Lam}[2]{\lambda#1.\, \{\!\!\{#2\}\!\!\}} +\renewcommand{\vec}{\overrightarrow} +\newcommand{\reflemma}[1]{Lemma~\ref{l:#1}} \ No newline at end of file diff --git a/notes.tex b/notes.tex index c7c14bd..264e827 100644 --- a/notes.tex +++ b/notes.tex @@ -241,8 +241,8 @@ % \end{example} \clearpage \section[Tentativi X-separability]{Tentativi $\mathbf X$--separability (July, 15$^{\mathbf{th}}\div\infty$)} -\newcommand{\perm}{\pi} -\newcommand{\Perm}[2]{\pi[#1,#2]} +\newcommand{\perm}{p} +\newcommand{\Perm}[2]{\operatorname{P}[#1,#2]} \newcommand{\xK}{\kappa} \newcommand{\xN}{n} \newcommand{\LAM}[2]{\Lambda_{#2,#1}} @@ -299,7 +299,7 @@ for every $\xK' \geq \xK{}$. \end{lemma} -\begin{lemma} +\begin{lemma}\label{l:k-prime-nf} Let $\tm$ a \knnf, $\var$ a variable, $i$ a natural number, and $\xK'\defeq \xK + i + 1$. Then for every $j \geq \xK'$, $\nf{\tm\Subst\var{\Perm i j}}$ is defined and it is a $\xK'$-nf. \end{lemma} @@ -309,19 +309,18 @@ 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\tmtwo\sigma$ is a $\xK'$-nf. + By \ih{} each term in $\vec{(\nf{\tmtwo\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 (\textcolor{red}{Serve lemma?}). - Therefore $\nf\tm = \lambda\vec\vartwo.\,\nf{(\tmtwo_i\sigma\vec\alpha)} \nf{\vec{(\tmtwo\sigma)}}$, + 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 $|\vec\tmtwo|\leq i$: - $\tm\sigma \to^* \lambda\vec\vartwo\vec\varthree.\, \varthree\vec\alpha \vec{(\tmtwo\sigma)}\vec\varthree $ for some $\varthree\in\vec\varthree$ - and $|\vec\varthree| = i + 1 - |\vec\tmtwo|$. - Conclude by \ih{} and because $|\vec\vartwo\vec\varthree| \leq \xK{} + i + 1 - |\vec\tmtwo| \leq \xK{} + i + 1 = \xK'$. + \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|$. + Conclude by \ih{} and because $|\vec\vartwo\vec\varthree\varthree'| \leq \xK{} + i - |\vec\tmtwo| + 1 \leq \xK{} + i + 1 = \xK'$. \end{itemize} \end{proof} @@ -345,16 +344,90 @@ % \end{itemize} % \end{proof} + +\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\vec\alpha} \EtaNeq \alpha_j$. +\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. + + By structural induction on $\tm$. + Let $\tm = \lambda\vec\vartwo.\, h\,\vec a$ for $|\vec\vartwo|\leq\xK$. + \TODO{} +\end{proof} + +% TODO: $\xK$-standard proof of $\eta$. + \begin{lemma} - For every \knnf{s} $\tm,\tmtwo$, + For every \knnf s $\tm$ and $\tmtwo$, every fresh variable $\var$, - $\perm\defeq\Perm{i}{i+k+1}$ permutator, + $\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} \begin{proof} - The implication from left to right is trivial. - We now prove that if $\nf{\tm\Subst\var\perm}\EtaEq\nf{\tmtwo\Subst\var\perm}$ - then also $\tm\EtaEq\tmtwo$. + Let $\sigma \defeq \Subst\var\perm$. + First of all, note that by \reflemma{k-prime-nf} + $\nf{\tm\sigma}$ and $\nf{\tmtwo\sigma}$ are defined and + are $\xK'$-nfs for $\xK'\defeq\xK + i + 1$. + + If $\tm\EtaEq\tmtwo$ then necessarily $\nf{\tm\sigma}\EtaEq\nf{\tmtwo\sigma}$. + Let us now assume that $\tm\EtaNeq\tmtwo$, and prove that + $\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$. + By (course-of-value) induction on the size of $\tm$ and $\tmtwo$, + and by cases on the definition of eta-difference: + \begin{itemize} + \item $h_1 \neq h_2$: we distinguish three subcases. + \begin{itemize} + \item $h_1,h_2\neq \var$: + it follows that $\nf{\tm\sigma} = \nf{(\lambda\vec\vartwo.\,h_1\,\vec a)\sigma} = \lambda\vec\vartwo.\,h_1\,\vec{(\nf{a\sigma})}$ + and $\nf{\tmtwo\sigma} = \nf{(\lambda\vec\vartwo.\,h_2\,\vec b)\sigma} = \lambda\vec\vartwo.\,h_2\,\vec{(\nf{b\sigma})}$, + 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 + \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|$: + if $h_1,h_2\neq\var$, then again $\nf{\tm\sigma} = \lambda\vec\vartwo.\,h_1\,\vec{(\nf{a\sigma})}$ + and $\nf{\tmtwo\sigma} = \lambda\vec\vartwo.\,h_2\,\vec{(\nf{b\sigma})}$, + 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: + \begin{itemize} + \item Both $|\vec a|,|\vec b|\leq i$: \TODO + \item w.l.o.g. $|\vec a|>i$ and $|\vec b|\leq i$: use boh \TODO + \item Both $|\vec a|,|\vec b|> i$: \TODO use the lemma above + plus another one. Reason on the numebr of arguments + $\Args{\nf{a_i\sigma\vec\alpha}}$ vs + $\Args{\nf{b_i\sigma\vec\alpha}}$. + If equal conclude, otherwise conclude by lemma above. + \end{itemize} + \item + $h_1 = h_2$ and $|\vec a| = |\vec b|$ + but $a_n \EtaNeq b_n$ for some $n$. + If $h_1=h_2\neq\var$, then again + $\lambda\vec\vartwo.\,h_1\,\vec{(\nf{a\sigma})} =% + \lambda\vec\vartwo.\,h_2\,\vec{(\nf{b\sigma})}$, + and we conclude by \ih{} since $a_n \EtaNeq b_n$ implies that + $\nf{a_n\sigma} \EtaNeq \nf{b_n\sigma}$. + {\color{red}[Can we use the \ih{} here?]} + + We now consider the other subcase $h_1=h_2=\var$, and the following subsubcases: + \begin{itemize} + \item $|\vec a| = |\vec b| \leq i$: \TODO easy + \item $|\vec a| = |\vec b| > i$ and $a_i\EtaEq b_i$: \TODO ok + \item $|\vec a| = |\vec b| > i$ and $a_i\EtaNeq b_i$: \TODO + by \ih{} already $\nf{a_i\sigma\vec\alpha}\EtaNeq\nf{b_i\sigma\vec\alpha}$ + and conclude by appending the $\vec a$ and $\vec b$. + \end{itemize} + \end{itemize} \end{proof} \end{document}