feat: redefine HashSet.union and add lemmas

[Paul-Lez]

This PR adds a few initial lemmas about unions on Raw₀ to get feedback from @TwoFX.

[TwoFX]

This lemma becomes strictly more general (as a simp lemma) if you don't take k and v separately, but take a parameter p from the sigma type and state the left-hand side as m.val.union {p}.

[Paul-Lez]

That makes sense - I've made the change you suggested. Now that I think of it, don't we want to formulate this lemma in terms of Raw_0 rather than Raw, e.g. changing the goal to something of the form

m.union ⟨{p}, by sorry⟩ = m.insert p.fst p.snd

[TwoFX]

Thinking about this more: since there is the lemma Std.DHashMap.singleton_eq_insert, the LHS of this lemma will actually not be in simp normal form in any user-facing situation, which suggests that we shouldn't have the lemma in this form. The correct statement is going to be a variant of your union_insert below, namely m.union (empty.insert k v) = m.insert k v (unlike the general case below, this is true on the nose, not just up to equivalence).

[TwoFX]

Presumably there are also left variants of the right lemmas?

[TwoFX]

This is only true up to equivalence of hash maps, as shown by the following example:

import Std

open Std

def m₁ : HashMap Nat Nat := ∅
def m₂ : HashMap Nat Nat := .ofList [(0, 0)]

-- Std.HashMap.ofList [(16, 1), (0, 0)]
#eval (m₁.union m₂).insert 16 1

-- Std.HashMap.ofList [(0, 0), (16, 1)]
#eval m₁.union (m₂.insert 16 1)

So the statement of this lemma should involve Equiv.

[TwoFX]

It would also be nice to have size lemmas similar to the ones for insertMany.

[Paul-Lez]

It would also be nice to have size lemmas similar to the ones for insertMany.

Sounds good, I'll add some more this week!

[TwoFX]

Work on this will continue at #10611.