feat: Port algebra/proofmode_classes.v (IsOp and related type classes)

[alvinylt]

Description

Ports algebra/proofmode_classes.v by implementing IsOp, its relevant type classes and type class instances.

Addresses #229.

Instances of these type classes exist in the following files but are yet to be ported.

• algebra/lib/frac_auth.v: frac_auth_is_op, frac_auth_is_op_core_id
• base_logic/lib/own.v: into_sep_own, into_and_own, from_sep_own, combineSepAs_iOwn, from_and_own_persistent
• algebra/dfrac.v: dfrac_is_op
• algebra/view.v: view_frag_is_op, view_auth_dfrac_is_op
• algebra/auth.v: auth_frag_is_op, auth_auth_dfrac_is_op

The following files are yet to be ported but includes instances of IsOp or relevant type classes.

• algebra/gmap.v
• algebra/numbers.v
• algebra/frac.v
• algebra/lib/gmap_view.v
• algebra/lib/mono_list.v
• algebra/lib/mono_nat.v
• algebra/lib/mono_Z.v
• algebra/lib/ufrac_auth.v
• base_logic/lib/ghost_var.v
• algebra/dyn_reservation_map.v
• algebra/reservation_map.v
• algebra/ufrac.v
• base_logic/proofmode.v

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

[MackieLoeffel]

Instead of having all these different versions of the IsOp typeclass as in Rocq, I think it should work to have a single IsOp typeclass if one is careful about how to set the input and output parameters using InOut. See here for an explanation how the input output handling works in the proof mode TC synthesis.

[MackieLoeffel]

Please also add instances for the IsOp typeclass and also the instances that use IsOp such that one can test whether it does the right thing.

[MackieLoeffel]

Please also add a comment here how IsOp can be used (i.e. both for merging and for splitting). You can base it on the comment in the Rocq version, but note that the details of TC search are different..