Looking for some help on the Sin_domain proof from Software Foundations Color.v

Here is the full module: https://softwarefoundations.cis.upenn.edu/vfa-current/Color.html

The theorem at hand:

Exercise: 3 stars (Sin_domain)
Lemma Sin_domain: ∀ A n (g: M.t A), S.In n (Mdomain g) ↔ M.In n g.

Usually, 3 stars indicates hard but not too hard, but I'm struggling to figure out how to attack this. If you unfold Mdomain it becomes a fold which then becomes M.xfoldi, which is fairly low level. I have a sense of how I could prove a bunch of low level lemmas about how xfoldi acts on various indices but...I feel like there has got to be a better way? That said it does have this disclaimer

This seems so obvious! But I didn't find a really simple proof of it.

My first instinct with this sort of thing is always try try and prove some sort of distribution principle about the thing at hand, such as

Mdomain (M.Node s1 o s2)

But since Mdomain is implemented in terms of a fold, it gets complicated pretty quickly. Again, probably not insurmountable but...I'm wondering if there is a better way (given I just spent many, many hours on Sremove_cardinal_less and Mremove_cardinal_less!)

Solution

Hint: Use WP.fold_rec_bis to prove a relation P between a map and the result of folding it (with M.fold). It is a form of induction principle:

Base case: the relation must hold between the empty map and the initial accumulator;
Induction step: if the relation holds of some map (and accumulator), then it holds after inserting a new key-value pair (and updating the accumulator accordingly).

As a technicality, it also requires a "compatibility" assumption (which is an explicit proof that your relation P is independent from the order of insertion).

  Theorem fold_rec_bis :
    forall (A:Type)(P : t elt -> A -> Type)(f : key -> elt -> A -> A),
     forall (i:A)(m:t elt),
     (forall m m' a, Equal m m' -> P m a -> P m' a) ->  (* Compatibility *)
     (P (empty _) i) ->                                 (* Base case *)
     (forall k e a m', MapsTo k e m -> ~In k m' ->      (* Induction step *)
       P m' a -> P (add k e m') (f k e a)) ->
     P m (fold f m i).