Attempt at a more efficient `iDestruct` tactic that avoids context duplication.

tests/proofmode.v

@@ -540,18 +540,18 @@ Proof. iIntros "HP" (Q) "_ #HPQ". by iApply "HPQ". Qed.
 Lemma test_and_sep (P Q R : PROP) : P ∧ (Q ∗ □ R) ⊢ (P ∧ Q) ∗ □ R.
 Proof.
   iIntros "H". repeat iSplit.
-  - iDestruct "H" as "[$ _]".
-  - iDestruct "H" as "[_ [$ _]]".
-  - iDestruct "H" as "[_ [_ #$]]".
+  - by iDestruct "H" as "[$ _]".
+  - by iDestruct "H" as "[_ [$ _]]".
+  - by iDestruct "H" as "[_ [_ #$]]".
 Qed.
 
 Lemma test_and_sep_2 (P Q R : PROP) `{!Persistent R, !Affine R} :
   P ∧ (Q ∗ R) ⊢ (P ∧ Q) ∗ R.
 Proof.
   iIntros "H". repeat iSplit.
-  - iDestruct "H" as "[$ _]".
-  - iDestruct "H" as "[_ [$ _]]".
-  - iDestruct "H" as "[_ [_ #$]]".
+  - by iDestruct "H" as "[$ _]".
+  - by iDestruct "H" as "[_ [$ _]]".
+  - by iDestruct "H" as "[_ [_ #$]]".
 Qed.
 
 Check "test_and_sep_affine_bi".

theories/base_logic/lib/boxes.v

@@ -212,7 +212,7 @@ Proof.
   iCombine "Hf" "HP" as "Hf".
   rewrite -big_opM_opM big_opM_fmap; iApply (fupd_big_sepM _ _ f).
   iApply (@big_sepM_impl with "Hf").
-  iIntros "!#" (γ b' ?) "[(Hγ' & #$ & #$) HΦ]".
+  iIntros "!#" (γ b' ?) "[(Hγ' & #? & #?) HΦ]". iFrame "#".
   iInv N as (b) "[>Hγ _]".
   iMod (box_own_auth_update γ with "[Hγ Hγ']") as "[Hγ $]"; first by iFrame.
   iModIntro. iSplitL; last done. iNext; iExists true. iFrame.

theories/proofmode/coq_tactics.v

@@ -623,6 +623,125 @@ Proof.
   - setoid_rewrite <-(right_id emp%I _ (Pout _)). auto.
 Qed.
 
+(** * Covfefe *)
+Definition covfefe (p : bool) (P : PROP) (Q : PROP)
+     (acts : list (envs_action PROP)) (Q' : PROP) :=
+  □?p P ∗ (([∗ list] act ∈ acts, envs_action_to_prop act) -∗ Q') ⊢ Q.
+
+Lemma covfefe_continue {A} (x : A) p P Q : covfefe p P Q [AContinue x p P] Q.
+Proof. by rewrite /covfefe /= right_id wand_elim_r. Qed.
+Lemma covfefe_name i p P Q : covfefe p P Q [ARename i p P] Q.
+Proof. by rewrite /covfefe /= right_id wand_elim_r. Qed.
+Lemma covfefe_fresh p P Q : covfefe p P Q [AFresh p P] Q.
+Proof. by rewrite /covfefe /= right_id wand_elim_r. Qed.
+Lemma covfefe_clear (p : bool) P Q :
+  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) →
+  covfefe p P Q [] Q.
+Proof.
+  intros. rewrite /covfefe /= left_id.
+  destruct p; simpl; by rewrite sep_elim_r.
+Qed.
+Lemma covfefe_pure (p : bool) P Q φ :
+  IntoPure P φ →
+  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) →
+  covfefe p P Q [APure φ] Q.
+Proof.
+  intros ? HPQ. rewrite /covfefe /= right_id. destruct p; simpl.
+  - by rewrite (into_pure P) intuitionistically_affinely wand_elim_r.
+  - destruct HPQ.
+    + by rewrite -(affine_affinely P) (into_pure P) wand_elim_r.
+    + rewrite (into_pure P) -{1}(persistent_absorbingly_affinely ⌜ _ ⌝)%I.
+      by rewrite absorbingly_sep_l wand_elim_r.
+Qed.
+Lemma covfefe_frame p P Q Q' :
+  Frame p P Q Q' →
+  covfefe p P Q [] Q'.
+Proof. intros. by rewrite /covfefe /= left_id. Qed.
+
+Lemma covfefe_and_l (p : bool) P Q P1 P2 res Q' :
+  (if p then IntoAnd p P P1 P2 : Type else
+   TCOr (IntoAnd p P P1 P2) (TCAnd (IntoSep P P1 P2)
+     (TCOr (Affine P2) (Absorbing Q)))) →
+  covfefe p P1 Q res Q' →
+  covfefe p P Q res Q'.
+Proof.
+  rewrite /covfefe /IntoAnd /IntoSep=> HP HP1. destruct p; simpl in *.
+  { by rewrite HP and_elim_l. }
+  destruct HP as [HP|[HP [?|?]]].
+  - by rewrite HP and_elim_l.
+  - by rewrite HP sep_elim_l.
+  - by rewrite HP (comm _ P1) -assoc HP1 sep_elim_r.
+Qed.
+Lemma covfefe_and_r (p : bool) P Q P1 P2 res Q' :
+  (if p then IntoAnd p P P1 P2 : Type else
+   TCOr (IntoAnd p P P1 P2) (TCAnd (IntoSep P P1 P2)
+     (TCOr (Affine P1) (Absorbing Q)))) →
+  covfefe p P2 Q res Q' →
+  covfefe p P Q res Q'.
+Proof.
+  rewrite /covfefe /IntoAnd /IntoSep=> HP HP1. destruct p; simpl in *.
+  { by rewrite HP and_elim_r. }
+  destruct HP as [HP|[HP [?|?]]].
+  - by rewrite HP and_elim_r.
+  - by rewrite HP sep_elim_r.
+  - by rewrite HP -assoc HP1 sep_elim_r.
+Qed.
+
+Lemma covfefe_and (p : bool) P Q P1 P2 res1 res2 Q' Q'' :
+  (if p then IntoAnd true P P1 P2 else IntoSep P P1 P2) →
+  covfefe p P1 Q res1 Q' →
+  covfefe p P2 Q' res2 Q'' →
+  covfefe p P Q (pm_app res1 res2) Q''.
+Proof.
+  rewrite (_ : pm_app = app) // /covfefe /IntoAnd /IntoSep /=. destruct p; simpl.
+  - intros -> HP1 HP2. rewrite intuitionistically_and persistent_and_sep_1.
+    rewrite -HP1 -assoc. apply sep_mono; first done.
+    apply wand_intro_l. rewrite assoc -(comm _ (□ _))%I -assoc.
+    by rewrite big_sepL_app -wand_curry wand_elim_r.
+  - intros -> HP1 HP2. rewrite -HP1 -assoc. apply sep_mono; first done.
+    apply wand_intro_l. rewrite assoc -(comm _ P2)%I -assoc.
+    by rewrite big_sepL_app -wand_curry wand_elim_r.
+Qed.
+
+Lemma covfefe_intuitionistic p P Q P' res Q' :
+  IntoPersistent p P P' →
+  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) →
+  covfefe true P' Q res Q' →
+  covfefe p P Q res Q'.
+Proof.
+  rewrite /covfefe /IntoPersistent /=. destruct p; simpl.
+  - rewrite /bi_intuitionistically. by intros -> _.
+  - intros HP HPQ HP'. destruct HPQ.
+    + by rewrite -(affine_affinely P) HP.
+    + rewrite HP -absorbingly_intuitionistically_into_persistently.
+      by rewrite absorbingly_sep_l HP'.
+Qed.
+
+Lemma covfefe_modal p P Q φ p' P' res Q' Q'' :
+  ElimModal φ p p' P P' Q Q' →
+  φ →
+  covfefe p' P' Q' res Q'' →
+  covfefe p P Q res Q''.
+Proof.
+  rewrite /ElimModal /covfefe /= => HP Hφ HP'.
+  rewrite -HP //. apply sep_mono; first done. by apply wand_intro_l.
+Qed.
+
+Lemma tac_covfefe Δ i p P Q Q' acts :
+  envs_lookup i Δ = Some (p, P) →
+  covfefe p P Q acts Q' →
+  match envs_replace_actions i p acts Δ with
+  | Some (Δ', φs, cs) => pm_foldr (λ P1 P2 : Prop, P1 → P2) (envs_entails Δ' Q') φs
+  | None => False
+  end →
+  envs_entails Δ Q.
+Proof.
+  rewrite envs_entails_eq /covfefe => ? <- HQ'.
+  destruct (envs_replace_actions _ _ _ _) as [[[Δ' φs] cs]|] eqn:Hact; last done.
+  rewrite envs_replace_actions_sound //. apply sep_mono, wand_mono=> //.
+  rewrite -persistent_and_affinely_sep_l. apply pure_elim_l=> Hφs.
+  move: HQ'. clear -Hφs. induction Hφs; simpl; auto.
+Qed.
 End bi_tactics.
 
 (** The following _private_ classes are used internally by [tac_modal_intro] /

theories/proofmode/environments.v

@@ -344,9 +344,60 @@ Definition env_to_prop {PROP : bi} (Γ : env PROP) : PROP :=
   in
   match Γ with Enil => emp%I | Esnoc Γ _ P => aux Γ P end.
 
+Inductive envs_action (PROP : bi) :=
+  | AFresh (p : bool) (P : PROP)
+  | ARename (j : ident) (p : bool) (P : PROP)
+  | AContinue {A} (x : A) (p : bool) (P : PROP)
+  | APure (φ : Prop).
+Arguments AFresh {_} _ _.
+Arguments ARename {_} _ _ _.
+Arguments AContinue {_ _} _ _ _.
+Arguments APure {_} _.
+
+Definition envs_action_to_prop {PROP} (act : envs_action PROP) : PROP :=
+  match act with
+  | AFresh p P | ARename _ p P | AContinue _ p P => □?p P
+  | APure φ => <affine> ⌜ φ ⌝
+  end%I.
+
+Fixpoint envs_replace_actions_filter {PROP}
+    (c : positive) (acts : list (envs_action PROP))
+    (Γp Γs : env PROP) (φs : list Prop) (cont : list (ident * sigT id)) :
+    positive * env PROP * env PROP * list Prop * list (ident * sigT id) :=
+  match acts with
+  | [] => (c,Γp,Γs,pm_reverse φs,pm_reverse cont)
+  | act :: acts =>
+     match act with
+     | AFresh q P =>
+        if q
+        then envs_replace_actions_filter (Pos_succ c) acts (Esnoc Γp (IAnon c) P) Γs φs cont
+        else envs_replace_actions_filter (Pos_succ c) acts Γp (Esnoc Γs (IAnon c) P) φs cont
+     | ARename j q P =>
+        if q
+        then envs_replace_actions_filter c acts (Esnoc Γp j P) Γs φs cont
+        else envs_replace_actions_filter c acts Γp (Esnoc Γs j P) φs cont
+     | AContinue x q P =>
+        if q
+        then envs_replace_actions_filter (Pos_succ c)
+          acts (Esnoc Γp (IAnon c) P) Γs φs ((IAnon c,existT _ x) :: cont)
+        else envs_replace_actions_filter (Pos_succ c)
+          acts Γp (Esnoc Γs (IAnon c) P) φs ((IAnon c,existT _ x) :: cont)
+     | APure φ => envs_replace_actions_filter c acts Γp Γs (φ :: φs) cont
+     end
+  end.
+
+Definition envs_replace_actions {PROP} (i : ident) (p : bool)
+    (acts : list (envs_action PROP)) (Δ : envs PROP) :
+    option (envs PROP * list Prop * list (ident * sigT id)) :=
+  let '(c,Γp,Γs,φs,cont) :=
+    envs_replace_actions_filter (env_counter Δ) acts Enil Enil [] [] in
+  Δ ← envs_simple_replace i p (if p then Γp else Γs) Δ;
+  Δ ← envs_app (beq p false) (if p then Γs else Γp) Δ;
+  Some (envs_set_counter c Δ, φs, cont).
+
 Section envs.
 Context {PROP : bi}.
-Implicit Types Γ : env PROP.
+Implicit Types Γ Γs Γp : env PROP.
 Implicit Types Δ : envs PROP.
 Implicit Types P Q : PROP.
 
@@ -716,4 +767,41 @@ Proof.
   - by rewrite right_id.
   - rewrite /= IH (comm _ Q _) assoc. done.
 Qed.
+
+Lemma envs_replace_actions_filter_sound c acts Γp Γs φs cont c' Γp' Γs' φs' cont' :
+  envs_replace_actions_filter c acts Γp Γs φs cont = (c', Γp', Γs', φs', cont') →
+  ([∗ list] act ∈ acts, envs_action_to_prop act)
+  ∗ <affine> ⌜ Forall id φs ⌝ ∗ □ [∧] Γp ∗ [∗] Γs
+  ⊢ <affine> ⌜ Forall id φs' ⌝ ∗ □ [∧] Γp' ∗ [∗] Γs'.
+Proof.
+  revert c Γp Γs φs cont c' Γp' Γs' φs' cont'.
+  induction acts as [|act acts IH];
+    intros c Γp Γs φs cont c' Γp' Γs' φs' cont' Hact; simplify_eq/=.
+  { by rewrite left_id (_ : pm_reverse = reverse) // Forall_reverse. }
+  destruct act as [[] P|j [] P|A x [] P|φ] eqn:?; (etrans; [|by eapply IH]);
+    rewrite /= ?intuitionistically_and ?and_sep_intuitionistically; try solve_sep_entails.
+  rewrite Forall_cons /= pure_and affinely_and -sep_and. solve_sep_entails.
+Qed.
+
+Lemma envs_replace_actions_sound Δ Δ' i p acts P φs cs :
+  envs_lookup i Δ = Some (p, P) →
+  envs_replace_actions i p acts Δ = Some (Δ', φs, cs) →
+  of_envs Δ ⊢ □?p P ∗
+    (([∗ list] act ∈ acts, envs_action_to_prop act) -∗
+     <affine> ⌜ Forall id φs ⌝ ∗ of_envs Δ').
+Proof.
+  rewrite /envs_replace_actions=> ? Hact.
+  destruct (envs_replace_actions_filter _ _ _ _ _ _)
+    as [[[[c Γp] Γs] φs'] cont] eqn:Hfilter.
+  destruct (envs_simple_replace _ _ _ _) as [Δ1|] eqn:?; simplify_eq/=.
+  destruct (envs_app _ _ _) as [Δ2|] eqn:?; simplify_eq/=.
+  move: Hfilter=> /envs_replace_actions_filter_sound /=. rewrite Forall_nil.
+  rewrite intuitionistically_True_emp affinely_True_emp affinely_emp !right_id.
+  intros ->. rewrite envs_simple_replace_sound // envs_app_sound //.
+  apply sep_mono; first done. apply wand_intro_l.
+  rewrite -!assoc. apply sep_mono; first done.
+  destruct p; simpl.
+  - by rewrite wand_curry assoc wand_elim_r envs_set_counter_sound.
+  - by rewrite !wand_elim_r envs_set_counter_sound.
+Qed.
 End envs.

theories/proofmode/ltac_tactics.v

@@ -1217,6 +1217,96 @@ Tactic Notation "iModCore" constr(H) :=
     |pm_prettify(* subgoal *)].
 
 (** * Basic destruct tactic *)
+Ltac iSolveCovfefe pat :=
+  lazymatch pat with
+  | IFresh =>
+     apply covfefe_fresh
+  | IDrop =>
+     apply covfefe_clear;
+       [pm_reduce; iSolveTC ||
+        let P := match goal with |- TCOr (Affine ?P) _ => P end in
+        fail "iDestruct: cannot clear " P "; not affine and the goal not absorbing"]
+  | IFrame =>
+     apply covfefe_frame;
+       [iSolveTC ||
+        let R := match goal with |- Frame _ ?R _ _ => R end in
+        fail "iDestruct: cannot frame" R]
+  | IIdent ?i =>
+     apply (covfefe_name i)
+  | IPureElim =>
+     eapply covfefe_pure;
+       [iSolveTC ||
+        let P := match goal with |- IntoPure ?P _ => P end in
+        fail "iDestruct:" P "not pure"
+       |pm_reduce; iSolveTC ||
+        let P := match goal with |- TCOr (Affine ?P) _ => P end in
+        fail "iDestruct:" P "not affine and the goal not absorbing"]
+  | IList [[?pat; IDrop]] =>
+     eapply covfefe_and_l;
+       [pm_reduce; iSolveTC ||
+        let P := match goal with |- context [ IntoAnd _ ?P _ _ ] => P end in
+        fail "iDestruct: cannot destruct" P
+       |iSolveCovfefe pat]
+  | IList [[IDrop; ?pat]] =>
+     eapply covfefe_and_r;
+       [pm_reduce; iSolveTC ||
+        let P := match goal with |- context [ IntoAnd _ ?P _ _ ] => P end in
+        fail "iDestruct: cannot destruct" P
+       |iSolveCovfefe pat]
+  | IList [[?pat1; ?pat2]] =>
+     eapply covfefe_and;
+       [pm_reduce; iSolveTC ||
+        let P :=
+          lazymatch goal with
+          | |- IntoSep ?P _ _ => P
+          | |- IntoAnd _ ?P _ _ => P
+          end in
+        fail "iDestruct: cannot destruct" P
+       |iSolveCovfefe pat1
+       |iSolveCovfefe pat2]
+  | IAlwaysElim ?pat =>
+     eapply covfefe_intuitionistic;
+       [iSolveTC ||
+        let P := match goal with |- IntoPersistent _ ?P _ => P end in
+        fail "iDestruct:" P "not persistent"
+       |pm_reduce; iSolveTC ||
+        let P := match goal with |- TCOr (Affine ?P) _ => P end in
+        fail "iDestruct:" P "not affine and the goal not absorbing"
+       |iSolveCovfefe pat]
+  | IModalElim ?pat =>
+     eapply covfefe_modal;
+       [iSolveTC ||
+        let P := match goal with |- ElimModal _ _ _ ?P _ _ _ => P end in
+        let Q := match goal with |- ElimModal _ _ _ _ _ ?Q _ => Q end in
+        fail "iMod: cannot eliminate modality" P "in" Q
+       |solve [iSolveSideCondition] ||
+        fail "iDestruct: `>`-pattern only supported with trivial side-conditions"
+       |iSolveCovfefe pat]
+  | _ => apply (covfefe_continue pat)
+  end.
+
+Tactic Notation "iCovfefe" constr(H) "as" constr(pat) "with" tactic(tac) :=
+  let rec go_cont cs :=
+    lazymatch cs with
+    | [] => idtac
+    | (?i, existT intro_pat ?pat) :: ?cs => tac i pat; go_cont cs
+    end in
+  let pat := intro_pat.parse_one pat in
+  notypeclasses refine (tac_covfefe _ H _ _ _ _ _ _ _ _);
+    [pm_reflexivity || fail "iDestruct:" H "not found"
+    |iSolveCovfefe pat
+    |lazymatch goal with
+     | |- context K [ envs_replace_actions ?i ?p ?acts ?Δ ] =>
+        lazymatch eval pm_eval in (envs_replace_actions i p acts Δ) with
+        | None => fail "iDestruct: name clash"
+        | Some (?Δ, ?φs, ?cs) =>
+           let res := context K [Some (Δ, φs, cs)] in
+           convert_concl_no_check res; pm_reduce;
+           repeat intro;
+           go_cont cs
+        end
+     end].
+
 Local Ltac iDestructHypGo Hz pat :=
   lazymatch pat with
   | IFresh =>
@@ -1228,16 +1318,15 @@ Local Ltac iDestructHypGo Hz pat :=
   | IFrame => iFrameHyp Hz
   | IIdent ?y => iRename Hz into y
   | IList [[]] => iExFalso; iExact Hz
-  | IList [[?pat1; IDrop]] => iAndDestructChoice Hz as Left Hz; iDestructHypGo Hz pat1
-  | IList [[IDrop; ?pat2]] => iAndDestructChoice Hz as Right Hz; iDestructHypGo Hz pat2
-  | IList [[?pat1; ?pat2]] =>
-     let Hy := iFresh in iAndDestruct Hz as Hz Hy; iDestructHypGo Hz pat1; iDestructHypGo Hy pat2
   | IList [[?pat1];[?pat2]] => iOrDestruct Hz as Hz Hz; [iDestructHypGo Hz pat1|iDestructHypGo Hz pat2]
   | IPureElim => iPure Hz as ?
   | IRewrite Right => iPure Hz as ->
   | IRewrite Left => iPure Hz as <-
-  | IAlwaysElim ?pat => iIntuitionistic Hz; iDestructHypGo Hz pat
-  | IModalElim ?pat => iModCore Hz; iDestructHypGo Hz pat
+  | IList [[_; IDrop]] => iCovfefe Hz as pat with iDestructHypGo
+  | IList [[IDrop; _]] => iCovfefe Hz as pat with iDestructHypGo
+  | IList [[_; _]] => iCovfefe Hz as pat with iDestructHypGo
+  | IAlwaysElim _ => iCovfefe Hz as pat with iDestructHypGo
+  | IModalElim _ => iCovfefe Hz as pat with iDestructHypGo
   | _ => fail "iDestruct:" pat "invalid"
   end.
 Local Ltac iDestructHypFindPat Hgo pat found pats :=

theories/proofmode/reduction.v

@@ -14,6 +14,7 @@ Declare Reduction pm_eval := cbv [
   envs_simple_replace envs_replace envs_split
   envs_clear_spatial envs_clear_intuitionistic envs_set_counter envs_incr_counter
   envs_split_go envs_split env_to_prop
+  envs_replace_actions_filter envs_replace_actions
   (* PM list and option combinators *)
   pm_app pm_rev_append pm_reverse pm_foldr
   pm_option_bind pm_from_option pm_option_fun