The Coq mailing list

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

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