The Coq mailing list

[Julien Forest <forest AT ensiie.fr>]

On Sat, 27 Mar 2010 20:54:39 +1100
Michael Day 
<mikeday AT yeslogic.com>
 wrote:

> Hi,
> 
> Recently I have been using the "measure" function of Program to create 
> fixpoints that decrease on some measure of the arguments, which is 
> enormously useful for proving termination of functions that are not 
> structurally recursive in an obvious way.
> 
> However, reasoning about these fixpoints in later proofs is hard, as 
> they expand to a large term based on Fix_measure_F_sub that is difficult 
> to simplify during induction proofs.
> 
> Are there any common tips or tricks for working with measure functions 
> effectively? In the Program.Wf module there is a lemma called F_unfold 
> and some others, can these be used for manipulating terms during proofs?
> 
> Best regards,
> 
> Michael
> 
> -- 
> Print XML with Prince!
> http://www.princexml.com
Hi, 
you can try to use Function instead of Program Fixpoint. The two
feature are not exactly equivalent. In particular, Function will give
you a fixpoint equation for you function (aka a proof that $forall x, f
x = body_of_f$) and an induction principle for f which will (hopefully)
help you to reason about f. 


Best regards, 
Julien Forest