Commit 3803dc19 authored by David Swasey's avatar David Swasey

Incorporate minor feedback from Ralf.

Pull progress bit out of the WP fixpoint,
make (most) wp adequacy notation only parsing, and
generalize forget_progress.
parent 34b93f99
......@@ -65,11 +65,11 @@ Implicit Types P Q : iProp Σ.
Implicit Types Φ : val Λ iProp Σ.
Implicit Types Φs : list (val Λ iProp Σ).
Notation world' E σ := (wsat ownE E state_interp σ)%I.
Notation world σ := (world' σ).
Notation world' E σ := (wsat ownE E state_interp σ)%I (only parsing).
Notation world σ := (world' σ) (only parsing).
Notation wp' E e Φ := (WP e @ p; E {{ Φ }})%I.
Notation wp e Φ := (wp' e Φ).
Notation wp' E e Φ := (WP e @ p; E {{ Φ }})%I (only parsing).
Notation wp e Φ := (wp' e Φ) (only parsing).
Notation wptp t := ([ list] ef t, WP ef @ p; {{ _, True }})%I.
Lemma wp_step E e1 σ1 e2 σ2 efs Φ :
......
......@@ -108,8 +108,8 @@ Proof.
iIntros (v) "Hv". by iApply "HwpK".
Qed.
Lemma ht_forget_progress E P Φ e :
{{ P }} e @ E {{ Φ }} {{ P }} e @ E ?{{ Φ }}.
Lemma ht_forget_progress p E P Φ e :
{{ P }} e @ p; E {{ Φ }} {{ P }} e @ E ?{{ Φ }}.
Proof.
by iIntros "#Hwp !# ?"; iApply wp_forget_progress; iApply "Hwp".
Qed.
......
......@@ -11,26 +11,26 @@ Class irisG' (Λstate : Type) (Σ : gFunctors) := IrisG {
}.
Notation irisG Λ Σ := (irisG' (state Λ) Σ).
Definition wp_pre `{irisG Λ Σ}
(wp : bool -c> coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) :
bool -c> coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ p E e1 Φ,
Definition wp_pre `{irisG Λ Σ} (p : bool)
(wp : coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) :
coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ E e1 Φ,
match to_val e1 with
| Some v => |={E}=> Φ v
| None => σ1,
state_interp σ1 ={E,}= if p then reducible e1 σ1 else True
e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs ={,E}=
state_interp σ2 wp p E e2 Φ
[ list] ef efs, wp p ef (λ _, True)
state_interp σ2 wp E e2 Φ
[ list] ef efs, wp ef (λ _, True)
end%I.
Local Instance wp_pre_contractive `{irisG Λ Σ} : Contractive wp_pre.
Local Instance wp_pre_contractive `{irisG Λ Σ} p : Contractive (wp_pre p).
Proof.
rewrite /wp_pre=> n wp wp' Hwp p E e1 Φ.
rewrite /wp_pre=> n wp wp' Hwp E e1 Φ.
repeat (f_contractive || f_equiv); apply Hwp.
Qed.
Definition wp_def `{irisG Λ Σ} :
bool coPset expr Λ (val Λ iProp Σ) iProp Σ := fixpoint wp_pre.
Definition wp_def `{irisG Λ Σ} p :
coPset expr Λ (val Λ iProp Σ) iProp Σ := fixpoint (wp_pre p).
Definition wp_aux : seal (@wp_def). by eexists. Qed.
Definition wp := unseal wp_aux.
Definition wp_eq : @wp = @wp_def := seal_eq wp_aux.
......@@ -172,8 +172,8 @@ Implicit Types v : val Λ.
Implicit Types e : expr Λ.
(* Weakest pre *)
Lemma wp_unfold p E e Φ : WP e @ p; E {{ Φ }} wp_pre wp p E e Φ.
Proof. rewrite wp_eq. apply (fixpoint_unfold wp_pre). Qed.
Lemma wp_unfold p E e Φ : WP e @ p; E {{ Φ }} wp_pre p (wp p) E e Φ.
Proof. rewrite wp_eq. apply (fixpoint_unfold (wp_pre p)). Qed.
Global Instance wp_ne p E e n :
Proper (pointwise_relation _ (dist n) ==> dist n) (@wp Λ Σ _ p E e).
......@@ -210,7 +210,8 @@ Proof.
iMod "Hclose" as "_". by iApply ("IH" with "HΦ").
Qed.
Lemma wp_forget_progress E e Φ : WP e @ E {{ Φ }} WP e @ E ?{{ Φ }}.
Lemma wp_forget_progress p E e Φ :
WP e @ p; E {{ Φ }} WP e @ E ?{{ Φ }}.
Proof.
iIntros "H". iLöb as "IH" forall (E e Φ). rewrite !wp_unfold /wp_pre.
destruct (to_val e) as [v|]; first iExact "H".
......
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