The Coq mailing list

[Kazuhiko Sakaguchi <pi8027 AT gmail.com>]

Hi, I attempted to solve exactly the same problem before. So I have a
few comments.

2022年4月1日(金) 15:37 Thomas Sewell <tals4 AT cam.ac.uk>:
>
> Hello, apologies about the beginner questions. I'm playing with a fiddly
> exercise trying to learn a bit about Coq, and I'd be interested in any
> feedback.
>
> I'm revisiting a toy problem which I've also attempted in other tools
> (Isabelle/HOL, HOL4, ACL2). The idea is to simplify Permutation goals,
> e.g. "Permutation (x :: y :: z :: bs) ((y :: cs) ++ (x :: ds))" might 
> reduce to
> "Permutation (z :: bs) (cs ++ ds)".
>
> This problem is good for highlighting performance aspects, since you can 
> easily
> scale up the goals by computing longer lists (e.g. with seq) and time your
> tactic on bigger problems. In Isabelle and HOL4, the aim is use SML snippets
> effectively, but in ACL2 and Coq it looks like reification/reflection is the
> way to go.
>
> I skimmed the reflection chapter of Chilpala's CPDT book to see some 
> examples.
> I have reification working based on an approach I saw there, which uses (or
> abuses?) Ltac matching to identify syntactically equal terms. This is then 
> used
> to assign a number to all the list elements with equal elements (e.g. the
> repeated x and y above) getting the same number. Unfortunately this 
> requires a
> lot of term comparisons, roughly O(n^2) in the number of unique terms. 
> Could we
> do better? Probably an OCaml plugin has access to a term order and can 
> build a
> binary tree, but this seems like a heavy replacement for a couple of Ltac
> functions. Is there anything more efficient I can do while staying mostly in
> Ltac (or Ltac2 or similar)?

You are right, but naive reification procedures have an advantage that
the index numbers preserve the same ordering as the occurrences in the
input terms (which allows you to make reflexive simplification
preserving the ordering of terms). Also, this is probably not a
bottleneck in practice since:
- many optimized reflexive tactics (e.g., ring and field) use naive
reification procedures without making your point an actual performance
issue, and
- term comparisons would be fast enough thanks to hash-consing (maybe
other experts can confirm this).
So, I suggest starting with a naive implementation and improving it
when you find it is a bottleneck.

Nowadays, many metalanguages, such as Ltac2, Coq-Elpi, and MetaCoq,
can replace this kind of intricate use of Ltac. You may find (or
implement) the feature you need (efficient total order on terms) in
some of them, but honestly I don't know if they provide such an API.
In my personal experience, implementing a reflexive tactic in Coq-Elpi
is extremely easy and it also achieves a decent performance, although
learning Coq-Elpi may take some time.

> With the list elements numbered, the idea is then to sort them on each side,
> scan, and move duplicated elements into a special comparison. This requires 
> a
> (roughly) a sort operation on list (nat * A), i.e. sorting actual elements 
> (of
> unknown type) by comparing computational identifiers (here nat, but this 
> could
> be replaced with a more efficient type).
>
> This is where things start going wrong. There's a merge-sort provided in the
> standard theories, but it gets its type parameter as a module parameter. To 
> my
> understanding, there's no way to use it polymorphically to sort list (nat * 
> A)
> or anything similar. Is that right? Is there a mechanism I haven't thought 
> of?
>
> The same seems to be true of other structures in the standard library (e.g. 
> the
> MSet implementations backed by sorted trees) which could be used to sort
> indirectly. I also collided with some anomalies when trying to instantiate 
> some
> modules, but apparently some of these are fixed in other versions of Coq, so
> I'll skip reporting them in detail and hope the issue goes away in time.
>
> Was I wrong to assume that this part would be easy?
>
> I've finished my exercise via the simple but clunky fix: copy the Mergesort
> library locally and factor out most of the implementation and some of the
> proofs into a part that uses a section variable rather than a module 
> parameter
> to pass the comparison function. Can anyone think of a better way?

I think you don't really need the `* A` part in reflection and what
you actually need is lists of type `list idx` where `idx` is some sort
of binary integers, which allow you to compare indices in O(log n)
time in reflection (note that `nat` is Peano natural numbers which is
not very efficient).

But, if you really need, there is a polymorphic `sort` function
defined in the Mathematical Components library:
https://github.com/math-comp/math-comp/blob/mathcomp-1.14.0/mathcomp/ssreflect/path.v#L885
I have another Coq library providing several efficient implementations
of mergesort, although it does not improve the performance regarding
`vm_compute` that much:
https://github.com/pi8027/stablesort

Also, since sorting is done by the repetition of "push" in any of
those implementations, you can easily define a function that sorts
trees directly without flattening it.

> Best regards and thanks for your patience,
>     Thomas.

Sorry for the short answers, but I'd like to elaborate on any of them
if you need.

Best,
Kazuhiko