Commit ac10cd49 authored by Amin Timany's avatar Amin Timany

Prove type soundness for stlc

parent b24e3d95
......@@ -5,6 +5,7 @@ stlc/typing.v
stlc/rules.v
stlc/logrel.v
stlc/fundamental.v
stlc/soundness.v
F_mu/lang.v
F_mu/typing.v
F_mu/rules.v
......
......@@ -31,15 +31,14 @@ Section typed_interp.
--------------------------------------
(_ _)) => iSplit
end : itauto.
Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) constr(Hp) :=
iApply (@wp_bind _ _ _ [ctx]);
iApply wp_impl_l;
iSplit; [| iApply Hp; trivial]; cbn;
eapply (@always_intro _ _ _ _);
iIntros {v} Hv.
Local Ltac value_case := iApply wp_value; cbn; rewrite ?to_of_val; trivial.
Lemma typed_interp Γ vs e τ :
......@@ -97,4 +96,4 @@ Section typed_interp.
iApply "Hv"; auto with itauto.
Qed.
End typed_interp.
End typed_interp.
\ No newline at end of file
Require Import iris.proofmode.tactics.
Require Import iris.program_logic.hoare.
Require Import iris.program_logic.lifting.
Require Import iris.algebra.upred_big_op.
Require Import stlc.lang stlc.typing stlc.rules stlc.logrel stlc.fundamental.
Require Import iris.program_logic.adequacy.
Import uPred.
Section Soundness.
Context {Σ : iFunctor}.
Lemma empty_env_subst e : e.[env_subst []] = e.
replace (env_subst []) with (ids) by reflexivity.
asimpl; trivial.
Qed.
Lemma wp_soundness e τ : typed [] e τ True WP e {{@interp Σ τ}}.
Proof.
iIntros {H} "".
rewrite -(empty_env_subst e).
iApply typed_interp; eauto.
Qed.
Theorem Soundness e τ :
typed [] e τ
e' thp, rtc step ([e], tt) (e' :: thp, tt)
¬ reducible e' tt is_Some (to_val e').
Proof.
intros H1 e' thp Hstp Hnr.
apply wp_soundness in H1.
edestruct(@wp_adequacy_reducible lang Σ (interp τ) e e' (e' :: thp) tt )
as [Ha|Ha]; eauto using cmra_unit_valid; try tauto.
- iIntros "H". iApply H1.
- constructor.
Qed.
End Soundness.
\ No newline at end of file
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment