Cannot guess decreasing argument of fix for nested match in Coq

Question

I have the following definition for terms :

Inductive term : Type :=
  | Var : variable -> term
  | Func : function_symbol -> list term -> term.

and a function pos_list taking a list of terms and returning a list of "positions" for each subterms. For instance for [Var "e"; Func "f" [Var "x"; Func "i" [Var "x"]]] I should get [[1]; [2]; [2; 1]; [2; 2]; [2; 2; 1]] where each element represents a position in the tree-hierarchy of subterms.

Definition pos_list (args:list term) : list position :=
  let fix pos_list_aux ts is head :=
    let enumeration := enumerate ts in
      let fix post_enumeration ts is head :=
        match is with
        | [] => []
        | y::ys =>
          let new_head := (head++y) in
          match ts with
          | [] => []
          | (Var _)::xs => [new_head] ++ (post_enumeration xs ys head)
          | (Func _ args')::xs =>
            [new_head] ++
            (pos_list_aux args' [] new_head) ++
            (post_enumeration xs ys head)
          end
        end
      in post_enumeration ts enumeration head
  in pos_list_aux args [] [].

With the above code I get the error

Error: Cannot guess decreasing argument of fix

on the first let fix construction but it seems to me that the call to (pos_list_aux args' [] new_head) (which is causing problems) takes as argument args' which is a subterm of (Func _ args') which is itself a subterm of ts.

What is wrong ?

Answer 1

term is a nested inductive type (because of list term in the Func constructor) and it frequently requires some additional work to explain to Coq that your function is total. This chapter of CPDT explains how to deal with this kind of situation (see "Nested inductive types" section):

The term “nested inductive type” hints at the solution to this particular problem. Just as mutually inductive types require mutually recursive induction principles, nested types require nested recursion.

Here is my attempt at solving your problem. First of all, let's add some imports and definitions so everything compiles:

Require Import Coq.Lists.List.
Import ListNotations.
Require Import Coq.Strings.String.
Require Import Coq.Strings.Ascii.

Definition variable := string.
Definition function_symbol := string.
Definition position := list nat.

Inductive term : Type :=
  | Var : variable -> term
  | Func : function_symbol -> list term -> term.

We begin by implementing a function that does the job for a single term. Notice that we define a nested function pos_list_many_aux which is almost what you wanted in the first place:

Definition pos_list_one (i : nat) (t : term) : list position :=
  let fix pos_list_one_aux (i : nat) (t : term) {struct t} : list position :=
      match t with
      | Var _ => [[i]]
      | Func _ args =>
          [i] :: map (cons i)
                     ((fix pos_list_many_aux i ts :=
                         match ts with
                         | [] => []
                         | t::ts =>
                             pos_list_one_aux i t ++ pos_list_many_aux (S i) ts
                         end) 1 args).     (* hardcoded starting index *)
      end
  in pos_list_one_aux i t.

Now, we will need an auxiliary function mapi (named borrowed from OCaml's stdlib). It's like map, but the mapping function also receives the index of the current list element.

Definition mapi {A B : Type} (f : nat -> A -> B) (xs : list A) : list B :=
  let fix mapi i f xs :=
    match xs with
    | [] => []
    | x::xs => (f i x) :: mapi (S i) f xs
    end
  in mapi 0 f xs.

And now everything is ready to define the pos_list function:

Definition pos_list (args : list term) : list position :=
  concat (mapi (fun i t => pos_list_one (S i) t) args).

Let's run your test:

Section Test.
  Open Scope string_scope.

  Compute pos_list [Var "e"; Func "f" [Var "x"; Func "i" [Var "x"]]].
  (*
   = [[1]; [2]; [2; 1]; [2; 2]; [2; 2; 1]] : list position
   *)
End Test.

Answer 2

If you explicitly tell Coq which argument you are recursing on, you get a slightly more informative error message.

let fix pos_list_aux ts is head {struct ts} :=

Now Coq says

Recursive call to pos_list_aux has principal argument equal to "args'" instead of
"xs".

And if you use {struct is} instead, Coq says

Recursive call to pos_list_aux has principal argument equal to "[]" instead of
a subterm of "is".

The simple syntactic rule that determines if the recursion is sound requires you to do the recursion with a term that comes from destructing the argument with a match is with ... end.

It is not trivially ok to use something taken from the head element, as args', or even in the case of recursion on is to use []. For instance, perhaps you create an infinite loop where you call yourself with [] as the recursion argument. The typechecker needs to prevent that.

The syntactic rule is "very simple" and does not apply trivially in this case, even though the recursion is "obviously" on a structurally smaller component in this case. So you will have to convince the typechecker in some more involved way that args' is ok.

Perhaps someone else can give an elegant way of doing that? My first try would be to see if Program handled this (but it didn't).