The Coq mailing list

[Adam Koprowski <adam.koprowski AT gmail.com>]

  Dear Bruno, Dear Matthieu,

  Thanks for the hints; I'll need to check more carefully what opaque constants are blocking the reduction - it was easy for this simplified example, however in the real one it's not so immediate. Btw. there was some discussion some time ago on the list about a Print Opaque Constants id, that would work similarly to Print Assumptions id, but searching for opaque constants; is it by any chance available in the trunk? That would make such hunting for opaque constants much easier :).

  Cheers,
   adam

On Fri, Jun 26, 2009 at 18:02, Matthieu Sozeau <mattam AT mattam.org> wrote:

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

-- 
=====================================================
Adam.Koprowski AT gmail.com, http://www.cs.ru.nl/~Adam.Koprowski

The difference between impossible and possible
lies in determination (Tommy Lasorda)
=====================================================