Cannot guess decreasing argument of fix for nested match in Coq

Viewed 2888

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 ?

2 Answers
Related