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: Gregory Malecha <gregory AT bedrocksystems.com>
  • To: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] lesson learned about reflection: atoms and transparency
  • Date: Wed, 8 Jul 2020 21:56:10 -0400
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gregory AT bedrocksystems.com; spf=None smtp.mailfrom=gregory AT bedrocksystems.com; spf=None smtp.helo=postmaster AT mail-pf1-f181.google.com
  • Ironport-phdr: 9a23:LoBs2RPsHoe1mTBV9A8l6mtUPXoX/o7sNwtQ0KIMzox0K/z7o8bcNUDSrc9gkEXOFd2Cra4d1ayP4+u8CSRAuc/H7ClfNsQUFlcssoY/p0QYGsmLCEn2frbBThcRO4B8bmJj5GyxKkNPGczzNBX4q3y26iMOSF2kbVImbuv6FZTPgMupyuu854PcYxlShDq6fLh+MAi6oR/eu8ULgIZuMLs9xxjGrnZHeOld2GdkKU6Okxrm6cq84Z5u/z5Mt/498sJLTLn3cbk/QbFEFjotLno75NfstRnNTAuP4mUTX2ALmRdWAAbL8Q/3UI7pviT1quRy1i+aPdbrTb8vQjSt871rSB7zhygZMTMy7XzahdZxjKJfpxKhugB/zovJa4ybKPZyYqXQds4dSmRcQ8ZRTDRBDZ2gYIsTAeQBOuNYoJP8p1sIsBCyAQahCefqxjJOm3T437A10/45HA7J0gwvHdIAvnrXotvoKqkdTfu4w7PUwTjZdf5axSvx5YrOfxs8of+MR7Vwcc/JxEcuDQPKkFqQqYv/PzKVy+8DtHKU7+5+Wu2zi24osRx6rz+gxsc2lIbJiYUVykrE9Chi24k6O8C3SFR8YdG4E5tQrCGbN5BqQsw8RmFoozw2xaEBuZ6+ZSUHzoksyBHDZfKdaYeI/g7jW/iLITd+nH9od7ayiwuv/UavyuDxV8i53EtFoCZbkdTBq24A2RPT5MaHSPZw8USs1DWT2w3T5exIPVw4mbbYJpM9wbM9mYcevELeFSH4n0X2ibWZdkQi+uWw5OTnY6nmpp+BN4BvkA3xLqMumsmnDesiKAQOW3KU9fyz1L3i4U35QKhKgeYsnqnYt5DXI9kQqK2hAwJNzIov9xKyAy2l3dkYh3ULMk9JdA6dg4T0OFzCPfb1BuqljVu2ijdk3fXGM6XhAprTKnjDl6/sfbNn5E5dzAo/1Mhf55xJBr0YLvL/R0z8uMHCAh82NAy0xOnnCNFj2Y8ERW2PBaqZPLvTsV+O+O0vP/GBaJEJtDv5MfQo5P7jgWUnlVMAYaWlx4YbZXOlEvh+JkWWe3vsgtMPEWcQuQo+SfTniFKYUTFNaHayWLg85zEgBY29E4jMW5qtgLud0ye4BZ1XZntGCkySHnftbIWIQesDaCWXIsN5iDwLSaChS5M91RGprAL1171nLvPN9iIEsZLjycN66vbIlRAy8Dx0F96S33uMT2FyhGMIRiU50LpxoUxnmR+/1v0ygfteFN9e4/5Eegg/PJ/Yied9Dpq6DgDGeNaKRVKrT/2pBDgwSpQ6xNpYMGhnHND3oQrO0C2wEvcwnriGD5w9uvbTxXX+INxs43zL2LMmhFo9U9BTOGi9wKV48l6AVMbyj0yFmvPyJuwn1ynX+TLfnDPS7nEdaxZ5VOD+ZV5aflHf94yr7E7OVbilCq82KRdMzNXEIaxPOIWw0Ad2Acz7MdGbWFqf3me9ARHSmOGJZYvuPn0ThWDTURhd1Q8U+nmCOE41ASLz+zuPXgwrLkrmZgbXycc7rXq6SkEuyATQNx9r2rav/RUWnu2HV/4WxfQPvyJz8zg=

Hi Jonathan --

On Wed, Jul 8, 2020 at 6:06 PM jonikelee AT gmail.com <jonikelee AT gmail.com> wrote:
On Wed, 8 Jul 2020 17:21:06 -0400
Gregory Malecha <gregory AT bedrocksystems.com> wrote:

>...
> I don't think that this would be a very difficult translation to pull
> off. In most cases there is a mechanical translation.

I did it by hand - the result is attached.  And, as advertised, it
delivered considerable speedup. About 100x faster for that
"slooooow" test case. 

But, I am curious about the mechanical translation from one proof style
to another.  Can you elaborate?
It is essentially what Coq's extraction mechanism does. I'm not aware of any implementation of it that will produce a Gallina term, but there might be something in the meta coq project (https://github.com/MetaCoq/metacoq).

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.

>
> > 
> > >
> > > One thing that I've wanted for a while is the ability to control
> > > reduction with quoting and anti-quoting mechanisms a.la. meta
> > > programming. For example, something that would look roughly like
> > > this.
> > >
> > > Compute List.rev ((QUOTE (List.rev []) :: QUOTE (a ++ b) :: nil)
> > > ++ []). = [QUOTE (List.rev []); QUOTE (a ++ b)]
> > >
> > > Note that QUOTE semantically acts as id, but for the purposes of
> > > reduction it blocks reduction of its "argument" (it really only
> > > allows substitutions). This would make it possible to write what
> > > you want without needing to introduce names. It also allows you
> > > to eliminate the required phase separation in standard reflective
> > > automation as mentioned by Guillaume (chapter 4, specifically
> > > 4.3, of my dissertation discusses some of these issues as well:
> > > https://gmalecha.github.io/publications/files/malecha-dissertation.pdf).
> > > 
> >
> > I have been having a discussion elsewhere with an Idris developer
> > involved in implementing erasability in Idris (now Idris2).  The new
> > Idris2 erasability binder annotations sound like they could be used
> > in the same way as you describe QUOTE, allowing one to selectively
> > determine which functions can and cannot compute on which arguments.
> > Furthermore, as they are built into Idris2, the language itself can
> > easily take advantage - skipping them completely during
> > computation, not just during extraction.  I wish Coq has something
> > similar, as it would also allow me to drop the erasure axiom
> > (relevant Prop) hack I use elsewhere.
> > 
> I think that QUOTE is a little bit different than erasability in
> general, though it might operate the same way for your purpose.
> Consider, for example, you have a reflective procedure that doesn't
> solve the goal:
>
> Definition simplify_things (ls : list Prop) : list Prop.
> Theorem simplify_things_ok : forall ls,
>    goalD (simplify_things ls) -> goalD ls.
>
> You can clearly still phrase this in the standard fully-reflective
> style (as Guillaume suggested):
>
> Definition rsimplify_things (ls : list term) : list term.
> Theorem simplify_things_ok' : forall (ls ls' : list term),
>   rsimplify_things ls = ls' ->
>   forall mp : instantiation, goalD mp ls' -> goalD mp ls.
>
> but things are a bit more verbose. Especially, note the (seemingly
> useless) equality proof, which hangs around because we want to use
> [vm_compute] to reduce [rsimplify_things], but we can not use
> [vm_compute] to simplify [goalD] because doing that would destroy the
> structure of our propositions.
>
> Using QUOTE, you can write the original soundness theorem, and simply
> introduce a QUOTE around every symbol that you want to leave
> uninterpreted.

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.

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

Jonathan




--

Gregory Malecha

Mail: gregory AT bedrocksystems.com

BedRock

Systems Inc
UNBREAKABLE FOUNDATION FOR

FORMALLY SECURED COMPUTING



Archive powered by MHonArc 2.6.19+.

Top of Page