The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Sun, 24 Apr 2011 14:49:17 +0200,
Hugo Herbelin 
<Hugo.Herbelin AT inria.fr>
 a écrit :

> Hi Cedric,
> 
> > > fix Pind2 (P : positive -> Prop) (H1 : P 1)
> > >           (Hind : forall p : positive, P p -> P (Psucc p))
> > >           (H:=
> > >            fun p : positive =>
> > >            Pind2 (fun p0 : positive => P p0~0) (let H2 := Hind 1
> > > H1 in H2) (fun (p0 : positive) (IHp : P p0~0) =>
> > >               let IHp0 := Hind p0~0 IHp in let IHp1 := Hind p0~1
> > > IHp0 in IHp1) p) (p : positive) {struct p} : P p :=
> > >   match p as p0 return (P p0) with
> > >   | p0~1 => let H0 := H p0 in let H2 := Hind p0~0 H0 in H2
> > >   | p0~0 => H p0
> > >   | 1 => H1
> > >   end
> > >      : forall P : positive -> Prop,
> > >        P 1 ->
> > >        (forall p : positive, P p -> P (Psucc p)) -> forall p :
> > > positive, P p
> 
> > but in what should have been generated by Hugo, shouldn't the 
> > "(H := fun ... => ...)" be inside a "let ... in ..." rather than a
> > parameter, or did I miss something?
> 
> If you mean that the above printed fixpoint cannot be built at
> top-level using a fixpoint definition (and in particular cannot be
> reparsed), the answer is yes and this is because the body of H depends
> on the recursive call Pind2, a "feature" of the internal
> representation of terms in the type-checking kernel that the "fix f
> binders {struct id} : type" construction of the high-level input
> language does not support.
> 
> If you mean that the fix tactic should only generate expressions that
> do not exploit this "feature" of the kernel (so that it is then
> reparsable), I can certainly approve. For information, the kernel
> representation of the above fixpoint (in informal syntax) is:
> 
> fix Pind2 {struct p}
>     := fun P H1 Hind (H:=...) p => match ... with ... end
>     :  forall P, P 1 -> (forall p, P p -> P (Psucc p)) -> forall p, P
> p
> 
> In particular, the kernel internal representation does not expect the
> body and the type of the fixpoint to share the very same prefix of
> binders, on the contrary of the high-level syntax, and only the type
> part of the internal expression has to satisfy the constraint that
> Pind2 does not recursively occur in it.

Is there some reason to allow a binding as parameter?
At first sight, it doesn't seem to be usefull to have such a feature.
I guess but I am not sure that it is to ease guard checking, as the
recursive call is isolated, but when you write the Fixpoint manually
(putting the "H:=..." under a "let" inside of the body), such a trick
doesn't appear when you do the "Print".
Maybe also it has to do with the "Guarded" command, as the kernel is
immediately provided a term having information on how the recursion is
done.
Is that also to say that with the tactics you can build "more
efficient" terms than without (as you can build terms you cannot
write using the gallina syntax)?

If no efficiency is involved, I think it would have been better for the
tactic to put the "H" under a "let" (just before the Qed/Defined
time, if the "Guarded" command is involved).
> 
> Hugo