The Coq mailing list

[Michael Day <mikeday AT yeslogic.com>]

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