Induction proofs on MSets

Question

I'm trying to use MSet library in a Coq development and I need a map function, which is absent from the library, but can be implemented using fold, as usual.

In the following gist, I've put a simplification of what I'm working on, full of axioms, just to get straight to the point.

My problem is to prove a property of the following map function:

Definition map (f : Exp -> Exp) s
  := MSet.fold (fun a ac => MSet.add (f a) ac) MSet.empty s.

Which uses fold from Coq MSet library. The property that I want to show is:

  Lemma map_lemma : forall s f e, In e (map f s) -> exists e', In e' s /\ e = f e'.
  Proof.
     induction s using set_induction ; intros ; try fsetdec.

Which is intended to show that if an element e in the set map f s, then exists another element e' in s, s.t. e = f e'. My difficulty is to prove the inductive case, since the induction hypothesis produced by set_induction does not seems useful at all.

Could someone provide me any clues on how should I proceed?

A note about sets don't include a map operation is because it only makes sense as such if the mapped function is injective and order-preserving. For all other cases, you are talking about "the image of a set under f", which has slightly different properties. — ejgallego

eponier eponier · Accepted Answer · 2017-11-30T12:34:16

First, I think there is a problem in your definition of smap. You must swap MSet.empty and s, otherwise you can prove:

Lemma snap_trivial : forall f s, smap f s= s.
Proof.
  intros. reflexivity.
Qed.

With the right definition, you can use the fold_rec lemma that is adapted to this kind of goal.

Induction proofs on MSets

1 Answers