Add iAccu tactic.

theories/proofmode/coq_tactics.v

@@ -126,6 +126,12 @@ Definition envs_split {PROP} (d : direction)
   ''(Δ1,Δ2) ← envs_split_go js Δ (envs_clear_spatial Δ);
   if d is Right then Some (Δ1,Δ2) else Some (Δ2,Δ1).
 
+Definition prop_of_env {PROP : bi} (Γ : env PROP) : PROP :=
+  let fix aux Γ acc :=
+    match Γ with Enil => acc | Esnoc Γ _ P => aux Γ (P ∗ acc)%I end
+  in
+  match Γ with Enil => emp%I | Esnoc Γ _ P => aux Γ P end.
+
 (* Coq versions of the tactics *)
 Section bi_tactics.
 Context {PROP : bi}.
@@ -420,6 +426,14 @@ Proof.
   destruct d; simplify_eq/=; solve_sep_entails.
 Qed.
 
+Lemma prop_of_env_sound Δ : of_envs Δ ⊢ prop_of_env (env_spatial Δ).
+Proof.
+  destruct Δ as [? Γ]. rewrite /of_envs /= and_elim_r sep_elim_r.
+  destruct Γ as [|Γ ? P0]=>//=. revert P0.
+  induction Γ as [|Γ IH ? P]=>P0; [rewrite /= right_id //|].
+  rewrite /= assoc (comm _ P0 P) IH //.
+Qed.
+
 Global Instance envs_Forall2_refl (R : relation PROP) :
   Reflexive R → Reflexive (envs_Forall2 R).
 Proof. by constructor. Qed.
@@ -1062,6 +1076,13 @@ Proof.
   apply wand_elim_r', wand_mono; last done. apply wand_intro_r, wand_intro_r.
   rewrite affinely_persistently_if_elim -assoc wand_curry. auto.
 Qed.
+
+(** * Accumulate hypotheses *)
+Lemma tac_accu Δ P :
+  prop_of_env (env_spatial Δ) = P →
+  envs_entails Δ P.
+Proof. rewrite envs_entails_eq=><-. apply prop_of_env_sound. Qed.
+
 End bi_tactics.
 
 (** The following _private_ classes are used internally by [tac_modal_intro] /

theories/proofmode/tactics.v

@@ -16,7 +16,7 @@ Declare Reduction env_cbv := cbv [
   envs_lookup envs_lookup_delete envs_delete envs_snoc envs_app
     envs_simple_replace envs_replace envs_split
     envs_clear_spatial envs_clear_persistent
-    envs_split_go envs_split].
+    envs_split_go envs_split prop_of_env].
 Ltac env_cbv :=
   match goal with |- ?u => let v := eval env_cbv in u in change v end.
 Ltac env_reflexivity := env_cbv; exact eq_refl.
@@ -1936,6 +1936,9 @@ Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(
     constr(pat) constr(Hclose) :=
    iInvCore N with Hs as (fun H => iDestructHyp H as (x1 x2 x3 x4) pat) Hclose.
 
+Tactic Notation "iAccu" :=
+  eapply tac_accu; env_reflexivity.
+
 Hint Extern 0 (_ ⊢ _) => iStartProof.
 
 (* Make sure that by and done solve trivial things in proof mode *)

theories/tests/proofmode.v

@@ -386,4 +386,10 @@ Proof.
   eexists. split. iIntros "HP #HQ". iFrame "HQ HP". iEmpIntro. done.
 Qed.
 
+Lemma test_iAccu P Q R S :
+  ∃ PP, (□P -∗ Q -∗ R -∗ S -∗ PP) ∧ PP = (Q ∗ R ∗ S)%I.
+Proof.
+  eexists. split. iIntros "#? ? ? ?". iAccu. done.
+Qed.
+
 End tests.