`decide equality` for Mutually Recursive Types in Coq?

Question

Is there any way to use the decide equality tactic with mutually recursive types in Coq?

For example, if I've got something like this:

Inductive LTree : Set :=
  | LNil
  | LNode (x: LTree) (y: RTree)
  with RTree : Set :=
    | RNil
    | RNode (x: Tree) (y: RTree).

Lemma eq_LTree : forall (x y : LTree), {x = y} + {x <> y}.
Proof.
    decide equality; auto.

This leaves me with the goal:

y0: RTree
y1: RTree
{y0 = y1} + {y0 <> y1}

But I can't solve that until I've derived equality for RTree, which will have the same problem.

Salverform

Answer 1

You can use decide equality in this case if you prove the two lemmas for LTrees and RTrees simultaneously:

Lemma eq_LTree : forall (x y : LTree), {x = y} + {x <> y}
with  eq_RTree : forall (x y : RTree), {x = y} + {x <> y}.
Proof.
  decide equality.
  decide equality.
Qed.

Chura

This is strange, Guarded complains after the first decide equality, but then Qed is not rejected. – Rundle

Never mind, I found a thread on coq-club discussing this particular problem. – Rundle