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.
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.
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
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.
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: Mar 29 2024 at 07:01 UTC