coq - 相互定义的归纳类型的可判定相等定义

Question

现在我有一个相互定义的感应类型 a 和 t:

Inductive a : Type :=
| basic : string -> (string * string) -> a
| complex : string -> list a -> nat -> list t -> (string * string) -> a
| complex2 : string -> list a -> a
with t : Type :=
| t_intro : string * a * (set string) * (set string) -> t.

我的问题是如何证明它们每个人的可判定相等定义？

Definition a_dec : forall (x y : a), {x = y} + {x <> y}.

Definition t_dec : forall (x y : t), {x = y} + {x <> y}.

Answer 1

您将在这里遇到两个单独的问题:

1. 您有互感类型，因此您需要声明一个互固定点，例如

   Fixpoint a_dec (x y : a) : { x = y } + { x <> y }
   with b_dec (x y : t) : { x = y } + { x <> y }.
   

   这样 Coq 会生成一个相互固定点，您可以在其中使用归纳假设(注意 不过守卫条件)。还有其他方法可以定义此固定点，但这是最简单的方法。

2. 您的类型不是 Coq 意义上的“结构上”递归:a 依赖于 List.list 类型， 因此 Coq 无法单独找到应用归纳法所需的结构关系。如果您只需要关于列表的引理并且根本不需要归纳，那么您就没有问题。否则，您可能必须定义自己的递归方案，或者在共同 block 中重新定义列表，以便 Coq 理解列表的元素是您类型的子项。

对于前一种方法，我建议您阅读this page (搜索嵌套归纳类型)。后一种解决方案可能如下所示:

    Inductive a : Type :=
    | basic : string -> (string * string) -> a
    | complex : string -> list_a -> nat -> list_t -> (string * string) -> a
    | complex2 : string -> list_a -> a
    with t : Type :=
    | t_intro : string * a * (set string) * (set string) -> t.
    with list_a : Type
    | anil : list_a
    | acons : a -> list_a -> list_a
    with list_t : Type
    | tnil : list_t
    | tcons : t -> list_t -> list_t
    .

使用此库，您将无法直接使用 List.list 库，但您仍然可以在 list_a 和 之间构建双向转换>列出一个(或t)以在不需要归纳时使用该库。

希望对你有帮助 五、