The Coq mailing list

["J.E.Kriener" <jek26 AT kent.ac.uk>]

Dear all,

here is a self-contained version of the script attached to my earlier 
question.

Thanks again,
Jael

________________________________________
From: J.E.Kriener 
[jek26 AT kent.ac.uk]
Sent: 20 February 2012 13:27
To: 
coq-club AT inria.fr
Subject: [Coq-Club] question about evaluating a complex fixpoint

Dear all,

I have a question relating to evaluating a complex fixpoint. I'm attaching 
the script (which uses the CoLoR - library) with the problem marked in 
capitals, but really I just want to find out whether I'm going about this the 
right way or missing something really basic:

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'.


        'compute' takes some time and then produces a huge term (much bigger 
then the fixpoint itself) which I don't know how to use. I got a tip that to 
use 'compute', I need to prove an 'unfolding lemma' and machinery for that 
can be found in Program.Wf, but I'm finding Program.Wf less than 
self-explanatory -
        Question: If that's the way to go, are there examples of unfolding 
lemmata and their proofs somewhere that I could look at?

        Question: Are these the wrong tactics to use? If so, what are the 
right ones?

Thanks very much,

Jael

Attachment: trial_compute.v
Description: trial_compute.v