Stream: math-comp users

Topic: `finmap`: rewriting `{fset K}` membership


view this post on Zulip Evgeniy Moiseenko (Nov 15 2021 at 09:58):

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.

view this post on Zulip Evgeniy Moiseenko (Nov 15 2021 at 10:01):

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.

view this post on Zulip Evgeniy Moiseenko (Nov 15 2021 at 10:29):

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

view this post on Zulip Ana de Almeida Borges (Nov 15 2021 at 12:09):

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.

view this post on Zulip Cyril Cohen (Nov 15 2021 at 15:55):

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: Feb 02 2023 at 15:04 UTC