% !TeX root = slides.tex
\section{Example 2: \texorpdfstring{\Leftrightarrow}{<=>} congruence (binary log. rel.)}

\begin{frame}{Towards Binary Logical Relations}
	\structure{Key Ideas of Unary Relations:}\rightThing{\alert{already seen}}\begin{enumerate}
		\item state \alert{type-indexed family of predicates} $\tndClaim{-}{-}$
		\item for every type $\tau$, \alert{prove predicate is preserved} under constructors $c\colon \tau_1 \to \ldots \to \tau_n \to \tau$:\[
		\text{if}\ \tndClaim{\tau_1}{t_1} \wedge \ldots \wedge \tndClaim{\tau_n}{t_n},\ \text{then}\ \tndClaim{\tau}{c\ t_1 \ldots\ t_n}
		\]
	\end{enumerate}
	
	\structure{How about $C_P(p, p') :=\; \lra{p}{p'}$?}
	\onslide<2->{\begin{enumerate}
			\item forms a type-indexed family of \alert{binary} predicates\\\rightOptional{together with $C_A(a,b) :=\; \lra{\metaInj(a)}{\metaInj(b)}$}
			%
			\item e.g. is preserved under $\wedge$:\begin{itemize}
				\item given $\lra{p}{p'}$ and $\lra{q}{q'}$
				\item we can derive $\lra{(p \wedge q)}{(p' \wedge q')}$
			\end{itemize}
	\end{enumerate}}
\end{frame}

\begin{frame}{Example 2: \texorpdfstring{$\Leftrightarrow$}{<=>} congruence in Prop. Logic}
	\begin{example}[PL Extended]
		We extend PL's grammar by
		\plExtGrammar
		and its proof calculus accordingly.
	\end{example}
	\begin{theorem}[Leftrightarrow (LRA) Congruence]
		$\Leftrightarrow$ is a congruence on $P$. That is, if $\;\lra{p}{p'}$ and $\lra{q}{q'}$, then\begin{columns}
			\begin{column}{0.5\textwidth}
				\begin{itemize}
					\item $\lra{\lnot p}{\lnot p'}$
					\item $\lra{p \wedge q}{p' \wedge q'}$
				\end{itemize}
			\end{column}%
			\hfill%
			\begin{column}{0.5\textwidth}
				\begin{itemize}
					\item $\lra{p \vee q}{p' \vee q'}$
					\item $\lra{(p \Leftrightarrow q)}{(p' \Leftrightarrow q')}$,
				\end{itemize}
			\end{column}
		\end{columns}
		\medskip
		
		and, trivially, if $\;\lra{\metaInj(a)}{\metaInj(a')}$, then $\lra{\metaInj(a)}{\metaInj(a')}$.
	\end{theorem}
\end{frame}

% typeset the assignment for either \wedge or \vee in the logical relation
% usage: expects a surrounding align, align*, or aligned environment; pass either \wedge or \vee as argument
\newcommand{\logicalRelationWedgeVee}[1]{%
	\mathnormal{#1} &:= \colM{\lam{p}{\prop}} \colMM{\lam{p'}{\prop}} \lam{p^\ast}{\lra{\colM{p}}{\colMM{p'}}}\hspace{2.3em}\text{\optional{{\footnotesize \cn{//} first arg of }}} \scriptstyle{\mathnormal{#1}}\\%
	&\quad\quad\quad\colM{\lam{q}{\prop}} \colMM{\lam{q'}{\prop}}\lam{q^\ast}{\lra{\colM{q}}{\colMM{q'}}}\quad\text{\optional{{\footnotesize \cn{//} second arg of }}} \scriptstyle{\mathnormal{#1}}\\%
	&\quad\quad\quad\quad\expTypeComment{\lra{\colM{p} #1 \colMM{q}}{\colM{p'} #1 \colMM{q'}}}%
}%
\begin{frame}{LRA as a Logical Relation}
	\only<-7>{%
		\onslide<2->{\structure{Recall:} \only<1>{the desired binary relation on atoms}}%
		\only<2>{$\atom\colon\type$}%
		\only<3>{$\prop\colon\type$}%
		\only<4>{$\inj\colon\atom\to\prop$}%
		\only<5>{$\mathnormal{\lnot}\colon\prop\to\prop$}%
		\only<6-7>{$\mathnormal{\wedge},\mathnormal{\vee}\colon\prop\to\prop\to\prop$}%
		\onslide<2->{, map to }%
		\only<2>{the desired binary relation on atoms}%
		\only<3>{the desired binary relation on propositions}%
		\only<4-5>{appropriate proof}%
		\only<6>{appropriate proofs}%
	}%
	\begin{align*}
		&\logRel{\LRA}{\colM{\id{\PL}} \times \colMM{\id{\PL}}}{\PL}{\PL} = \{\\
		&\quad\quad\begin{aligned}
			\onslide<2->{
				\atom &:= \colM{\lam{a}{\atom}} \colMM{\lam{a'}{\atom}} \lra{\inj(a)}{\inj(a')}\\
			}
			\onslide<3->{
				\prop &:= \colM{\lam{p}{\prop}} \colMM{\lam{p'}{\prop}} \lra{p}{p'}\only<2>{\\}\only<3->{\\[0.6em]}
			}
			%
			\onslide<4->{
				\inj  &:= \colM{\lam{a}{\atom}} \colMM{\lam{a'}{\atom}} \lam{a^\ast}{\lra{\colM{\inj(a)}}{\colMM{\inj(a')}}}\  a^\ast\\
			}
			%
			\onslide<5->{
				\mathnormal{\lnot} &:= \colM{\lam{p}{\prop}} \colMM{\lam{p'}{\prop}} \lam{p^\ast}{\lra{\colM{p}}{\colMM{p'}}}\\
				&\quad\quad\quad\expTypeComment{\lra{\colM{\lnot p}}{\colMM{\lnot p'}}}\\
			}
			%
			\onslide<6->{
				\logicalRelationWedgeVee{\wedge}\\
			}
			\onslide<7->{
				\logicalRelationWedgeVee{\vee}
			}
		\end{aligned}\onslide<8>{\\&\}}
	\end{align*}
\end{frame}

\begin{frame}{Logical Relations: A Second Definition}
	\vspace{-0.5em}
	\begin{definition}
		Let $T$ be a theory and $(r_c)_{c \in T}$ a family of $T$-expressions. Define
		\vspace{-0.75em}
		\begin{align*}
			&r(\type) &&= \lam{A}{\type} \colMM{\lam{A'}{\type}} A \to \colMM{A'} \to \type\\
			&r(\tpi{a}{A} B) &&= \lam{f}{(\tpi{a}{A} B)} \colMM{\lam{f'}{(\tpi{a'}{A'} B')}}\\
			&&&\quad\quad\quad \tpi{x}{A} \colMM{\tpi{x'}{A'}} \tpi{x^\ast}{r(A)\ x\ \colMM{x'}}\\
			&&&\quad\quad\quad\quad r(B)\ (f\ x)\ \colMM{(f'\ x')}\\
			&r(A\ B) &&= r(A)\ B\ B'\ r(B)\\
			&r(\lam{x}{A} B) &&= \lam{x}{A} \colMM{\lam{x'}{A'}} \lam{x^\ast}{r(A)\ x\ \colMM{x'}} r(B)\\
			&r(c) &&= r_c\\
			&r(x) &&= x^\ast\\[-2em]
		\end{align*}
		where $A'$ denotes systematic priming.
		We call $r$ a \defemph{binary logical relation on $\id{T} \times \colMM{\id{T}}$} if $\vdash_T r_c\colon r(\tpName)\ c\ \colMM{c}$ for all constants $c\colon\tpName$ in $T$.
	\end{definition}
	\only<-2>{\begin{itemize}
			\only<1>{\item $\prop\colon\type$, hence $r_{\prop}\colon \prop \to \colMM{\prop} \to \type$\\\rightThing{$\optional{r_{\prop} := \ulam{p}}\colMM{\ulam{p'}} \optional{\lra{p}{p'}}$}}%
			%
			\only<2>{\item $\mathnormal{\lnot}\colon\prop\to\prop$, hence
				$r_{\mathnormal{\lnot}}
				\colon
				\tpi{p\,\colMM{p'}}{\prop}
				\tpi{p^\ast}{\lra{p}{p'}} \lra{\lnot p}{\lnot p'}$}
	\end{itemize}}%
	\only<3->{
		\begin{block}{}
			\textbf{Theorem (Basic Lemma).} If $\;\vdash_T t \colon \tpName$, then $\vdash_T r(t) \colon r(\tpName)\ t\ t'$.
		\end{block}
	}
\end{frame}

\begin{frame}{Example 2: Summary}
	\structure{Summary:} we have \alert{$n$-ary logical relations} of the form\[
		\logRel{r}{\id{T}\times\cdots\times\id{T}}{T}{T} = \{\ldots\}
	\]
	\begin{itemize}
		\item they associate to every type $\tpName$ an \alert{$n$-ary relation} $C_{\tpName}(-,\ldots,-)$
		\item their well-typedness expresses that these relations are congruences
		\item ``the basic lemma'' states: if $t\colon \tpName$, then $C_{\tpName}(t, \ldots, t)$\\\rightOptional{reflexivity? TODO}
	\end{itemize}
	\medskip

	\structure{Next:} Logical Relations along a \alert{non-trivial} morphism
\end{frame}