The Coq mailing list

[Jonas Oberhauser <s9joober AT googlemail.com>]

As Adam has said and Frédéric points out again, the problem is your
Fixpoint. Coq will not fix-reduce unless the structure of the
recursive argument is known.

There are multiple ways to deal with this. The one most
straight-forward would be: make
the structure known to coq!

destruct prog. simpl.

and there you are.

Other ways, as pointed out by Frédéric: Change the recursive argument
to something of which you know the structure, or by Adam: Do not make
a fixpoint what is not a fixpoint ; )
In your case I would recommend Adam's solution, but sometimes that is
not possible, since you can't modify the code or it has to be a
recursive definition. My approach does work always, but it hurts more.

For whom it may concern:
I had a hard time thinking about why this fix-reduce restriction is
really necessary.

The reason is, of course, strong normalization.

Consider this example:

Inductive bad := bogus : bad -> bad.
Fixpoint f (b:bad) : bad := f (match b with bogus b' => b' end).

This types well in Coq.
If you would apply f to an assumed b of bad, an unrestricted
fix-reduce would yield no normal form. The reduction would diverge!

With kind regards,
Jonas

PS: I'm sorry, I /think/ I sent my reply to frederic when I actually
wanted to reply to the mailinglist. Sorry at those who received this
content twice, sorry at Jael who probably didn't receive it at all.
I'm not very confident with all this technical stuff like e-mails and
mailing lists in particular ;(

Best wishes,
Jonas

2012/2/21 Jael E. Kriener 
<jek26 AT kent.ac.uk>:
> 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.
>
>