From b31c8abc6c4a0f890dd10c89c5711aa485b29470 Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Wed, 4 Sep 2024 12:41:17 +0200 Subject: [PATCH] initial definition of soundness theorems --- coq/_CoqProject | 2 +- coq/soundness.v | 83 +++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 84 insertions(+), 1 deletion(-) create mode 100644 coq/soundness.v diff --git a/coq/_CoqProject b/coq/_CoqProject index f4fd193..48aa4ab 100644 --- a/coq/_CoqProject +++ b/coq/_CoqProject @@ -6,5 +6,5 @@ subtype.v typing.v morph.v smallstep.v +soundness.v bbencode.v - diff --git a/coq/soundness.v b/coq/soundness.v new file mode 100644 index 0000000..4547e6f --- /dev/null +++ b/coq/soundness.v @@ -0,0 +1,83 @@ +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. +