The Coq mailing list

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

Thanks for that detailed explanation, Guillaume!

In my example tests so far, there is no significant speedup between
the original if-then-else method and the vm_cast_no_check eq_refl
method.  Of course, these examples are pretty small.  The eq_refl method
has slightly larger proof terms, as expected.

I think in this case, perhaps the type of the reified goal is so quickly
convertible back to the type of the goal (the denote routines have very
low complexity) that I will not likely encounter any significant speed
difference.  The time taken to reduce do_reflection will probably
overwhelm the convertibility check even more for larger cases. Unless
the time taken by Coq's convertibility checking grows much faster than
the reduction time within vm_cast_no_check?

BTW: I finished the transitive closure component.  Next up is using the
transitive closure to find contradictions (a<a) when the normal process
fails to solve the goal.

On Thu, 9 Jul 2020 10:31:14 +0200
Guillaume Melquiond <guillaume.melquiond AT inria.fr> wrote:

> Le 09/07/2020 à 04:41, jonikelee AT gmail.com a écrit :
> > 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?  
> 
> No, this does not help. There are several processing stages when
> writing "let R := eval vm_compute in (do_reflection ...) in exact R".
> 
> 1. Use the typing engine to check that "do_reflection ..." is
> well-typed. 2. Use the VM machinery to reduce "do_reflection ...".
> 3. Use the convertibility check to verify that R is convertible to
> the goal. 4. At Qed, use the convertibility check to verify that R is
> convertible to the goal.
> 
> Note that steps 3 and 4 are expensive, since the type of R is
> presumably way different from the goal. In fact, it might even have
> been faster not to use "vm_compute" and thus do step 2 in the first
> place.
> 
> Now, if your goal is "foo = true" and you do "vm_compute ; exact
> (eq_refl true)", then the steps are as follows:
> 
> 1. Use the VM machinery to reduce "foo = true".
> 2. Use the convertibility check to verify that "eq_refl true" is
> convertible to the goal (now "true = true").
> 3. Rinse and repeat at Qed time.
> 
> Notice that the convertibility check is now used only in a trivial way
> and thus instant. So, this is a huge speedup.
> 
> But there is still an overhead. Indeed, step 3 is redundant with
> steps 1 and 2. Unfortunately, step 3 cannot be removed. So, we just
> have to remove steps 1 and 2, right? That is how you do it: "abstract
> (vm_cast_no_check (eq_refl true))".
> 
> To summarize, the optimal way to do a proof by reflection is as
> follows. You have a property "is_foo", a decision procedure "foo" that
> (semi-)decides it, and a correctness lemma "foo_correct : foo = true
> -> is_foo". And you solve the goal by doing:
> 
> apply foo_correct.
> abstract (vm_cast_no_check (eq_refl true)).
> 
> Note: If this is the very last step of your whole proof script, you
> can remove "abstract". In fact, you can always remove "abstract", but
> unless it is the very last step of a proof, a failure of the decision
> procedure can lead to very confusing error message.
> 
> Best regards,
> 
> Guillaume