Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Ltac question/challenge: working with open terms

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Ltac question/challenge: working with open terms


Chronological Thread 
  • From: Adam Chlipala <adamc AT csail.mit.edu>
  • To: robert <robdockins AT fastmail.fm>
  • Cc: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Ltac question/challenge: working with open terms
  • Date: Sun, 15 Sep 2013 15:42:50 -0400

On 09/15/2013 03:25 PM, robert wrote:

I've copied below a simplified version of a tactic I've been playing with recently to automatically convert terms into applicative form using SKI combinators. (why? I'm evaluating the hypothesis that proof automation for properties about functions works better when things are in applicative form)

 

The hard part here is opening up lambda-terms to work on their bodies. I've found a trick that lets me do pretty much what I want, but it has the side-effect of generating useless and potentially large proof structure. I've found this can have a noticable effect on Qed time for some examples. I wonder if there is a way to accomplish the same thing without cluttering up the generated proof.


Have you read Section 15.5 of CPDT <http://adam.chlipala.net/cpdt/>?  I haven't read all of the code you included, but the prose makes it sound like that section shows how to do what you're looking for.



Archive powered by MHonArc 2.6.18.

Top of Page