The Coq mailing list

[S3 <scubed2 AT gmail.com>]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

How do you have induction over a data structure
that contains a list?

Here is what I want to induct over:

Inductive BlueTree : Set :=
| BlueLeaf
| RedLeaf
| Branch (a : list BlueTree)
.

I need the assumption that the list elements have
the property when I get to them since they are structurally smaller.

If I put a list as part of the data structure, I can do this:

Inductive BlueTree : Set :=
| BlueLeaf
| RedLeaf
| Branch (a : List)
with List : Set :=
| Nil
| Cons (a : BlueTree) (b : List)
.

Scheme BlueTree_List_ind := Induction for BlueTree Sort Prop
with List_BlueTree_ind := Induction for List Sort Prop.

or, similarly,

Theorem BlueTree_List_ind : forall (P : BlueTree -> Prop) (P0 : List -> Prop),
  P BlueLeaf ->
  P RedLeaf ->
  (forall a : List, P0 a -> P (Branch a)) ->
  P0 Nil ->
  (forall a : BlueTree, P a -> forall b : List, P0 b -> P0 (Cons a b)) ->
  forall b : BlueTree, P b
.
  intros.
  refine ((
fix F (b : BlueTree) : P b := _
with F0 (l : List) : P0 l := _
for F
) b).
    apply F.
  apply F0.
Qed.


However, I can't seem to translate this back to the original data structure.

Theorem BlueTree_list_ind : forall (P : BlueTree -> Prop) (P0 : list BlueTree
- -> Prop),
  P BlueLeaf ->
  P RedLeaf ->
  (forall a : list BlueTree, P0 a -> P (Branch a)) ->
  P0 nil ->
  (forall a : BlueTree, P a -> forall b : list BlueTree, P0 b -> P0 (a::b)) ->
  forall b : BlueTree, P b
.
  intros.
  refine ((
fix F (b : BlueTree) : P b := _
with F0 (l : list BlueTree) : P0 l := _
for F
) b).
Error: Fixpoints should be on the same mutual inductive declaration.

I'm not sure what that means.  I guess that means that both parts
of the data structure should be defined in the same statement with a
with clause?  How do I use a plain, existing list?
Is that possible?

- -- 
$_="sccc,gB1,a_oo,JosBackuSa,g11,ug1a,oscc,cBBg,JcgaBuucaB_s11_Juc_c";
while(($c,$b,$a)=m/^(.)([^,]*),(.*)$/){$_=$a;s/$c/$b/g;}
print map chr length,split /_/;
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.17 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/

iEYEARECAAYFAk+4nYYACgkQxzVgPqtIcfvfLgCeKnftO9wrJO8Gh/nDSsB8GJht
RWIAnA7PAaTenPlMJ8r1Llej9anB15/p
=/MmH
-----END PGP SIGNATURE-----