The Coq mailing list

[Fr�d�ric Besson <frederic.besson AT inria.fr>]

Hello Jael,

For your Fpd function, which argument do you wish to recurse on ?
As you did not write {struct ...} annotation, Coq infers {struct prog}.
If I write {struct a} instead, the definition is also accepted but the 
computational behaviour is not the same -- simpl works.

(Sometimes, it can be useful to define the "same" function with different 
{struct x} annotations and prove their equivalence.)

Best,

--
Frédéric




On 21 févr. 2012, at 10:20, Jael E. Kriener wrote:

> Thanks for the quick reply, Adam!
> 
> I attached the wrong file the second time around - I'm very sorry! This one 
> is self-contained and useful. Sorry again.
> 
> Is it possible that using 8.4beta might make this trivial?
> 
> Jael
> 
> 
> On 20/02/12 20:26, Adam Chlipala wrote:
>> 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.
> 
> <compute-problem.v>