The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Le 26 juin 09 à 11:35, Adam Koprowski a écrit :

>    Dear all,

Hi Adam,

>   I have problems with reducing a function defined by means of a  
> Program with a measure. The manual promises:
> The reduction is a little more involved, although it works using  
> lazy evaluation;
>   This does not seem to be the case for me. Attached please find a  
> simplified example showing the problem. The [eval] function does not  
> reduce as expected, see the last line. Few comments:
> 	•  I'm showing a simplified example of a problem I have (yes, I  
> know that here [eval] is not recursive),
> 	•  it's for the trunk version of Coq; I don't remember and have a  
> difficult time figuring out what was the syntax for measures over  
> several arguments in Coq 8.2.
> 	•  I changed several things to axioms for space considerations -  
> defining them does not resolve the problem.

Well, you should at least define them. Measured functions are still  
recuring on the accessibility proof of the underlying relation
(x_measure_wf here). It seems to get stuck for just this reason here  
(at least at first). To prove that well_founded (MR ...) you
can first apply [measure_wf] from Program.Wf. Also, it's quite  
dangerous to use [auto] in these proofs, as it can introduce opaque
lemmas.

Hope this helps,
-- Matthieu