The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

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.