Compare commits
No commits in common. "2d557e51e49d5f4af0a14d47e71649bc895d3708" and "b31c8abc6c4a0f890dd10c89c5711aa485b29470" have entirely different histories.
2d557e51e4
...
b31c8abc6c
4 changed files with 44 additions and 70 deletions
|
@ -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)
|
(expr_ty_app (expr_ty_abs x e) a) -->β (expr_specialize x a e)
|
||||||
|
|
||||||
| E_AppLam : forall x τ e a,
|
| 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,
|
| E_AppLet : forall x t e a,
|
||||||
(expr_let x t a e) -->β (expr_subst x a e)
|
(expr_let x t a e) -->β (expr_subst x a e)
|
||||||
|
|
||||||
where "s '-->β' t" := (beta_step s t).
|
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 :=
|
Inductive multi {X : Type} (R : X -> X -> Prop) : X -> X -> Prop :=
|
||||||
| Multi_Refl : forall (x : X), multi R x x
|
| Multi_Refl : forall (x : X), multi R x x
|
||||||
| Multi_Step : forall (x y z : X),
|
| Multi_Step : forall (x y z : X),
|
||||||
|
|
28
coq/terms.v
28
coq/terms.v
|
@ -30,33 +30,6 @@ Inductive expr_term : Type :=
|
||||||
| expr_descend : type_term -> expr_term -> expr_term
|
| 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 *)
|
(* values *)
|
||||||
Inductive is_value : expr_term -> Prop :=
|
Inductive is_value : expr_term -> Prop :=
|
||||||
| V_Abs : forall x τ e,
|
| V_Abs : forall x τ e,
|
||||||
|
@ -71,6 +44,7 @@ Inductive is_value : expr_term -> Prop :=
|
||||||
.
|
.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
Declare Scope ladder_type_scope.
|
Declare Scope ladder_type_scope.
|
||||||
Declare Scope ladder_expr_scope.
|
Declare Scope ladder_expr_scope.
|
||||||
Declare Custom Entry ladder_type.
|
Declare Custom Entry ladder_type.
|
||||||
|
|
|
@ -20,23 +20,11 @@ This document lists the Coq-Sourcecode from commit
|
||||||
\label{coq:equiv}
|
\label{coq:equiv}
|
||||||
\inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/equiv.v}
|
\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}
|
\subsection{typing.v}
|
||||||
\label{coq:typing}
|
\label{coq:typing}
|
||||||
\inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/typing.v}
|
\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}
|
\subsection{smallstep.v}
|
||||||
\label{coq:smallstep}
|
\label{coq:smallstep}
|
||||||
\inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/smallstep.v}
|
\inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/smallstep.v}
|
||||||
|
|
||||||
\subsection{soundness.v}
|
|
||||||
\label{coq:smallstep}
|
|
||||||
\inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/soundness.v}
|
|
||||||
|
|
||||||
|
|
|
@ -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}.
|
such that \( \emptyset \vdash \metavariable{e} : \metavariable{\tau} \) by \ref{def:typerules}.
|
||||||
\end{definition}
|
\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}.
|
such that \( \emptyset \vdash \metavariable{e} :\approx \metavariable{\tau} \) by \ref{def:typerules} and \ref{def:semtyperules}.
|
||||||
\end{definition}
|
\end{definition}
|
||||||
|
|
||||||
|
|
||||||
\begin{definition}["is" Typing Relation]
|
\begin{definition}[Syntactic Typing Relation]
|
||||||
|
|
||||||
\label{def:typerules}
|
\label{def:typerules}
|
||||||
\begin{mathpar}
|
\begin{mathpar}
|
||||||
|
@ -626,37 +626,30 @@ such that \( \emptyset \vdash \metavariable{e} :\approx \metavariable{\tau} \) b
|
||||||
\end{mathpar}
|
\end{mathpar}
|
||||||
\end{definition}
|
\end{definition}
|
||||||
|
|
||||||
\begin{definition}["compatible" Typing Relation]
|
\begin{definition}[Semantic Typing Relation]
|
||||||
\label{def:semtyperules}
|
\label{def:semtyperules}
|
||||||
\begin{mathpar}
|
\begin{mathpar}
|
||||||
\inferrule[TCompat-NativeRepr]{
|
\inferrule[T-NativeRepr]{
|
||||||
\Gamma\vdash \metavariable{e} : \metavariable{\tau}
|
\Gamma\vdash \metavariable{e} : \metavariable{\tau}
|
||||||
}{
|
}{
|
||||||
\Gamma\vdash \metavariable{e} :\approx \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}\\
|
\Gamma \vdash \metavariable{e} :\approx \metavariable{\tau}\\
|
||||||
% \metavariable{\tau} \precsim \metavariable{\tau'}\\
|
% \metavariable{\tau} \precsim \metavariable{\tau'}\\
|
||||||
%\exists \metavariable{h} \text{ s.t. }
|
%\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'}
|
\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 \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{mathpar}
|
||||||
\end{definition}
|
\end{definition}
|
||||||
|
@ -782,16 +775,13 @@ Evaluation of an expression \(\metavariable{e} \in \nonterm{E}\) is defined by e
|
||||||
\exprterminal{\text{ in }}\metavariable{e}
|
\exprterminal{\text{ in }}\metavariable{e}
|
||||||
\rightarrow_\beta
|
\rightarrow_\beta
|
||||||
\{ \metavariable{x} \mapsto \metavariable{a} \} \metavariable{e}
|
\{ \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}
|
\metavariable{e}
|
||||||
|
\exprterminal{\text{ as }}
|
||||||
|
\metavariable{\tau}
|
||||||
\rightarrow_\beta
|
\rightarrow_\beta
|
||||||
\metavariable{v}
|
|
||||||
\metavariable{e}
|
\metavariable{e}
|
||||||
}
|
}
|
||||||
\end{mathpar}
|
\end{mathpar}
|
||||||
|
|
Loading…
Reference in a new issue