GitLab

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.