83 lines
1.4 KiB
Coq
83 lines
1.4 KiB
Coq
From Coq Require Import Strings.String.
|
|
Require Import terms.
|
|
Require Import subst.
|
|
Require Import equiv.
|
|
Require Import subtype.
|
|
Require Import smallstep.
|
|
Require Import typing.
|
|
|
|
Include Terms.
|
|
Include Subst.
|
|
Include Equiv.
|
|
Include Subtype.
|
|
Include Smallstep.
|
|
Include Typing.
|
|
|
|
|
|
Module Soundness.
|
|
|
|
(* e is stuck when it is neither a value, nor can it be reduced *)
|
|
Definition is_stuck (e:expr_term) : Prop :=
|
|
~(is_value e) ->
|
|
~(exists e', e -->β e')
|
|
.
|
|
|
|
(* every exactly typed term is not stuck *)
|
|
Lemma exact_progress :
|
|
forall (e:expr_term),
|
|
(is_exactly_typed e) -> ~(is_stuck e)
|
|
.
|
|
Proof.
|
|
|
|
Admitted.
|
|
|
|
(* every well typed term is not stuck *)
|
|
Lemma progress :
|
|
forall (e:expr_term),
|
|
(is_well_typed e) -> ~(is_stuck e)
|
|
.
|
|
Proof.
|
|
|
|
Admitted.
|
|
|
|
(* reduction step preserves the type *)
|
|
Lemma exact_preservation :
|
|
forall Γ e e' τ,
|
|
(Γ |- e \is τ) ->
|
|
(e -->β e') ->
|
|
(Γ |- e' \is τ)
|
|
.
|
|
Proof.
|
|
(*
|
|
intros.
|
|
generalize dependent e'.
|
|
induction H.
|
|
intros e' I.
|
|
inversion I.
|
|
*)
|
|
Admitted.
|
|
|
|
|
|
(* reduction step preserves well-typedness *)
|
|
Lemma preservation :
|
|
forall Γ e e' τ,
|
|
(Γ |- e \compatible τ) ->
|
|
(e -->β e') ->
|
|
(Γ |- e' \compatible τ)
|
|
.
|
|
Proof.
|
|
Admitted.
|
|
|
|
(* every well-typed expression can be reduced to a value *)
|
|
Theorem soundness :
|
|
forall (e:expr_term),
|
|
(is_well_typed e) ->
|
|
(exists e', e -->β* e' /\ (is_value e'))
|
|
.
|
|
Proof.
|
|
intros.
|
|
|
|
Admitted.
|
|
|
|
End Soundness.
|
|
|