From: acondolu Date: Tue, 17 Jul 2018 10:55:52 +0000 (+0100) Subject: Almost complete proof of Lemma 2 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=afac35ce3b2f0240a762f51c3379ff4048233a0d;p=fireball-separation.git Almost complete proof of Lemma 2 *** Passo su carta a cercare prova di Lemma 3 *** --- diff --git a/macros.tex b/macros.tex index b9ac79d..2ea3dde 100644 --- a/macros.tex +++ b/macros.tex @@ -1,3 +1,8 @@ +\usepackage{blindtext} +\usepackage{enumerate} +\usepackage{hyperref, bookmark} +\usepackage{amsmath, amsfonts, amssymb, amsthm} +\usepackage{xcolor} \usepackage{bussproofs} \theoremstyle{plain} @@ -78,3 +83,6 @@ \newcommand{\varfour}{w} \newcommand{\Red}[2]{\xrightarrow{#2}_{#1}} +\newcommand{\TODO}{\textcolor{red}{TODO}} + +\renewcommand{\Lam}[2]{\lambda#1.\, \{\!\!\{#2\}\!\!\}} \ No newline at end of file diff --git a/notes.tex b/notes.tex index 142ea4d..c7c14bd 100644 --- a/notes.tex +++ b/notes.tex @@ -1,16 +1,8 @@ \documentclass[12pt]{article} -\usepackage{blindtext} -\usepackage{enumerate} -\usepackage{hyperref, bookmark} -\usepackage{amsmath, amsfonts, amssymb, amsthm} -\usepackage{xcolor} - \title{Strong Separation} % \author{---} \date{\vspace{-2em}\today{}} - \input{macros} -\renewcommand{\Lam}[2]{\lambda#1.\, \{\!\!\{#2\}\!\!\}} \begin{document} @@ -248,32 +240,39 @@ % % \end{example} \clearpage -\section{Tentativi $\mathbf X$--separability (July, 15$^{\mathbf{th}}\div\infty$)} +\section[Tentativi X-separability]{Tentativi $\mathbf X$--separability (July, 15$^{\mathbf{th}}\div\infty$)} \newcommand{\perm}{\pi} \newcommand{\Perm}[2]{\pi[#1,#2]} \newcommand{\xK}{\kappa} \newcommand{\xN}{n} \newcommand{\LAM}[2]{\Lambda_{#2,#1}} \newcommand{\LAMNK}{\LAM\xN\xK} -\newcommand{\Apply}[2]{(#1\mapsto#2)} -\newcommand{\kn}{$(\kappa,n)$} -\newcommand{\knnf}{\kn{}-nf} +% \newcommand{\kn}{$(\kappa,n)$} +\newcommand{\knnf}{$\xK{}$-nf} \newcommand{\Lams}[1]{\operatorname{lams}(#1)} \newcommand{\Args}[1]{\operatorname{args}(#1)} \newcommand{\Head}[1]{\operatorname{head}(#1)} +\newcommand{\nf}[1]{#1{\downarrow}} +\newcommand{\Nat}{\mathbb{N}} \begin{definition}[$\Lams\cdot,\Args\cdot,\Head\cdot$] \[\Lams{\lambda\vec\var.\,\vartwo\,\vec\tm} \defeq |\vec\var| \] \[\Args{\lambda\vec\var.\,\vartwo\,\vec\tm} \defeq |\vec\tm| \] \[\Head{\lambda\vec\var.\,\vartwo\,\vec\tm} \defeq \vartwo \] \end{definition} -\begin{definition}[\kn{}-normal forms] +\begin{definition}[$\xK$-normal forms] First recall that terms in normal form have the shape $\lambda\vec\var.\,\vartwo\,\vec\tm$, where the terms $\vec\tm$ are in normal form too. - We define inductively the set of \knnf s (for $\xK,\xN$ natural numbers): + We define inductively the set of \knnf s (where $\xK$ is a natural number): $\lambda\vec\var.\,\vartwo\,\vec\tm$ is a \knnf{} iff - $|\vec\var|\leq\xK$, $|\vec\tm|\leq\xN$, and every term in $\vec\tm$ is a \knnf{}. + $|\vec\var|\leq\xK$% + %, $|\vec\tm|\leq\xN$ + , and every term in $\vec\tm$ is a \knnf{} as well. +\end{definition} + +\begin{definition}[Normal form $\nf\cdot$] + \end{definition} \begin{definition}[Permutator $\Perm\cdot\cdot$]~ @@ -282,39 +281,80 @@ with $|\vec\var| = i$ and $|\vec\alpha| = j$. \end{definition} -\begin{definition}{$\Apply\cdot\cdot$} - We denote by $\tmtwo\Apply\var\tm$ the normal form of $\tmtwo\Subst\var\tm$ in normal form -- - if it has one. -\end{definition} +{\color{yellow}\begin{definition}[Good permutation] + Let $\tm$ a \knnf. + $\Perm i j$ is \emph{good} for $\tm$ if + $i<\Args\tm$ and $j \geq \xK + i + 1$. +\end{definition}} + +% \begin{lemma} +% Let $\tm$ in nf. +% Let $\vec\alpha$ fresh variables. +% If $|\vec\alpha|\geq \lams\tm$, +% then the normal form of $\tm\,\vec\alpha$ is inert. +% \end{lemma} + +\begin{lemma}[Monotonicity]\label{l:k-nf-mono} + If $\tm$ is a \knnf{}, then it is also a $\xK'$-nf + for every $\xK' \geq \xK{}$. +\end{lemma} \begin{lemma} - Let $\tm$ a \knnf, and $\Head\tm=\var$. - If $A\leq \Args\tm$ and $B \geq \xK + A + 1$, - let $\tmtwo\defeq\tm\Apply\var{\Perm{A}{B}}$ in: - $\Lams\tm=\Lams\tmtwo$ and $\tmtwo\in\LAM ? ?$ + 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} \begin{proof} - By induction on the normal form structure of $\tm$. - Let $\tm=\lambda\vec\var.\,\vartwo\,\vec\tmtwo$: + 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 cases: \begin{itemize} - \item if $\vartwo=\var$, then - $\tm\Apply\var\perm = \lambda\var_1\ldots\var_{???}.\,\var\,\vec\tmthree$ - \item if $\vartwo\neq\var$, then $\tm\Apply\var\perm = \lambda\vec\var.\,\vartwo\,\vec\tmthree$ - where $\vec\tmthree\defeq \vec\tmtwo\Apply\var\perm$. - Conclude by inductive hypothesis. + \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. + 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)}}$, + 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'$. \end{itemize} + \end{proof} -\begin{corollary} - Let $\tm \defeq \var\,f_1\cdots f_m$ a \knnf. - If $A\leq m$ and $B \geq A + \xK$, - then $\tm\Apply\var{\Perm{A}{B}}$ is an inert. -\end{corollary} + +% \begin{lemma} +% Let $\tm$ a \knnf, and $\Head\tm=\var$. +% If $i<\Args\tm$ and $j \geq \xK + i + 1$, +% then $\tmtwo\defeq\nf{\tm\Subst\var{\Perm i j}}$ is defined; +% $\Lams\tm=\Lams{\tmtwo}$; $\tmtwo$ is a $(j,\xN + j)$-nf. +% \end{lemma} +% \begin{proof}\color{red}\TODO{} +% By induction on the normal form structure of $\tm$: +% let $\tm=\lambda\vec\var.\,\vartwo\,\vec\tmtwo$. +% By \ih{}, $\nf{\tmtwo\Subst\var\perm}$ are $(j,\xN+j)$-nfs. +% \begin{itemize} +% \item if $\vartwo=\var$, then +% $\nf{\tm\Subst\var\perm} = \lambda\var_1\ldots\var_{???}.\,\var\,\vec\tmthree$ +% \item if $\vartwo\neq\var$, then $\nf{\tm\Subst\var\perm} = \lambda\vec\var.\,\vartwo\,\vec\tmthree$ +% where $\vec\tmthree\defeq \nf{\vec\tmtwo\Subst\var\perm}$. +% Conclude by inductive hypothesis. +% \end{itemize} +% \end{proof} \begin{lemma} - For every $\tm,\tmtwo$ be \knnf{s}, + For every \knnf{s} $\tm,\tmtwo$, every fresh variable $\var$, $\perm\defeq\Perm{i}{i+k+1}$ permutator, - $\tm\EtaEq\tmtwo$ iff $\tm\Apply\var\perm\EtaEq\tmtwo\Apply\var\perm$. + $\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$. +\end{proof} \end{document}