Compare commits

..

No commits in common. "c7794d8a89c93104b8096907f18bf883bad335da" and "13165a7951b9322b65a6debc17ffe01c8d245f6d" have entirely different histories.

3 changed files with 48 additions and 132 deletions

View file

@ -36,36 +36,10 @@ Coercion type_var : string >-> type_term.
Coercion expr_var : string >-> expr_term. Coercion expr_var : string >-> expr_term.
(* (*
Coercion type_var : string >-> type_term. Notation "( x )" := x (at level 70).
Coercion expr_var : string >-> expr_term. Notation "x ~ y" := (type_rung x y) (at level 69, left associativity).
Notation "< x y >" := (type_app x y) (at level 68, left associativity).
Notation "'$' x" := (type_id x) (at level 66).
*) *)
Declare Scope ladder_type_scope.
Declare Scope ladder_expr_scope.
Declare Custom Entry ladder_type.
Notation "[ e ]" := e (e custom ladder_type at level 80) : ladder_type_scope.
(* TODO: allow any variable names in notation, not just α,β,γ *)
Notation "'∀α.' τ" := (type_univ "α" τ) (in custom ladder_type at level 80) : ladder_type_scope.
Notation "'∀β.' τ" := (type_univ "β" τ) (in custom ladder_type at level 80) : ladder_type_scope.
Notation "'∀γ.' τ" := (type_univ "γ" τ) (in custom ladder_type at level 80) : ladder_type_scope.
Notation "'<' σ τ '>'" := (type_spec σ τ) (in custom ladder_type at level 80, left associativity) : ladder_type_scope.
Notation "'(' τ ')'" := τ (in custom ladder_type at level 70) : ladder_type_scope.
Notation "σ '->' τ" := (type_fun σ τ) (in custom ladder_type at level 75, right associativity) : ladder_type_scope.
Notation "σ '->morph' τ" := (type_morph σ τ) (in custom ladder_type at level 75, right associativity) : ladder_type_scope.
Notation "σ '~' τ" := (type_ladder σ τ) (in custom ladder_type at level 70, right associativity) : ladder_type_scope.
Notation "'α'" := (type_var "α") (in custom ladder_type at level 60, right associativity) : ladder_type_scope.
Notation "'β'" := (type_var "β") (in custom ladder_type at level 60, right associativity) : ladder_type_scope.
Notation "'γ'" := (type_var "γ") (in custom ladder_type at level 60, right associativity) : ladder_type_scope.
Open Scope ladder_type_scope.
Definition t1 : type_term := [ α.β.(α~β~γ)->β->(α->α)->β ].
Compute t1.
Close Scope ladder_type_scope.
End Terms. End Terms.

View file

@ -21,69 +21,35 @@ Inductive context_contains : context -> string -> type_term -> Prop :=
(context_contains Γ x X) -> (context_contains Γ x X) ->
(context_contains (ctx_assign y Y Γ) x X). (context_contains (ctx_assign y Y Γ) x X).
Reserved Notation "Gamma '|-' x '\is' X" (at level 101, x at next level, X at level 0). Reserved Notation "Gamma '|-' x '\in' X" (at level 101, x at next level, X at level 0).
Reserved Notation "Gamma '|-' x '\compatible' X" (at level 101, x at next level, X at level 0).
Inductive expr_type : context -> expr_term -> type_term -> Prop := Inductive expr_type : context -> expr -> ladder_type -> Prop :=
| T_Var : forall Γ x τ, | T_Var : forall Γ x X,
(context_contains Γ x τ) -> (context_contains Γ x X) ->
(Γ |- x \is τ) Γ |- x \in X
| T_Let : forall Γ s (σ:type_term) t τ x, | T_Let : forall Γ s (σ:ladder_type) t τ x,
(Γ |- s \is σ) -> Γ |- s \in σ ->
(Γ |- t \is τ) -> Γ |- t \in τ ->
(Γ |- (expr_let x σ s t) \is τ) Γ |- (expr_let x σ s t) \in τ
| T_TypeAbs : forall Γ (e:expr_term) (τ:type_term) α, | T_Abs : forall (Γ:context) (x:string) (X:ladder_type) (t:expr) (T:ladder_type),
Γ |- e \is τ -> Γ |- t \in T ->
Γ |- (expr_ty_abs α e) \is (type_univ α τ) Γ |- (expr_tm_abs x X t) \in (type_fun X T)
| T_TypeApp : forall Γ α (e:expr_term) (σ:type_term) (τ:type_term), | T_App : forall (Γ:context) (f:expr) (a:expr) (S:ladder_type) (T:ladder_type),
Γ |- e \is (type_univ α τ) -> Γ |- f \in (type_fun S T) ->
Γ |- (expr_ty_app e σ) \is (type_subst α σ τ) Γ |- a \in S ->
Γ |- (expr_tm_app f a) \in T
| T_Abs : forall (Γ:context) (x:string) (σ:type_term) (t:expr_term) (τ:type_term), where "Γ '|-' x '\in' X" := (expr_type Γ x X).
(context_contains Γ x σ) ->
Γ |- t \is τ ->
Γ |- (expr_tm_abs x σ t) \is (type_fun σ τ)
| T_App : forall (Γ:context) (f:expr_term) (a:expr_term) (σ:type_term) (τ:type_term),
Γ |- f \is (type_fun σ τ) ->
Γ |- a \is σ ->
Γ |- (expr_tm_app f a) \is τ
where "Γ '|-' x '\is' τ" := (expr_type Γ x τ).
Inductive expr_type_compatible : context -> expr_term -> type_term -> Prop :=
| T_Compatible : forall Γ x τ,
(Γ |- x \is τ) ->
(Γ |- x \compatible τ)
where "Γ '|-' x '\compatible' τ" := (expr_type_compatible Γ x τ).
Example typing1 : Example typing1 :
forall Γ, ctx_empty |-
(context_contains Γ "x" (type_var "T")) -> (expr_ty_abs "T" (expr_tm_abs "x" (type_var "T") (expr_var "x"))) \in
Γ |- (expr_ty_abs "T" (expr_tm_abs "x" (type_var "T") (expr_var "x"))) \is
(type_univ "T" (type_fun (type_var "T") (type_var "T"))). (type_univ "T" (type_fun (type_var "T") (type_var "T"))).
Proof. Proof.
intros.
apply T_TypeAbs.
apply T_Abs.
apply H.
apply T_Var.
apply H.
Admitted.
Example typing2 :
ctx_empty |- (expr_ty_abs "T" (expr_tm_abs "x" (type_var "T") (expr_var "x"))) \is
(type_univ "T" (type_fun (type_var "T") (type_var "T"))).
Proof.
apply T_TypeAbs.
apply T_Abs.
Admitted. Admitted.
End Typing. End Typing.

View file

@ -176,11 +176,11 @@ $$\\$$
\metavariable{x} \quad \valnonterm{\typevars}{\exprvars} \metavariable{x} \quad \valnonterm{\typevars}{\exprvars}
}{Value Conactenation} }{Value Conactenation}
\otherform{ %\otherform{
\exprterminal{\Lambda} \metavariable{\alpha} \quad % \exprterminal{\Lambda} \metavariable{\alpha} \quad
\exprterminal{\mapsto} \quad % \exprterminal{\mapsto} \quad
\valnonterm{ \typevars \cup \{ \metavariable{\alpha} \} } % \valnonterm{ \typevars \cup \{ \metavariable{\alpha} \} }
\{Type-Function Value} %}{Type-Function Value}
\otherform{ \otherform{
\exprterminal{\lambda} \metavariable{x} \quad \exprterminal{\lambda} \metavariable{x} \quad
@ -371,8 +371,8 @@ As usual, each rule is composed of premises (above the horizontal line) and a co
} }
\inferrule[T-TypeApp]{ \inferrule[T-TypeApp]{
\metavariable{\tau} \in \typenonterm{\typevars \cup \{\metavariable{\alpha}\}} \\ \Gamma \vdash \metavariable{e} : \metavariable{\tau} \\
\Gamma \vdash \metavariable{e} : \typeterminal{\forall} \metavariable{\alpha} \typeterminal{.} \metavariable{\tau} \\ \metavariable{\tau} \in \typenonterm{\typevars \cup \metavariable{\alpha}} \\
\metavariable{\sigma} \in \typenonterm{\typevars} \metavariable{\sigma} \in \typenonterm{\typevars}
}{ }{
\Gamma \vdash ( \metavariable{e} \quad \metavariable{\sigma} ) : \{\metavariable{\alpha} \mapsto \metavariable{\sigma}\} \metavariable{\tau} \Gamma \vdash ( \metavariable{e} \quad \metavariable{\sigma} ) : \{\metavariable{\alpha} \mapsto \metavariable{\sigma}\} \metavariable{\tau}
@ -520,66 +520,42 @@ which are given in \ref{def:evalrules}.
\begin{lemma}[\(\beta\)-reduction preserves \(\delta\)-normalform] \begin{lemma}[\(\beta\)-reduction preserves \(\delta\)-normalform]
\label{lemma:preserve-delta-normalform} Assume \metavariable{e} is in \(\delta\)-normalform and \(\metavariable{e} \rightarrow \metavariable{e'}\). Then \(\metavariable{e'}\) is in \(\delta\)-normalform as well.
Assume \metavariable{e} is in \(\delta\)-normalform and \(\metavariable{e} \rightarrow_\beta \metavariable{e'}\). Then \(\metavariable{e'}\) is in \(\delta\)-normalform as well.
\begin{proof} \begin{proof}
\todo{} \todo{}
\end{proof} \end{proof}
\end{lemma} \end{lemma}
\begin{lemma}[\(\delta\)-normalform eliminates compatibility]
\label{lemma:eliminate-compat}
Assume \(\emptyset \vdash \metavariable{e} :\approx \metavariable{\tau}\) and \(\metavariable{e} \rightarrow_{\delta}^* \metavariable{e'}\) such that \(\metavariable{e'}\) is in \(\delta\)-normalform.
Then \(\emptyset \vdash \metavariable{e'} : \metavariable{\tau}\)
\begin{proof}
\end{proof}
\end{lemma}
\subsection{Proof of Syntactic Type Soundness} \subsection{Proof of Syntactic Type Soundness}
\begin{lemma}[\(\beta\)-Preservation]
\label{lemma:beta-preservation}
Assume the expression \(\metavariable{e}\) is \textbf{syntactically well-typed}, i.e. \(\emptyset \vdash \metavariable{e} : \metavariable{\tau}\) for some type \(\metavariable{\tau}\). Then forall \(\metavariable{e'}\) with \(\metavariable{e} \rightarrow_{\beta} \metavariable{e'}\) it holds that \(\emptyset \vdash \metavariable{e'} : \metavariable{\tau}\) as well.
\begin{proof}
\todo{}
\end{proof}
\end{lemma}
\begin{lemma}[\(\delta\)-Preservation]
\label{lemma:delta-preservation}
\begin{proof}
\todo{}
\end{proof}
\end{lemma}
\begin{lemma}[Preservation]
\label{lemma:preservation}
Assume the expression \(\metavariable{e}\) is well typed, i.e. \(\emptyset \vdash \metavariable{e} : \metavariable{\tau}\) for some type \(\metavariable{\tau}\). Then forall \(\metavariable{e'}\) with \(\metavariable{e} \rightarrow_{eval} \metavariable{e'}\) it holds that \(\emptyset \vdash \metavariable{e'} : \metavariable{\tau}\) as well.
\begin{proof}
\todo{}
\end{proof}
\end{lemma}
\begin{lemma}[Progress] \begin{lemma}[Progress]
\label{lemma:progress} \label{lemma:progress}
If \(\emptyset \vdash \metavariable{e} : \metavariable{\tau}\), then either \(\metavariable{e}\) is a value or there exists some \(\metavariable{e'}\) such that \(\metavariable{e} \rightarrow_{eval} \metavariable{e'}\) If \(\emptyset \vdash \metavariable{e} : \metavariable{\tau}\), then either \(\metavariable{e}\) is a value or there exists some \(\metavariable{e'}\) such that \(\metavariable{e} \rightarrow_{eval} \metavariable{e'}\)
\begin{proof} \begin{proof}
\todo{} \todo{}
\end{proof} \end{proof}
\end{lemma} \end{lemma}
\begin{theorem}[Soundness]
If \(\emptyset \vdash \metavariable{e}:\approx\metavariable{\tau}\), then it never occurs that \(\metavariable{e} \rightarrow_{eval}^{*} \metavariable{e'}\) where \metavariable{e'} is in normal form but not a value. \begin{lemma}[Preservation]
\label{lemma:preservation}
\begin{proof}
\todo{}
\end{proof}
\end{lemma}
\begin{theorem}[Type Soundness]
If \(\emptyset \vdash \metavariable{e}:\metavariable{\tau}\), then it never occurs that \(\metavariable{e} \rightarrow_{eval}^{*} \metavariable{e'}\) where \metavariable{e'} is in normal form but not a value.
\begin{proof} \begin{proof}
By \ref{lemma:}
Follows from \ref{lemma:progress} and \ref{lemma:preservation}. Follows from \ref{lemma:progress} and \ref{lemma:preservation}.
\end{proof} \end{proof}
\end{theorem} \end{theorem}