Proving properties for inductives with nested inductives

Using Coq
1

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?

2

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
3

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.

4

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

5

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.

6

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