## Stream: math-comp users

### Topic: `finmap`: rewriting `{fset K}` membership

#### Evgeniy Moiseenko (Nov 15 2021 at 09:58):

I have trouble understanding how `rewrite` lemmas in `finmap.v` library supposed to work.

Giving the following context:

``````Context {K : choiceType}.
Context {P : pred K} {fK : subFinType P}.
``````

I want to do the following rewriting.

``````(x \in [fsetval y in fK]) = if insub x is Some x' then in_mem x' (mem fK) else false.
``````

I suppose that the lemma `in_fset_val` should do the job:

``````Lemma in_fset_val A (p : finmempred [eqType of A]) (k : K) :
(k \in imfset key val p) = if insub k is Some a then in_mem a p else false.
``````

Yet it fails.

``````The LHS of in_fset_val
(_ \in imfset _ val _)
does not match any subterm of the goal
``````

So I ended up reproving lemma `in_fset_val` using `imfsetP`.
But I am sure there should be a better way.

So the question is why really `in_fset_val` fails in my case? What goes wrong here?
I've tried to sort it out by myself but I failed. The notations in `finmap.v` (including `[fsetval y in fK]`) are quite involved and use locking and phantom types heavily.

#### Evgeniy Moiseenko (Nov 15 2021 at 10:01):

Minimal (not-)working example:

``````Context {K : choiceType}.
Context {P : pred K} {fK : subFinType P}.

Lemma test x :
(x \in [fsetval y in fK]) = if insub x is Some x' then in_mem x' (mem fK) else false.
Proof.
Fail (rewrite in_fset_val).
``````

#### Evgeniy Moiseenko (Nov 15 2021 at 10:29):

Just noticed that my example can be simplified:

``````Lemma in_fsetval k :
(k \in [fsetval k' in fK]) = (insub k : option fK).
``````

In my actual code I need a slightly more evolved lemma:

``````Lemma in_fsetval_seq k (s : seq fK) :
(k \in [fsetval k' in s]) =
if insub k is Some k' then k' \in s else false.
``````

`rewrite in_fset_val` also fails here

#### Ana de Almeida Borges (Nov 15 2021 at 12:09):

I'm confused by what is going on too. My go-to in these situations is to `have` the lemma I want to rewrite with, manually feed it the relevant inputs, and observe where it fails. In this case:

``````Lemma test x :
(x \in [fsetval y in fK]) =
if insub x is Some x' then in_mem x' (mem fK) else false.
Proof.
Fail have := @in_fset_val _ K fK.
(* The term "fK" has type "subFinType (T:=K) P"
while it is expected to have type "{fset K}". *)
``````

so I guess you just aren't in the conditions of `in_fset_val`. Probably someone with more experience can tell you how to move things around so that you can prove your statement. My attempts haven't really gotten anywhere.

#### Cyril Cohen (Nov 15 2021 at 15:55):

I suspect that there might be a canonical instance missing somewhere in finmap... I did not touch this code for a long time so I might be mistaken. I will take a look later this week. I'm glad you found a workaround using `imfsetP` meanwhile.

Last updated: Feb 02 2023 at 15:04 UTC