## Stream: math-comp users

### Topic: ✔ Different representations for elements of finsets

#### Ricardo (Jan 19 2023 at 21:00):

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.

#### Ricardo (Jan 19 2023 at 21:03):

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.
`

#### Paolo Giarrusso (Jan 19 2023 at 21:17):

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?

#### Ricardo (Jan 19 2023 at 21:21):

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

#### Ricardo (Jan 19 2023 at 21:23):

I think I understand what you're saying now.

#### Ricardo (Jan 19 2023 at 21:24):

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

#### Ricardo (Jan 19 2023 at 21:24):

Is that what you're saying?

Yes

#### Ricardo (Jan 19 2023 at 21:36):

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

#### Notification Bot (Jan 19 2023 at 21:54):

Ricardo has marked this topic as resolved.

Last updated: Jul 23 2024 at 19:02 UTC