Make `iDestruct` work on `▷ ∃` if goal is except_0/update
BIs have the interesting rule bi.later_exist_except_0
which allows to commute ▷
and ∃ x : A
even if the domain A
of the existential is not inhabited:
bi.later_exist_except_0 : ▷ (∃ a : A, Φ a) -∗ ◇ (∃ a : A, ▷ Φ a)
Instead, you get an except-0 (◇
) modality, which can be eliminated if the goal is, for example, an update modality.
This trick is not commonly known, so it would be great if the proof mode's iDestruct
tactic could use bi.later_exist_except_0
automatically instead of just failing when the domain A
is not inhabited.
This is what happens now:
From iris.proofmode Require Import tactics.
From iris.bi Require Import updates.
Lemma test `{BiFUpd PROP} {A} (Φ : A → PROP) (Q : PROP) E :
▷ (∃ x, Φ x) ={E}=∗ Q.
Proof.
iIntros "H".
(* Goal:
"H" : ▷ (∃ x : A, Φ x)
--------------------------------------∗
|={E}=> Q *)
(* Tactic failure: iExistDestruct: cannot destruct (▷ (∃ x : A, Φ x))%I. *)
Fail iDestruct "H" as (x) "H".
(* Works *)
iMod (bi.later_exist_except_0 with "H") as (x) "H".
I tried to implement what I proposed in this MR some day, but I could not find a satisfactory generalization of the IntoExist
class. After all, that class then needs to take the goal into account to eliminate the ◇ modality.
An alternative, we could use the pm_error
infrastructure from #413 (which still needs to be ported to IntoExists
) to give an error that points the user to bi.later_exist_except_0
in case the domain A
is not inhabited.