Yannick Zakowski (Dec 09 2023 at 12:58): Yannick Zakowski (Dec 09 2023 at 12:58):Dear all,
I am finally starting to play with stdpp, and must be doing something wrong with finmap: in short, in a seemingly simple case, setoid_rewrite works in both context and goal, rewrite works nowhere, and the provided tactic simplify_map_eq works in the goal but not the context. I'd be interested in understanding both what is happening behind the scene, and what's the proper practice.
Please consider the following minimal code (tested on stdpp 1.9.0, coq 8.18.dev) to illustrate the issue:
From stdpp Require Export
fin_maps
natmap
.
Definition val := nat.
Definition store := (natmap val).
Lemma weird (σ : store) v k
(EQ : <[k := v]> σ !! k = σ !! k) :
<[k := v]> σ !! k = σ !! k.
Proof.
(* I want to simplify both my goal and my hypothesis *)
(* `rewrite` simply fails to see the pattern: why? *)
Fail rewrite lookup_insert.
Fail rewrite lookup_insert in EQ.
(* `setoid_rewrite` does the job properly *)
setoid_rewrite lookup_insert.
setoid_rewrite lookup_insert in EQ.
Restart.
(* `simplify_map_eq` does only half the job: why? *)
simplify_map_eq.
Abort.
I think you want to do From stdpp Require Export prelude fin_maps natmap. At least I've had various strange stuff without the whole prelude imported.
Yannick Zakowski (Dec 09 2023 at 13:34):That's a good point, but that doesn't seem to change the behaviour here.
Karl Palmskog (Dec 09 2023 at 13:49):The whole problem seems to be a missing Inhabited instance, which one can get via a FMap instance.
Definition val := nat.
Definition store := natmap.
Instance store_fmap : FMap store := _.
Lemma weird (σ : store val) v k
(EQ : <[k := v]> σ !! k = σ !! k) :
<[k := v]> σ !! k = σ !! k.
Proof. by simplify_map_eq. Qed.
a colleague of mine did some initialization/proving with nmap here, might be helpful also.
Yannick Zakowski (Dec 09 2023 at 13:55):Oh, of course. Having to declare this instance makes a lot of sense, I got thrown off by setoid_rewrite succeeding nonetheless, but it should indeed have to be declared I guess. Thanks!
Karl Palmskog (Dec 09 2023 at 13:57):apparently, this works as well, natmap actually exports the natmap_fmap instance:
Definition val := nat.
Definition store := natmap.
Lemma weird (σ : store val) v k
(EQ : <[k := v]> σ !! k = σ !! k) :
<[k := v]> σ !! k = σ !! k.
Proof. by simplify_map_eq. Qed.
So the original code should work with Definition store changed to Notation store.
Yannick Zakowski (Dec 09 2023 at 14:05):Hmm... right if I understand correctly, the root of the problem is to unify the M argument from the lemma.
M A = store and is lost. Somehow setoid_rewrite must be more aggressive on unfolding constants to find its way.store, it's still lost where it sees M A = store, but it finds the instance store_fmap and gets M from its parametersstore being only partially applied, it sees M A = store val and can therefore unify M = store, and from there even if it does not have an explicit instance for store, the typeclass resolution is happy to unfold the constant to fetch the natmap oneI think it makes sense, perfect. Thanks for the help!
Paolo Giarrusso (Dec 09 2023 at 21:52):As a note: the typical/recommended "standard" dictionary type is gmap K V. (But I don't think that matters here)
Paolo Giarrusso (Dec 09 2023 at 21:54):TC search struggling with higher-order unification is... unfortunate but not too surprising. If you have definitions, it often makes sense to make them TC opaque and lift typeclasses — but I've never seen that for maps, since you have something like 10 typeclasses to lift :sweat_smile:
Last updated: Oct 13 2024 at 01:02 UTC