feat: remaining specialisation patterns

[alvinylt]

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:

• program_logic/total_weakestpre.v: add_modal_fupd_twp
• proofmode/class_instances_embedding.v: add_modal_embed_bupd_goal, add_modal_embed_fupd_goal
• proofmode/monpred.v: add_modal_at_bupd_goal, add_modal_at_fupd_goal

Other Changes

• Similar to the changes in PR feat: remaining introduction patterns and case destruction patterns #496, SpecPat.parse is extended to return a pair for Syntax and specPat values so that processWand can use withRef to provide more precise syntax highlighting for error messages.

• 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