From 61819129615a340975307c83dd12f2fe99ee9fcd Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Sat, 27 Oct 2018 15:43:04 +0200
Subject: [PATCH] bump iris
---
opam | 2 +-
theories/examples/repeat.v | 3 +-
theories/lang.v | 2 +-
theories/lang/ra_lang.v | 14 ++---
theories/lang/surface.v | 6 +-
theories/lifting.v | 108 ++++++++++++++++--------------------
theories/lifting_vProp.v | 28 +++++-----
theories/tactics.v | 4 +-
theories/weakestpre.v | 8 ++-
theories/wp_tactics.v | 6 +-
theories/wp_tactics_vProp.v | 40 +++++++------
11 files changed, 109 insertions(+), 112 deletions(-)
diff --git a/opam b/opam
index c5a7746a..61cdb5ef 100644
--- a/opam
+++ b/opam
@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/igps" ]
depends: [
- "coq-iris" { (= "dev.2018-10-05.4.464c2449") | (= "dev") }
+ "coq-iris" { (= "dev.2018-10-22.2.46e20e91") | (= "dev") }
]
diff --git a/theories/examples/repeat.v b/theories/examples/repeat.v
index b682d818..6d9f1495 100644
--- a/theories/examples/repeat.v
+++ b/theories/examples/repeat.v
@@ -24,6 +24,5 @@ Proof.
iIntros (v) "H". iDestruct "H" as (l) "(% & R)".
rewrite /= H0 /= {H0}.
wp_lam.
- case HD: (bool_decide _);
- wp_op; rewrite HD; [by wp_if_true|by wp_if_false].
+ case HD: (bool_decide _); wp_op; rewrite HD; [by wp_if_true|by wp_if_false].
Qed.
diff --git a/theories/lang.v b/theories/lang.v
index 916b5814..9a4329d7 100644
--- a/theories/lang.v
+++ b/theories/lang.v
@@ -25,7 +25,7 @@ Proof.
by rewrite IHK.
Qed.
-Lemma prim_step_view_mono e V1 σ1 e2 V2 σ2 efs : ectx_language.prim_step (Λ:=ra_lang.ra_ectx_lang) (e, V1) σ1 (e2, V2) σ2 efs → V1 ⊑ V2.
+Lemma prim_step_view_mono e V1 σ1 κs e2 V2 σ2 efs : ectx_language.prim_step (Λ:=ra_lang.ra_ectx_lang) (e, V1) σ1 κs (e2, V2) σ2 efs → V1 ⊑ V2.
Proof.
destruct 1. destruct e1', e2'.
cbn in *.
diff --git a/theories/lang/ra_lang.v b/theories/lang/ra_lang.v
index fd9dc005..8dd5b478 100644
--- a/theories/lang/ra_lang.v
+++ b/theories/lang/ra_lang.v
@@ -91,13 +91,13 @@ Inductive step (V : View)
.
Inductive head_step :
-∀ (e : expr) (σ : state) (e' : expr) (σ' : state) (ef : list expr), Prop :=
+∀ (e : expr) (σ : state) (κs: list Empty_set) (e' : expr) (σ' : state) (ef : list expr), Prop :=
| pure_step σ π e e' (BaseStep : base.head_step e e')
- : head_step (e, π) σ (e', π) σ []
+ : head_step (e, π) σ [] (e', π) σ []
| impure_step σ σ' V V' e e' ef evt
(ExprStep : step V e evt e' ef)
(MachStep : machine_red σ evt V σ' V')
- : head_step (e, V) σ (e', V') σ' ef
+ : head_step (e, V) σ [] (e', V') σ' ef
.
Lemma to_of_val v : to_val (of_val v) = Some v.
@@ -109,7 +109,7 @@ Proof.
move => [<- <-]. f_equal. exact: base.of_to_val.
Qed.
-Lemma val_stuck σ1 e1 σ2 e2 ef : head_step e1 σ1 e2 σ2 ef → to_val e1 = None.
+Lemma val_stuck σ1 e1 κs σ2 e2 ef : head_step e1 σ1 κs e2 σ2 ef → to_val e1 = None.
Proof.
inversion 1; subst; last inversion ExprStep;
first (cbv -[base.to_val]; by erewrite base.val_stuck; last eassumption);
@@ -130,8 +130,8 @@ Proof.
exact: base.fill_item_no_val_inj H1 H2 H3.
Qed.
-Lemma head_ctx_step_val Ki e σ e2 σ2 ef :
- head_step (fill_item Ki e) σ e2 σ2 ef → is_Some (to_val e).
+Lemma head_ctx_step_val Ki e σ κs e2 σ2 ef :
+ head_step (fill_item Ki e) σ κs e2 σ2 ef → is_Some (to_val e).
Proof.
inversion 1; subst; last inversion ExprStep; subst; simplify_option_eq;
first
@@ -178,7 +178,7 @@ Proof. intros. destruct e. cbv -[base.subst]. f_equal. exact: base.is_closed_nil
Lemma is_closed_of_val X v : is_closed X (of_val v).
Proof. exact: base.is_closed_of_val. Qed.
-Lemma head_step_mono e1 V1 σ1 e2 V2 σ2 efs : head_step (e1, V1) σ1 (e2, V2) σ2 efs → V1 ⊑ V2.
+Lemma head_step_mono e1 V1 σ1 κs e2 V2 σ2 efs : head_step (e1, V1) σ1 κs (e2, V2) σ2 efs → V1 ⊑ V2.
Proof.
inversion 1; subst; first done.
exact: machine_red_mono.
diff --git a/theories/lang/surface.v b/theories/lang/surface.v
index 192e7af8..4b8181cf 100644
--- a/theories/lang/surface.v
+++ b/theories/lang/surface.v
@@ -7,8 +7,8 @@ From igps.lang Require base ra_lang.
Import base.
-Definition head_step e1 σ1 e2 σ2 efs :=
- ra_lang.head_step (e1, fst σ1) (snd σ1) (e2, fst σ2) (snd σ2) (map (fun e => (e, fst σ2)) efs).
+Definition head_step e1 σ1 κs e2 σ2 efs :=
+ ra_lang.head_step (e1, fst σ1) (snd σ1) κs (e2, fst σ2) (snd σ2) (map (fun e => (e, fst σ2)) efs).
(** Language *)
Lemma surface_ectxi_language_mixin :
@@ -22,7 +22,7 @@ Proof.
- intros. destruct σ1 as [V1 σ1]. destruct σ2 as [V2 σ2]. cbn in H.
cut (ra_lang.to_val (e1, V1) = None).
+ cbn. by rewrite fmap_None.
- + refine (ectxi_language.mixin_val_stuck _ _ _ _ _ _ _ _ _ _ H).
+ + refine (ectxi_language.mixin_val_stuck _ _ _ _ _ _ _ _ _ _ _ H).
exact ra_lang.ra_ectxi_language_mixin. (* ???? *)
- intros.
cut (Inj eq eq (ra_lang.fill_item Ki)).
diff --git a/theories/lifting.v b/theories/lifting.v
index 915248cc..0be8e257 100644
--- a/theories/lifting.v
+++ b/theories/lifting.v
@@ -20,13 +20,13 @@ Implicit Types Φ : ra_lang.val → iProp Σ.
Implicit Types ef : option (ra_lang.expr).
(** Hot fix for fork *)
-Definition atomic' e := ∀ σ1 e2 σ2 efs, prim_step (Λ:=ra_ectx_lang) e σ1 e2 σ2 efs → is_Some (to_val e2).
+Definition atomic' e := ∀ σ1 κs e2 σ2 efs, prim_step (Λ:=ra_ectx_lang) e σ1 κs e2 σ2 efs → is_Some (to_val e2).
Lemma wp_lift_atomic_step2 {E Φ} e1 σ1 :
atomic' e1 →
reducible e1 σ1 →
▷ ownP σ1 ∗
- ▷ (∀ v2 σ2 efs,
- ⌜prim_step e1 σ1 (of_val v2) σ2 efs⌠∧ ownP σ2 -∗
+ ▷ (∀ κs v2 σ2 efs,
+ ⌜prim_step e1 σ1 κs (of_val v2) σ2 efs⌠∧ ownP σ2 -∗
|==> (|={E}=> Φ v2) ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
⊢ WP e1 @ E {{ Φ }}.
Proof.
@@ -34,9 +34,9 @@ Proof.
iApply (ownP_lift_step _ E _ e1).
iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver+. iModIntro.
iExists σ1. iFrame "Hσ"; iSplit; eauto.
- iNext; iIntros (e2 σ2 efs) "% oP".
- edestruct (Hatomic σ1 e2 σ2 efs) as [v2 <-%of_to_val]; eauto.
- iDestruct ("H" $! v2 σ2 efs with "[$oP]") as ">[HΦ $]"; first by auto.
+ iNext; iIntros (κs e2 σ2 efs) "% oP".
+ edestruct (Hatomic σ1 κs e2 σ2 efs) as [v2 <-%of_to_val]; eauto.
+ iDestruct ("H" $! _ v2 σ2 efs with "[$oP]") as ">[HΦ $]"; first by auto.
iMod "Hclose". iMod "HΦ". iApply wp_value; eauto.
exact: of_to_val.
Qed.
@@ -45,15 +45,15 @@ Lemma wp_lift_atomic_head_step2 {E Φ} e1 σ1 :
atomic' e1 →
head_reducible e1 σ1 →
▷ ownP σ1 ∗
- ▷ (∀ v2 σ2 efs,
- ⌜ectx_language.head_step e1 σ1 (of_val v2) σ2 efs⌠∧ ownP σ2 -∗
+ ▷ (∀ κs v2 σ2 efs,
+ ⌜ectx_language.head_step e1 σ1 κs (of_val v2) σ2 efs⌠∧ ownP σ2 -∗
|==> (|={E}=> Φ v2) ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
⊢ WP e1 @ E {{ Φ }}.
Proof.
iIntros (??) "[? H]". iApply wp_lift_atomic_step2; eauto.
- by eapply head_prim_reducible.
- iFrame. iNext.
- iIntros (???) "[% ?]". iApply "H". iFrame.
+ iIntros (????) "[% ?]". iApply "H". iFrame.
iPureIntro. by apply head_reducible_prim_step.
Qed.
@@ -233,18 +233,18 @@ Proof.
have ? := (wp_fork_help H). subst; simpl in *; simplify_eq.
inversion Step; simplify_eq;
[inversion BaseStep|inversion ExprStep]; simplify_eq; eauto.
- - eexists _, σ, _.
+ - eexists _, _, σ, _.
eright.
+ by econstructor.
+ by eright.
- iSplitL "HP"; first by [].
- iNext. iIntros "% % % [% HP]". destruct a.
+ iNext. iIntros (κs v2 σ2 efs) "[% HP]". destruct v2.
inversion H; [by inversion BaseStep|inversion ExprStep].
- assert (Inv' : phys_inv a0) by exact: (proj1 (machine_red_safe _ _ _)).
+ assert (Inv' : phys_inv σ2) by exact: (proj1 (machine_red_safe _ _ _)).
inversion MachStep; subst; first by inversion ThreadRed. simpl.
destruct v; try discriminate.
destruct l; try discriminate.
- inversion H10. simplify_eq.
+ inversion H11. simplify_eq.
iDestruct ("HΦ" with "[$HP]") as ">[$ $]"; last done.
iFrame (Inv'). iSplit; [|iSplit]; iPureIntro.
+ inversion FRed; subst. by destruct (machine_red_safe Inv VOk MachStep).
@@ -340,7 +340,7 @@ Proof.
move: (VOk _ _ Local0) => [m [In [EqLoc [EqTime SubView]]]].
assert (IsVal := initialized_reads_value _ _ _ Init m In EqLoc EqTime).
case HVal: (mval m) => [| |v]; try (by rewrite HVal in IsVal; inversion IsVal).
- eexists.
+ eexists. eexists.
exists σ.
econstructor. eright; first by constructor.
econstructor; try eauto.
@@ -351,10 +351,9 @@ Proof.
eapply proof => //.
intros. by exists tl.
- iSplitL "HP"; first by [].
- iNext. iIntros "% % % % HP". destruct a.
- match goal with | [H : ectx_language.head_step _ _ _ _ _ |- _ ] => inversion H end;
- [by inversion BaseStep|inversion ExprStep].
- assert (Inv' : phys_inv a0) by exact: (proj1 (machine_red_safe _ _ _)).
+ iNext. iIntros (κ e2 σ2 efs STEP) "HP".
+ inversion STEP; [by inversion BaseStep|inversion ExprStep].
+ assert (Inv' : phys_inv σ2) by exact: (proj1 (machine_red_safe _ _ _)).
inversion MachStep; last by (subst; discriminate).
subst. iSplit; last by rewrite big_opL_nil.
inversion ThreadRed. subst.
@@ -386,8 +385,7 @@ Proof.
assert (IsVal := initialized_reads_value _ _ _ Init m In EqLoc EqTime).
case Hmv: (mval m) => [| |v];
try (by rewrite Hmv in IsVal; inversion IsVal).
- eexists.
- exists σ.
+ do 2 eexists. exists σ.
econstructor. eright; first by constructor.
econstructor; try eauto.
+ move => ? [<-]. by econstructor.
@@ -396,10 +394,9 @@ Proof.
rewrite -> Hmv, EqTime, EqLoc in proof.
eapply proof => //. exists tl => //.
- iSplitL "HP"; first by [].
- iNext. iIntros "% % % % HP". destruct a.
- match goal with | [H : ectx_language.head_step _ _ _ _ _ |- _ ] => inversion H end;
- [by inversion BaseStep|inversion ExprStep].
- assert (Inv' : phys_inv a0) by exact: (proj1 (machine_red_safe _ _ _)).
+ iNext. iIntros (κ e2 σ2 efs STEP) "HP".
+ inversion STEP; [by inversion BaseStep|inversion ExprStep].
+ assert (Inv' : phys_inv σ2) by exact: (proj1 (machine_red_safe _ _ _)).
inversion MachStep; last by (subst; discriminate).
subst. iSplit; last by rewrite big_opL_nil.
inversion ThreadRed. subst.
@@ -462,18 +459,16 @@ Proof.
eapply Pos.le_lt_trans; last by apply Pos.lt_add_r.
by apply tMax, elem_of_hist. }
- eexists.
- exists (mkState (add_ins (mem σ) m Disj) (nats σ)).
+ do 2 eexists. exists (mkState (add_ins (mem σ) m Disj) (nats σ)).
econstructor. eright; first by constructor.
econstructor; try eauto => //.
+ move => ? [<-]. by econstructor.
+ econstructor => //. by rewrite -Local0.
+ simpl. econstructor; eauto.
- iSplitL "HP"; first by [].
- iNext. iIntros "% % % % HP". destruct a as [v' π'].
- match goal with | [H : ectx_language.head_step _ _ _ _ _ |- _ ] => inversion H end;
- [by inversion BaseStep|inversion ExprStep].
- assert (Inv' : phys_inv a0) by exact: (proj1 (machine_red_safe _ _ _)).
+ iNext. iIntros (κ e2 σ2 efs STEP) "HP".
+ inversion STEP; [by inversion BaseStep|inversion ExprStep].
+ assert (Inv' : phys_inv σ2) by exact: (proj1 (machine_red_safe _ _ _)).
inversion MachStep; last by (subst; discriminate).
subst. iSplit; last by rewrite big_opL_nil.
inversion ThreadRed. subst. simplify_option_eq.
@@ -533,9 +528,8 @@ Proof.
eapply Pos.le_lt_trans; last by apply Pos.lt_add_r.
by apply tMax, elem_of_hist. }
- eexists.
- exists (mkState (add_ins (mem σ) m Disj)
- (<[l:= mtime m]> (nats σ))).
+ do 2 eexists.
+ exists (mkState (add_ins (mem σ) m Disj) (<[l:= mtime m]> (nats σ))).
econstructor. eright; first by constructor.
econstructor; try eauto => //.
+ move => ? [<-]. by econstructor.
@@ -549,10 +543,9 @@ Proof.
by apply tMax, elem_of_hist.
+ by econstructor.
- iSplitL "HP"; first by [].
- iNext. iIntros "% % % % HP". destruct a as [v' π'].
- match goal with | [H : ectx_language.head_step _ _ _ _ _ |- _ ] => inversion H end;
- [by inversion BaseStep|inversion ExprStep].
- assert (Inv' : phys_inv a0) by exact: (proj1 (machine_red_safe _ _ _)).
+ iNext. iIntros (κ e2 σ2 efs STEP) "HP".
+ inversion STEP; [by inversion BaseStep|inversion ExprStep].
+ assert (Inv' : phys_inv σ2) by exact: (proj1 (machine_red_safe _ _ _)).
inversion MachStep; last by (subst; discriminate).
subst. iSplit; last by rewrite big_opL_nil.
inversion ThreadRed. subst. simplify_option_eq.
@@ -610,9 +603,8 @@ Proof.
{ rewrite Local0 -EqTime.
eapply Pos.le_lt_trans; last by apply Pos.lt_add_r.
by apply tMax, elem_of_hist. }
- eexists.
- exists (mkState (add_ins (mem σ) m Disj)
- (<[l:=mtime m]> (nats σ))).
+ do 2 eexists.
+ exists (mkState (add_ins (mem σ) m Disj) (<[l:=mtime m]> (nats σ))).
econstructor. eright; first by constructor.
econstructor; try eauto => //.
+ move => ? [<-]. by econstructor.
@@ -626,10 +618,9 @@ Proof.
by apply tMax, elem_of_hist.
+ by econstructor.
- iSplitL "HP"; first by [].
- iNext. iIntros "% % % % HP". destruct a as [v' π'].
- match goal with | [H : ectx_language.head_step _ _ _ _ _ |- _ ] => inversion H end;
- [by inversion BaseStep|inversion ExprStep]. subst.
- assert (Inv' : phys_inv a0) by exact: (proj1 (machine_red_safe _ _ _)).
+ iNext. iIntros (κ e2 σ2 efs STEP) "HP".
+ inversion STEP; [by inversion BaseStep|inversion ExprStep].
+ assert (Inv' : phys_inv σ2) by exact: (proj1 (machine_red_safe _ _ _)).
inversion MachStep; last by (subst; discriminate).
subst. simpl. iSplit; last done.
inversion ThreadRed. subst.
@@ -725,7 +716,7 @@ Proof.
apply (Pos.lt_irrefl (mtime m0)).
rewrite -{2}Eq. eapply Pos.le_lt_trans; last by apply Pos.lt_add_r.
by apply tMax, elem_of_hist. }
- eexists.
+ do 2 eexists.
exists (mkState (add_ins (mem σ) m Disj)
(nats σ)).
econstructor. eright; first by constructor.
@@ -736,7 +727,7 @@ Proof.
{ rewrite -Eqv -Hv -H0. by destruct m'. }
{ exists tl. split => //. rewrite -EqTime.
by apply tMax, elem_of_hist. }
- + eexists.
+ + do 2 eexists.
exists (mkState (mem σ) (nats σ)).
econstructor. eright. eapply ra_lang.CasFailS; eauto.
econstructor; try eauto => //=.
@@ -748,10 +739,9 @@ Proof.
exists tl. split => //.
rewrite -EqTime. by apply tMax, elem_of_hist.
- iSplitL "HP"; first by [].
- iNext. iIntros "% % % % HP". destruct a as [v' π'].
- match goal with | [H : ectx_language.head_step _ _ _ _ _ |- _ ] => inversion H end;
- [by inversion BaseStep|..].
- assert (Inv' : phys_inv a0) by exact: (proj1 (machine_red_safe _ _ _)).
+ iNext. iIntros (κ e2 σ2 efs STEP) "HP".
+ inversion STEP; [by inversion BaseStep|].
+ assert (Inv' : phys_inv σ2) by exact: (proj1 (machine_red_safe _ _ _)).
subst.
inversion ExprStep; inversion MachStep; subst; try discriminate; simpl;
(iSplit; last done).
@@ -838,7 +828,7 @@ Proof.
apply (Pos.le_lt_trans _ (mtime m')).
- rewrite TEq. by apply tMax, elem_of_hist.
- apply Pos.lt_add_r. }
- eexists.
+ do 2 eexists.
exists (mkState (add_ins (mem σ) m Disj) (nats σ)).
econstructor. eright; first by constructor.
econstructor; try eauto => //=.
@@ -849,10 +839,9 @@ Proof.
{ exists tl. split => //. rewrite -EqTime.
by apply tMax, elem_of_hist. }
- iSplitL "HP"; first by [].
- iNext. iIntros "% % % % HP". destruct a as [v' π'].
- match goal with | [H : ectx_language.head_step _ _ _ _ _ |- _ ] => inversion H end;
- [by inversion BaseStep|..].
- assert (Inv' : phys_inv a0) by exact: (proj1 (machine_red_safe _ _ _)).
+ iNext. iIntros (κ e2 σ2 efs STEP) "HP".
+ inversion STEP; [by inversion BaseStep|].
+ assert (Inv' : phys_inv σ2) by exact: (proj1 (machine_red_safe _ _ _)).
subst.
inversion ExprStep; inversion MachStep; subst; try discriminate; simpl;
iSplit; last done.
@@ -904,7 +893,7 @@ Proof.
case (decide (mloc m = mloc m0)) => [LEq|LNEq];
last by left. exfalso. apply (Fresh _ HIn). rewrite /m in LEq.
by simpl in LEq. }
- eexists.
+ do 2 eexists.
exists (mkState (add_ins (mem σ) m Disj) (<[l := mtime m]> (nats σ))).
econstructor. eright; first by constructor.
econstructor; try eauto => //.
@@ -922,10 +911,9 @@ Proof.
{ by rewrite Eq /=. }
+ constructor; eauto. by rewrite NVl.
- iSplitL "HP"; first by [].
- iNext. iIntros "% % % % HP". destruct a as [v' π'].
- match goal with | [H : ectx_language.head_step _ _ _ _ _ |- _ ] => inversion H end;
- [by inversion BaseStep|inversion ExprStep].
- assert (Inv' : phys_inv a0) by exact: (proj1 (machine_red_safe _ _ _)).
+ iNext. iIntros (κ e2 σ2 efs STEP) "HP".
+ inversion STEP; [by inversion BaseStep|inversion ExprStep].
+ assert (Inv' : phys_inv σ2) by exact: (proj1 (machine_red_safe _ _ _)).
inversion MachStep; last by (subst; discriminate).
subst. simpl. iSplit; last done.
assert (AllocRed: alloc_red (mem σ) V l (EWrite na l A)). { by apply ARed. }
diff --git a/theories/lifting_vProp.v b/theories/lifting_vProp.v
index b6a1e1b4..9b95f54d 100644
--- a/theories/lifting_vProp.v
+++ b/theories/lifting_vProp.v
@@ -18,9 +18,9 @@ Proof.
+ simplify_eq. now rewrite -fill_view.
+ simplify_eq. now rewrite -fill_view.
+ now eauto.
- - intros σ1 [e2' V'] σ2 efs HStep.
- move: pure_step_det => /(_ (V, σ1) e2' (V', σ2) (map (fst) efs)) H.
- destruct H as (? & ? & ?).
+ - intros σ1 κ [e2' V'] σ2 efs HStep.
+ move: pure_step_det => /(_ (V, σ1) κ e2' (V', σ2) (map (fst) efs)) H.
+ destruct H as (? & ? & ? & ?).
+ inversion HStep; cbn in *.
destruct e1' as [e1' V1'], e2'0 as [e2'0 V2'0]. cbn in *.
exists K (e1') (e2'0).
@@ -31,8 +31,7 @@ Proof.
{ simplify_eq. unfold surface.head_step. cbn. exact H1. }
{ simplify_eq. inversion ExprStep; simplify_eq; cbn; try exact H1.
inversion MachStep. simplify_map_eq. inversion ThreadRed. simplify_eq.
- exact H1.
- }
+ exact H1. }
+ simplify_eq. by destruct efs.
Qed.
@@ -43,15 +42,18 @@ Local Set Default Proof Using "Σ Iris".
Implicit Types P Q : vProp Σ.
Implicit Types Φ : base.val → vProp Σ. (* TODO: fix imports *)
-Lemma wp_pure_step_later `{Inhabited (state)} E e1 e2 φ Φ :
- (PureExec φ 1 e1 e2) →
+Lemma wp_pure_step_later `{Inhabited (state)} E e1 e2 φ n Φ :
+ (PureExec φ n e1 e2) →
φ →
- ▷ WP e2 @ E {{ Φ }} ⊢ WP e1 @ E {{ Φ }}.
+ ▷^n WP e2 @ E {{ Φ }} ⊢ WP e1 @ E {{ Φ }}.
Proof.
- iStartProof (uPred _). iIntros (?? V) "W".
+ iIntros (Hexec ?). iStartProof (uPred _). iIntros (V) "W".
rewrite WP_Def.wp_eq /WP_Def.wp_def /=. iIntros (V' HV' π) "G".
- iApply program_logic.lifting.wp_pure_step_fupd; [apply pure_exec_view; eassumption|done|].
- iIntros "!>". by iApply "W".
+ iApply (program_logic.lifting.wp_pure_step_fupd _ _ E);
+ [apply pure_exec_view;eassumption|done|]. clear Hexec.
+ induction n as [|n IH]; rewrite //=.
+ - by iApply "W".
+ - rewrite -step_fupd_intro //. iIntros "!>". by apply IH.
Qed.
End Lifting.
@@ -68,11 +70,11 @@ Ltac inv_head_step :=
try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
and can thus better be avoided. *)
inversion H; subst; clear H
- | H : surface.head_step ?e _ _ _ _ |- _ =>
+ | H : surface.head_step ?e _ _ _ _ _ |- _ =>
try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
and can thus better be avoided. *)
inversion H; subst; clear H
- | H : ra_lang.head_step ?e _ _ _ _ |- _ =>
+ | H : ra_lang.head_step ?e _ _ _ _ _ |- _ =>
try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
and can thus better be avoided. *)
inversion H; subst; clear H
diff --git a/theories/tactics.v b/theories/tactics.v
index aed8f267..e92719e9 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -355,7 +355,7 @@ Ltac inv_head_step :=
try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
and can thus better be avoided. *)
inversion H; subst; clear H
- | H : ra_lang.head_step ?e _ _ _ _ |- _ =>
+ | H : ra_lang.head_step ?e _ _ _ _ _ |- _ =>
try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
and can thus better be avoided. *)
inversion H; subst; clear H
@@ -405,7 +405,7 @@ Tactic Notation "do_head_step" tactic3(tac) :=
try match goal with |- head_reducible _ _ => eexists _, _, _ end;
simpl;
match goal with
- | |- head_step ?e1 ?σ1 ?e2 ?σ2 ?ef =>
+ | |- head_step ?e1 ?σ1 ?κ ?e2 ?σ2 ?ef =>
first [idtac|econstructor];
(* solve [to_val] side-conditions *)
first [rewrite ?to_of_val; reflexivity|simpl_subst; tac; fast_done]
diff --git a/theories/weakestpre.v b/theories/weakestpre.v
index 7aac4c3f..0afb35d8 100644
--- a/theories/weakestpre.v
+++ b/theories/weakestpre.v
@@ -145,7 +145,7 @@ Proof.
iApply (fupd_mask_mono E1 _); first done.
iExact "H". (* TODO why does `done` not work? *)
}
- iIntros (σ1) "Hσ". iMod (fupd_intro_mask' E2 E1) as "Hclose"; first done.
+ iIntros (σ1 κ κs) "Hσ". iMod (fupd_intro_mask' E2 E1) as "Hclose"; first done.
iMod ("H" with "[$]") as "[$ H]".
iModIntro. iIntros (e2 σ2 efs Hstep).
iMod ("H" with "[//]") as "H". iIntros "!> !>". iMod "H" as "($ & H & $)"; auto.
@@ -174,7 +174,8 @@ Proof.
iIntros (V ? ?).
rewrite !bi.forall_elim bi.pure_impl_forall bi.forall_elim //.
destruct (ra_lang.to_val ((e, V))) as [v|] eqn:?; [by iMod "H"|].
- iIntros "S" (σ1) "Hσ1". iMod "H". iApply ("H" with "S Hσ1").
+ iIntros "S" (σ1 κ κs) "Hσ1". iMod ("H" with "S") as "H".
+ iApply ("H" $! σ1 κ κs with "Hσ1").
Qed.
Lemma wp_fupd E e Φ : WP e @ E {{ v, |={E}=> Φ v }} ⊢ WP e @ E {{ Φ }}.
Proof. iIntros "H". iApply (wp_strong_mono E); try iFrame; auto. Qed.
@@ -201,7 +202,8 @@ Proof.
rewrite /to_val /= /ra_lang.to_val /=.
iIntros (-> ?) "H". iIntros (V'' HV'' π) "S".
iSpecialize ("H" with "[//]").
- iIntros (σ1) "Hσ". iMod "HR". iMod ("H" with "S [$]") as "[$ H]".
+ iIntros (σ1 κ κs) "Hσ". iMod "HR". iSpecialize ("H" with "S").
+ iMod ("H" $! σ1 κ κs with "[$]") as "[$ H]".
iModIntro; iIntros (e2 σ2 efs Hstep).
iMod ("H" $! e2 σ2 efs with "[% //]") as "H".
iIntros "!> !>". iMod "H" as "($ & H & $)".
diff --git a/theories/wp_tactics.v b/theories/wp_tactics.v
index 91f80b53..0d5e5bf3 100644
--- a/theories/wp_tactics.v
+++ b/theories/wp_tactics.v
@@ -5,10 +5,10 @@ From iris.proofmode Require Import coq_tactics tactics.
From igps Require Export lifting tactics_vProp ghosts.
Import uPred.
-Lemma tac_wp_pure `{ghosts.foundationG Σ} K Δ Δ' E e1 e2 φ Φ :
- PureExec (Λ:=ra_lang) φ 1 e1 e2 →
+Lemma tac_wp_pure `{ghosts.foundationG Σ} K Δ Δ' E e1 e2 φ n Φ :
+ PureExec (Λ:=ra_lang) φ n e1 e2 →
φ →
- MaybeIntoLaterNEnvs 1 Δ Δ' →
+ MaybeIntoLaterNEnvs n Δ Δ' →
envs_entails Δ' (WP fill K e2 @ E {{ Φ }}) →
envs_entails Δ (WP fill K e1 @ E {{ Φ }}).
Proof.
diff --git a/theories/wp_tactics_vProp.v b/theories/wp_tactics_vProp.v
index 96b7d217..30130b8a 100644
--- a/theories/wp_tactics_vProp.v
+++ b/theories/wp_tactics_vProp.v
@@ -16,19 +16,26 @@ Ltac wp_expr_eval t :=
Ltac wp_expr_simpl := wp_expr_eval simpl.
Ltac wp_expr_simpl_subst := wp_expr_eval simpl_subst.
-Lemma tac_wp_pure `{foundationG Σ} Δ Δ' E e1 e2 φ Φ :
- (PureExec (Λ:=surface_lang) φ 1 (e1) (e2)) →
+Lemma tac_wp_pure `{foundationG Σ} K Δ Δ' E e1 e2 φ n Φ :
+ PureExec φ n e1 e2 →
φ →
- MaybeIntoLaterNEnvs 1 Δ Δ' →
- envs_entails Δ' (WP e2 @ E {{ Φ }}) →
- envs_entails Δ (WP e1 @ E {{ Φ }}).
+ MaybeIntoLaterNEnvs n Δ Δ' →
+ envs_entails Δ' (WP fill K e2 @ E {{ Φ }}) →
+ envs_entails Δ (WP fill K e1 @ E {{ Φ }}).
Proof.
rewrite envs_entails_eq=> ??? HΔ'. rewrite into_laterN_env_sound /=.
- rewrite HΔ' -wp_pure_step_later //.
+ rewrite HΔ' wp_eq /wp_def /=. iStartProof (iProp _).
+ iIntros "% /= H" (ð“¥ ? ?) "?".
+ iApply (lifting.wp_pure_step_later _ _ (fill K e1, _) (fill K e2, _) φ);
+ [|done|].
+ { rewrite -2!fill_view => ?.
+ by apply (pure_step_nsteps_ctx (@ectxi_language.fill ra_lang.ra_ectxi_lang K)),
+ (pure_exec_view φ). }
+ iNext. by iApply ("H" with "[//] [$]").
Qed.
Lemma tac_wp_value `{foundationG Σ} Δ E Φ e v :
- (IntoVal (e) (v)) →
+ IntoVal e v →
envs_entails Δ (Φ v) → envs_entails Δ (WP e @ E {{ Φ }}).
Proof. rewrite envs_entails_eq=> <- ->. now apply: wp_value'. Qed.
@@ -37,16 +44,15 @@ Ltac wp_value_head := eapply tac_wp_value; [apply _|reduction.pm_prettify].
Tactic Notation "wp_pure" open_constr(efoc) :=
iStartProof;
lazymatch goal with
- | |- envs_entails _ (WP_Def.wp ?E ?e ?Q) => tactics_vProp.reshape_expr e ltac:(fun K e' =>
- unify e' efoc;
- eapply tac_wp_pure;
- [
- refine (@language.pure_exec_ctx _ _ (ectx_language.ectx_lang_ctx (Λ:=surface_ectx_lang) K) _ _ e' _ _); apply _ (* FIXME *)
- (* PureExec *)
- |try fast_done (* The pure condition for PureExec *)
- |apply _ (* IntoLaters *)
- |wp_expr_simpl_subst; try wp_value_head (* new goal *)
- ])
+ | |- envs_entails _ (WP_Def.wp ?E ?e ?Q) =>
+ tactics_vProp.reshape_expr e ltac:(fun K e' =>
+ unify e' efoc;
+ eapply (tac_wp_pure K);
+ [simpl; apply _ (* PureExec *)
+ |try fast_done (* The pure condition for PureExec *)
+ |apply _ (* IntoLaters *)
+ |wp_expr_simpl_subst; try wp_value_head (* new goal *)
+ ])
|| fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a reduct"
| _ => fail "wp_pure: not a 'wp'"
end.
--
GitLab