56 lines
988 B
Coq
56 lines
988 B
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 well typed term is not stuck *)
|
|
Lemma progress :
|
|
forall (e:expr_term),
|
|
(is_well_typed e) -> ~(is_stuck e)
|
|
.
|
|
Proof.
|
|
|
|
Admitted.
|
|
|
|
(* reduction step preserves well-typedness *)
|
|
Lemma preservation :
|
|
forall Γ e e' τ,
|
|
(Γ |- e \is τ) ->
|
|
(e -->β e') ->
|
|
(Γ |- e' \is τ)
|
|
.
|
|
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.
|
|
|