feat: port gmultiset big-operators (big_opMS/big_sepMS)

[lihaokun]

Description

Port of Coq Iris's gmultiset big-operators — big_opMS (algebra/big_op.v) and big_sepMS (bi/big_op.v) — addressing the Multisets subtask of #260. iris-lean abstracts its finite collections rather than porting stdpp's concrete types 1:1 (cf. FiniteSet/GenSets ↔ stdpp fin_sets, with big_opS generic over FiniteSet), so this introduces an abstract FiniteMultiSet typeclass and defines bigOpMS/bigSepMS generically over it, mirroring the FiniteSet/bigOpS/bigSepS structure. All proved, 0 sorry.

Iris/Iris/Std/GenMultiSets.lean — the interface

MultiSet / LawfulMultiSet / FiniteMultiSet / LawfulFiniteMultiSet: a Nat-valued multiplicity (the multiset analog of ∈), ⊎ (multiset sum) alongside ∪/∩/∖, toList, the multiplicity/toList laws, ext, and ind (Coq gmultiset_ind). It is FiniteSet minus nodup, plus ⊎ and multiplicity — exposing exactly what the big-operators need.

Iris/Iris/Algebra/BigOp.lean — bigOpMS (16 @[rocq_alias] + 11 #rocq_ignore)

bigOpMS o f X := bigOpL o (fun _ x => f x) (toList X) + [^ o mset] notation; the empty/singleton/disj_union/insert/delete/unit/op/ne/proper/gen_proper/ext/elements/closed lemmas and the hom/hom_weak monoid homomorphisms. The #rocq_ignores match big_opS's exactly: the ne'/proper' Proper instances, the cross-big-op opL/opM/opS/opMS (proven at BI level as bigSepMS_comm_*), the Leibniz _L variants, and the unseal machinery.

Iris/Iris/BI/BigOp/{BigOp,BigSepMSet}.lean — bigSepMS (44 @[rocq_alias])

bigSepMS := bigOpMS sep + [∗mset] notation, and the full big_sepMS_* suite: mono/proper/ne, empty/singleton/disj_union/insert/delete, the persistent/affine/timeless instances, sep/and/wand, elem_of(_acc)(_acc_impl), pure(_1)/affinely_pure_2, intro/impl/forall, persistently, later(_2)/laterN(_2), subseteq, sepL/sepM/sepS/sepMS, and dup. Hooked into Iris/BI/BigOp.lean.

Iris/Iris/BI/Embedding.lean — follow-up

embed_big_sepMS / embed_big_sepMS_2, previously #rocq_ignored pending this port, become one-liners via BigOpMS.hom (mirroring embed_big_sepS).

Scope

Every Coq big_opMS_*/big_sepMS_* in algebra/big_op.v and bi/big_op.v is aliased or justifiably ignored (checked against ROCQ_REVISION b9b6cf04). The big_sepMS_{bupd,fupd,plain,plainly,objective} and big_opMS_{own,auth_frag,view_frag,None,singletons} that live in bi/updates.v, bi/plainly.v, bi/monpred.v, algebra/{auth,view,gmultiset}.v, and base_logic/lib/own.v are out of scope — they belong to those modules' ports and are unblocked as follow-ups by this PR.

Checklist

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

Addresses the Multisets subtask of #260.