Stream: math-comp users

Topic: Request for Comments/ Code review


view this post on Zulip Notification Bot (Nov 01 2022 at 16:41):

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

view this post on Zulip Ana de Almeida Borges (Nov 02 2022 at 08:42):

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

view this post on Zulip Ana de Almeida Borges (Nov 02 2022 at 08:54):

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:

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

view this post on Zulip Ana de Almeida Borges (Nov 02 2022 at 09:08):

Some other things...

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.


view this post on Zulip Ana de Almeida Borges (Nov 02 2022 at 09:21):

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

can be simply

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

view this post on Zulip Ana de Almeida Borges (Nov 02 2022 at 09:29):

view this post on Zulip Ana de Almeida Borges (Nov 02 2022 at 09:35):

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.

view this post on Zulip Ana de Almeida Borges (Nov 02 2022 at 09:42):

view this post on Zulip Ana de Almeida Borges (Nov 02 2022 at 09:48):

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

view this post on Zulip Enrico Tassi (Nov 02 2022 at 10:35):

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?

view this post on Zulip walker (Nov 02 2022 at 10:56):

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

view this post on Zulip walker (Nov 02 2022 at 10:59):

@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

view this post on Zulip Gaëtan Gilbert (Nov 02 2022 at 11:03):

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

view this post on Zulip walker (Nov 02 2022 at 11:08):

I am not sure I am following

view this post on Zulip Gaëtan Gilbert (Nov 02 2022 at 11:12):

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

view this post on Zulip Enrico Tassi (Nov 02 2022 at 11:13):

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.

view this post on Zulip walker (Nov 02 2022 at 11:20):

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.

view this post on Zulip walker (Nov 02 2022 at 11:20):

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

view this post on Zulip Paolo Giarrusso (Nov 02 2022 at 12:14):

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?

view this post on Zulip Alexander Gryzlov (Nov 02 2022 at 20:11):

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.

view this post on Zulip Karl Palmskog (Nov 02 2022 at 20:14):

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

view this post on Zulip Alexander Gryzlov (Nov 02 2022 at 20:45):

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 :)

view this post on Zulip walker (Nov 02 2022 at 21:35):

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

view this post on Zulip walker (Nov 02 2022 at 23:22):

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

view this post on Zulip walker (Nov 02 2022 at 23:29):

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

view this post on Zulip Paolo Giarrusso (Nov 02 2022 at 23:40):

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

view this post on Zulip Paolo Giarrusso (Nov 02 2022 at 23:43):

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

view this post on Zulip Paolo Giarrusso (Nov 02 2022 at 23:50):

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.

view this post on Zulip walker (Nov 03 2022 at 11:57):

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.

view this post on Zulip Michael Soegtrop (Nov 03 2022 at 12:28):

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

view this post on Zulip Ana de Almeida Borges (Nov 03 2022 at 13:04):

@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: Feb 08 2023 at 07:02 UTC