Merge branch 'robbert/pure_exec_nsteps' into 'master'

Support multiple steps in `PureExec`.

See merge request FP/iris-coq!179

CHANGELOG.md

@@ -79,6 +79,7 @@ Changes in Coq:
 * Changed `IntoVal` to be directly usable for rewriting `e` into `of_val v`, and
   changed `AsVal` to be usable for rewriting via the `[v <-]` destruct pattern.
 * `wp_fork` is now written in curried form.
+* `PureExec`/`wp_pure` now supports taking multiple steps at once.
 
 ## Iris 3.1.0 (released 2017-12-19)
 

theories/heap_lang/lifting.v

@@ -53,7 +53,8 @@ Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
 Local Ltac solve_pure_exec :=
   unfold IntoVal in *;
   repeat match goal with H : AsVal _ |- _ => destruct H as [??] end; subst;
-  apply det_head_step_pure_exec; [ solve_exec_safe | solve_exec_puredet ].
+  intros ?; apply nsteps_once, pure_head_step_pure_step;
+    constructor; [solve_exec_safe | solve_exec_puredet].
 
 Class AsRec (e : expr) (f x : binder) (erec : expr) :=
   as_rec : e = Rec f x erec.
@@ -64,37 +65,37 @@ Proof. by unlock. Qed.
 
 Instance pure_rec f x (erec e1 e2 : expr)
     `{!AsVal e2, AsRec e1 f x erec, Closed (f :b: x :b: []) erec} :
-  PureExec True (App e1 e2) (subst' x e2 (subst' f e1 erec)).
+  PureExec True 1 (App e1 e2) (subst' x e2 (subst' f e1 erec)).
 Proof. unfold AsRec in *; solve_pure_exec. Qed.
 
 Instance pure_unop op e v v' `{!IntoVal e v} :
-  PureExec (un_op_eval op v = Some v') (UnOp op e) (of_val v').
+  PureExec (un_op_eval op v = Some v') 1 (UnOp op e) (of_val v').
 Proof. solve_pure_exec. Qed.
 
 Instance pure_binop op e1 e2 v1 v2 v' `{!IntoVal e1 v1, !IntoVal e2 v2} :
-  PureExec (bin_op_eval op v1 v2 = Some v') (BinOp op e1 e2) (of_val v').
+  PureExec (bin_op_eval op v1 v2 = Some v') 1 (BinOp op e1 e2) (of_val v').
 Proof. solve_pure_exec. Qed.
 
-Instance pure_if_true e1 e2 : PureExec True (If (Lit (LitBool true)) e1 e2) e1.
+Instance pure_if_true e1 e2 : PureExec True 1 (If (Lit (LitBool true)) e1 e2) e1.
 Proof. solve_pure_exec. Qed.
 
-Instance pure_if_false e1 e2 : PureExec True (If (Lit (LitBool false)) e1 e2) e2.
+Instance pure_if_false e1 e2 : PureExec True 1 (If (Lit (LitBool false)) e1 e2) e2.
 Proof. solve_pure_exec. Qed.
 
 Instance pure_fst e1 e2 v1 `{!IntoVal e1 v1, !AsVal e2} :
-  PureExec True (Fst (Pair e1 e2)) e1.
+  PureExec True 1 (Fst (Pair e1 e2)) e1.
 Proof. solve_pure_exec. Qed.
 
 Instance pure_snd e1 e2 v2 `{!AsVal e1, !IntoVal e2 v2} :
-  PureExec True (Snd (Pair e1 e2)) e2.
+  PureExec True 1 (Snd (Pair e1 e2)) e2.
 Proof. solve_pure_exec. Qed.
 
 Instance pure_case_inl e0 v e1 e2 `{!IntoVal e0 v} :
-  PureExec True (Case (InjL e0) e1 e2) (App e1 e0).
+  PureExec True 1 (Case (InjL e0) e1 e2) (App e1 e0).
 Proof. solve_pure_exec. Qed.
 
 Instance pure_case_inr e0 v e1 e2 `{!IntoVal e0 v} :
-  PureExec True (Case (InjR e0) e1 e2) (App e2 e0).
+  PureExec True 1 (Case (InjR e0) e1 e2) (App e2 e0).
 Proof. solve_pure_exec. Qed.
 
 Section lifting.

theories/heap_lang/proofmode.v

@@ -30,18 +30,18 @@ Tactic Notation "wp_expr_eval" tactic(t) :=
 Ltac wp_expr_simpl := wp_expr_eval simpl.
 Ltac wp_expr_simpl_subst := wp_expr_eval simpl_subst.
 
-Lemma tac_wp_pure `{heapG Σ} Δ Δ' s E e1 e2 φ Φ :
-  PureExec φ e1 e2 →
+Lemma tac_wp_pure `{heapG Σ} Δ Δ' s E e1 e2 φ n Φ :
+  PureExec φ n e1 e2 →
   φ →
-  MaybeIntoLaterNEnvs 1 Δ Δ' →
+  MaybeIntoLaterNEnvs n Δ Δ' →
   envs_entails Δ' (WP e2 @ s; E {{ Φ }}) →
   envs_entails Δ (WP e1 @ s; E {{ Φ }}).
 Proof.
   rewrite envs_entails_eq=> ??? HΔ'. rewrite into_laterN_env_sound /=.
   rewrite HΔ' -lifting.wp_pure_step_later //.
 Qed.
-Lemma tac_twp_pure `{heapG Σ} Δ s E e1 e2 φ Φ :
-  PureExec φ e1 e2 →
+Lemma tac_twp_pure `{heapG Σ} Δ s E e1 e2 φ n Φ :
+  PureExec φ n e1 e2 →
   φ →
   envs_entails Δ (WP e2 @ s; E [{ Φ }]) →
   envs_entails Δ (WP e1 @ s; E [{ Φ }]).

theories/program_logic/ectx_language.v

@@ -206,23 +206,24 @@ Section ectx_language.
       econstructor; eauto.
   Qed.
 
-  Lemma det_head_step_pure_exec (P : Prop) e1 e2 :
-    (∀ σ, P → head_reducible e1 σ) →
-    (∀ σ1 e2' σ2 efs,
-      P → head_step e1 σ1 e2' σ2 efs → σ1 = σ2 ∧ e2=e2' ∧ efs = []) →
-    PureExec P e1 e2.
+  Record pure_head_step (e1 e2 : expr Λ) := {
+    pure_head_step_safe σ1 : head_reducible e1 σ1;
+    pure_head_step_det σ1 e2' σ2 efs :
+      head_step e1 σ1 e2' σ2 efs → σ1 = σ2 ∧ e2 = e2' ∧ efs = []
+  }.
+
+  Lemma pure_head_step_pure_step e1 e2 : pure_head_step e1 e2 → pure_step e1 e2.
   Proof.
-    intros Hp1 Hp2. split.
-    - intros σ ?. destruct (Hp1 σ) as (e2' & σ2 & efs & ?); first done.
+    intros [Hp1 Hp2]. split.
+    - intros σ. destruct (Hp1 σ) as (e2' & σ2 & efs & ?).
       eexists e2', σ2, efs. by apply head_prim_step.
-    - intros σ1 e2' σ2 efs ? ?%head_reducible_prim_step; eauto.
+    - intros σ1 e2' σ2 efs ?%head_reducible_prim_step; eauto.
   Qed.
 
-  Global Instance pure_exec_fill K e1 e2 φ :
-    PureExec φ e1 e2 →
-    PureExec φ (fill K e1) (fill K e2).
+  Global Instance pure_exec_fill K φ n e1 e2 :
+    PureExec φ n e1 e2 →
+    PureExec φ n (fill K e1) (fill K e2).
   Proof. apply: pure_exec_ctx. Qed.
-
 End ectx_language.
 
 Arguments ectx_lang : clear implicits.

theories/program_logic/language.v

@@ -133,31 +133,40 @@ Section language.
     by rewrite -!Permutation_middle !assoc_L Ht.
   Qed.
 
-  Class PureExec (P : Prop) (e1 e2 : expr Λ) := {
-    pure_exec_safe σ :
-      P → reducible e1 σ;
-    pure_exec_puredet σ1 e2' σ2 efs :
-      P → prim_step e1 σ1 e2' σ2 efs → σ1 = σ2 ∧ e2 = e2' ∧ efs = [];
+  Record pure_step (e1 e2 : expr Λ) := {
+    pure_step_safe σ1 : reducible e1 σ1;
+    pure_step_det σ1 e2' σ2 efs :
+      prim_step e1 σ1 e2' σ2 efs → σ1 = σ2 ∧ e2 = e2' ∧ efs = []
   }.
 
-  Lemma hoist_pred_pure_exec (P : Prop) (e1 e2 : expr Λ) :
-    (P → PureExec True e1 e2) →
-    PureExec P e1 e2.
-  Proof. intros HPE. split; intros; eapply HPE; eauto. Qed.
+  (* TODO: Exclude the case of [n=0], either here, or in [wp_pure] to avoid it
+  succeeding when it did not actually do anything. *)
+  Class PureExec (φ : Prop) (n : nat) (e1 e2 : expr Λ) :=
+    pure_exec : φ → nsteps pure_step n e1 e2.
 
-  (* We do not make this an instance because it is awfully general. *)
-  Lemma pure_exec_ctx K `{LanguageCtx Λ K} e1 e2 φ :
-    PureExec φ e1 e2 →
-    PureExec φ (K e1) (K e2).
+  Lemma pure_step_ctx K `{LanguageCtx Λ K} e1 e2 :
+    pure_step e1 e2 →
+    pure_step (K e1) (K e2).
   Proof.
     intros [Hred Hstep]. split.
     - unfold reducible in *. naive_solver eauto using fill_step.
-    - intros σ1 e2' σ2 efs ? Hpstep.
+    - intros σ1 e2' σ2 efs Hpstep.
       destruct (fill_step_inv e1 σ1 e2' σ2 efs) as (e2'' & -> & ?); [|exact Hpstep|].
       + destruct (Hred σ1) as (? & ? & ? & ?); eauto using val_stuck.
-      + edestruct (Hstep σ1 e2'' σ2 efs) as (-> & -> & ->); auto.
+      + destruct (Hstep σ1 e2'' σ2 efs) as (-> & -> & ->); auto.
   Qed.
 
+  Lemma pure_step_nsteps_ctx K `{LanguageCtx Λ K} n e1 e2 :
+    nsteps pure_step n e1 e2 →
+    nsteps pure_step n (K e1) (K e2).
+  Proof. induction 1; econstructor; eauto using pure_step_ctx. Qed.
+
+  (* We do not make this an instance because it is awfully general. *)
+  Lemma pure_exec_ctx K `{LanguageCtx Λ K} φ n e1 e2 :
+    PureExec φ n e1 e2 →
+    PureExec φ n (K e1) (K e2).
+  Proof. rewrite /PureExec; eauto using pure_step_nsteps_ctx. Qed.
+
   (* This is a family of frequent assumptions for PureExec *)
   Class IntoVal (e : expr Λ) (v : val Λ) :=
     into_val : of_val v = e.

theories/program_logic/lifting.v

@@ -123,23 +123,25 @@ Proof.
   by iIntros (e' efs' σ (_&->&->)%Hpuredet).
 Qed.
 
-Lemma wp_pure_step_fupd `{Inhabited (state Λ)} s E E' e1 e2 φ Φ :
-  PureExec φ e1 e2 →
+Lemma wp_pure_step_fupd `{Inhabited (state Λ)} s E E' e1 e2 φ n Φ :
+  PureExec φ n e1 e2 →
   φ →
-  (|={E,E'}▷=> WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
+  Nat.iter n (λ P, |={E,E'}▷=> P) (WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
-  iIntros ([??] Hφ) "HWP".
-  iApply (wp_lift_pure_det_step with "[HWP]").
-  - intros σ. specialize (pure_exec_safe σ). destruct s; eauto using reducible_not_val.
+  iIntros (Hexec Hφ) "Hwp". specialize (Hexec Hφ).
+  iInduction Hexec as [e|n e1 e2 e3 [Hsafe ?]] "IH"; simpl; first done.
+  iApply wp_lift_pure_det_step.
+  - intros σ. specialize (Hsafe σ). destruct s; eauto using reducible_not_val.
   - destruct s; naive_solver.
-  - by rewrite big_sepL_nil right_id.
+  - rewrite /= right_id. by iApply (step_fupd_wand with "Hwp").
 Qed.
 
-Lemma wp_pure_step_later `{Inhabited (state Λ)} s E e1 e2 φ Φ :
-  PureExec φ e1 e2 →
+Lemma wp_pure_step_later `{Inhabited (state Λ)} s E e1 e2 φ n Φ :
+  PureExec φ n e1 e2 →
   φ →
-  ▷ WP e2 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}.
+  ▷^n WP e2 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
-  intros ??. rewrite -wp_pure_step_fupd //. rewrite -step_fupd_intro //.
+  intros Hexec ?. rewrite -wp_pure_step_fupd //. clear Hexec.
+  induction n as [|n IH]; by rewrite //= -step_fupd_intro // IH.
 Qed.
 End lifting.

theories/program_logic/total_lifting.v

@@ -68,12 +68,14 @@ Proof.
   by iIntros "!>" (e' efs' σ (_&->&->)%Hpuredet).
 Qed.
 
-Lemma twp_pure_step `{Inhabited (state Λ)} s E e1 e2 φ Φ :
-  PureExec φ e1 e2 →
+Lemma twp_pure_step `{Inhabited (state Λ)} s E e1 e2 φ n Φ :
+  PureExec φ n e1 e2 →
   φ →
   WP e2 @ s; E [{ Φ }] ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
-  iIntros ([??] Hφ) "HWP".
-  iApply (twp_lift_pure_det_step with "[HWP]"); [eauto|naive_solver|auto].
+  iIntros (Hexec Hφ) "Hwp". specialize (Hexec Hφ).
+  iInduction Hexec as [e|n e1 e2 e3 [Hsafe ?]] "IH"; simpl; first done.
+  iApply twp_lift_pure_det_step; [done|naive_solver|].
+  iModIntro. rewrite /= right_id. by iApply "IH".
 Qed.
 End lifting.