Stream: Coq users

Topic: Confusion on rewrites over stdpp's finmaps


view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Dec 09 2023 at 13:32):

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.

view this post on Zulip Yannick Zakowski (Dec 09 2023 at 13:34):

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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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.

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

view this post on Zulip 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)

view this post on Zulip 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: Jun 13 2024 at 19:02 UTC