universal property for products

main.tex

 \documentclass{article}
 
-\usepackage{amsmath,amssymb}
+\usepackage{amsmath,amssymb,amsthm}
 \usepackage{tikz-cd}
 \usepackage{mathpartir}
 
 \newtheorem{theorem}{Theorem}
+\newtheorem{corollary}[theorem]{Corollary}
 \newtheorem{definition}{Definition}
 
 \newcommand{\type}{\,\,\text{type}}
 \newcommand{\ctx}{\,\,\text{ctx}}
 \newcommand{\ltdyn}{\sqsubseteq}
+\newcommand{\gtdyn}{\sqsupseteq}
+\newcommand{\equidyn}{\mathrel{\gtdyn\ltdyn}}
 \newcommand{\ltdynv}{\mathrel{\sqsubseteq_V}}
 \newcommand{\ltdynt}{\mathrel{\sqsubseteq_T}}
 
+\newcommand{\upcast}[2]{\langle #2 \leftarrowtail #1 \rangle}
+\newcommand{\dncast}[2]{\langle #1 \twoheadleftarrow #2 \rangle}
+
 \newcommand{\Set}{\text{Set}}
 \newcommand{\relto}{\to}
 \newcommand{\M}{\mathcal{M}}
@@ -76,11 +82,11 @@
     \inferrule{x:A \in \Gamma}
     {\Gamma \vdash^v x : A}
 
-    \inferrule{\gamma : \pi_{x:A \in \Gamma} \Delta \vdash \gamma(x) : A\and
+    \inferrule{\gamma : \prod_{x:A \in \Gamma} \Delta \vdash \gamma(x) : A\and
       \Gamma \vdash v : B
     }{\Delta \vdash v[\gamma] : B}
 
-    \inferrule{\gamma : \pi_{x:A \in \Gamma} \Delta \vdash \gamma(x) : A\and
+    \inferrule{\gamma : \prod_{x:A \in \Gamma} \Delta \vdash \gamma(x) : A\and
       \Gamma \vdash t : B
     }{\Delta \vdash t[\gamma] : B}
 
@@ -101,6 +107,171 @@
   \caption{GTTv Judgmental Term, Value Rules}
 \end{figure}
 
+\begin{mathpar}
+  \inferrule
+  {}
+  {\Phi, x \ltdyn x' : A \ltdyn A' \vdash \ret x \ltdyn \ret x' : A \ltdyn A'}
+
+  \inferrule
+  {\Phi \vdash t \ltdyn t' : A \ltdyn A'\and
+    \Phi, x \ltdyn x' : A \ltdyn A' \vdash u \ltdyn u' : C \ltdyn C'}
+  {\Phi \vdash \lett x = t; u \ltdyn \lett x' = t'; u' : C \ltdyn C'}
+\end{mathpar}
+
+\begin{mathpar}
+  \inferrule
+  {\Gamma \vdash^v v : A \and A \ltdyn A'}
+  {\Gamma \vdash^T \upcast{A}{A'}v : A'}
+
+  \inferrule
+  {\Gamma \vdash^v v : A' \and A \ltdyn A'}
+  {\Gamma \vdash^T \dncast{A}{A'}v : A}
+
+  \inferrule
+  {}
+  {x \ltdyn x' : A \ltdyn A' \vdash \upcast{A}{A'}x \ltdyn \ret x' : A'}
+
+  \inferrule
+  {}
+  {x : A \vdash \ret x \ltdyn \upcast{A}{A'}x : A \ltdyn A'}
+
+  \inferrule
+  {}
+  {x \ltdyn x' : A \ltdyn A' \vdash \ret x \ltdyn \dncast{A}{A'}x' : A'}
+
+  \inferrule
+  {}
+  {x' : A' \vdash \dncast{A}{A'}x' \ltdyn x' : A \ltdyn A'}
+\end{mathpar}
+
+\begin{mathpar}
+  \inferrule{A \type \and B \type}{A \times B \type}
+
+  \inferrule
+  {\Gamma \vdash v_1 : A_1 \and \Gamma \vdash v_2 : A_2}
+  {\Gamma \vdash^{V} (v_1, v_2) : A_1 \times A_2}
+
+  \inferrule
+  {\Gamma \vdash t : A_1 \times A_2\and
+    \Gamma, x_1 : A_1, x_2 : A_2 \vdash u : C}
+  {\Gamma \vdash \lett (x,x') = t; u : C}
+  
+  \inferrule
+  {}
+  {x \ltdyn x' : A \ltdyn A', y \ltdyn y' : B \ltdyn B' \vdash \ret (x,y) \ltdyn \ret (x',y') : A \times B \ltdyn A' \times B'}
+
+  \inferrule
+  {\Phi \vdash t \ltdyn t' : A \times B \ltdyn A' \times B'\and
+    \Phi, x \ltdyn x' : A \ltdyn A', y \ltdyn y' : B \ltdyn B' \vdash u \ltdyn u' : C \ltdyn C'}
+  {\Phi \vdash \lett (x,y) = t; u \ltdyn \lett (x',y') = t'; u' : C \ltdyn C'}
+
+  \inferrule
+  {}
+  {\Gamma \vdash \lett (x_1,x_2) = (v_1,v_2); t \equidyn t[v_1/x_1,v_2/x_2] : C}
+
+  \inferrule
+  {}
+  {\Gamma \vdash t \equidyn \lett (x_1,x_2) = t; \ret (x_1,x_2) : A_1 \times A_2}
+\end{mathpar}
+
+\begin{theorem}[Product Contract]
+  If $A_1 \ltdyn A_1'$ and $A_2 \ltdyn A_2'$ then
+
+  \begin{align*}
+  x' : A_1' \times A_2' \vdash
+  \dncast{A_1\times A_2}{A_1'\times A_2'}x'
+  &\equidyn\\
+  \lett (x_1', x_2') = x'; \lett y_1 = \dncast{A_1}{A_1'}x_1'; \lett y_2 = \dncast{A_2}{A_2'}x_2'; \ret (y_1,y_2)&\equidyn\\
+  \lett (x_1', x_2') = x'; \lett y_2 = \dncast{A_2}{A_2'}x_2'; \lett y_1 = \dncast{A_1}{A_1'}x_1'; \ret (y_1,y_2)\\
+  \end{align*}
+\end{theorem}
+\begin{proof}
+  First, we show the direction that requires $\eta$ expansion.
+  \begin{mathpar}
+    \inferrule{}
+    {
+  \dncast{A_1\times A_2}{A_1'\times A_2'}x'
+  \ltdyn
+  \lett (x_1', x_2') = x'; \lett y_1 = \dncast{A_1}{A_1'}x_1'; \lett y_2 = \dncast{A_2}{A_2'}x_2'; \ret (y_1,y_2)}
+  \end{mathpar}
+
+  By the Down-Left rule, it is sufficient to prove that under $x \ltdyn x' : (A_1 \times A_2) \ltdyn (A_1' \times A_2')$,
+  \begin{mathpar}
+  {x \ltdyn
+  \lett (x_1', x_2') = x'; \lett y_1 = \dncast{A_1}{A_1'}x_1'; \lett y_2 = \dncast{A_2}{A_2'}x_2'; \ret (y_1,y_2)}
+  \end{mathpar}
+
+  By the $\eta$ rule for products and the let-rule for values, $x :
+  A_1 \times A_2$ can be expanded as follows:
+  \begin{align*}
+  x &\equidyn
+  \lett (x_1,x_2) = x; \ret (x_1,x_2)\\
+  &\equidyn
+  \lett (x_1,x_2) = x; \lett y_1 =\ret x_1; \ret (y_1,x_2)\\
+  &\equidyn
+  \lett (x_1,x_2) = x; \lett y_1 = \ret x_1; \lett y_2 = \ret x_2; \ret (y_1,y_2)
+  \end{align*}
+
+Now that we have the two sides with the same structre, we use the
+congruence rules for product pattern matching and we have to use the
+Down-Right rule twice:
+
+\begin{mathpar}
+  x_1 \ltdyn x_1' : A_1 \ltdyn A_1' \vdash \ret x_1 \ltdyn \dncast{A_1}{A_1'}{x_1'} : A_1
+  
+  x_2 \ltdyn x_2' : A_2 \ltdyn A_2' \vdash \ret x_2 \ltdyn \dncast{A_2}{A_2'}{x_2'} : A_2
+\end{mathpar}
+
+Next, we show the reverse inequality using $\eta$ contraction
+
+  \begin{mathpar}
+    {
+      \lett (x_1', x_2') = x'; \lett y_1 = \dncast{A_1}{A_1'}x_1'; \lett y_2 = \dncast{A_2}{A_2'}x_2'; \ret (y_1,y_2)\ltdyn \dncast{A_1\times A_2}{A_1'\times A_2'}x' }
+  \end{mathpar}
+
+  This time, we need to use congruence \emph{first}, because the
+  downcast is on the right, we can't use the Down-Right rule unless
+  the left side is already at the less dynamic type.
+
+  So we rewrite the right side as
+  \begin{align*}
+    \dncast{A_1\times A_2}{A_1'\times A_2'}x'
+    &\ltdyn
+    \lett (x_1',x_2') = x'; \dncast{A_1\times A_2}{A_1'\times A_2'}(x_1',x_2')\\
+    &\ltdyn
+    \lett (x_1',x_2') = x'; \lett y_1' = x_1'; \dncast{A_1\times A_2}{A_1'\times A_2'}(x_1',x_2')\\
+    &\ltdyn
+    \lett (x_1',x_2') = x'; \lett y_1' = x_1'; \lett y_2' = x_2'; \dncast{A_1\times A_2}{A_1'\times A_2'}(x_1',x_2')
+  \end{align*}
+\end{proof}
+
+Then the proof is again by the congruence rules, using Down-Left twice
+and Down-Right once:
+
+\begin{mathpar}
+  x_1' : A_1' \vdash \dncast{A_1}{A_1'}x_1' \ltdyn \ret x_1'
+
+  x_2' : A_2' \vdash \dncast{A_2}{A_2'}x_2' \ltdyn \ret x_2'
+
+  x_1 \ltdyn x_1', x_2 \ltdyn x_2' \vdash (x_1,x_2) \ltdyn \dncast{A_1\times A_2}{A_1'\times A_2'}(x_1',x_2')
+\end{mathpar}
+
+\begin{corollary}[Projections commute]
+ For any $A \ltdyn A', B \ltdyn B'$ and $\Gamma, x:A, y : B \vdash t : C$,
+ \[
+ \lett x = \dncast{A}{A'}x'; \lett y = \dncast B {B'} y'; t
+ \equidyn
+ \lett y = \dncast B {B'} y'; \lett x = \dncast{A}{A'}x'; t
+ \]
+\end{corollary}
+\begin{proof}
+  By the previous theorem, both are equivalent to
+  \[
+  \lett z = \dncast{A\times B}{A' \times B'}(x',y');
+  \lett (x,y) = z;
+  t
+  \]
+\end{proof}
 
 \end{document}