WIP coq: debruijn terms

coq/smallstep.v

@@ -65,38 +65,16 @@ 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_tm_app (expr_tm_abs x τ e) a) -->β (expr_subst x a e)
+    (expr_app (expr_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,6 +30,33 @@ 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,
@@ -44,7 +71,6 @@ 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,11 +20,23 @@ 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}[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}