Skip to content

fix: Wrong priorities of AndIntoSep instances #555

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
MackieLoeffel merged 4 commits into from
Jul 31, 2026
+20 −1
Merged

fix: Wrong priorities of AndIntoSep instances #555

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
7962c99
`AndIntoSep` fix
lzy0505 Jul 30, 2026
1d51530
Merge branch 'master' into zliu/fix-icase-affine
lzy0505 Jul 30, 2026
bdd4d14
Fix
lzy0505 Jul 30, 2026
360b411
fix fix
MackieLoeffel Jul 31, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 3 additions & 2 deletions Iris/Iris/ProofMode/Instances.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -414,12 +414,13 @@ instance (priority := default + 10) fromSep_persistently [BI PROP] (P Q1 Q2 : PR
from_sep := persistently_sep_mpr.trans (persistently_mono h.1)

-- AndIntoSep
@[ipm_class, rocq_alias AndIntoSep]
@[ipm_backtrack, rocq_alias AndIntoSep]
Comment thread
MackieLoeffel marked this conversation as resolved.
Outdated
class inductive AndIntoSep {PROP} [BI PROP] : PROP → outParam PROP → PROP → outParam PROP → Prop
| affine (P Q Q' : PROP) [Affine P] [h : FromAffinely Q' Q] : AndIntoSep P P Q Q'
| affinely (P Q : PROP) : AndIntoSep P iprop(<affine> P) Q Q

attribute [instance] AndIntoSep.affine AndIntoSep.affinely
attribute [instance (default + 10)] AndIntoSep.affine
attribute [instance] AndIntoSep.affinely

-- IntoSep
@[rocq_alias into_sep_sep]
Expand Down
19 changes: 19 additions & 0 deletions Iris/Iris/Tests/Tactics.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1892,6 +1892,25 @@ example [BI PROP] (Q : PROP) : □ Q ⊢ Q := by
iintro H
icases H with ⟨HA, HB⟩

/- Tests `AndIntoSep` instances -/
/--
error: unsolved goals
PROP : Type u_1
inst✝¹ : BI PROP
inst✝ : BIAffine PROP
P Q : PROP
⊢
□x✝ : P
∗R : <pers> Q
⊢ Q
-/
#guard_msgs in
example [BI PROP] [BIAffine PROP] (P Q : PROP) :
(□ P) ∧ <pers> Q ⊢ Q := by
iintro H
icases H with ⟨#_, R⟩


/-- Tests `icases` with a case destruction pattern for rewriting pure equalities -/
example [BI PROP] (m n : Nat) (a b c : Prop) :
⊢@{PROP} ⌜m = 2⌝ -∗ ⌜3 = n⌝ -∗ ⌜a = b⌝ -∗ ⌜b = c⌝ -∗ ⌜m.succ = n ∧ a = c⌝ := by
Expand Down