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

有没有办法在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的相等性之前，我无法解决这个问题。

最佳答案

如果您同时证明了decide equality和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.

关于functional-programming - Coq中相互递归类型的`decide equality`？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/48268929/

RTREE

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