Skip to content

feat: remaining specialisation patterns - #500

Open
alvinylt wants to merge 113 commits into
leanprover-community:masterfrom
ISTA-PLV:SpecPats
Open

feat: remaining specialisation patterns#500
alvinylt wants to merge 113 commits into
leanprover-community:masterfrom
ISTA-PLV:SpecPats

Conversation

@alvinylt

@alvinylt alvinylt commented Jul 5, 2026

Copy link
Copy Markdown
Contributor

Description

Implements the remaining specialisation patterns.

Addresses #215 and #239.

Feature in SpecPat Remarks Ported?
Nested specialisation patterns (.ident with specialisation patterns) The functions processWand and iSpecializeCore are now mutual definitions. Similarly, pmTerm and specPat are defined by mutual induction, so the definitions in ProofModeTerm.lean are moved into SpecPattern.lean.
Subgoal for persistent premise (.goal with kind := .persistent) For the specialisation pattern [# $H₁ … $Hₙ ], where H₁ … Hₙ are framed. Every hypotheses must be preceded by $ as persistent premises do not consume spatial hypotheses, otherwise processWand throws a runtime error.
Auto-framing for persistent premise (.autoframe .persistent) For the specialisation pattern [#$].
Subgoal for premise with modality (.goal with kind := .modal) For the specialisation pattern [> $H₁ … $Hₙ ]. This requires porting the type class AddModal and its instances. One of the instances uses wandM, which is being ported in PR #470 for iinv.
Auto-framing for premise with modality (.autoframe .modal) For the specialisation pattern [>$].

The original SpecializeState contains the field pf : Q($orig ⊢ $e ∗ □?$p $out), but orig ⊢ e ∗ □?p out does not hold in general when the specialisation patterns involve .autoframe .modal or .goal with kind := .modal. The assertion therefore has to be weakened as (e ∗ □?p out ⊢ goal) → orig ⊢ goal. The problem is that e ∗ □?p out ⊢ goal is still required by the theorem specialize_dup_context for context duplication. The current solution is to have (e ∗ □?p out ⊢ goal) → orig ⊢ goal as a mandatory field and orig ⊢ e ∗ □?p out as an optional field in SpecializeState. Context duplication is possible only when the proof orig ⊢ e ∗ □?p out exists. Context duplication is mutually exclusive with specialisation patterns involving modalities.

The missing AddModal instances are also being ported. This addresses #237 in full, as well as #255 and #400 in part.

AddModal instance Located in ... (Rocq) Located in.. (Lean) Ported?
add_modal_fupd_wp weakestpre.v WeakestPre.lean
add_modal_forall class_instances.v Instances.lean
add_modal_tforall class_instances.v Instances.lean
add_modal_wand class_instances.v Instances.lean
add_modal_wandM class_instances.v Instances.lean
add_modal_except_0 class_instances_later.v InstancesLater.lean
add_modal_except_0_later class_instances_later.v InstancesLater.lean
add_modal_later class_instances_later.v InstancesLater.lean
add_modal_later_except_0 class_instances_later.v InstancesLater.lean
add_modal_bupd class_instances_updates.v InstancesUpdates.lean
add_modal_fupd class_instances_updates.v InstancesUpdates.lean
add_modal_id classes.v Classes.lean

There are also several modules yet to be ported in which AddModal instances are located:

Other Changes

More syntax highlighting using withRef

  • Docstrings are added for the specialisation pattern syntax, similar to the changes in PR doc: tactic descriptions with docstrings #464.
  • Bug fix: use ProofModeM.trySynthInstance instead of the built-in synthesiser (trySynthInstance) for type classes with the ipm_class annotation.
  • Added missing ipm_backtrack annotations to the type class instances intoAnd_sep, intoAnd_sep_affine and intoAbsorbingly_absorbing.
  • The function argument e for iFrame is made implicit as it can always be inferred using hyps.

Checklist

  • My code follows the mathlib naming and code style conventions
  • I have added my name to the authors section of any appropriate files

alvinylt added 30 commits July 4, 2026 16:51
…frame .spatial`

Proofs for `.autoframe .spatial` not yet complete
…ted `iSpecializeCore` and `iHave` signature
Comment thread Iris/Iris/ProofMode/Patterns/SpecPattern.lean Outdated
Comment thread Iris/Iris/ProofMode/Patterns/SpecPattern.lean Outdated
Comment thread Iris/Iris/ProofMode/Patterns/SpecPattern.lean Outdated
Comment thread Iris/Iris/ProofMode/Tactics/Rewrite.lean Outdated
Comment thread Iris/Iris/ProofMode/Tactics/Specialize.lean Outdated
alvinylt added a commit to ISTA-PLV/iris-lean that referenced this pull request Jul 30, 2026
@alvinylt
alvinylt requested a review from MackieLoeffel August 2, 2026 14:06
q(specialize_forall (A2 := $e) (p := $p) $inst $x)
return specState.update hyps p out' pfStep
-- Subgoal with `[ H₁ … Hₙ ]` or `[- H₁ … Hₙ ]`
| .goal { kind := .spatial, negate, trivial, frame := f, hyps := hs } g => do

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The cases for .spatial, .intuitionistic, and .modal are very similar. Can you combine them into one case with some if statements to avoid the duplication? Then one can also maybe avoid some of the helper functions.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is tricky: the cases .spatial, intuitionistic and .modal are all different in terms of the type classes synthesis steps and theorems used. For any two of the three cases, there is at most one common line of code, but there isn't any part of the code shared by all three cases.

Instead, it makes more sense to deduplicate code with the following pairing:

  • .goal with .kind := .spatial ([ H1 ... ], [- H1 ... ]) and .autoframe with .kind := .spatial ([$])
  • .goal with .kind := .intuitionistic ([ #H1 ... ]) and .autoframe with .kind := .intuitionistic ([#$])
  • .goal with .kind := .modal ([> H1 ... ], [>- H1 ... ]) and .autoframe with .kind := .modal ([>$])

I have refactored the code so that all these cases processSpecGoal, which then does pattern matching on .kind.

The deduplication is minimal (code reduced by 16 lines), but since we are moving plenty of things out of the mutual induction block, the build time seems to be significantly reduced.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Commit: 0631755

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think you can unify the spatial and modal cases if you use the trivial AddModal instance for the spatial case (i.e. prove AddModal for the spatial case using addModal_id).

Good observation that moving things out of the mutual induction block reduces build time!

Comment thread Iris/Iris/ProofMode/Tactics/Specialize.lean Outdated
Comment thread Iris/Iris/ProofMode/Tactics/Specialize.lean Outdated
Comment thread Iris/Iris/ProofMode/InstancesLater.lean
Comment thread Iris/Iris/ProofMode/InstancesLater.lean Outdated
Comment thread Iris/Iris/ProofMode/Porting.lean Outdated
Comment thread Iris/Iris/ProofMode/Tactics/Specialize.lean Outdated
Comment thread Iris/Iris/ProofMode/Tactics/Specialize.lean Outdated
Comment thread Iris/Iris/ProofMode/Tactics/Specialize.lean Outdated
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants