Commit 56cbb5ac authored by Amin Timany's avatar Amin Timany

Prove type soundness for Fμ

parent ac10cd49
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 F_mu.lang F_mu.typing F_mu.rules F_mu.logrel F_mu.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 expr _) by reflexivity.
asimpl; trivial.
Qed.
Definition free_type_context : leibniz_var -n> leibniz_val -n> iProp lang Σ :=
{|
cofe_mor_car :=
λ x,
{|
cofe_mor_car :=
λ y, (True)%I
|}
|}.
Global Instance free_context_interp_Persistent :
context_interp_Persistent free_type_context.
Proof. intros x v; apply const_persistent. Qed.
Lemma wp_soundness e τ
: typed [] e τ True WP e {{@interp Σ τ free_type_context}}.
Proof.
iIntros {H} "".
rewrite -(empty_env_subst e).
iPoseProof (@typed_interp _ _ _ []) as "Hi"; eauto; try typeclasses eauto.
iApply "Hi"; 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.
eapply wp_soundness in H1; eauto.
edestruct(@wp_adequacy_reducible lang Σ (interp τ free_type_context)
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
......@@ -11,6 +11,7 @@ F_mu/typing.v
F_mu/rules.v
F_mu/logrel.v
F_mu/fundamental.v
F_mu/soundness.v
F_mu_ref/lang.v
F_mu_ref/typing.v
F_mu_ref/rules.v
......
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