I am wondering what the best way to prove properties of nested inductive types is.

Let’s consider first a general tree data structure such as:

```
Inductive Tree :=
| node : nat -> Tree_list -> Tree
with Tree_list :=
| tree_nil : Tree_list
| tree_cons : Tree -> Tree_list -> Tree_list.
```

Deciding equality for this is easy with `decide equality`

:

```
Proposition tree_eq_dec (t1 t2 : Tree) : {t1 = t2} + {t1 <> t2}
with tree_list_eq_dec (l1 l2 : Tree_list) : {l1 = l2} + {l1 <> l2}.
Proof.
decide equality.
decide equality.
decide equality.
Defined.
```

Now I would like to use `list`

from the standard library instead. I define:

```
From Coq Require Import List.
Inductive Tree :=
| node : nat -> list Tree -> Tree.
```

But now Coq rejects the following:

```
Proposition tree_eq_dec (t1 t2 : Tree) : {t1 = t2} + {t1 <> t2}
with tree_list_eq_dec (l1 l2 : list Tree) : {l1 = l2} + {l1 <> l2}.
```

saying

```
Error: Cannot find common (mutual) inductive premises or coinductive conclusions in the statements.
```

I have then attempted to define a strong enough induction principle that will allow me to prove this,

but it ends up being quite involved to prove this (seemingly) simple property. Indeed, with a fixpoint

it is quite easy to do:

```
Fixpoint Tree_eq_dec (t1 t2 : Tree) : {t1 = t2} + {t1 <> t2}.
Proof.
set (Tree_list_eq_dec := list_eq_dec Tree_eq_dec).
decide equality.
decide equality.
Defined.
```

But this time I was lucky that there was `list_eq_dec`

in the standard libraries. For other properties I may not be as lucky, and stating all properties similarly to `list_eq_dec`

is tedious.

Is there a way to have Coq accept the definition with mutual propositions?

You may want to take a look at the Nfix plugin, or at this file which shows a pattern for manual definition of recursors and induction principles over nested inductives. Chapter 14.3 in the Coq’Art book also describes this topic.

2 Likes

Thank you! The Nfix plugin looks like exactly what I wanted. The induction principle from that file also looks very general – at least I was able to show decidable equality in a quite natural way using it.

You may also use Equations to prove the elimination principles and call it with induction as usual.

Does `Scheme Equality for Tree`

do what you want? You can also `Set Decidable Equality Schemes`

and `Set Boolean Equality Schemes`

before defining the inductive, I believe.

Edit: oops, I read too quickly. I now see that you want properties other than decidable equality for this inductive, rather than decidable equality for other inductives.

As suggested above, one straightforward way to get induction principles is to use the Equations plugin. Here is one example that could be useful:

```
Require Import List. Import ListNotations.
From Equations Require Import Equations.
Inductive tree {A : Type} : Type :=
| atom : A -> tree
| node : list tree -> tree.
Section Tree_ind2.
Variable A : Type.
Variable P : @tree A -> Prop.
Variable P_list : list (@tree A) -> Prop.
Hypothesis P_nil : P_list [].
Hypothesis P_cons : forall t l, P t -> P_list l -> P_list (t :: l).
Hypothesis P_atom : forall a, P (atom a).
Hypothesis P_node : forall l, P_list l -> P (node l).
Equations tree_ind2 (t : @tree A) : P t :=
{ tree_ind2 (atom a) := P_atom a;
tree_ind2 (node l) := P_node l (tree_ind2_list l) }
where tree_ind2_list (l : list (@tree A)) : P_list l :=
{ tree_ind2_list [] := P_nil;
tree_ind2_list (tn :: l') := P_cons tn l' (tree_ind2 tn) (tree_ind2_list l') }.
End Tree_ind2.
```

1 Like