Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] RE: question about evaluating a complex fixpoint

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] RE: question about evaluating a complex fixpoint


chronological Thread 
  • From: Adam Chlipala <adamc AT csail.mit.edu>
  • To: "J.E.Kriener" <jek26 AT kent.ac.uk>
  • Cc: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] RE: question about evaluating a complex fixpoint
  • Date: Mon, 20 Feb 2012 15:26:28 -0500

On 02/20/2012 12:52 PM, J.E.Kriener wrote:
I've defined a function over (dependent) types using Fixpoint and refine. Now 
I'm trying to prove something about it. So I'm trying to apply it to some 
specific arguments and look at the result. But I seem to be unable to simply 
do that:

         'simpl' won't change a thing,
         neither will 'unfold ; simpl'.

[simpl] seems to do everything I expect in your simplified example. What about the behavior surprises you?

Your example is odd, in that you use [Fixpoint] to define a non-recursive function. Keep in mind that applications of recursive functions can only simplify when the top-level structure of the recursive argument is known. Perhaps an annotation to indicate which argument is recursive would help you somewhere.

But I would just use [Definition] instead of [Fixpoint], in any case.

P.S.: The example still imports CoLoR modules, though it doesn't use them later.



Archive powered by MhonArc 2.6.16.

Top of Page