相互定义的归纳类型的可判定等式定义(the decidable equality definitions for mutually defined inductive types)

相互定义的归纳类型的可判定等式定义(the decidable equality definitions for mutually defined inductive types)

现在我有一个相互定义的归纳类型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}.

Now I have a mutually defined inductive Type a and 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.

My problem is how to proof the decidable equality definition for each of them?

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

最满意答案

这里有两个不同的问题：

你有互感类型，所以你需要声明一个相互的固定点，例如

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

通过这种方式，Coq可以生成一个相互固定点，您可以使用两种感应假设（尽管要注意保护条件）。 还有其他方法可以定义此修复点，但这是最简单的方法。

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

对于前一种方法，我建议您阅读此页面 （搜索嵌套的归纳类型）。 后一种解决方案可能如下所示：

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和list a （ list_a之间建立一个双向转换， list_a在不需要归纳时使用该库。

希望它有所帮助，V。

You will have two separate issues here:

You have mutual inductive type, so you need to declare a mutual fixpoint, for example

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

This way Coq generates a mutual fixpoint where you can use both induction hypothesis (beware of the guard condition though). There are other ways to define this fixpoint but this is the easiest one.

Your type is not "structurally" recursive in Coq's sense: a relies on the List.list type, so Coq won't be able to find alone the structural relation it needs to apply induction. If you only need lemmas about lists and no induction at all, then you don't have a problem. Otherwise you might have to define you own recursion scheme, or to redefine list within your mutual block, so that Coq understands that element of the lists are subterms of your type.

For the former approach, I advise you to read this page (search for nested inductive types). The latter solution may look like:

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 .

With this one, you won't be able to directly use the List.list library, but you can still build a two way translation between list_a and list a (resp. t) to use the library when no induction is necessary.

Hope it helps, V.