The Coq mailing list

[Jean-Francois Monin <jeanfrancois.monin AT rd.francetelecom.com>]

Beware: my problem is not in the definition of the fixpoint
but in its use.

  JF

Pierre Courtieu a ecrit :
 > 
 > 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