The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

On Wed, 8 Jul 2020 21:56:10 -0400
Gregory Malecha <gregory AT bedrocksystems.com> wrote:

> ...
> > The decision procedure is still missing a transitive closure
> > component, though.  And that appears difficult to incorporate...
> >  
> If this is difficult due to termination, then the standard solution
> here is to use fuel.

That's part of it.


> ...
> > I think I misunderstood, then.  I thought the point to QUOTE was to
> > continue to use the proof-carying style instead of the
> > fully-reflective (Guillaume's) style, but still achieve both the
> > performance benefit and the modularity (reflective computations
> > cannot attempt to eliminate atoms from the original goal) that are
> > provided by the fully-reflective style.
> >  
> Sorry, no. The proof carrying style will always be slower because
> there are extra reductions and memory used to explicitly build the
> proof term.

Is that a shortcoming of Coq or something more ominous?  In my intuition
about erasability, it seems it should be possible for the execution to
use code with all erasable terms erased.

> 
> >  
> > >
> > > In your context, you could write
> > >
> > > Theorem reflection_works' : forall (f : Sorted_formula),
> > >     if solve_sorted f then sfDenote f else True.  
> >
> > Yes.  The attached file does that (although I changed the function
> > name from "solve_sorted" to "do_reflection" to avoid confusion with
> > the same named tactic).
> >  
> If [do_reflection] takes a long time to compute, you will want to
> change to the style where you introduce an explicit equality proof
> and use [vm_compute] to reduce it. This can be a *significant*
> savings for large reflective procedures. The section of my
> dissertation that I pointed you to should have a detailed description
> of why.
> 

If this is just due to the advantage of vm_compute over the execution
engine normally used for checking convertibility, then would it be
possible instead to use:

   let R := eval vm_compute in (do_reflection ...) in exact R

in the solve_sorted tactic in place of exact (do_reflection ...)
with no need for an explicit equality proof?

Jonathan