soundness.v 1.02 KB
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
From iris.proofmode Require Import tactics.
From iris.program_logic Require Import adequacy.

Theorem soundness Σ `{invPreG Σ} e τ e' thp σ σ' :
  ( `{irisG F_mu_lang Σ}, []  e : τ) 
Ralf Jung's avatar
Ralf Jung committed
7
  rtc erased_step ([e], σ) (thp, σ')  e'  thp 
Amin Timany's avatar
Amin Timany committed
8 9
  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
  eapply (wp_adequacy Σ); eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
12
  iIntros (Hinv ?). iModIntro. iExists (λ _ _, True%I), (λ _, True%I). iSplit=> //.
Amin Timany's avatar
Amin Timany committed
13
  replace e with e.[env_subst[]] by by asimpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
14
  set (HΣ := IrisG _ _ Hinv (λ _ _ _, True)%I (λ _, True)%I).
Amin Timany's avatar
Amin Timany committed
15 16 17 18 19
  iApply (wp_wand with "[]"). iApply Hlog; eauto. by iApply interp_env_nil. auto.
Qed.

Corollary type_soundness e τ e' thp σ σ' :
  []  e : τ 
Ralf Jung's avatar
Ralf Jung committed
20
  rtc erased_step ([e], σ) (thp, σ')  e'  thp 
Amin Timany's avatar
Amin Timany committed
21 22 23 24 25
  is_Some (to_val e')  reducible e' σ'.
Proof.
  intros ??. set (Σ := invΣ).
  eapply (soundness Σ); eauto using fundamental.
Qed.