coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] automatically normalize terms of certain types - is this possible?

From: Jonathan Leivent <jonikelee AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] automatically normalize terms of certain types - is this possible?
Date: Wed, 30 Sep 2015 10:42:54 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f178.google.com
Ironport-phdr: 9a23:IC1I4RELWmjdO61lVXw+jZ1GYnF86YWxBRYc798ds5kLTJ75oM6wAkXT6L1XgUPTWs2DsrQf27aQ7firATBIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/ni6bso9aLP01hv3mUX/BbFF2OtwLft80b08NJC50a7V/3mEZOYPlc3mhyJFiezF7W78a0+4N/oWwL46pyv+YJa6jxfrw5QLpEF3xmdjltvIy4/SXEGCCI/zM3Vngc2k5DBBGA5xXnVL/wtDH7v6xzwn/JE9fxSOUWXjKr86diTlfMhSYZOjgluDXVjcpxj69frR+JqBl2woqSa4aQYqktNpjBdM8XEDISFv1aUDZMV8blN9MC

Is it possible, using something like canonical structures or type classes, to convince Coq to always normalize terms of certain types for which a normal form exists, using a tactic that produces that normal form?

An example would be ring_simplify on ring terms.

Currently, I'm using an extern hint to do this, but of course that only works during (e)auto, and it makes (e)auto quite slow, as it has to search for ring terms at every step.

-- Jonathan

[Coq-Club] automatically normalize terms of certain types - is this possible?, Jonathan Leivent, 09/30/2015