coq/smallstep.v

@@ -65,16 +65,38 @@ Inductive beta_step : expr_term -> expr_term -> Prop :=
     (expr_ty_app (expr_ty_abs x e) a) -->β (expr_specialize x a e)
 
   | E_AppLam : forall x τ e a,
-    (expr_app (expr_abs x τ e) a) -->β (expr_subst x a e)
+    (expr_tm_app (expr_tm_abs x τ e) a) -->β (expr_subst x a e)
-
-  | E_AppMorph : forall x τ e a,
-    (expr_app (expr_morph x τ e) a) -->β (expr_subst x a e)
 
   | E_AppLet : forall x t e a,
     (expr_let x t a e) -->β (expr_subst x a e)
 
 where "s '-->β' t" := (beta_step s t).
 
+
+
+Inductive delta_step : expr_term -> expr_term -> Prop :=
+
+  | E_ImplicitCast : forall (Γ:context) (f:expr_term) (h:string) (a:expr_term) (τ:type_term) (s:type_term) (p:type_term),
+
+    (context_contains Γ h (type_morph p s)) ->
+    Γ |- f \is (type_fun s τ) ->
+    Γ |- a \is p ->
+    (expr_tm_app f a) -->δ (expr_tm_app f (expr_tm_app (expr_var h) a))
+
+where "s '-->δ' t" := (delta_step s t).
+
+
+Inductive eval_step : expr_term -> expr_term -> Prop :=
+  | E_Beta : forall s t,
+    (s -->β t) ->
+    (s -->eval t)
+
+  | E_Delta : forall s t,
+    (s -->δ t) ->
+    (s -->eval t)
+
+where "s '-->eval' t" := (eval_step s t).
+
 Inductive multi {X : Type} (R : X -> X -> Prop) : X -> X -> Prop :=
   | Multi_Refl : forall (x : X), multi R x x
   | Multi_Step : forall (x y z : X),

coq/terms.v

@@ -30,33 +30,6 @@ Inductive expr_term : Type :=
   | expr_descend : type_term -> expr_term -> expr_term
 .
 
-
-(* TODO
-
-Inductive type_DeBruijn : Type :=
-  | id : nat -> type_DeBruijn
-  | var : nat -> type_DeBruijn
-  | fun : type_DeBruijn -> type_DeBruijn -> type_DeBruijn
-  | univ : type_DeBruijn -> type_DeBruijn
-  | spec : type_DeBruijn -> type_DeBruijn -> type_DeBruijn
-  | morph : type_DeBruijn -> type_DeBruijn -> type_DeBruijn
-  | ladder : type_DeBruijn -> type_DeBruijn -> type_DeBruijn
-
-Inductive expr_DeBruijn : Type :=
-  | var : nat -> expr_DeBruijn
-  | ty_abs : expr_DeBruijn -> expr_DeBruijn
-  | ty_app : expr_DeBruijn -> type_DeBruijn -> expr_Debruijn
-  | abs   : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
-  | morph : type_DeBruijn -> expr_DeBruijn -> expr_Debruijn
-  | app : expr_DeBruijn -> expr_DeBruijn -> expr_Debruijn
-  | let : type_DeBruijn -> expr_DeBruijn -> expr_Debruijn -> expr_Debruijn
-  | ascend : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
-  | descend : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
-.
-*)
-
-
-
 (* values *)
 Inductive is_value : expr_term -> Prop :=
   | V_Abs : forall x τ e,
@@ -71,6 +44,7 @@ Inductive is_value : expr_term -> Prop :=
 .
 
 
+
 Declare Scope ladder_type_scope.
 Declare Scope ladder_expr_scope.
 Declare Custom Entry ladder_type.

paper/appendix.tex

@@ -20,23 +20,11 @@ This document lists the Coq-Sourcecode from commit
 \label{coq:equiv}
 \inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/equiv.v}
 
-\subsection{subtype.v}
-\label{coq:typing}
-\inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/subtype.v}
-
 \subsection{typing.v}
 \label{coq:typing}
 \inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/typing.v}
 
-\subsection{morph.v}
-\label{coq:typing}
-\inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/morph.v}
-
 \subsection{smallstep.v}
 \label{coq:smallstep}
 \inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/smallstep.v}
 
-\subsection{soundness.v}
-\label{coq:smallstep}
-\inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/soundness.v}
-

paper/main.tex

@@ -531,18 +531,18 @@ can be derived from the context \(\Gamma\) where \(\metavariable{e} \in \nonterm
 
 
 
-\begin{definition}[Representational Well-Typedness]
+\begin{definition}[Syntactic Well-Typedness]
-An expression \(\metavariable{e} \in \nonterm{E}\) is \textbf{representationally well-typed} if there exists a type \(\metavariable{\tau} \in \nonterm{T}\),
+An expression \(\metavariable{e} \in \nonterm{E}\) is \textbf{syntactically 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}[Compatible Well-Typedness]
+\begin{definition}[Semantic Well-Typedness]
-An expression \(\metavariable{e} \in \nonterm{E}\) is \textbf{compatibly well-typed} if there exists a type \(\metavariable{\tau} \in \nonterm{T}\),
+An expression \(\metavariable{e} \in \nonterm{E}\) is \textbf{semantically 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}["is" Typing Relation]
+\begin{definition}[Syntactic Typing Relation]
 
 \label{def:typerules}
 \begin{mathpar}
@@ -626,37 +626,30 @@ such that \( \emptyset \vdash \metavariable{e} :\approx \metavariable{\tau} \) b
 \end{mathpar}
 \end{definition}
 
-\begin{definition}["compatible" Typing Relation]
+\begin{definition}[Semantic Typing Relation]
 \label{def:semtyperules}
 \begin{mathpar}
-	\inferrule[TCompat-NativeRepr]{
+	\inferrule[T-NativeRepr]{
 		\Gamma\vdash \metavariable{e} : \metavariable{\tau}
 	}{
 		\Gamma\vdash \metavariable{e} :\approx \metavariable{\tau}
 	}
 
-	\inferrule[TCompat-Let]{
+	\inferrule[T-CoercedRepr]{
-		\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. }
-		\metavariable{h}:\typeterminal{\metavariable{\tau}\rightarrow_\text{morph}\metavariable{\tau'}} \in \Gamma
+		\Gamma \vdash \metavariable{h}: \typeterminal{\metavariable{\tau}\rightarrow_\text{morph}\metavariable{\tau'}}
 	}{
 		\Gamma \vdash \metavariable{e} :\approx \metavariable{\tau'}
 	}
 
-	\inferrule[TCompat-App]{
+
-		\Gamma \vdash \metavariable{f} : \metavariable{\sigma} \typeterminal{\rightarrow} \metavariable{\tau}\\
+	\inferrule[T-CompatibleApp]{
+		\Gamma \vdash \metavariable{f} : \metavariable{\sigma} \rightarrow \metavariable{\tau}\\
 		\Gamma \vdash \metavariable{a} :\approx \metavariable{\sigma}
 	}{
-		\Gamma \vdash \exprterminal{(\metavariable{f} \text{ } \metavariable{a})} :\approx \metavariable{\tau}
+		\Gamma \vdash \exprterminal{(\metavariable{f} \text{ } \metavariable{a})} : \metavariable{\tau}
 	}
 \end{mathpar}
 \end{definition}
@@ -782,16 +775,13 @@ 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]{
 	}{
-		\exprterminal{( \lambda \metavariable{x}:\metavariable{\sigma} \mapsto \metavariable{e} )}
-		\exprterminal{\text{ as }}
-		\typeterminal{\metavariable{\tau}}
 		\metavariable{e}
+		\exprterminal{\text{ as }}
+		\metavariable{\tau}
 		\rightarrow_\beta
-		\metavariable{v}
 		\metavariable{e}
 	}
 \end{mathpar}