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.

That's a good point, but that doesn't seem to change the behaviour here.

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.

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!

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`

.

Hmm... right if I understand correctly, the root of the problem is to unify the `M`

argument from the lemma.

- with my original version, it only sees
`M A = store`

and is lost. Somehow`setoid_rewrite`

must be more aggressive on unfolding constants to find its way. - with the additional explicit instance for
`store`

, it's still lost where it sees`M A = store`

, but it finds the instance`store_fmap`

and gets`M`

from its parameters - with a notation obviously it has everything it needs
- with
`store`

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`

one

I think it makes sense, perfect. Thanks for the help!

As a note: the typical/recommended "standard" dictionary type is gmap K V. (But I don't think that matters here)

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: Jun 13 2024 at 19:02 UTC