soundness.v 891 Bytes
Newer Older
Amin Timany's avatar
Amin Timany committed
1
From iris_examples.logrel.stlc 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.

Lemma wp_soundness `{irisG stlc_lang Σ} e τ : []  e : τ  (WP e {{  τ  }})%I.
Proof.
Amin Timany's avatar
Amin Timany committed
7 8
  iIntros (?).
  replace e with e.[env_subst[]] by by asimpl.
Amin Timany's avatar
Amin Timany committed
9 10 11 12
  iApply fundamental; eauto. iApply interp_env_nil.
Qed.

Theorem soundness e τ e' thp :
Ralf Jung's avatar
Ralf Jung committed
13
  []  e : τ  rtc erased_step ([e], ()) (thp, ())  e'  thp 
Amin Timany's avatar
Amin Timany committed
14 15 16
  is_Some (to_val e')  reducible e' ().
Proof.
  set (Σ := invΣ). intros.
Robbert Krebbers's avatar
Robbert Krebbers committed
17
  cut (adequate NotStuck e () (λ _ _, True)); first (intros [_ Hsafe]; eauto).
Ralf Jung's avatar
Ralf Jung committed
18
  eapply (wp_adequacy Σ _). iIntros (Hinv ?).
Robbert Krebbers's avatar
Robbert Krebbers committed
19
  iModIntro. iExists (λ _ _, True%I), (λ _, True%I). iSplit=>//.
Robbert Krebbers's avatar
Robbert Krebbers committed
20
  set (HΣ := IrisG _ _ Hinv (λ _ _ _, True)%I (λ _, True)%I).
Amin Timany's avatar
Amin Timany committed
21 22 23
  iApply (wp_wand with "[]"). by iApply wp_soundness. eauto.
Qed.