The Coq mailing list

[Gregory Malecha <gmalecha AT gmail.com>]

Hello, Jannis --

This is a problem that I have though a lot about. For my dissertation two years ago [1] I wrote the MirrorCore system (github.com/gmalecha/mirror-core) which implements a fair amount of what you described. The current (released) version contains an embedding of the simply typed lambda calculus which can be extended with a user-defined set of types and symbols (e.g. nat and plus). In addition to the reflected language, MirrorCore contains a reflective tactic language, called Rtac, that is similar to Ltac, and a reflective rewriting engine. Both of these are discussed in detail in last year's ESOP paper with Jesper Bengtson[2].

I am currently working with some people on adding second-class polymorphism, and have a slightly longer-term goal of adding full first-class polymorphism. 

I have thought a bit about implementing something like Knuth-Bendix on top of it, but I have not really started implementing it beyond a little bit of sketching. Personally, I think that it would be extremely useful to the community.

I would be very interested in discussing your ideas further. I also think that leveraging some of the existing work on mirror-core could make it easier to get up and running and my collaborators and I would be very interested in using your work to help with our broader goals of reflective automation for program verification (see, e.g. the examples in [1], [2], and [3]).

[1] Dissertation: https://gmalecha.github.io/publication/2015/02/01/extensible-proof-engineering-in-intensional-type-theory/

[2] ESOP'16: https://gmalecha.github.io/publication/2016/01/01/extensible-and-efficient-automation-through-reflective-tactics/

[3] ITP'14: https://gmalecha.github.io/publication/2014/07/14/compositional-computational-reflection/

On Sat, Oct 8, 2016 at 9:57 AM 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.

--

- gregory malecha
  gmalecha.github.io