soundness.v 976 Bytes
Newer Older
Amin Timany's avatar
Amin Timany committed
1
From iris_examples.logrel.F_mu Require Export fundamental.
Amin Timany's avatar
Amin Timany committed
2 3 4 5 6 7 8 9
From iris.proofmode Require Import tactics.
From iris.program_logic Require Import adequacy.

Theorem soundness Σ `{invPreG Σ} e τ e' thp σ σ' :
  ( `{irisG F_mu_lang Σ}, []  e : τ) 
  rtc step ([e], σ) (thp, σ')  e'  thp 
  is_Some (to_val e')  reducible e' σ'.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
10
  intros Hlog ??. cut (adequate NotStuck e σ (λ _ _, True)); first (intros [_ ?]; eauto).
Amin Timany's avatar
Amin Timany committed
11 12 13 14 15 16 17 18 19 20 21 22 23 24 25
  eapply (wp_adequacy Σ); eauto.
  iIntros (Hinv). iModIntro. iExists (λ _, True%I). iSplit=> //.
  rewrite -(empty_env_subst e).
  set (HΣ := IrisG _ _ Hinv (λ _, True)%I).
  iApply (wp_wand with "[]"). iApply Hlog; eauto. by iApply interp_env_nil. auto.
Qed.

Corollary type_soundness e τ e' thp σ σ' :
  []  e : τ 
  rtc step ([e], σ) (thp, σ')  e'  thp 
  is_Some (to_val e')  reducible e' σ'.
Proof.
  intros ??. set (Σ := invΣ).
  eapply (soundness Σ); eauto using fundamental.
Qed.