Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] relevance of evaluating accessibility arguments

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] relevance of evaluating accessibility arguments


chronological Thread 
  • 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 




Archive powered by MhonArc 2.6.16.

Top of Page