Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 193
    • Issues 193
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 19
    • Merge requests 19
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Artifacts
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Model experiments
  • 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

`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