Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] lesson learned about reflection: atoms and transparency

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] lesson learned about reflection: atoms and transparency


Chronological Thread 
  • From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
  • To: Guillaume Melquiond <guillaume.melquiond AT inria.fr>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] lesson learned about reflection: atoms and transparency
  • Date: Sat, 11 Jul 2020 01:20:42 -0400
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk1-f179.google.com
  • Ironport-phdr: 9a23:IfaCtRAOupnNDEIyi6B8UyQJP3N1i/DPJgcQr6AfoPdwSP37oMywAkXT6L1XgUPTWs2DsrQY0rSQ6fqrCDZIoc7Y9ixbLdoUD15NoP5VtjRoONSCB0z/IayiRA0BN+MGamVY+WqmO1NeAsf0ag6aiHSz6TkPBke3blItdaz6FYHIksu4yf259YHNbAVUnjq9Zq55IAmroQnLucQanIpvJrwvxhfXrXdFf/pazn5sKV6Pghrw/Mi98INj/ihKp/4t68tMWrjmcqolSrBVEC4oOH0v6s3xshnDQwqP5n8CXWgTjxFFHQvL4gzkU5noqif1ufZz1yecPc3tULA7Qi+i4LtxSB/pkygIKTg0+3zKh8NqjaJbpBWhpwFjw4PRfYqYOuZycr/bcNgHXmdKQNpfWDJdDYO9d4sPDvQOPeBEr4nmulACqQKyCRSwCO/zzzNFgGL9068n3OQ7CQzI0gwuEcwTvnrXrtr1OqAcXu+pw6fH1jjDc+pW1C3h5IXSbhwso/eBVq9wf8rLzkkvEhvIgluSqYziOTOV1+cNvHaf7+V+S+2ikGEnqwRrrTiuwscgkJXGhoUQylzK6C50x4Q1Jdq+SE56Yt6rDp9QuD+EOIZtTcMiRntnuCc+yrEcpZG7ey0KxY0hyhXCZPOJb5KG7Qj/VOaNPzh4nnRldaqjihqs80WtxfPxW8u13VhEriRIjtnBu3QT2hHS9MWKV/tw8lu81TuOyQze9PxJLF47mKbHNZMvzKI9m5kXvEnDGCL9hUb4jLeOe0k65uSl7/7rb7bmq5OGKYN4lB/yPr4zlsG9Bek0KhYCUmmH9eih0bDv4En0T6lPg/A5k6TVrIzWKMEVq6O4DQ9Y14gu5hm8Ajqm1dkUg3cHLFxAdRKJkYflJk/CLfXlAvihgFmjijFmzO3cMLL7GJXCNH3Dna/hfblj705czxI+zdVF6JJVDrENOevzWkzsuNDBAB81Lg65zuL9BNVy0YMeXm2PAquHP6/IrVCI4ecvL/GNZI8Tpjn9N+Ao6+DygXI9g1MQfqmk0YEJZHymAPhqOViVbHjoj9sZFGcFpAs+TOjkiF2YVj5TYm6/X6A75jE9CYKmDpnMRoSzj7Ofxyq7EZhWaXpHClCIC3vna4KEW/IUZCKIPsBhiiAEVaSmS4I50BGhqgv6y6N6LurV/S0Ys4nu1dl05+3Wjh4y7yZ7A96c02GLVWF0n3kHSyU43KBluUZ90EuM0bBkg/xEEtxe/+9GUgAjNZLF0+N6D83yVRnac9eSSFemR82mDisrQtIwxd8OeUd9FM+4ghDNxSr5S4MSwpOWBZgw+7/Z0jDUKsJk1nfB0qVp21Y7Q89LPHCji+h6+gzKGo/OlUmxlqCwdK1a0jSbp0mZym/b9kNfVg9zXKHIUFgQY0LXqZLy4UaIB+usDrImMQZFxMOqJa5Da9mvhlJDEqSwcO/Can68zj/jTS2DwamBOc+zIz1EgXftTXMcmgVWxk6ocAgzAiD7/TDbBT1qUEvsOgbiqLYv7ny8SUAwwkeBaEgzj+PkqC5QvuSVTrYo5pxBvS4grztuG1PkhoDZDtOBo0xqe6AOOIphsmcC7nrQsklGBrLlN7pr3wdMfAF+vkeo3BJyWN1N

Guillaume,

I was able to find larger cases where the vm_cast_no_check eq_refl
method is significantly faster, so my hypothesis that the reflection
time would always overwhelm the convertibility check time is incorrect.
However, it seems that the following may be at least as fast as the
vm_cast_no_check eq_refl method. Define do_reflection using the
if-then-else method, and apply it as

abstract(vm_cast_no_check(do_reflection ...))

instead of

exact (do_reflection ...).

Is it possible that the use of abstract is preventing the duplicate
convertibility check?

Note that, unlike "vm_cast_no_check bogus" alone, which doesn't fail
until Qed, "abstract (vm_cast_no_check bogus)" does fail immediately,
hence it is checked at the close of the abstracted subproof. So my guess
is that the convertibility check is performed only once at the close of
the abstracted subproof and not again within the original goal or at its
Qed. Does that make sense?

That would suggest a generally useful tactic:

Ltac fast_exact X := abstract(vm_cast_no_check X).

On Thu, 9 Jul 2020 18:52:03 -0400
"jonikelee AT gmail.com" <jonikelee AT gmail.com> wrote:

> 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
>




Archive powered by MHonArc 2.6.19+.

Top of Page