functional-programming - Coq 中的相互递归类型为 `decide equality`？

Question

有没有办法在 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

在这种情况下，如果您同时证明 LTree 和 RTree 的两个引理，则可以使用决定相等性:

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.