Retraction on Coq and lists

Okay, so everything I said the other day about mutually defining your ASTs in Coq with custom lists, and then using Coq's implicit coercions to move back and forth between lists as defined in Coq's standard library, does not work.  Firstly, the coercions will not always be inserted when you will need them, and even inserting the coercions manually does not work out well as Coq will then not be able to determine that recursive functions you define on your ASTs will necessarily terminate.

So I have switched back to using lists from the standard library and hoping that defining custom induction principles based upon Yves Bertot's suggestion in the discussion here will work for everything I need to do.

2 Comments »

  1. Andrew said,

    December 18, 2007 @ 1:28 pm

    Let the good times roll!

    Have you tried using the termination ordering stuff for functions that was added in 8.1? I think it generates a separate lemma you prove to show termination. Haven’t tried it myself…

  2. washburn said,

    January 8, 2008 @ 1:57 pm

    No I have not tried using the new »Function« form of definition. I might have been able to use it in the places I was running into problems, but I figured that if I was having that much difficulty with really simple functions, then I was probably on the wrong track. In retrospect, I think the problems may have also been caused by the fact that the typechecker will apparently unfold functions defined using »Definition«, but not ones defined using »Fixpoint«.

RSS feed for comments on this post · TrackBack URI

Leave a Comment