Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 170
    • Issues 170
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 23
    • Merge requests 23
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Issues
  • #428
Closed
Open
Issue created Jul 22, 2021 by Robbert Krebbers@robbertkrebbersMaintainer

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.

Edited Jul 22, 2021 by Robbert Krebbers
Assignee
Assign to
Time tracking