My Inductive function over a pair of lists gives "Cannot guess decreasing argument of fix."

Question

This is the smallest example that causes the problem. It should decrease, but I don't know how to reassure Coq that it will. I'm going to have to compare lots of lists of pairs for what I'm doing so this is going to come up again and again.

The error: "Cannot guess decreasing argument of fix."

Require Import Coq.Lists.List.
Import ListNotations.

Inductive type_t : Type :=
  | Tuple (elements: list type_t)
  | Nil. 

Fixpoint equal (x: type_t) (y: type_t) : bool :=
  match x, y with
  | Tuple xs, Tuple ys => equal_pairs xs ys
  | Nil, Nil => true
  | _, _ => false 
  end

with equal_pairs (xs: list type_t) (ys: list type_t) : bool :=
  match xs, ys with
  | x :: xs', y :: ys' => if equal x y then equal_pairs xs' ys' else false
  | [], [] => true
  | _, _ => false
  end.
```

Answer 1

You need to change your equal definition to the following to let Coq know that your definition is indeed syntactically decreasing.

Fixpoint equal (x: type_t) (y: type_t) : bool :=
  match x, y with
  | Tuple xs, Tuple ys =>
    (* Note this *)
    (fix equal_pairs xs ys :=
      match xs, ys with
      | x :: xs', y :: ys' => if equal x y then equal_pairs xs' ys' else false
      | [], [] => true
      | _, _ => false
      end
    ) xs ys
  | Nil, Nil => true
  | _, _ => false 
  end.

Your original definition completely makes sense but Coq's termination checker is somehow weak; for nested types you need to write nested anonymous recursive functions to bypass this limitation.

Answer 2

It is a limitation of mutual fixpoints. The guard checker requires that the structural arguments are on mutually defined inductive types. The solution is to replace with nested fixpoints as the type_t is nested with that of list.

Answer 3

Let me give a more complete answer. It recollects some code that you can find in the library Kruskal-Trees that I specifically designed to deal with various kinds of rose trees (trees nested with lists or else vectors):

Instantiated on your case, one could for instance write the following code:

Require Import List.
Import ListNotations.

Unset Elimination Schemes.

Inductive type_t : Type :=
  | Tuple (elements: list type_t)
  | Nil.

Set Elimination Schemes.

Section type_t_ind.

  Variables (P : type_t -> Prop)
            (HP_Tuple : forall el, (forall x, In x el -> P x) -> P (Tuple el))
            (HP_Nil : P Nil).

  Fixpoint type_t_ind x : P x.
  Proof.
    destruct x as [ el | ].
    + apply HP_Tuple.
      induction el as [ | x el IHl ].
      * intros _ [].
      * intros y [ <- | ].
        - apply type_t_ind.
        - now apply IHl.
    + apply HP_Nil.
  Qed.

End type_t_ind.

Definition sub_type_t x y :=
  match y with 
  | Tuple el => In x el
  | Nil => False
  end.

Fact wf_sub_type_t : well_founded sub_type_t.
Proof.
  intros x.
  induction x; now constructor.
Qed.

Section type_t_rect.

  Variables (P : type_t -> Type)
            (HP_Tuple : forall el, (forall x, In x el -> P x) -> P (Tuple el))
            (HP_Nil : P Nil).

  Definition type_t_rect x : P x.
  Proof.
    induction x as [ [ el | ] IH ] using (well_founded_induction_type wf_sub_type_t).
    + apply HP_Tuple, IH.
    + apply HP_Nil.
  Qed.

End type_t_rect.

Definition type_t_rec (P : _ -> Set) := type_t_rect P.

Hint Resolve in_eq in_cons : core.

Definition list_eq_dec_dep {X} (l m : list X) :
      (forall x y, In x l -> In y m -> { x = y } + { x <> y })
   -> { l = m } + { l <> m }.
Proof.
  induction l as [ | x l IHl ] in m |- *; intros Hl.
  + destruct m; [ auto | now right ].
  + destruct m as [ | y m ]; [ now right | ].
    destruct (Hl x y) as [ <- | C ]; auto.
    2: right; contradict C; now inversion C.
    destruct (IHl m) as [ <- | C ]; eauto.
    right; contradict C; now inversion C.
Qed. 

Definition equal_full (x y : type_t) : { x = y } + { x <> y }.
Proof.
  induction x as [ el IH | ] in y |- *.
  + destruct y as [ em | ].
    * destruct (list_eq_dec_dep el em) as [ <- | C ]; eauto.
      right; contradict C; now inversion C.
    * now right.
  + destruct y; [ now right | auto ].
Qed.
```