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

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 将无法单独找到应用归纳所需的结构关系。如果您只需要关于lists 的引理而根本不需要归纳，那么您就没有问题。否则，您可能必须定义自己的递归方案，或在相互块中重新定义列表，以便 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 和list a（分别为t）之间构建双向转换来使用该库当不需要诱导时。

希望对你有帮助， 五、

Answer 2

您的类型具有嵌套归纳，它们是归纳类型的递归出现，作为其他归纳类型（在您的情况下是对和列表）的参数。

与其他情况一样，您需要通过归纳来展示您想要的内容。不幸的是，与更简单的类型不同，Coq 没有为此类类型自动生成归纳原则的内置机制，因此您必须推出自己的机制。有一些关于一般问题here 的有趣链接。以下是如何解决您的问题，结合嵌套和相互递归。请注意Forall' 用于陈述归纳假设的辅助归纳

Require Import String.
Require Import List.
Require Import ListSet.
Import ListNotations.

Set Implicit Arguments.

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.

Inductive Forall' A (T : A -> Type) : list A -> Type :=
| Forall_nil' : Forall' T []
| Forall_cons' : forall x l, T x -> Forall' T l -> Forall' T (x :: l).

Definition build_forall A (T : A -> Type) (f : forall x, T x) :=
  fix F l : Forall' T l :=
  match l with
  | [] => Forall_nil' _
  | x :: l' => Forall_cons' x (f x) (F l')
  end.

Lemma forall_eq_dec A (l : list A) (H : Forall' (fun x => forall y, {x = y} + {x <> y}) l) :
  forall l', {l = l'} + {l <> l'}.
Proof.
  induction H as [| x l Hx Hl IH]; intros [|y l']; try (right; congruence); eauto.
  specialize (IH l').
  destruct IH; subst; try (right; congruence).
  destruct (Hx y); subst; try (right; congruence).
  eauto.
Qed.

Fixpoint a_ind' (Ta : a -> Type) (Tt : t -> Type)
                (H1 : forall s p, Ta (basic s p))
                (H2 : forall s la, Forall' Ta la ->
                      forall n lt, Forall' Tt lt ->
                      forall p, Ta (complex s la n lt p))
                (H3 : forall s la, Forall' Ta la -> Ta (complex2 s la))
                (H4 : forall s x, Ta x ->
                      forall ss1 ss2, Tt (t_intro (s, x, ss1, ss2))) x {struct x} : Ta x :=
  match x with
  | basic s p => H1 s p
  | complex s la n lt p => H2 s la (build_forall _ (a_ind' H1 H2 H3 H4) la)
                              n lt (build_forall _ (t_ind' H1 H2 H3 H4) lt)
                              p
  | complex2 s la => H3 s la (build_forall _ (a_ind' H1 H2 H3 H4) la)
  end
with t_ind' (Ta : a -> Type) (Tt : t -> Type)
            (H1 : forall s p, Ta (basic s p))
            (H2 : forall s la, Forall' Ta la ->
                  forall n lt, Forall' Tt lt ->
                  forall p, Ta (complex s la n lt p))
            (H3 : forall s la, Forall' Ta la -> Ta (complex2 s la))
            (H4 : forall s x, Ta x ->
                  forall ss1 ss2, Tt (t_intro (s, x, ss1, ss2))) x {struct x} : Tt x :=
  match x with
  | t_intro (s, x, ss1, ss2) => H4 s x (a_ind' H1 H2 H3 H4 x) ss1 ss2
  end.

Definition a_and_t_ind (Ta : a -> Type) (Tt : t -> Type)
                (H1 : forall s p, Ta (basic s p))
                (H2 : forall s la, Forall' Ta la ->
                      forall n lt, Forall' Tt lt ->
                      forall p, Ta (complex s la n lt p))
                (H3 : forall s la, Forall' Ta la -> Ta (complex2 s la))
                (H4 : forall s x, Ta x ->
                      forall ss1 ss2, Tt (t_intro (s, x, ss1, ss2))) :
  (forall x, Ta x) * (forall x, Tt x) :=
  (a_ind' H1 H2 H3 H4, t_ind' H1 H2 H3 H4).

Lemma pair_dec A B (HA : forall x y : A, {x = y} + {x <> y})
                   (HB : forall x y : B, {x = y} + {x <> y}) :
  forall x y : A * B, {x = y} + {x <> y}.
Proof. decide equality. Qed.

Definition a_and_t_dec : (forall x y : a, {x = y} + {x <> y}) *
                         (forall x y : t, {x = y} + {x <> y}).
Proof.
  apply a_and_t_ind.
  - intros s p [s' p'| |]; try (right; congruence).
    destruct (string_dec s s'); try (right; congruence).
    subst.
    destruct (pair_dec string_dec string_dec p p'); try (right; congruence).
    subst. eauto.
  - intros s la Hla n lt Hlt p y.
    destruct y as [|s' la' n' lt' p'|]; try (right; congruence).
    destruct (string_dec s s'); subst; try (right; congruence).
    destruct (forall_eq_dec Hla la'); subst; try (right; congruence).
    destruct (NPeano.Nat.eq_dec n n'); subst; try (right; congruence).
    destruct (forall_eq_dec Hlt lt'); subst; try (right; congruence).
    destruct (pair_dec string_dec string_dec p p'); subst; try (right; congruence).
    eauto.
  - intros s la Hla [| |s' la']; try (right; congruence).
    destruct (string_dec s s'); subst; try (right; congruence).
    destruct (forall_eq_dec Hla la'); subst; try (right; congruence).
    eauto.
  - intros s x Hx ss1 ss2 [[[[s' x'] ss1'] ss2']].
    destruct (string_dec s s'); subst; try (right; congruence).
    destruct (Hx x'); subst; try (right; congruence).
    destruct (list_eq_dec string_dec ss1 ss1'); subst; try (right; congruence).
    destruct (list_eq_dec string_dec ss2 ss2'); subst; try (right; congruence).
    eauto.
Qed.

Definition a_dec := fst a_and_t_dec.
Definition t_dec := snd a_and_t_dec.