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.