Stream: math-comp users

Topic: Encapsulation for finmap with default value?

Karl Palmskog (Aug 06 2020 at 20:14):

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"?

Cyril Cohen (Aug 06 2020 at 23:24):

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

Cyril Cohen (Aug 06 2020 at 23:24):

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

Cyril Cohen (Aug 06 2020 at 23:29):

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

Karl Palmskog (Aug 07 2020 at 15:43):

@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.

Cyril Cohen (Aug 07 2020 at 16:17):

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 .
...

Cyril Cohen (Aug 07 2020 at 16:19):

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

Karl Palmskog (Aug 11 2020 at 10:17):

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?

Cyril Cohen (Aug 11 2020 at 10:20):

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.

Cyril Cohen (Aug 11 2020 at 10:21):

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

Cyril Cohen (Aug 11 2020 at 10:22):

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

Karl Palmskog (Aug 11 2020 at 10:25):

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

Cyril Cohen (Aug 11 2020 at 12:41):

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

Last updated: Jan 29 2023 at 19:02 UTC