feat: iframe tactic and input/output handling for IPM synthesis

[MackieLoeffel]

Description

Implement the iframe tactic and make it available in specialization patterns and cases patterns.

Additional implement input / output handling to IPM synthesis roughly in the style of Hint Mode in Rocq. See the comment on ParamKind for a detailed description:

The parameters of a class declared with `ipm_class` are categorized into the following categories:

1. in: This is the default for a parameter when not annotated in another way.
2. out: These are parameters marked with `outParam`. These parameters must be mvars when starting typeclass search.
3. semiOut: These are parameters marked with `semiOutParam`. The preceding parameter must be of type `InOut`. The value of the `InOut` parameter decides whether the `semiOut` parameter is treated as an input or an output.
4. uncheckedIn: These are parameters marked with `uncheckedInParam`. These behave like `in` parameters, but allow mvars to match terms (see below).
5. inout: Parameters of type `InOut`, must appear before semiOut parameters (see above).

The following constraints apply to the parameters: (In the following, semiOut parameters are treated as inputs if the preceding `InOut` is `in` and as outputs if the `InOut` is `out`.)
1. semiOut parameters must have a preceding `InOut` parameter.
2. For each synthesis problem, all output parameters must be mvars.
3. When an input parameter is a mvar, it is not considered to match an instance which does not have an mvar at the top-level. This is to prevent accidentally instantiating mvars. Note that this only applies for mvars the top-level (matching the behavior of Hint Mode : ! in Rocq), since this is the simplest version to implement and catches most (all?) of the cases.

Checklist

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

[lzy0505]

Amazing work! I’ll review it this week.