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.

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).
admit.
Admitted.
```

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

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.

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: Jul 25 2024 at 17:02 UTC