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 169
    • Issues 169
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 24
    • Merge requests 24
  • 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
  • #422
Closed
Open
Issue created Jun 14, 2021 by Robbert Krebbers@robbertkrebbersMaintainer

`iApply` does not use `FromAssumption` for goal matching

From iris.proofmode Require Import tactics.

Typeclasses eauto := debug.

Lemma foo {PROP : bi} (P Q : PROP) :
  (P -∗ □ Q) -∗ Q.
Proof.
  iIntros "H".
  Fail iApply "H".
  iApply ("H" with "[]").
Admitted.

Lemma bar {PROP : bi} (P : PROP) (Q : nat → PROP) :
  (P -∗ ∀ n, Q n) -∗ Q 10.
Proof.
  iIntros "H".
  Fail iApply "H".
  iApply ("H" with "[]").
Admitted.

When using iApply in combination with the with clause, it will first iSpecialize and then use iApply, which in these examples turns to the degenerate case of iExact. The iExact tactic uses FromAssumption to deal with minor mismatches between the hypothesis and the goal. For example, it will eliminate ∀s and modalities (like □).

When using iApply without the with clause, it will launch a search using IntoWand where the goal with unified with the conclusion of the lemma. If there's a mismatch (like the ones above), it will fail.

The problem is the instance:

Global Instance into_wand_wand p q P Q P' :
  FromAssumption q P P' → IntoWand p q (P' -∗ Q) P Q.

Here, Q should match exactly. I tried strengtening it to:

Global Instance into_wand_wand p q P Q P' Q' :
  FromAssumption q P P' →
  FromAssumption (p && q) Q' Q →
  IntoWand p q (P' -∗ Q') P Q.

However, that causes other problems: in some cases the above instance will be triggered instead of instances like into_wand_bupd_args causing the following to go wrong:

Lemma fooz `{!BiBUpd PROP} (P Q : PROP) :
  (P -∗ Q) -∗ |==> Q.
Proof.
  iIntros "H".
  iApply "H". (* should be [|==> P], but will be [P] with the new [into_wand_wand] *)

This issue came up in practice Simuliris.

Assignee
Assign to
Time tracking