The Coq mailing list

[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)?

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?

Best regards and thanks for your patience,

    Thomas.