coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Hugo Herbelin <Hugo.Herbelin AT inria.fr>
- To: AUGER Cedric <Cedric.Auger AT lri.fr>
- Cc: Daniel Schepler <dschepler AT gmail.com>, coq-club AT inria.fr
- Subject: Re: [Coq-Club] Having trouble understanding a proof term generated by fix
- Date: Sun, 24 Apr 2011 14:49:17 +0200
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.
Hugo
- [Coq-Club] Having trouble understanding a proof term generated by fix, Daniel Schepler
- Re: [Coq-Club] Having trouble understanding a proof term generated by fix,
Hugo Herbelin
- Re: [Coq-Club] Having trouble understanding a proof term generated by fix,
AUGER Cedric
- Re: [Coq-Club] Having trouble understanding a proof term generated by fix, Hugo Herbelin
- Re: [Coq-Club] Having trouble understanding a proof term generated by fix, Daniel Schepler
- Re: [Coq-Club] Having trouble understanding a proof term generated by fix,
AUGER Cedric
- Re: [Coq-Club] Having trouble understanding a proof term generated by fix,
Hugo Herbelin
Archive powered by MhonArc 2.6.16.