From 1bd55cd8c38434bcaa37b331be1d309dec310545 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Wed, 4 Sep 2024 12:45:33 +0200
Subject: [PATCH] paper: rename inference rules to match coq definitions

---
 paper/main.tex | 44 +++++++++++++++++++++++++++-----------------
 1 file changed, 27 insertions(+), 17 deletions(-)

diff --git a/paper/main.tex b/paper/main.tex
index d8eab57..3a21b30 100644
--- a/paper/main.tex
+++ b/paper/main.tex
@@ -531,18 +531,18 @@ can be derived from the context \(\Gamma\) where \(\metavariable{e} \in \nonterm
 
 
 
-\begin{definition}[Syntactic Well-Typedness]
-An expression \(\metavariable{e} \in \nonterm{E}\) is \textbf{syntactically well-typed} if there exists a type \(\metavariable{\tau} \in \nonterm{T}\),
+\begin{definition}[Representational Well-Typedness]
+An expression \(\metavariable{e} \in \nonterm{E}\) is \textbf{representationally well-typed} if there exists a type \(\metavariable{\tau} \in \nonterm{T}\),
 such that \( \emptyset \vdash \metavariable{e} : \metavariable{\tau} \) by \ref{def:typerules}.
 \end{definition}
 
-\begin{definition}[Semantic Well-Typedness]
-An expression \(\metavariable{e} \in \nonterm{E}\) is \textbf{semantically well-typed} if there exists a type \(\metavariable{\tau} \in \nonterm{T}\),
+\begin{definition}[Compatible Well-Typedness]
+An expression \(\metavariable{e} \in \nonterm{E}\) is \textbf{compatibly well-typed} if there exists a type \(\metavariable{\tau} \in \nonterm{T}\),
 such that \( \emptyset \vdash \metavariable{e} :\approx \metavariable{\tau} \) by \ref{def:typerules} and \ref{def:semtyperules}.
 \end{definition}
 
 
-\begin{definition}[Syntactic Typing Relation]
+\begin{definition}["is" Typing Relation]
 
 \label{def:typerules}
 \begin{mathpar}
@@ -626,30 +626,37 @@ such that \( \emptyset \vdash \metavariable{e} :\approx \metavariable{\tau} \) b
 \end{mathpar}
 \end{definition}
 
-\begin{definition}[Semantic Typing Relation]
+\begin{definition}["compatible" Typing Relation]
 \label{def:semtyperules}
 \begin{mathpar}
-	\inferrule[T-NativeRepr]{
+	\inferrule[TCompat-NativeRepr]{
 		\Gamma\vdash \metavariable{e} : \metavariable{\tau}
 	}{
 		\Gamma\vdash \metavariable{e} :\approx \metavariable{\tau}
 	}
 
-	\inferrule[T-CoercedRepr]{
+	\inferrule[TCompat-Let]{
+		\Gamma \vdash \metavariable{e} : \metavariable{\sigma} \\
+		\Gamma , \metavariable{x}:\metavariable{\sigma} \vdash \metavariable{t} :\approx \metavariable{\tau}
+	}{
+		\Gamma \vdash (\exprterminal{\text{let }}\metavariable{x}\exprterminal{\text{ = }}\metavariable{e}\exprterminal{\text{ in }} \metavariable{t}) :\approx \metavariable{\tau}
+	}
+
+
+	\inferrule[TCompat-Morph]{
 		\Gamma \vdash \metavariable{e} :\approx \metavariable{\tau}\\
 %		\metavariable{\tau} \precsim \metavariable{\tau'}\\
 		%\exists \metavariable{h} \text{ s.t. }
-		\Gamma \vdash \metavariable{h}: \typeterminal{\metavariable{\tau}\rightarrow_\text{morph}\metavariable{\tau'}}
+		\metavariable{h}:\typeterminal{\metavariable{\tau}\rightarrow_\text{morph}\metavariable{\tau'}} \in \Gamma
 	}{
 		\Gamma \vdash \metavariable{e} :\approx \metavariable{\tau'}
 	}
 
-
-	\inferrule[T-CompatibleApp]{
-		\Gamma \vdash \metavariable{f} : \metavariable{\sigma} \rightarrow \metavariable{\tau}\\
+	\inferrule[TCompat-App]{
+		\Gamma \vdash \metavariable{f} : \metavariable{\sigma} \typeterminal{\rightarrow} \metavariable{\tau}\\
 		\Gamma \vdash \metavariable{a} :\approx \metavariable{\sigma}
 	}{
-		\Gamma \vdash \exprterminal{(\metavariable{f} \text{ } \metavariable{a})} : \metavariable{\tau}
+		\Gamma \vdash \exprterminal{(\metavariable{f} \text{ } \metavariable{a})} :\approx \metavariable{\tau}
 	}
 \end{mathpar}
 \end{definition}
@@ -775,13 +782,16 @@ Evaluation of an expression \(\metavariable{e} \in \nonterm{E}\) is defined by e
 		\exprterminal{\text{ in }}\metavariable{e}
 		\rightarrow_\beta
 		\{ \metavariable{x} \mapsto \metavariable{a} \} \metavariable{e}
-	}\and
-	\inferrule[E-Ascribe]{
+	}
+	
+	\inferrule[E-AppLamAscribe]{
 	}{
-		\metavariable{e}
+		\exprterminal{( \lambda \metavariable{x}:\metavariable{\sigma} \mapsto \metavariable{e} )}
 		\exprterminal{\text{ as }}
-		\metavariable{\tau}
+		\typeterminal{\metavariable{\tau}}
+		\metavariable{e}
 		\rightarrow_\beta
+		\metavariable{v}
 		\metavariable{e}
 	}
 \end{mathpar}