An implementation of the wp_pure tactic

theories/F_mu_ref_conc/rules.v

@@ -4,7 +4,7 @@ From iris.base_logic Require Export invariants big_op.
 From iris.algebra Require Import auth frac agree gmap.
 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Export gen_heap.
-From iris_logrel.F_mu_ref_conc Require Export lang notation.
+From iris_logrel.F_mu_ref_conc Require Export lang notation pureexec.
 Import uPred.
 
 (** The CMRA for the heap of the implementation. This is linked to the
@@ -104,16 +104,28 @@ Section lang_rules.
     WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}.
   Proof. exact: wp_ectx_bind. Qed.
 
+  Lemma wp_pure E e1 e2 φ Φ :
+    PureExec φ e1 e2 →
+    φ →
+    ▷ WP e2 @ E {{ Φ }} ⊢ WP e1 @ E {{ Φ }}.
+  Proof.
+    iIntros (? Hφ) "HWP".
+    iApply (wp_lift_pure_det_head_step_no_fork' with "HWP").
+    { destruct (pure_exec_safe Hφ ∅) as (e' & σ' & efs & Hst).
+      eapply val_stuck.
+      apply Hst. }
+    { apply (pure_exec_safe Hφ). }
+    { apply (pure_exec_puredet Hφ). }
+  Qed.
+
   Lemma wp_rec E f x erec e1 e2 Φ :
     e1 = Rec f x erec →
     is_Some (to_val e2) →
     Closed (x :b: f :b: ∅) erec →
     ▷ WP subst' f e1 (subst' x e2 erec) @ E {{ Φ }} ⊢ WP App e1 e2 @ E {{ Φ }}.
   Proof.
-    intros -> [v2 ?] ?.
-    rewrite -(wp_lift_pure_det_head_step_no_fork (App _ _)
-       (subst' f (Rec f x erec) (subst' x e2 erec))); eauto.
-    intros; inv_head_step; eauto.
+    iIntros (? [v ?] ?) "HWP". subst.
+    iApply (wp_pure with "HWP"); [ eapply pure_rec | exact I ]; eauto.
   Qed.
 
   Lemma wp_tlam E e Φ {Hcl: Closed ∅ e} : ▷ WP e @ E {{ Φ }} ⊢ WP TApp (TLam e) @ E {{ Φ }}.

theories/F_mu_ref_conc/tactics.v

 From iris.program_logic Require Export weakestpre.
-From iris.proofmode Require Export tactics.
+From iris.proofmode Require Export tactics coq_tactics.
 From iris_logrel.F_mu_ref_conc Require Export rules lang reflection.
 Set Default Proof Using "Type".
 Import lang.
 
+(* * Tactics for solving specific goals *)
+
+(* Applied to goals that are equalities of expressions. Will try to unlock the
+   LHS once if necessary, to get rid of the lock added by the syntactic sugar. *)
+Ltac solve_of_val_unlock := try apply of_val_unlock; fast_done.
+Hint Extern 0 (of_val _ = _) => solve_of_val_unlock : typeclass_instances.
+
+Ltac tac_rel_done := split_and?; try
+  lazymatch goal with
+  | [ |- of_val _ = _ ] => solve_of_val_unlock
+  | [ |- Closed _ _ ] => solve_closed
+  | [ |- to_val _ = Some _ ] => solve_to_val
+  | [ |- is_Some (to_val _)] => solve_to_val
+  end.
+
 (* * WP tactics *)
 (** The tactic [reshape_expr e tac] decomposes the expression [e] into an
 evaluation context [K] and a subexpression [e']. It calls the tactic [tac K e']
@@ -77,17 +92,76 @@ Tactic Notation "wp_bind" open_constr(efoc) :=
   | _ => fail "wp_bind: not a 'wp'"
   end.
 
-(* * Tactics for solving specific goals *)
+Lemma tac_wp_pure `{heapG Σ} K φ e1 e2 ℶ1 ℶ2 E Φ :
+  IntoLaterNEnvs 1 ℶ1 ℶ2 →
+  PureExec φ e1 e2 →
+  φ →
+  (ℶ2 ⊢ WP fill K e2 @ E {{ Φ }}) →
+  (ℶ1 ⊢ WP fill K e1 @ E {{ Φ }}).
+Proof.
+  intros ?? Hφ Hgoal.
+  rewrite into_laterN_env_sound /=.
+  rewrite Hgoal.
+  iIntros "HWP".
+  wp_bind_core K.
+  iApply wp_pure; eauto.
+  iApply (wp_bind_inv with "HWP").
+  { (* TODO: how to get rid of this? *)
+    change lang with (ectx_lang expr).
+    change fill with (ectx_language.fill).
+    eapply ectx_lang_ctx. }
+Qed.
 
-(* Applied to goals that are equalities of expressions. Will try to unlock the
-   LHS once if necessary, to get rid of the lock added by the syntactic sugar. *)
-Ltac solve_of_val_unlock := try apply of_val_unlock; fast_done.
-Hint Extern 0 (of_val _ = _) => solve_of_val_unlock : typeclass_instances.
-
-Ltac tac_rel_done := split_and?; try
+Tactic Notation "wp_pure" open_constr(efoc) :=
+  iStartProof;
   lazymatch goal with
-  | [ |- of_val _ = _ ] => solve_of_val_unlock
-  | [ |- Closed _ _ ] => solve_closed
-  | [ |- to_val _ = Some _ ] => solve_to_val
-  | [ |- is_Some (to_val _)] => solve_to_val
+  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+    unify e' efoc;
+    eapply (tac_wp_pure K);
+    [apply _ (* IntoLaters *)
+    |apply _ (* PureExec *)
+    |try (exact I || reflexivity || tac_rel_done)
+    |simpl_subst/= (* new goal *)])
   end.
+
+Tactic Notation "wp_rec" := wp_pure (App (Rec _ _ _) _) || wp_pure (App _ _).
+Tactic Notation "wp_seq" := wp_rec.
+Tactic Notation "wp_let" := wp_rec.
+Tactic Notation "wp_fst" := wp_pure (Fst (Pair _ _)).
+Tactic Notation "wp_snd" := wp_pure (Snd (Pair _ _)).
+Tactic Notation "wp_proj" := wp_pure (_ (Pair _ _)).
+Tactic Notation "wp_unfold" := wp_pure (Unfold (Fold _)).
+Tactic Notation "wp_fold" := wp_unfold.
+Tactic Notation "wp_if" := wp_pure (If _ _ _).
+Tactic Notation "wp_if_true" := wp_pure (If #true _ _).
+Tactic Notation "wp_if_false" := wp_pure (If #false _ _).
+Tactic Notation "wp_case_inl" := wp_pure (Case (InjL _) _ _).
+Tactic Notation "wp_case_inr" := wp_pure (Case (InjL _) _ _).
+Tactic Notation "wp_case" := wp_pure (Case _ _ _).
+Tactic Notation "wp_op" := wp_pure (BinOp _ _ _).
+
+Ltac wp_value := iApply wp_value; eauto.
+
+(* TODO: move to tests/ *)
+From iris_logrel.F_mu_ref_conc Require Export notation.
+
+Lemma wp_rec1 `{heapG Σ} Φ :
+  ▷ Φ #4
+  ⊢ WP (λ: "y", (λ: "x", "x" + #3) "y") #1 {{ Φ }}.
+Proof.
+  iIntros "Z".
+  wp_rec.
+  wp_rec.
+  wp_op.
+  wp_value.
+Qed.
+
+Lemma wp_proj2 `{heapG Σ} Φ :
+  ▷ Φ #1
+  ⊢ WP Fst (Fst (#1,#2,#4)) {{ Φ }}.
+Proof.
+  iIntros "HΦ".
+  wp_proj.
+  wp_proj.
+  wp_value.
+Qed.