Commit d4d61110 authored by Robbert Krebbers's avatar Robbert Krebbers

Use consistent meta variables for `wp_invariance`.

parent 8cc7110c
Pipeline #17584 passed with stage
in 13 minutes and 46 seconds
...@@ -209,15 +209,15 @@ Proof. ...@@ -209,15 +209,15 @@ Proof.
iIntros (v2 t2'' [= -> <-]). by rewrite to_of_val. iIntros (v2 t2'' [= -> <-]). by rewrite to_of_val.
Qed. Qed.
Corollary wp_invariance Σ Λ `{!invPreG Σ} s e σ1 t2 σ2 φ : Corollary wp_invariance Σ Λ `{!invPreG Σ} s e1 σ1 t2 σ2 φ :
( `{Hinv : !invG Σ} κs, ( `{Hinv : !invG Σ} κs,
(|={}=> (|={}=>
(stateI : state Λ list (observation Λ) nat iProp Σ) (stateI : state Λ list (observation Λ) nat iProp Σ)
(fork_post : val Λ iProp Σ), (fork_post : val Λ iProp Σ),
let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in
stateI σ1 κs 0 WP e @ s; {{ _, True }} stateI σ1 κs 0 WP e1 @ s; {{ _, True }}
(stateI σ2 [] (pred (length t2)) - E, |={,E}=> ⌜φ⌝))%I) (stateI σ2 [] (pred (length t2)) - E, |={,E}=> ⌜φ⌝))%I)
rtc erased_step ([e], σ1) (t2, σ2) rtc erased_step ([e1], σ1) (t2, σ2)
φ. φ.
Proof. Proof.
intros Hwp [n [κs ?]]%erased_steps_nsteps. intros Hwp [n [κs ?]]%erased_steps_nsteps.
......
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