Meta theory: induction over terms with abstract variables

[Robbert Krebbers]

Hi,

I'm trying to formalize Gamma Infinity, an approach to type theory without the need for explicit contexts (by Geuvers, McKinna, and Wiedijk, http://www.cs.ru.nl/~james/2009-TLCA/submitted.pdf). An essential feature is that free variables are annotated with types; for example s ^ (N* -> N*) is the successor function on the natural numbers.

My pseudo terms are defined as follows.

Inductive binder : Set := abs | pi.
Inductive trm (var : Set) : Set :=
    srt : sort -> trm var
  | bvr : nat -> trm var
  | fvr : var -> trm var
  | bnd : binder -> trm var -> trm var -> trm var
  | app : trm var -> trm var -> trm var

Here bound variables are represented by de Bruijn indexes and free variables are abstract. In this way I can use a regular representation of free variables to obtain the pseudo terms of a PTS or the following type to obtain the pseudo terms of Gamma Infinity.

Inductive avar : Set :=  avr : var -> trm avar -> avar

In this way I don't have to state various notions like opening, closing and substitution twice. Now I tried defining the induction scheme as follows:

Variables (P : avar -> Set) (Q : atrm -> Set).

Hypothesis
  (H  : forall s : sort, Q (asrt s))
  (H0 : forall n : nat, Q (abvr n))
  (H1 : forall a : avar, P a -> Q (afvr a))
  (H2 : forall (b : binder) (t1 : atrm) (t2 : atrm),
     Q t1 -> Q t2 -> Q (abnd b t1 t2))
  (H3 : forall (t1 : atrm) (t2 : atrm),
     Q t1 -> Q t2 -> Q (aapp t1 t2))
  (H4 : forall (v : var) (t : atrm), Q t -> P (avr v t)).

Fixpoint avar_rec2 (a : avar) : P a :=
  match a as x return P x with
  | avr v t => H4 v t (trm_rec2 t)
  end
with trm_rec2 (t : trm avar) : Q t :=
  match t as t0 return Q t0 with
  | srt s => H s
  | bvr n => H0 n
  | fvr a => H1 a (avar_rec2 a)
  | bnd b t0 t1 => H2 b t0 t1 (trm_rec2 t0) (trm_rec2 t1)
  | app t0 t1 => H3 t0 t1 (trm_rec2 t0) (trm_rec2 t1)
  end.

Unfortunately this does not work, the system gives the following error:

  Error:
  Recursive definition of trm_rec2 is ill-formed
  ...
  Recursive call to avar_rec2 has principal argument equal to "a"
  instead of a subterm of t

If I change it to the following definition, where the second fixpoint is inline, it works. But then trm_rec2 is not accessible from the outside.

Fixpoint avar_rec2 (a : avar) : P a :=
  match a as x return P x with
  | avr v t => H4 v t ((
    fix trm_rec2 (t : atrm) : Q t :=
      match t as t0 return Q t0 with
      | srt s => H s
      | bvr n => H0 n
      | fvr a => H1 a (avar_rec2 a)
      | bnd b t0 t1 => H2 b t0 t1 (trm_rec2 t0) (trm_rec2 t1)
      | app t0 t1 => H3 t0 t1 (trm_rec2 t0) (trm_rec2 t1)
      end
    ) t)
  end.

I can't quite figure out why Coq is complaining about it. Is anyone able to help me out on this?

Thanks in advance,

Robbert

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/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

[Adam Chlipala-3]

Robbert Krebbers wrote:

> Fixpoint avar_rec2 (a : avar) : P a :=
>  match a as x return P x with
>  | avr v t => H4 v t (trm_rec2 t)
>  end
> with trm_rec2 (t : trm avar) : Q t :=
>  match t as t0 return Q t0 with
>  | srt s => H s
>  | bvr n => H0 n
>  | fvr a => H1 a (avar_rec2 a)
>  | bnd b t0 t1 => H2 b t0 t1 (trm_rec2 t0) (trm_rec2 t1)
>  | app t0 t1 => H3 t0 t1 (trm_rec2 t0) (trm_rec2 t1)
>  end.
>
> Unfortunately this does not work, the system gives the following error:
>
>  Error:
>  Recursive definition of trm_rec2 is ill-formed
>  ...
>  Recursive call to avar_rec2 has principal argument equal to "a"
>  instead of a subterm of t
>
> If I change it to the following definition, where the second fixpoint
> is inline, it works. But then trm_rec2 is not accessible from the
> outside.
>
> Fixpoint avar_rec2 (a : avar) : P a :=
>  match a as x return P x with
>  | avr v t => H4 v t ((
>    fix trm_rec2 (t : atrm) : Q t :=
>      match t as t0 return Q t0 with
>      | srt s => H s
>      | bvr n => H0 n
>      | fvr a => H1 a (avar_rec2 a)
>      | bnd b t0 t1 => H2 b t0 t1 (trm_rec2 t0) (trm_rec2 t1)
>      | app t0 t1 => H3 t0 t1 (trm_rec2 t0) (trm_rec2 t1)
>      end
>    ) t)
>  end.
>
> I can't quite figure out why Coq is complaining about it. Is anyone
> able to help me out on this?

Mutual recursion is only allowed using types that were defined as
mutually inductive.  Your [term] and [avar] types aren't defined
mutually, so it isn't allowed.  Instead, you need to use a "nested"
recursion scheme, as you've done above.

I suggest defining a version of [term_rec2] that is parametrized by the
definition of [avar_rec2].  Then you should be able to define
[avar_rec2] using that new function, and then [term_rec2] should be
definable with no further recursion.

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/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

[Brian E. Aydemir]

Quoting Robbert Krebbers <robbertkrebbers@...>:

> Fixpoint avar_rec2 (a : avar) : P a :=
>  match a as x return P x with
>  | avr v t => H4 v t (trm_rec2 t)
>  end
> with trm_rec2 (t : trm avar) : Q t :=
>  match t as t0 return Q t0 with
>  | srt s => H s
>  | bvr n => H0 n
>  | fvr a => H1 a (avar_rec2 a)
>  | bnd b t0 t1 => H2 b t0 t1 (trm_rec2 t0) (trm_rec2 t1)
>  | app t0 t1 => H3 t0 t1 (trm_rec2 t0) (trm_rec2 t1)
>  end.
>
> Unfortunately this does not work, the system gives the following error:
>
>  Error:
>  Recursive definition of trm_rec2 is ill-formed
>  ...
>  Recursive call to avar_rec2 has principal argument equal to "a"
>  instead of a subterm of t

I've encountered this problem before [1], and as far as I know, Adam's  
suggestion is the way to go.  For the sake of concreteness, I've  
included below code that implements the basic idea.

Cheers,
Brian

[1] A non-bug report involving lists and a separate inductive type:
     http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=1751

(* *********************************************************************** *)

Parameter sort : Set.

Inductive binder : Set := abs | pi.
Inductive trm (var : Set) : Set :=
    srt : sort -> trm var
  | bvr : nat -> trm var
  | fvr : var -> trm var
  | bnd : binder -> trm var -> trm var -> trm var
  | app : trm var -> trm var -> trm var.

(* *********************************************************************** *)

Section Induction.

Variables
   (var : Set)
   (P : var -> Set)
   (Q : trm var -> Set)
   (f : forall v, P v).

Hypotheses
  (H  : forall s : sort, Q (srt _ s))
  (H0 : forall n : nat, Q (bvr _ n))
  (H1 : forall a : var, P a -> Q (fvr _ a))
  (H2 : forall b t1 t2, Q t1 -> Q t2 -> Q (bnd _ b t1 t2))
  (H3 : forall t1 t2, Q t1 -> Q t2 -> Q (app _ t1 t2)).

Fixpoint trm_rec' (t : trm var) : Q t :=
   match t with
     | srt s => H s
     | bvr n => H0 n
     | fvr v => H1 v (f v)
     | bnd b t1 t2 => H2 b t1 t2 (trm_rec' t1) (trm_rec' t2)
     | app t1 t2 => H3 t1 t2 (trm_rec' t1) (trm_rec' t2)
   end.

End Induction.

(* *********************************************************************** *)

Parameter var : Set.
Inductive avar : Set :=  avr : var -> trm avar -> avar.

Notation atrm := (trm avar).
Notation asrt := (srt avar).
Notation abvr := (bvr avar).
Notation afvr := (fvr avar).
Notation abnd := (bnd avar).
Notation aapp := (app avar).

(* *********************************************************************** *)

Section Induction2.

Variables
   (P : avar -> Set)
   (Q : atrm -> Set).

Hypothesis
  (H  : forall s : sort, Q (asrt s))
  (H0 : forall n : nat, Q (abvr n))
  (H1 : forall a : avar, P a -> Q (afvr a))
  (H2 : forall (b : binder) (t1 : atrm) (t2 : atrm),
     Q t1 -> Q t2 -> Q (abnd b t1 t2))
  (H3 : forall (t1 : atrm) (t2 : atrm),
     Q t1 -> Q t2 -> Q (aapp t1 t2))
  (H4 : forall (v : var) (t : atrm), Q t -> P (avr v t)).

Fixpoint avar_rec2 (v : avar) : P v :=
   match v with
     | avr v t => H4 v t (trm_rec' _ P Q avar_rec2 H H0 H1 H2 H3 t)
   end.

Definition trm_rec2 := trm_rec' _ P Q avar_rec2 H H0 H1 H2 H3.

End Induction2.

(*
avar_rec2
      : forall (P : avar -> Set) (Q : atrm -> Set),
        (forall s : sort, Q (asrt s)) ->
        (forall n : nat, Q (abvr n)) ->
        (forall a : avar, P a -> Q (afvr a)) ->
        (forall (b : binder) (t1 t2 : atrm), Q t1 -> Q t2 -> Q (abnd b  
t1 t2)) ->
        (forall t1 t2 : atrm, Q t1 -> Q t2 -> Q (aapp t1 t2)) ->
        (forall (v : var) (t : atrm), Q t -> P (avr v t)) ->
        forall v : avar, P v

trm_rec2
      : forall (P : avar -> Set) (Q : atrm -> Set),
        (forall s : sort, Q (asrt s)) ->
        (forall n : nat, Q (abvr n)) ->
        (forall a : avar, P a -> Q (afvr a)) ->
        (forall (b : binder) (t1 t2 : atrm), Q t1 -> Q t2 -> Q (abnd b  
t1 t2)) ->
        (forall t1 t2 : atrm, Q t1 -> Q t2 -> Q (aapp t1 t2)) ->
        (forall (v : var) (t : atrm), Q t -> P (avr v t)) ->
        forall t : atrm, Q t
*)

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/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

[Robbert Krebbers]

Hi,

Brian E. Aydemir wrote:
> I've encountered this problem before [1], and as far as I know, Adam's
> suggestion is the way to go.  For the sake of concreteness, I've
> included below code that implements the basic idea.
>
> Cheers,
> Brian
>
> [1] A non-bug report involving lists and a separate inductive type:
>     http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=1751
Thanks for the help, your answers really helped me out!

I just read the bug report you mentioned, but I'm still wondering why it
isn't allowed. Is it possible to create a 'badly defined' function this
way? If so I would be interested in an example (which Yves believed
exists, but wasn't able to show in that thread).

Cheers,

Robbert

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/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

[Bruno Barras]

Robbert Krebbers a écrit :

> Hi,
>
> Brian E. Aydemir wrote:
>> I've encountered this problem before [1], and as far as I know, Adam's
>> suggestion is the way to go.  For the sake of concreteness, I've
>> included below code that implements the basic idea.
>>
>> Cheers,
>> Brian
>>
>> [1] A non-bug report involving lists and a separate inductive type:
>>     http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=1751
> Thanks for the help, your answers really helped me out!
>
> I just read the bug report you mentioned, but I'm still wondering why it
> isn't allowed. Is it possible to create a 'badly defined' function this
> way? If so I would be interested in an example (which Yves believed
> exists, but wasn't able to show in that thread).

It is related to impredicativity: you cannot consider that f x is always
a subterm of f (more precisely, the guard condition assumes that if f is
a subterm of an inductive object a, then (f x) is a strict subterm of a).
If you consider a list of impredicative functions, assuming that outputs
of such functions are strict subterms of the list leads to non
normalizing terms:

Require Import List.

(* if f were considered a subterm of x, then this would be accepted
    (with the -impredicative-set option) *)
Fixpoint loop (x:list (forall A:Set, A->A)) : True :=
   match x with
   | nil => I
   | cons f _ => loop (f _ x)
   end.

Eval compute (loop (cons (fun _ x => x))).

Removing the dead code, and putting the inductive in Prop, which is
always impredicative, we can show a paradox:

Inductive I : Prop :=
| C: (forall P:Prop, P->P) -> I.

Definition i0 := C (fun _ x => x).

Fixpoint ni i : False :=
   match i with
   | C f => ni (f _ i)
   end.

Check (ni i0).

(example due to Th. Coquand in "Pattern Matching with Dependent Types")

Hope this helps,

Bruno Barras.

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/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

[hugo.herbelin]

Hi,

I've been told that Stéphane Lescuyer has written a plugin that allows
you to write the first form as a syntactic sugar for both the second
form of avar_rec2 and a (re)definition trm_rec2 from avar_rec2.

Alternatively, I'm pretty sure there are extensions of the
well-foundness condition that would support the first form w/o
endangering consistency (e.g. by considering that the recursive
subterms of a term in the instance of a parametric inductive type are
the ones one would have obtained if the instantiated type had been
defined directly w/o using a parameter) but I don't see anyone working
in this direction these days.

Hugo Herbelin

> Fixpoint avar_rec2 (a : avar) : P a :=
>   match a as x return P x with
>   | avr v t => H4 v t (trm_rec2 t)
>   end
> with trm_rec2 (t : trm avar) : Q t :=
>   match t as t0 return Q t0 with
>   | srt s => H s
>   | bvr n => H0 n
>   | fvr a => H1 a (avar_rec2 a)
>   | bnd b t0 t1 => H2 b t0 t1 (trm_rec2 t0) (trm_rec2 t1)
>   | app t0 t1 => H3 t0 t1 (trm_rec2 t0) (trm_rec2 t1)
>   end.
>
> Unfortunately this does not work, the system gives the following error:
>
>   Error:
>   Recursive definition of trm_rec2 is ill-formed
>   ...
>   Recursive call to avar_rec2 has principal argument equal to "a"
>   instead of a subterm of t

(...)

> If I change it to the following definition, where the second fixpoint is inline, it works. But then trm_rec2 is not accessible from the outside.
>
> Fixpoint avar_rec2 (a : avar) : P a :=
>   match a as x return P x with
>   | avr v t => H4 v t ((
>     fix trm_rec2 (t : atrm) : Q t :=
>       match t as t0 return Q t0 with
>       | srt s => H s
>       | bvr n => H0 n
>       | fvr a => H1 a (avar_rec2 a)
>       | bnd b t0 t1 => H2 b t0 t1 (trm_rec2 t0) (trm_rec2 t1)
>       | app t0 t1 => H3 t0 t1 (trm_rec2 t0) (trm_rec2 t1)
>       end
>     ) t)
>   end.

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/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

[roconnor]

On Wed, 21 Oct 2009, Robbert Krebbers wrote:

> Unfortunately this does not work, the system gives the following error:
>
> Error:
> Recursive definition of trm_rec2 is ill-formed
> ...
> Recursive call to avar_rec2 has principal argument equal to "a"
> instead of a subterm of t

I have a simlar problem on a more complex data structure.  Below I present
what I hope is a simple (but silly) example that captures the problem I am
having.

Require Import List.

Inductive tree (A:Type) :=
  node : A -> list (tree A) -> tree A.

Section Foo.

Variables (A:Type) (P : tree A -> Prop) (Q: list (tree A) -> list (tree A)
->  Prop).

Hypotheses
  (H:forall (a:A) (l m:list (tree A)), Q l m -> P (node A a l))
  (H0: forall l, Q nil l)
  (H0': forall l, Q l nil)
  (H1: forall t, P t -> forall s, P s -> forall l m, Q l m -> Q (cons t l)
(cons s m)).

Section Z.

Hypothesis (tree_ind0 : forall t, P t).

Fixpoint Z (l : list (tree A)) (m:list (tree A)) : Q l m :=
match l as l return Q l m with
| nil => H0 m
| cons t l0 =>
   match m as m return Q (cons t l0) m with
   | nil => H0' (cons t l0)
   | cons s m0 => H1 t (tree_ind0 t) s (tree_ind0 s) l0 m0 (Z l0 m0)
   end
end.

End Z.

Fixpoint tree_ind0 (t:tree A) : P t :=
  match t as x return P x with
   (* Here I pass the same list twice to Z, but in my real
      problem my "tree" type has two separate lists that
      are processed in parallel *)
  | node a l => H a l l (Z tree_ind0 l l)
  end.

(* This Fixpoint definition fails with the message:
    Recursive call to tree_ind0 has principal argument equal to "s"
    instead of one of the following variables: l l0 t0 l1.
    *)

End Foo.

Essentially I have two lists as substructures of my structure (lists that
contain further members of my structure (my structure is simply
s-expressions)) that are to be processed in parallel to create the output.

When passing one list, the nested recursion works fine; however to process
two lists in parallel I do recursion on one list, and decompose the other
list as I go.  However Coq doesn't seem to recognise that decompostion of
the second list is a substructure.

Anyone have a solution to this type of problem?

For what it's worth, it seems that Agda can handle this case without
difficulty.  I've attached the Agda code.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''
module tree2 where

data list (A : Set) : Set where
 nil : list A
 cons : A -> list A -> list A

data tree (A : Set) : Set where
 node : A -> list (tree A) -> tree A

module Foo (A : Set)
           (P : tree A -> Set)
           (Q : list (tree A) -> list (tree A) -> Set)
           (H : (a : A) -> (l m : list (tree A)) -> Q l m -> P (node a l))
           (H0 : (l : list (tree A)) -> Q nil l)
           (H0' : (l : list (tree A)) -> Q l nil)
           (H1 : (t : tree A) -> P t -> (s : tree A) -> P s ->
                 (l m : list (tree A)) -> Q l m -> Q (cons t l) (cons s m))
           where
 mutual
  treeInd : (t : tree A) -> P t
  treeInd (node y y') = H y y' y' (Z y' y')
 
  Z : (l m : list (tree A)) -> Q l m
  Z nil m = H0 m
  Z (cons y y') nil = H0' ((cons y y'))
  Z (cons y y') (cons y0 y1) = H1 y (treeInd y) y0 (treeInd y0) y' y1 (Z y' y1)

[Adam Chlipala-3]

roconnor@... wrote:

> Fixpoint Z (l : list (tree A)) (m:list (tree A)) : Q l m :=
> match l as l return Q l m with
> | nil => H0 m
> | cons t l0 =>
>   match m as m return Q (cons t l0) m with
>   | nil => H0' (cons t l0)
>   | cons s m0 => H1 t (tree_ind0 t) s (tree_ind0 s) l0 m0 (Z l0 m0)
>   end
> end.
>
> End Z.
>
> Fixpoint tree_ind0 (t:tree A) : P t :=
>  match t as x return P x with
>   (* Here I pass the same list twice to Z, but in my real
>      problem my "tree" type has two separate lists that
>      are processed in parallel *)
>  | node a l => H a l l (Z tree_ind0 l l)
>  end.
>
> (* This Fixpoint definition fails with the message:
>    Recursive call to tree_ind0 has principal argument equal to "s"
>    instead of one of the following variables: l l0 t0 l1.
>    *)

It's not surprising that this fails.  Even though you don't need to
write a termination annotation in the definition of [Z], Coq infers one
for you.  It has to pick one or the other of the two arguments.  
Whichever one it picks, the matching call to [tree_ind0] isn't
structurally recursive.  I think this comes down to the fundamental
limitation that [Fixpoint] needs a termination argument based on just a
single input.  You could perhaps get around this by changing [Z] to take
a pair as input, possibly also switching to [Function] instead of
[Fixpoint].

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/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

[Yves Bertot]

Adam Chlipala wrote:

>
> It's not surprising that this fails.  Even though you don't need to
> write a termination annotation in the definition of [Z], Coq infers
> one for you.  It has to pick one or the other of the two arguments.  
> Whichever one it picks, the matching call to [tree_ind0] isn't
> structurally recursive.  I think this comes down to the fundamental
> limitation that [Fixpoint] needs a termination argument based on just
> a single input.  You could perhaps get around this by changing [Z] to
> take a pair as input, possibly also switching to [Function] instead of
> [Fixpoint].
>

Having only one principal argument for guarded recursion is not the
problem, I believe.  In my opinion, the problem is that when analyzing
an internal fix construct, only the principal argument is used to pass
legitimate guarded variables to the body of the fix construct.   This
can be seen in Coq sources, file kernel/inductive.ml
It is beyond my competence to change this file and be sure that it does
not break consistency.

concerning Russell's initial problem, it is possible to workaround it,
by collecting the values of recursive calls on the second list in a
first pass, putting them in a list, and retrieving them during the
second recursive traversal.
This may be unsatisfactory for efficiency reasons, but I believe it
works. Here is my proposal.

Require Import List.

Inductive tree (A:Type) :=
 node : A -> list (tree A) -> tree A.

Section Foo.

Variables (A:Type) (P : tree A -> Prop) (Q: list (tree A) -> list (tree
A) ->  Prop).

Hypotheses
 (H:forall (a:A) (l m:list (tree A)), Q l m -> P (node A a l))
 (H0: forall l, Q nil l)
 (H0': forall l, Q l nil)
 (H1: forall t, P t -> forall s, P s -> forall l m, Q l m -> Q (cons t
l) (cons s m)).

Section Z.

Hypothesis (tree_ind0 : forall t, P t).

Fixpoint unqualify (l : list {x | P x}) :=
  match l with nil => nil | a::tl => let (v, _) := a in v::unqualify tl end.

(* this function is easier to construct by proof. *)
Fixpoint Z1 (l : list (tree A)) : {l' | unqualify l' = l} :=
  match l return {l' | unqualify l' = l} with
    nil => exist (fun l' => unqualify l' = nil) nil (refl_equal _)
  | x::tl => let (l1, h) := Z1 tl in
    exist (fun l' => unqualify l' = x::tl)
      (exist (fun x => P x) x (tree_ind0 x)::l1)
      match h in _ = b return x::unqualify l1 = x::b with
         refl_equal => refl_equal (x::unqualify l1)
      end
  end.

Fixpoint Z (l : list (tree A)) (m: list {x | P x}) : Q l (unqualify m) :=
  match l return Q l (unqualify m) with
    nil => H0 (unqualify m)
  | t::l0 => match m return Q (t::l0) (unqualify m) with
               nil => H0' (t::l0)
             | (exist s' Ps')::m0 => H1 _ (tree_ind0 t) _ Ps' _ _ (Z l0 m0)
             end
  end.
End Z.

Fixpoint tree_ind0 (t:tree A) : P t :=
 match t as x return P x with
 | node a l =>
      let (l', h) := Z1 tree_ind0 l in H a l (unqualify l') (Z tree_ind0
l l')
 end.
End Foo.

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/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

[roconnor]

On Sun, 25 Oct 2009, Yves Bertot wrote:

> Having only one principal argument for guarded recursion is not the problem,
> I believe.  In my opinion, the problem is that when analyzing an internal fix
> construct, only the principal argument is used to pass legitimate guarded
> variables to the body of the fix construct.   This can be seen in Coq
> sources, file kernel/inductive.ml
> It is beyond my competence to change this file and be sure that it does not
> break consistency.

Thanks for looking at this.  I suspected that was the problem, but it is
hard or impossible to find a description of the guardedness
specification.

> concerning Russell's initial problem, it is possible to workaround it, by
> collecting the values of recursive calls on the second list in a first pass,
> putting them in a list, and retrieving them during the second recursive
> traversal.
> This may be unsatisfactory for efficiency reasons, but I believe it works.
> Here is my proposal.

Thanks for this.  I was beginning to think of something along these lines,
but I hadn't worked out the details yet.

In my actual problem I found a way of eliminating the recursive call to
elements of my second list by using information that can be found in the
first list.  However this solution is really specific to my actual problem
and won't work in general like your solution does.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/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