The Coq mailing list

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

Le 30/06/2020 à 20:00, jonikelee AT gmail.com a écrit :
> I've attached the now working reflection code as a stand-alone .v file,
> so that you can judge if it does reflection properly.

Your final theorem states:

reflect_sorted :
forall (A : Set) (ordA : Ordered A)
  (atomics : list (@Atom A)) (f : Sorted_formula),
if solve_sorted atomics f then sfDenote atomics f else True

Your decision procedure "solve_sorted" suffers from two flaws, in my
opinion. First, it takes "atomics" as argument, that is, it has access
to all the atoms and performs computations on them, instead of
considering them as opaque. A proper decision procedure would only take
the reified formula "f" as argument.

Second, it does not return a value of type "bool" but a value of type
"option P" with "P:Prop". In other words, it computes a large proof term
of type "P" for naught. Sure, the return type becomes "bool" if you were
to extract your procedure and run it outside of Coq, but you are running
it inside Coq. (Hopefully, the laziness of Coq's conversion checker will
avoid building the whole proof term, but that might require a lot of
tweaking using the "Strategy" command.)

To summarize, I see little hope that a function "solve_sorted" with such
a signature will ever work in an efficient manner. Unfortunately, this
signature is a direct consequence of your proof style, so I have no
simple suggestion to provide.

Best regards,

Guillaume