Hello,

So I was implementing the Extentional tries by Xavier Leroy (also I checked his implementation) but this time I was aiming to have a robust implementation (API-wise) so I kind of followed the approach taken by coq-stdpp except for I tried to use ssreflection as much as possible.

What I am asking for is general code review, maybe if you can see some bad patterns, ways to write shorter and better proofs, or maybe

even some misuses of ssreflect/mathcomp on my end.

The point here is that to be able to improve I need feedback on what may I be doing wrong (even from guidelines perspective)

The codebase is still at very early stage and very few lemmas / APIs, which will also make it easier to fix any bad coq habits I ended up developing.

https://gitlab.com/thewalker77/ssrmap

This topic was moved here from #Coq users > Request for Comments/ Code review by Karl Palmskog.

This is not at all important, but it made me happy when it was implemented, so you might enjoy it too: you can rewrite in intro patterns, so for example the proof

```
elim => [p3 IHp3 | p3 IHp3 |] p2 p1 /=;
by [rewrite IHp3|].
```

can be written as

```
by elim => [p3 IHp3 | p3 IHp3 |] p2 p1 //= /[!IHp3].
```

Three other notes in terms of style: I would use `//`

to get rid of the trivial goal instead of keeping it around and having to sidestep it with `[rewrite IHp3|]`

.

The other two I quote from the mathcomp style guidelines:

- Lines end with a point . and only have ; inside them.
- Lines that close a goal must start with a terminator (by or exact). You should consider using an editor that highlight those terminators in a specific color (e.g. red) [Proof General does this, I'm not sure about others].

So in the example above, even if you don't want to use `//`

, the proof would be:

```
by elim => [p3 IHp3 | p3 IHp3 |] p2 p1 /=; [rewrite IHp3|].
```

Some other things...

- A shorter way to write
`have : foo; last first`

is`suff : foo`

- The ssr idiom for
`rewrite <- H`

is`rewrite -H`

(if you use`rewrite <- H`

you are in fact using the standard Coq`rewrite`

, not the ssr`rewrite`

) - You can transform

```
elim => [p IHp | p IHp |] /=.
- by rewrite rev_xI rev_app IHp.
- by rewrite rev_xO rev_app IHp.
- by [].
```

into

```
by elim => [p IHp | p IHp |] //=; rewrite ?rev_xI ?rev_xO rev_app IHp.
```

Whether you should or not is more debatable - your version has the advantage of clearly delineating which tactics solve which goal, which can be good for maintainability. I typically use `//`

as much as possible (eg I don't have any `by []`

in my code) but tend to avoid `rewrite ?lemma`

.

```
```

`by case => [||].`

can be simplified to`by case`

, and similarly with`elim`

.- if you use
`apply H`

you are using the standard Coq`apply`

, not the ssr one, which is available with`apply: H`

- Usually
`by`

doesn't need help with unfolding or simplifying, so that

```
by case => [|l] [|r] p [a|];
rewrite /builder /lookup /=.
```

can be simply

```
by case => [|l] [|r] p [a|].
```

- The ssr idiom for
`change x with y`

is`rewrite -[x]/y`

- Typically we avoid changing the context (eg
`change x with y in *`

), especially if this can be avoided by doing the change before introducing anything in the first place (eg this line can be avoided if you do the`change`

(or`rewrite -[...](...)`

) before the`elim`

)

If you have several similar-ish lemmas about the same thing, and especially if their applicability is obvious in any given circumstance (eg `lookup_builder_l`

, `_r`

, and `_a`

), you can create a rewrite rule with all of them and let Coq decide which one to use:

```
Definition lookup_builderE :=
(lookup_builder_r, lookup_builder_l, lookup_builder_a).
```

Then in proofs you can `rewrite lookup_builderE`

(or `rewrite !lookup_builderE`

) instead of picking the relevant one(s) yourself. The typical example from mathcomp is `inE`

, which keeps being extended as more lemmas about `_ \in _`

become available.

- The ssr idiom for
`specialize (H x)`

is either`have := H x`

or`move: (H x)`

`split; by []`

can be simply`by split`

(and this in general holds for`whatever; by []`

I think this is it from my review; I basically only looked at the proofs without even stepping through them (other than to make sure my alternatives work). They seem overall fine, even if sometimes they can be shortened and some vanilla tactics replaced by ssr ones. (I frowned at some of the multi-line `try ...`

proofs, but you have such huge and somewhat repetitive data structures that I don't know what could be done to avoid them, other than perhaps definitions such as `lookup_builderE`

.)

I've the impression that

```
Structure type := Pack{
KT: eqType;
VT: eqType;
MT: eqType -> eqType -> Type;
ops: forall V, operations KT V MT;
lms: lemmas VT ops;
}.
```

should be more like

```
Structure type (KT VT : eqType) := Pack{
MT : Type;
....
}
```

but it is a bit unclear to me what you want to do with it. Do you want to prove it forms a fintype?

@Ana de Almeida Borges thanks a lot for the extensive review, I wil lcertainly start following most if not all of your suggestions.

@Enrico Tassi I tried doing things the way you describe, but things eventually broke here:

```
Record operations (K V: eqType) (M: eqType -> eqType -> Type) := Operations {
....
Merge (V1 V2: eqType): (option V1 -> option V2 -> option V) ->
M K V1 ->
M K V2 ->
M K V;
....
}
```

I realized I need to have same `M`

(which is `MT`

) indexed by different Key /Value types.

But I might be wrong

why are K and V parameters instead of forall-bound?

I am not sure I am following

something like

```
Record operations (M: eqType -> eqType -> Type) := Operations {
Empty K V : M K V;
...
}.
Record lemmas (M: eqType -> eqType -> Type) (ops: operations M) := Lemmas {
LookupEmpty K V : forall k, Lookup ops k (@Empty K V ops) = None;
....
}.
Structure type := Pack{
MT: eqType -> eqType -> Type;
ops : operations MT;
lms : lemmas ops;
}.
```

Hum, I see, but then I think I don't the point of this interface in the first place. At least, not in the context of mathcomp.

Your maps (the implementation) is an eqType, which is great, but that interface does not give you an eqType for its third field (`MT`

), which seems the objective to me.

I will have to try that and see if it works, it looks cleaner, but I don't understand SC enough to spot if there is an issue, but this certainly look cleaner.

I was planning to also implment eqType for MT in the near future as well (probably it was the next thing to implement)

Why do you need an eqType on values, BTW? On keys it makes sense, on values it shouldn't usually be needed in a map?

Oh nice, I wanted to check out Leroy&Appel's trees at some point, even have an issue about it in my FAV port repo: https://github.com/clayrat/fav-ssr/issues/8. Speaking of which, we could probably unify this and some of the FAV code into a single repo with various tree-based finmap implementations.

might be an option do a MathComp SSR red-black tree map? See https://github.com/coq-community/coq-mmaps

Yeah, that should be fairly straightforward, the biggest part missing in FAV would be a `subset`

test, but I think that can also be done "join" style, at least Haskell `containers`

implementation suggests so, I actually also have an issue about that: https://github.com/clayrat/fav-ssr/issues/10 :)

we can certainly do that, but I would still take the opportunity to complete my implementation as a learning experience.

Gaëtan Gilbert said:

why are K and V parameters instead of forall-bound?

Figured one out, At least the key must be a paremeter and cannot be forall because there is this one function:

```
Record operations (K V: eqType) (M: eqType -> eqType -> Type) := Operations {
ToList: M K V -> seq (K * V);
}
```

Since `K`

is parameter, we can have a not to general finite map (like map from key being `positive`

) so the result will be:

```
ToList: M positive_eqType V -> seq (positive * V);
```

But if (at least) the key was in a forall quantifier, then I don't know how to speialize the whole data operations to be specific to one type of key

When I tried it ... it gave me something like:

```
ToList: M K V -> seq (K * V);
```

While the real implementation was something like `Trie V -> Seq (positive * v)`

because key was fixed. But I think the value can be turned into forall, for now I will git checkout * and retry.

Paolo Giarrusso said:

Why do you need an eqType on values, BTW? On keys it makes sense, on values it shouldn't usually be needed in a map?

One of the main lemmas is that `uniq(to_list som_tree)`

. But ` to_list`

returns `seq (K * V)`

to use uniq, that seq must be eqType so `V`

must be `eqType`

That lemma using uniq could just apply M to an eqType, if even that is needed

That is, have M : eqType -> Type -> Type, then state that `forall ... (V : eqType) (some_tree : M K V), ... uniq (to_list some_tree)`

I also have concerns about requiring eqType for writing `uniq`

: you can define uniqueness without decidable equality. I understand math-comp prefers decidable predicates, but it seems questionable here.

Enrico Tassi said:

Hum, I see, but then I think I don't the point of this interface in the first place. At least, not in the context of mathcomp.

Your maps (the implementation) is an eqType, which is great, but that interface does not give you an eqType for its third field (`MT`

), which seems the objective to me.

The point of the interface was to implement the so many lemmas for maps for this interface and then link multiple finite map implementations to the same interface, I am not sure if that is the expected usecase.

@Ana de Almeida Borges : I have a question on your note:

The ssr idiom for change x with y is rewrite -[x]/y

I wonder if this results from a proof term point of view in a `change`

or a `rewrite`

- in most cases a `change`

leads to an easier and faster ot Qed proof term than a `rewrite`

.

@Michael Soegtrop I had never thought about it, but cursory testing seems to show it leads to a proof term identical to the one obtained with `change`

.

Last updated: Jul 15 2024 at 20:02 UTC