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: Oct 13 2024 at 01:02 UTC