refactor: Simplify Heaps API

[markusdemedeiros]

Description

While the initial heaps API was sufficient for porting and using potentially infinite map-like resources, PR #131 defines a richer theory for finite maps which is not compatible with the existing API. In this PR, I refactor the heaps API and CMRA's so that both formalizations can be supported under the same framework.

This PR is currently a work in progress, however there are three major changes so far.

• Require all heaps to be higher-kinded. The old typeclass for Heaps had the form Store T K V, representing the notion that the type T behaved as a (total) map K -> V. This would allow the use of specialized data structures which were not able to represent all possible value types. Now, the PartialMap (T : Type _ -> Type) K typeclass can only support types that are capable of holding any value, but this substantially simplifies the interface. In particular, the hhmap and dmap classes can be removed in favour of requiring the type T be functorial.
• Partiality by default. Store T K V was a type of total maps, and (partial) heaps extended ``Heap T K (Option V)`. This was counterintuitive, and in hindsight, not necessary.
• Move from equality (and ext in the FiniteMaps interface) to pointwise equality.

The Finite Maps section from #131 will be likely be changed substantially. Lemmas which do not use finiteness are being generalized to PartialMap. I am planning on inverting the FiniteMap hierarchy to better match the typeclass-based approach in stdpp.

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

Generative AI Guidelines

AI assistance is permitted when making contributions to Iris-Lean, however, generative AI systems tend to produce code which takes a long time to review.
Please carefully review your code to ensure it meets the following standards.

• Your PR should avoid duplicating constructions found in Iris-Lean or in the Lean standard library.
• have statements that do not aid readability or code reuse should be inlined.
• Your proofs should be shortened such that their overall structure is explicable to a human reader. As a goal, aim to express one idea per line.
• In general, proofs should not perform substantially more case splitting than their Rocq counterparts.

In our experience, a good place to begin refactoring is by re-arranging and combining independent tactic invocations.
We also find that pointing generative AI systems to the Mathlib code style guidelines can help them perform some of this refactoring work.