The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

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