Notification Bot (Nov 01 2022 at 16:41): Notification Bot (Nov 01 2022 at 16:41):This topic was moved here from #Coq users > Request for Comments/ Code review by Karl Palmskog.
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].
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|].
Some other things...
have : foo; last first is suff : foorewrite <- H is rewrite -H (if you use rewrite <- H you are in fact using the standard Coq rewrite, not the ssr rewrite)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.apply H you are using the standard Coq apply, not the ssr one, which is available with apply: Hby doesn't need help with unfolding or simplifying, so thatby case => [|l] [|r] p [a|];
rewrite /builder /lookup /=.
can be simply
by case => [|l] [|r] p [a|].
change x with y is rewrite -[x]/ychange 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) 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.
Ana de Almeida Borges (Nov 02 2022 at 09:42):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 [] 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.)
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?
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.
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
Gaëtan Gilbert (Nov 02 2022 at 11:03):why are K and V parameters instead of forall-bound?
walker (Nov 02 2022 at 11:08):I am not sure I am following
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;
}.
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.
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.
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)
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?
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.
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
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 :)
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.
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.
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
Paolo Giarrusso (Nov 02 2022 at 23:40):That lemma using uniq could just apply M to an eqType, if even that is needed
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)
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.
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.
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.
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