feat: port HeapLang pure step tactics

[kdvkrs]

Description

Port the wp_pure wrapper tactic family from iris_heap_lang/proofmode.v: wp_lam, wp_let, wp_seq, wp_closure, wp_if, wp_if_true, wp_if_false, wp_proj, wp_inj, wp_pair, wp_unop, wp_binop, wp_op, wp_case, and wp_match.

The Lean implementation follows the Rocq implementation with these tactics being mostly thin wrappers around wp_pure.

Raise the precedence of wp_pure's focus argument to hl_exp:10 mirroring wp_bind. At default precedence, e.g. wp_pure <pat>; wp_lam misparses the ; as focus pattern instead of sequencing.

Add a test section per tactic covering at least one successful and one failing case.

Partially addresses #480

AI Disclaimer: I am familiar with the Iris-Rocq HeapLang tactic implementation and used Claude Code to help navigate the codebase and assist with testcase boilerplate.

Checklist

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

[lzy0505]

Thanks for the PR! It looks good and is ready for merging.

One minor thing: the error messages mentioning other tactics are a bit confusing. Worth opening an issue to resolve later.

[alvinylt]

One minor thing: the error messages mentioning other tactics are a bit confusing. Worth opening an issue to resolve later.

@lzy0505 Are you referring to, for example, an error thrown by wp_lam with the error message mentioning iapply?

This has actually been an issue with some existing IPM tactics (see one of the example proofs in Tests/Tactics.lean) when functions in the IPM tactic implementation hard-code the error message. This problem is particularly obvious when introduction/cases/specialisation patterns are used in many tactics, and functions such as iCasesCore, iIntroCore and iSpecializeCore are shared amongst them.

I have (partially) addressed this in some of the open PRs by passing the tactic names to the functions that uses throwError (see example), but I think a possible, better solution is to extend ProofModeM with the tactic name as a field so that we only have to pass the tactic name once when ProofModeM.runTactic is called, and to define a new function (e.g. throwIPMError) to prepend the correct IPM tactic name before throwing the error.

[lzy0505]

@alvinylt Yes. We should address this systematically. Extending ProofModeM seems reasonable.