coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- [Coq-Club] question about evaluating a complex fixpoint, J.E.Kriener
- [Coq-Club] RE: question about evaluating a complex fixpoint,
J.E.Kriener
- Re: [Coq-Club] RE: question about evaluating a complex fixpoint, Adam Chlipala
- Re: [Coq-Club] RE: question about evaluating a complex fixpoint,
Jael E. Kriener
- Re: [Coq-Club] RE: question about evaluating a complex fixpoint, Frédéric Besson
- Re: [Coq-Club] RE: question about evaluating a complex fixpoint, Jonas Oberhauser
- Re: [Coq-Club] RE: question about evaluating a complex fixpoint,
Jael E. Kriener
- Re: [Coq-Club] RE: question about evaluating a complex fixpoint, Adam Chlipala
- [Coq-Club] RE: question about evaluating a complex fixpoint,
J.E.Kriener
Archive powered by MhonArc 2.6.16.