Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Program + measure -> reduction problems.

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Program + measure -> reduction problems.


chronological Thread 
  • From: Matthieu Sozeau <mattam AT mattam.org>
  • To: Adam Koprowski <adam.koprowski AT gmail.com>
  • Cc: Coq Club <coq-club AT pauillac.inria.fr>
  • Subject: Re: [Coq-Club] Program + measure -> reduction problems.
  • Date: Fri, 26 Jun 2009 12:02:04 -0400
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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





Archive powered by MhonArc 2.6.16.

Top of Page