the decidable equality definitions for mutually defined inductive types

Question

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}.

Answer 1

You will have two separate issues here:

1. 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.

2. 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.

Answer 2

Your types have nested inductives, which are recursive occurrences of inductive types as arguments to other inductive types (in your case, pairs and lists).

As in other cases, you need induction to show what you want. Unfortunately, unlike simpler types, Coq doesn't come with a baked-in mechanism for automatically generating induction principles for such types, so you have to roll out your own. There are some interesting links about the general problem here. Here's how one can solve your case, combining nested and mutual recursion. Note the Forall' auxiliary inductive for stating the inductive hypothesis

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.