Coq 中相互递归类型的“决定相等性”？

Question

有什么方法可以在 Coq 中对相互递归类型使用 decide equality 策略吗？

例如，如果我有这样的东西：

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

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

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.