The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Hi. Just for the record, let me mention the related work of Nguyen Quang Huy some years ago...

- Compact normalisation trace via lazy rewriting

10.1016/S1571-0661(04)00269-5

- Certifying term rewriting proof in ELAN
10.1016/S1571-0661(04)00295-6

- Rewriting Calculus and Automation of Proofs in Proof Assistants
http://protheo.loria.fr/users/nguyenqh/Thesis/thesis.pdf

- An ELAN-based tactic for AC rewriting in Coq is available here

- A Coq/ELAN interface for equational reasoning in Coq

See http://protheo.loria.fr/users/nguyenqh/ .

Le 08/10/2016 à 16:45, Stefan Ciobaca a écrit :

Nice! I would be very much interested in such a system.

I am aware of the following PhD thesis http://homepage.cs.uri.edu/faculty/hamel/pubs/theses/phd-thesis-kaplan.pdf in which (part) of rewriting logic is formalized in Coq. I'm not sure to what degree you can reuse this, but it might be a good starting point.

Best,
Stefan

On Sat, Oct 8, 2016 at 4:56 PM, Jannis Limperg <jannis AT limperg.de> wrote:
Dear Coq-Club,

I'm currently prototyping a library for general reflection-based
rewriting. The goal is to allow users to relatively easily specify
rewriting systems for arbitrary theories and use them to
normalise/simplify terms. To that end, I currently plan to proceed as
follows:


- Define a generic representation of terms, probably similar to that of
the CoLoR library.
- Have users provide a signature describing which interpreted symbols
their terms contain, and an interpretation function from the
representation to actual terms.
- Define a generic reflection tactic that, given a signature, reflects
the user's terms into the representation. (Not sure how much the user
has to help here.)
- Define transformations of representation terms for common properties
(associativity, symmetry, etc. pp.) and prove them correct (given a
proof that the user's terms actually have those properties). Allow users
to define transformations specific to their theories.
- Tie different transformations together with a fixpoint construction. [1]


One may view this as a generalisation of the ring/field tactics (though
I don't plan to reimplement those, at least not initially). Compared to
autorewrite, my scheme has the advantage of being able to exploit orders
on representation terms, which comes in handy when normalising symmetric
operations.

Now finally the question: Are you aware of any similar systems (in Coq
or elsewhere), or do you have any general advice/gotchas that I should
be aware of? I'd like to make as sure as possible that such a library
has at least a chance of being useful before spending a lot of time on it.

Thanks,
Jannis


[1] I plan to have the user be responsible for the termination of their
rewriting system. Everything else imho just leads to massive complexity.