coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre Courtieu <Pierre.Courtieu AT sophia.inria.fr>
- To: Jean-Francois Monin <jeanfrancois.monin AT rd.francetelecom.com>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] relevance of evaluating accessibility arguments
- Date: Mon, 18 Nov 2002 13:12:22 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hello,
If you allow to reduce Fixpoint when the decreasing argument is not a
head-constructor term, then you will generally be able to do it
infinetely.
My (short) experience is that if it is a limitation then I chose the
wrong decreasing argument. Typically when the first Case in the
fixpoint is not on the decreasing argument:
Fixpoint f [x:A; a:(accessible x)] : B :=
Cases x of
| ... => b
| ... =>
Cases a of
| recursive calls
|
However in some rare cases there is no other choice for the decreasing
argument, and then it would be nice to be able to force (by rewrite?)
one step of beta-reduction inside a fixpoint. Using "Case a" to be
able to reduce is annoying, is there another way?
Pierre
Jean-Francois Monin
<jeanfrancois.monin AT rd.francetelecom.com>
wrote:
> Hello,
>
> Consider the following context:
>
> A, B : Set.
> Inductive accessible : A -> Prop := ...
> Fixpoint f [x:A; a:(accessible x)] : B := ...
>
> Now, given a closed value x:A and a non canonical proof a:(accessible x),
> I would expect that a lazy evaluation of (f x a) reduces to its normal
> form without evaluating a.
> But it does not seem to be the case. For example, if the following
> is an opaque theorem:
> Theorem all_acc : (x:A)(accessible x),
> you can observe that (f x (all_acc x)) is not computed in Coq V3.1,
> though the value of the second argument is not used the result
> (only its existence is important).
>
> On the other hand, it works if a is not the decreasing argument
> of the fixpoint f.
>
> What is happening ?
>
> Jean-Francois
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
> http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
--
Pierre Courtieu
- [Coq-Club] relevance of evaluating accessibility arguments, Jean-Francois Monin
- Re: [Coq-Club] relevance of evaluating accessibility arguments, Pierre Courtieu
- Re: [Coq-Club] relevance of evaluating accessibility arguments,
Randy Pollack
- lRe: [Coq-Club] relevance of evaluating accessibility arguments,
Eduardo Gimenez
- Re: [Coq-Club] relevance of evaluating accessibility arguments,
Jean-Francois Monin
- Message not available
- Re: [Coq-Club] relevance of evaluating accessibility arguments, Jean-Francois Monin
- Message not available
- Re: [Coq-Club] relevance of evaluating accessibility arguments,
Jean-Francois Monin
- lRe: [Coq-Club] relevance of evaluating accessibility arguments,
Eduardo Gimenez
- Re: [Coq-Club] relevance of evaluating accessibility arguments,
Jean-Francois Monin
- Re: [Coq-Club] relevance of evaluating accessibility arguments,
Judicael Courant
- Re: [Coq-Club] relevance of evaluating accessibility arguments,
Jean-Francois Monin
- Re: [Coq-Club] relevance of evaluating accessibility arguments, Benjamin Werner
- Re: [Coq-Club] relevance of evaluating accessibility arguments,
Jean-Francois Monin
- Re: [Coq-Club] relevance of evaluating accessibility arguments,
Judicael Courant
- Re: [Coq-Club] relevance of evaluating accessibility arguments,
Randy Pollack
- Re: [Coq-Club] relevance of evaluating accessibility arguments, Nicolas Magaud
- Re: [Coq-Club] relevance of evaluating accessibility arguments, Pierre Courtieu
Archive powered by MhonArc 2.6.16.