coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Program + measure -> reduction problems., Adam Koprowski
- Re: [Coq-Club] Program + measure -> reduction problems., Bruno Barras
- Re: [Coq-Club] Program + measure -> reduction problems., Matthieu Sozeau
- Re: [Coq-Club] Program + measure -> reduction problems.,
Adam Koprowski
- Re: [Coq-Club] Program + measure -> reduction problems., Matthieu Sozeau
- Re: [Coq-Club] Program + measure -> reduction problems.,
Adam Koprowski
Archive powered by MhonArc 2.6.16.