在Coq中"判断相等递归类型的相等性"？

Question

有没有办法decide equality在Coq中使用相互递归类型的策略？

例如,如果我有这样的事情:

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.

这让我有了目标:

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

但是在我导出相等性之前我无法解决这个RTree问题,因为它会产生同样的问题.

Answer 1

decide equality如果你同时证明LTrees和RTrees 的两个引理,你可以使用这种情况:

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.