The Coq mailing list

[Gregory Malecha <gregory AT bedrocksystems.com>]

It is a bit unfortunate that Coq's reduction mechanism works in this way, I too have often found that there are times that I would like to do lightweight computation using efficient reduction mechanisms. My understanding is that IPM suffers some of the same issues, you want to partition the hypotheses efficiently, but you don't want to compute inside them and it doesn't always make sense to go the full Atom route that Guillaume suggested above.

One thing that I've wanted for a while is the ability to control reduction with quoting and anti-quoting mechanisms a.la. meta programming. For example, something that would look roughly like this.

Compute List.rev ((QUOTE (List.rev []) :: QUOTE (a ++ b) :: nil) ++ []).

= [QUOTE (List.rev []); QUOTE (a ++ b)]

Note that QUOTE semantically acts as id, but for the purposes of reduction it blocks reduction of its "argument" (it really only allows substitutions). This would make it possible to write what you want without needing to introduce names. It also allows you to eliminate the required phase separation in standard reflective automation as mentioned by Guillaume (chapter 4, specifically 4.3, of my dissertation discusses some of these issues as well: https://gmalecha.github.io/publications/files/malecha-dissertation.pdf).

On Tue, Jun 30, 2020 at 4:00 AM Guillaume Melquiond <guillaume.melquiond AT inria.fr> wrote:

Le 29/06/2020 à 21:21, jonikelee AT gmail.com a écrit :

> I just learned an interesting lesson about writing decision
> procedures using reflection in Coq.  It's probably one that others have
> encountered before - so "tl;dr" if this is a familiar refrain: functions
> used within reflection procedures are not the only elements where
> transparency (Defined vs. Qed) needs to be considered.  Atoms matter,
> too.

You seem to be using a rather peculiar definition of reflection. Atoms
should be opaque, by definition. Or rather, since the ability to
distinguish atoms is critical for most decision procedures, atoms should
just be addresses (e.g., closed integers generated by a gensym
function). For example, a decision procedure on propositional logic will
manipulate terms of the following type:

Inductive term : Set :=
  | Atom (n : nat)
  | Neg (t : term)
  | And (t1 t2 : term).

An object of type term is necessarily closed, unless your reification
procedure contains a bug. As a consequence, your computations should
never get stuck.

From reading your email, I am under the impression that your Atom
constructor takes an argument that comes directly from the original goal
or hypotheses. If so, this no longer qualifies as reflection.

Best regards,

Guillaume

--

Gregory Malecha

Mail: gregory AT bedrocksystems.com

BedRock

Systems Inc
UNBREAKABLE FOUNDATION FOR

FORMALLY SECURED COMPUTING