feat: remaining introduction patterns and case destruction patterns

[alvinylt]

Description

Implements the remaining introduction patterns and case destruction patterns.

Addresses #213 and #239.

Features that are only used with iintro on the top level are implemented as introduction patterns in IntroPattern.lean and Intro.lean.

Feature in Rocq	Corresponding constructor in IntroPat	Remarks	Ported?
IForall (*)	all (*)	Introduces all universal quantifiers.	✓
IAll (**)	allwand (**)	Introduces all universal quantifiers, pure arrows and wands.	✓
IPureIntro (!%)	pureintro (!%)	Introduces a pure proof goal, which is basically the same as running ipureintro. This does not necessarily have to be the last in the introduction pattern sequence. If there are further introduction patterns, attempt to enter IPM again and handle the rest of the patterns. This means applying iintro !% %_ !% to ⊢@{PROP} ⌜⌜ϕ⌝ ⊢@{PROP} ⌜ϕ⌝⌝ works.	✓
ISimpl (/=)	simp (/=)	Apply dsimp. Using dsimp instead of simp here so that it resembles the use of simpl in Rocq. To solve the goal directly, one can use //= instead (see below).	✓
IDone (//=)	simptrivial (//=)	Shorthand for applying /= and then //.	✓
IClear ({ selPat })	clear ({ selPatFrame* })	The new syntax selPatFrame is an optional ! followed by a selection pattern. Hypotheses chosen by selection pattern without ! are cleared from the context.	✓
IClearFrame ({ $selPat })	clear ({ selPatFrame* })	Similar to the above feature. Hypotheses chosen by the selection pattern with a leading ! are framed. Using ! instead of $ because the latter is used for anti-quotation in Lean, which would otherwise cause parsing errors, particularly for $#, $∗, etc.	✓

One feature that is not only used with iintro but also with other tactics (e.g., icases) is implemented as a case destruction pattern in CasesPattern.lean and Cases.lean.

Feature in Rocq	Corresponding constructor in iCasesPat	Description	Ported?
IRewrite (<-, ->)	rewrite (←, →)	Rewrite using a pure Lean equality and then remove the equality hypothesis from the context. This also works as an introduction pattern when a pure Lean equality ϕ exists as a pure premise or ⌜ϕ⌝ exists as a wand premise.	✓

Another feature is related to ipure and other tactics involving case destruction patterns.

Feature in Lean	Description	Ported?
Pure destruction patterns	Extending ipure and other IPM tactics so that pure hypotheses can be destructed using the built-in destruction patterns in Lean. For example, given p ∧ q → ⊢ □ ⌜((a ∧ b) ∧ c)⌝ -∗ P -∗ Q -∗ R, one should be able to apply iintro %⟨hp, hq⟩ %⟨⟨ha, hb⟩, hc⟩ HP HQ.	✓ (see the related diff)

Here we are re-using the built-in syntax rcasesPat and functions in RCases.lean for rintro/rcases, which is more expressive than intro/cases.

Other Changes

• Some code refactoring in Clear.lean and Pure.lean so that features in relation to iclear can be reused for the new introduction patterns.
• For iFrame in Frame.lean and iCasesCore in Cases.lean, the arguments bi and e are made implicit as they can always be inferred using other arguments.
• Added a line in SelPattern.lean to use addLocalVarInfo for prettier syntax highlighting of pure hypotheses in the selection patterns.
• Generalised the type signature of the continuation function k for iIntroCore in Intro.lean so that the level u is universally quantified. Similar to the change to ProofModeContinuation in PR feat: iinduction #430.
• Minor improvement: iIntroCore and iCasesCore takes a string (tactic name) as an argument so that they print more accurate error messages. Same for some functions that iIntroCore and iCasesCore use.
• The new field ref : Syntax is introduced into iCasesPat so that iCasesCore uses withRef for more precise syntax highlighting of errors. This resolves a to-do comment added in a previous commit.

Before using withRef in iCasesCore:

After using withRef in iCasesCore:

• Added docstring comments to syntax declarations in relation to casesPat, introPat and specPat for pop-up descriptions when one hovers over the patterns. Similar to PR doc: tactic descriptions with docstrings #464, where docstrings annotate elaborations for tactics.

• In the .one case in iCasesCore, use Hyps.addWithInfo instead of .mkHyp and .mkSep. The previous approach ensures that, when the Hyps instance is an .emp, the new hypothesis is added using .mkHyp rather than .mkSep. The function Hyps.add (which is in turn used by Hyps.addWithInfo) was not able to handle this automatically, which prevented iCasesCore from using Hyps.addWithInfo directly. The function Hyps.addWithInfo is now updated to handle this. See commit c59afb6 for the relevant changes. This resolves two to-do comments made in a previous commit.

Checklist

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