Hi. I have roughly the following proof state.

```
m : {fmap K -> V}
ks : {fset K}
v : V
============================
forall k : domf m,
m k == v ->
fsval k \in ks ->
forall l : K,
l \in fsval (A:=domf m) @` [fset k | k in domf m & m k == v] ->
l \in ks
```

This looks easily provable but I don't know how. I tried using `rewrite inE`

to simplify the `l \in fsval (A:=domf m) @` [fset k | k in domf m & m k == v]`

expression but it doesn't work. Any help or pointers would be much appreciated.

The code to get to that proof state.

```
From mathcomp Require Import all_ssreflect finmap.
Open Scope fset.
Lemma foo (K V : choiceType) (m : {fmap K -> V})
(ks : {fset K}) (v : V) :
forall k : domf m,
m k == v ->
fsval k \in ks ->
forall l : K,
l \in val @` [fset k0 | k0 : domf m & m k0 == v] ->
l \in ks.
Proof.
Admitted.
```

For this to be true, any chance you need parentheses around (forall k, ... fsval k in ks)? Otherwise it seems ks might contain just k, instead of the preimage of v?

Isn't k the preimage of v? At least one of the preimages.

I think I understand what you're saying now.

k happens to be a preimage of v and be in ks but other preimages of v might not be in ks

Is that what you're saying?

Yes

I see. So the proof state that I arrived at isn't provable. I should take a different approach probably.

Ricardo has marked this topic as resolved.

Last updated: Jul 23 2024 at 19:02 UTC