soundness.v 858 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 7 8 9 10 11
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.
  iIntros (?). rewrite -(empty_env_subst e).
  iApply fundamental; eauto. iApply interp_env_nil.
Qed.

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