feat(data/{list/alist,finmap}): implicit key type

[spl]

Make the key type α implicit in both alist and finmap. This brings these types into line with the underlying sigma and simplifies usage since α is inferred from the value function type β : α → Type v.

• reviewed and applied the coding style: coding, naming
• make sure definitions and lemmas are put in the right files
• make sure definitions and lemmas are not redundant

[cipher1024]

This is similar to the array / darray module. Should we have a similar separation: finmap / dfinmap? I think that would be easier to use.

[digama0]

If finmap here uses prod instead of sigma then probably not; it would duplicate a lot of theorems for no real gain. If it uses sigma then there isn't much point in having the special case at all. Maybe it could be a notation?

[cipher1024]

Why not make finmap a def? def finmap (α β : Type*) := dfinmap (λ x : α, β)

[cipher1024]

It has the benefit of being a functor and traversable.

[cipher1024]

make a separate dfinmap and finmap definition so that we can define a functor and traversable instance on finmap

[spl]

This is similar to the array / darray module. Should we have a similar separation: finmap / dfinmap? I think that would be easier to use.

make a separate dfinmap and finmap definition so that we can define a functor and traversable instance on finmap

@cipher1024 I'm not sure I follow. I believe you're referring to the following?

structure d_array (n : nat) (α : fin n → Type u) :=
(data : Π i : fin n, α i)

def array (n : nat) (α : Type u) : Type u :=
d_array n (λ _, α)

Given that, are you suggesting a restructuring to have the following?

structure dfinmap {α : Type u} (β : α → Type v) : Type (max u v) :=
(entries : multiset (sigma β)) 
(nodupkeys : entries.nodupkeys)

def finmap (α : Type u) (β : Type v) : Type (max u v) :=
dfinmap (λ _ : α, β)

In other words, the existing finmap becomes the above dfinmap and finmap effectively becomes a prod-to-sigma-like wrapper.

First, I'm guessing you're in favor of the implicit {α : Type u} in dfinmap. I believe that, even in this layered approach, it's still useful.

Second, does this alleviate the duplication of definitions and theorems for dfinmap and finmap?

• I think it would be useful to have a non-key-value-dependent finmap in practice. I predict that most uses of finmap will be non-dependent: all the uses I've found in Coq are non-dependent.
• However, the dependent finmap is more general, and I would hate to duplicate it all for both. Would notation be better for the non-dependent finmap?

Finally, I believe the above restructuring is orthogonal to this PR, and I'd like to push this through first. There are also a lot more things I'd like to add to the existing finmap. Would it be acceptable to do those first before thinking about a non-dep finmap, or would it be better to introduce the non-dep finmap first?

[cipher1024]

Given that, are suggesting a restructuring to have the following?

structure dfinmap {α : Type u} (β : α → Type v) : Type (max u v) :=
(entries : multiset (sigma β))
(nodupkeys : entries.nodupkeys)

def finmap (α : Type u) (β : Type v) : Type (max u v) :=
dfinmap (λ _ : α, β)

Yes that's what I'm suggesting.

Finally, I believe the above restructuring is orthogonal to this PR, and I'd like to push this through first. There are also a lot more things I'd like to add to the existing finmap. Would it be acceptable to do those first before thinking about a non-dep finmap, or would it be better to introduce the non-dep finmap first?

Sure. After that, the functor instance should be simple enough. For the traversable instance, we should probably talk.

[johoelzl]

@cipher1024 and @digama0 given that both of you approved this, I merged the PR.

[cipher1024]

Thanks!