Stream: math-comp users

Topic: ✔ Different representations for elements of finsets


view this post on Zulip 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.

view this post on Zulip 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.
Admitted.

view this post on Zulip 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?

view this post on Zulip Ricardo (Jan 19 2023 at 21:21):

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

view this post on Zulip Ricardo (Jan 19 2023 at 21:23):

I think I understand what you're saying now.

view this post on Zulip 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

view this post on Zulip Ricardo (Jan 19 2023 at 21:24):

Is that what you're saying?

view this post on Zulip Paolo Giarrusso (Jan 19 2023 at 21:31):

Yes

view this post on Zulip 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.

view this post on Zulip Notification Bot (Jan 19 2023 at 21:54):

Ricardo has marked this topic as resolved.


Last updated: Jul 23 2024 at 19:02 UTC