feat: more expressive semiOutParam attribute for ipm_class declarations

[alvinylt]

Description

The InOut datatype defined in ProofModeM/SynthInstance.lean is used along with semiOutParam in IPM type class declarations. Currently, we are reusing the attribute semiOutParam from the core Lean libraries (Init.Prelude), except that the semi-output parameters must be preceded by an InOut value so that it is clear whether particular type class instances require that parameter to be an input or an output.

The type class IsOp, introduced in PR #401, is an example where semiOutParam is used:

class IsOp [CMRA α] (_ : InOut) (a : semiOutParam α) (_ : InOut) (b1 : semiOutParam α) (_ : InOut) (b2 : semiOutParam α)

We express IsOp .in a .out b1 .out b2 for the splitting operation and IsOp .out a .in b1 .in b2 for the merging operation. If we would like to use the type class for both directions, then currently the only way to do that is to parameterise all three InOut arguments. That is, IsOp ioa a iob1 b1 iob2 b2 where ioa, iob1 and iob2 are arbitrary. However, this is quite inelegant as we know that b1 and b2 must always be the opposite of a.

My suggestion with this PR is to modify semiOutParam to remove the restriction that the InOut value must be the immediately preceding argument. Instead, we have the semiOutParamIPM attributes with two more explicit arguments to specify which InOut value to use. With io : InOut := .in, semiOutParamIPM io α false (or semiOutParamIPM io α) refers to an input parameter and semiOutParamIPM io α true refers to an output parameter. Likewise, with io : InOut := .out, semiOutParamIPM io α false (or semiOutParamIPM io α) refers to an output parameter and semiOutParamIPM io α true refers to an input parameter.

In fact, there is no longer any restriction for the InOut value to be a parameter in the type signature of the type class. In other words, we are able to use pattern matching, conditional branching and any reducible function to map other types of values to an InOut value.

With this design, IsOp is reformulated as follows, where d : IsOp.Direction is either .merge or .split.

class IsOp [CMRA α]
    (d : IsOp.Direction) (a : semiOutParamIPM d.mapToInOut α)
    (b1 : semiOutParamIPM d.mapToInOut.negate α)
    (b2 : semiOutParamIPM d.mapToInOut.negate α) where
  is_op : a ≡ b1 • b2

There is then no need for one to think about the underlying details of type class synthesis when defining an IsOp instance.

There are six IPM type classes in the codebase that use semi-output parameters.

• AsEmpValid
• FromWand
• IntoWand
• FromAssumption
• FromPure
• IsOp

In fact, there is a similar situation with AsEmpValid, where the PROP and bi always practically have the same type class synthesis direction. As a result, it has also benefited from this PR:

class AsEmpValid (d : AsEmpValid.Direction) (φ : Prop)
    (PROP : semiOutParamIPM d.mapToInOut $ Type _)
    (bi : semiOutParamIPM d.mapToInOut $ BI PROP)
    (P : outParam $ PROP)

This is meant to just be a syntactic improvement, so there should not be any impact on the type class synthesiser's behaviour. The core of this implementation is the type signature parsing in ProofModeM/SynthInstanceAttr.lean. Since we now have semiOutParamIPM, any use of semiOutParam in type class declarations with the ipm_class annotation is explicitly rejected to avoid confusion.

A caveat is that, for regular type class declarations (i.e., those without the ipm_class annotation), the attribute semiOutParamIPM is ignored. These two attributes are relevant to IPM type classes only and should not be used for regular, non-IPM type classes anyway.

As we are not reusing Lean's built-in semiOutParam attribute, a side effect is that the built-in type class synthesiser is unable to recognise that an argument is a semi-output parameter. This is a problem when an IPM type class is defined in terms of some non-IPM type classes. In this case, the type class synthesis for the non-IPM type classes by default uses the built-in type class synthesiser. Originally, with the semiOutParam attribute, Lean's built-in synthesiser is able to defer a premise whose type still mentions an unresolved semi-out parameter. This is why synthInstanceMainCore is slightly modified to handle the deferral explicitly.

Checklist

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