I have a record which contains a bunch of plain Coq functions like `nat -> seq X`

and `nat -> nat -> seq Y`

with default value `[::]`

, and I want to have at least an eqType for the record (assuming eqTypes for `X`

and `Y`

).

What is the best "structure" to replace the functions with so I don't have to change a lot in the proofs about the record? For example, if I use a `{finmap nat -> seq X}`

, I will have to explicitly write a function on top that returns the empty list when a key (`nat`

) is not found, and `nat -> nat -> ...`

will have to use a tuple or similar.

Is there an obvious way to encapsulate "finmaps with defaults"?

Karl Palmskog said:

Is there an obvious way to encapsulate "finmaps with defaults"?

The answer is finitely supported functions `fsfun`

https://github.com/math-comp/finmap/blob/master/finmap.v#L16

https://github.com/math-comp/finmap/blob/master/finmap.v#L106-L132

The theory has not been used much, so you might want to extend&PR math-comp/finmap

@Cyril Cohen would something like this make sense to add upstream? I certainly need it for my purposes.

```
Definition setfs (K : choiceType) (V : eqType) (default : K -> V)
(fs: {fsfun K -> V for default}) (k : K) (v : V) : {fsfun K -> V for default} := (* ... *)
Lemma getfs_set (K : choiceType) (V : eqType) (default : K -> V)
(fs: {fsfun K -> V for default}) (k : K) (v : V) :
(setfs fs k v) k = v.
Proof. (* ... *) Qed.
Lemma setfs_get (K : choiceType) (V : eqType) (default : K -> V)
(fs: {fsfun K -> V for default}) (k : K) :
(setfs fs k (fs k)) = fs.
Proof. (* ... *) Qed.
Lemma setfsNK (K : choiceType) (V : eqType) (default : K -> V)
(fs: {fsfun K -> V for default}) (k k' : K) (v : V) :
(setfs fs k v) k' = if k' == k then v else fs k'.
Proof. (*... *) Qed.
```

That would be nice indeed!

Ideally it should mimic (and/or wrap) the notations `[fun/eta... with x |-> ...]`

from `eqtype`

. Something like

```
Notation "[fsfun[key] f with x1 |-> y1, ..., xn |-> yn]" := ...
Lemma fsfun_withE : [fsfun f with x |-> y] z = if z == x then y else f x.
...
Lemma fsfun_withx : [fsfun f with x |-> y] x = y.
...
Lemma fsfun_with_id : [fsfun f with x |-> f x] = f.
...
Lemma finsupp_with :
finsupp [fsfun f with x |-> y] = if y == default x then finsupp f `\ x else x |` finsup f .
...
```

And maybe `[fsfun f without x] := [fsfun f with x |-> default x]`

.

Thanks a lot (https://github.com/math-comp/finmap/pull/72). Looking ahead, another thing on the wishlist for `fsfun`

would be handling of curried functions, e.g., `{fsfun nat -> nat -> seq nat with [::]}`

. Is this likely to be straightforward or difficult to add?

Karl Palmskog said:

Thanks a lot (https://github.com/math-comp/finmap/pull/72). Looking ahead, another thing on the wishlist for

`fsfun`

would be handling of curried functions, e.g.,`{fsfun nat -> nat -> seq nat with [::]}`

. Is this likely to be straightforward or difficult to add?

It's essentially a matter of notation hacking I would say, so the difficulty is unpredictable from my perspective.

actually, I backtrack on this... how would you distinguish finite support arguments from regular ones ?

e.g. in your example is it finitely supported on the first argument, or both?

in my example they would all/both be finitely supported. I guess just using tuples would work in most cases I'm interested in.

Anyway you don't need to use tuples, you an uncurrify the function: `{fsfun nat * nat -> seq nat with [::]}`

should work

Last updated: Jul 25 2024 at 16:02 UTC