Induction proofs on MSets

Link:: https://stackoverflow.com/q/47572526

Display all goals and responses

Question

I'm trying to use MSet library in a Coq development and I need a smap 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 smap function:

Definition smap (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 smap_lemma : forall s f e,
    In e (smap f s) -> exists e', In e' s /\ e = f e'.forall (s : t) (f : Exp -> Exp) (e : elt),
In e (smap f s) ->
exists e' : elt, In e' s /\ e = f e'
Proof.forall (s : t) (f : Exp -> Exp) (e : elt),
In e (smap f s) ->
exists e' : elt, In e' s /\ e = f e'
  induction s using set_induction; intros; try fsetdec.s1, s2: t
x: elt
H: ~ In x s1
H0: Add x s1 s2
IHs1: forall (f : Exp -> Exp) (e : elt),
In e (smap f s1) ->
exists e' : elt, In e' s1 /\ e = f e'
f: Exp -> Exp
e: elt
H1: In e (smap f s2)
exists e' : elt, In e' s2 /\ e = f e'

Which is intended to show that if an element e in the set smap 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: A note about sets don't include a smap 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.

Answer

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

Lemma smap_trivial : forall f s, smap f s = s.forall (f : Exp -> Exp) (s : t), smap f s = s
Proof.forall (f : Exp -> Exp) (s : t), smap f s = s
  intros.f: Exp -> Exp
s: t
smap f s = s reflexivity.
Qed.

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