From c4e7da6085719433398ecfdfb35fe285d59b493c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lennard=20G=C3=A4her?= <l.gaeher@posteo.de>
Date: Thu, 28 Jul 2022 16:58:19 +0200
Subject: [PATCH] tactics

---
 iris_heap_lang/primitive_laws.v |   4 +-
 iris_heap_lang/proofmode.v      | 116 ++++++++++++++++++++++++++++++++
 tests/heap_lang.ref             |  34 ++++++++++
 tests/heap_lang.v               |  39 +++++++++++
 4 files changed, 191 insertions(+), 2 deletions(-)

diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index bfc3a73d7..6aed55fee 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -176,7 +176,7 @@ Lemma wp_pure_step_credits_lb ϕ e1 e2 s E n Φ :
   PureExec ϕ 1 e1 e2 →
   ϕ →
   steps_lb n -∗
-  (£ (S n) -∗ steps_lb (S n) -∗ WP e2 @ s; E {{ Φ }}) -∗
+  ▷ (£ (S n) -∗ steps_lb (S n) -∗ WP e2 @ s; E {{ Φ }}) -∗
   WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (Hpure Hphi) "Hlb Hwp".
@@ -203,7 +203,7 @@ Qed.
 Lemma wp_pure_step_credit s E e1 e2 ϕ Φ :
   PureExec ϕ 1 e1 e2 →
   ϕ →
-  (£ 1 -∗ WP e2 @ s; E {{ Φ }}) -∗
+  ▷ (£ 1 -∗ WP e2 @ s; E {{ Φ }}) -∗
   WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (Hexec Hphi) "Hwp".
diff --git a/iris_heap_lang/proofmode.v b/iris_heap_lang/proofmode.v
index 49f45e643..e27ad5f9a 100644
--- a/iris_heap_lang/proofmode.v
+++ b/iris_heap_lang/proofmode.v
@@ -53,6 +53,64 @@ Proof.
   rewrite -total_lifting.twp_pure_step //.
 Qed.
 
+Lemma tac_wp_pure_credit `{!heapGS_gen hlc Σ} Δ Δ' s E j K e1 e2 ϕ Φ :
+  PureExec ϕ 1 e1 e2 →
+  ϕ →
+  MaybeIntoLaterNEnvs 1 Δ Δ' →
+  (match envs_app false (Esnoc Enil j (£ 1)) Δ' with
+    | Some Δ'' =>
+       envs_entails Δ'' (WP fill K e2 @ s; E {{ Φ }})
+    | None => False
+    end) →
+  envs_entails Δ (WP (fill K e1) @ s; E {{ Φ }}).
+Proof.
+  rewrite envs_entails_unseal=> ??? HΔ.
+  pose proof @pure_exec_fill.
+  rewrite -wp_pure_step_credit; last done.
+  rewrite into_laterN_env_sound /=. apply later_mono.
+  destruct (envs_app _ _ _) as [Δ''|] eqn:HΔ'; [ | contradiction ].
+  rewrite envs_app_sound //; simpl.
+  rewrite right_id. apply wand_intro_r. by rewrite wand_elim_l.
+Qed.
+
+Local Lemma wp_pure_step_credits_lb' `{!heapGS_gen hlc Σ} ϕ e1 e2 s E n Φ :
+  PureExec ϕ 1 e1 e2 →
+  ϕ →
+  ▷ (steps_lb n ∗ (£ (S n) -∗ steps_lb (S n) -∗ WP e2 @ s; E {{ Φ }})) -∗
+  WP e1 @ s; E {{ Φ }}.
+Proof.
+  iIntros (??) "[>Ha Hb]". by iApply (wp_pure_step_credits_lb with "Ha Hb").
+Qed.
+Lemma tac_wp_pure_credits_lb `{!heapGS_gen hlc Σ} Δ Δ' s E i j K e1 e2 ϕ n Φ :
+  PureExec ϕ 1 e1 e2 →
+  ϕ →
+  MaybeIntoLaterNEnvs 1 Δ Δ' →
+  envs_lookup i Δ' = Some (false, steps_lb n)%I →
+  (match envs_simple_replace i false (Esnoc Enil i (steps_lb (S n))) Δ' with
+  | Some Δ'' =>
+     match envs_app false (Esnoc Enil j (£ (S n))) Δ'' with
+     | Some Δ''' => envs_entails Δ''' (WP fill K e2 @ s; E {{ Φ }})
+     | None => False
+     end
+  | None => False
+  end) →
+  envs_entails Δ (WP (fill K e1) @ s; E {{ Φ }}).
+Proof.
+  rewrite envs_entails_unseal=> ??? Hlb HΔ.
+  pose proof @pure_exec_fill.
+  rewrite -(wp_pure_step_credits_lb' _ _ _ _ _ n); last done.
+  rewrite into_laterN_env_sound /=.
+  destruct (envs_simple_replace _ _ _) as [Δ'''|] eqn:HΔ'''; [ | contradiction ].
+  destruct (envs_app _ _ _) as [Δ''|] eqn:HΔ'; [ | contradiction ].
+  rewrite envs_simple_replace_sound; [ | done..]. simpl.
+  rewrite right_id !later_sep.
+  apply sep_mono; first done.
+  apply later_mono. apply wand_intro_r. apply wand_intro_r.
+  rewrite -sep_assoc sep_comm -sep_assoc.
+  rewrite wand_elim_r.
+  rewrite envs_app_sound // /= right_id wand_elim_r //.
+Qed.
+
 Lemma tac_wp_value_nofupd `{!heapGS_gen hlc Σ} Δ s E Φ v :
   envs_entails Δ (Φ v) → envs_entails Δ (WP (Val v) @ s; E {{ Φ }}).
 Proof. rewrite envs_entails_unseal=> ->. by apply wp_value. Qed.
@@ -134,6 +192,64 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
   | _ => fail "wp_pure: not a 'wp'"
   end.
 
+Tactic Notation "wp_pure" open_constr(efoc) "as" constr(H) :=
+  iStartProof;
+  let Htmp := iFresh in
+  let finish _ :=
+    pm_reduce;
+    (iDestructHyp Htmp as H || fail 2 "wp_pure: " H " is not fresh");
+    wp_finish
+    in
+  lazymatch goal with
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+    let e := eval simpl in e in
+    reshape_expr e ltac:(fun K e' =>
+      unify e' efoc;
+      eapply (tac_wp_pure_credit _ _ _ _ Htmp K e');
+      [iSolveTC                       (* PureExec *)
+      |try solve_vals_compare_safe    (* The pure condition for PureExec --
+         handles trivial goals, including [vals_compare_safe] *)
+      |iSolveTC                       (* IntoLaters *)
+      |finish ()                      (* new goal *)
+      ])
+    || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a redex"
+  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
+    fail "wp_pure: credit generation is not supported for a TWP"
+  | _ => fail "wp_pure: not a 'wp'"
+  end.
+Tactic Notation "wp_pure" "as" constr(H) :=
+  wp_pure _ as H.
+
+Tactic Notation "wp_pure" open_constr(efoc) "with" constr(Hlb) "as" constr(H) :=
+  iStartProof;
+  let Htmp := iFresh in
+  let finish _ :=
+    pm_reduce;
+    (iDestructHyp Htmp as H || fail 2 "wp_pure: " H " is not fresh");
+    wp_finish
+    in
+  let find_lb _ := iAssumptionCore || fail 2 "wp_pure: cannot find " Hlb " : steps_lb _" in
+  lazymatch goal with
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+    let e := eval simpl in e in
+    reshape_expr e ltac:(fun K e' =>
+      unify e' efoc;
+      eapply (tac_wp_pure_credits_lb _ _ _ _ Hlb Htmp K e');
+      [iSolveTC                       (* PureExec *)
+      |try solve_vals_compare_safe    (* The pure condition for PureExec --
+         handles trivial goals, including [vals_compare_safe] *)
+      |iSolveTC                       (* IntoLaters *)
+      |find_lb ()                     (* The [steps_lb _] hypothesis *)
+      |finish ()                      (* new goal *)
+      ])
+    || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a redex"
+  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
+    fail "wp_pure: credit generation is not supported for a TWP"
+  | _ => fail "wp_pure: not a 'wp'"
+  end.
+Tactic Notation "wp_pure" "with" constr(Hlb) "as" constr(H) :=
+  wp_pure _ with Hlb as H.
+
 (* TODO: do this in one go, without [repeat]. *)
 Ltac wp_pures :=
   iStartProof;
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 2ca1c26e8..b8693465a 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -179,6 +179,40 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
              (@iris_invGS HasLc heap_lang Σ (@heapGS_irisGS HasLc Σ heapGS0))))
        (@top coPset coPset_top) (@top coPset coPset_top)
        (@bi_pure (uPredI (iResUR Σ)) True))
+"test_wp_pure_credit_succeed"
+     : string
+1 goal
+  
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  ============================
+  "Hcred" : £ 1
+  --------------------------------------∗
+  |={⊤}=> True
+"test_wp_pure_credit_fail"
+     : string
+The command has indeed failed with message:
+Tactic failure: wp_pure:  "Hcred"  is not fresh.
+"test_wp_pure_credits_lb_succeed"
+     : string
+1 goal
+  
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  n : nat
+  ============================
+  "Hlb" : steps_lb (S n)
+  "Hcred" : £ (S n)
+  --------------------------------------∗
+  |={⊤}=> True
+"test_wp_pure_credits_lb_fail1"
+     : string
+The command has indeed failed with message:
+Tactic failure: wp_pure: cannot find  "Hl"  : steps_lb _.
+"test_wp_pure_credits_lb_fail2"
+     : string
+The command has indeed failed with message:
+Tactic failure: wp_pure:  "Hlb"  is not fresh.
 1 goal
   
   Σ : gFunctors
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 2bb43ba85..0dca981bb 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -336,6 +336,45 @@ Section tests.
     Show.
     Unset Printing All.
   Abort.
+
+  Check "test_wp_pure_credit_succeed".
+  Lemma test_wp_pure_credit_succeed :
+    ⊢ WP #42 + #420 {{ v, True }}.
+  Proof.
+    wp_pure as "Hcred". Show. done.
+  Qed.
+
+  Check "test_wp_pure_credit_fail".
+  Lemma test_wp_pure_credit_fail :
+    ⊢ True -∗ WP #42 + #420 {{ v, True }}.
+  Proof.
+    iIntros "Hcred".
+    Fail wp_pure as "Hcred".
+  Abort.
+
+  Check "test_wp_pure_credits_lb_succeed".
+  Lemma test_wp_pure_credits_lb_succeed n :
+    ⊢ steps_lb n -∗ WP #42 + #420 {{ v, True }}.
+  Proof.
+    iIntros "Hlb".
+    wp_pure with "Hlb" as "Hcred". Show. done.
+  Qed.
+
+  Check "test_wp_pure_credits_lb_fail1".
+  Lemma test_wp_pure_credits_lb_fail1 n :
+    ⊢ steps_lb n -∗ WP #42 + #420 {{ v, True }}.
+  Proof.
+    iIntros "Hlb".
+    Fail wp_pure with "Hl" as "Hcred".
+  Abort.
+
+  Check "test_wp_pure_credits_lb_fail2".
+  Lemma test_wp_pure_credits_lb_fail2 n :
+    ⊢ steps_lb n -∗ WP #42 + #420 {{ v, True }}.
+  Proof.
+    iIntros "Hlb".
+    Fail wp_pure with "Hlb" as "Hlb".
+  Abort.
 End tests.
 
 Section mapsto_tests.
-- 
GitLab