The Coq mailing list

[Christian Doczkal <christian.doczkal AT inria.fr>]

It might be worthwhile to point out that the particular example you give is 
indeed structurally recursive. That is, the following, which is basically 
just removing the "Program" and "{measure _}" parts actually works:

-------------------------------------------------

Require Import List.
Import ListNotations.

Set Implicit Arguments.

Inductive arb : Type :=
| A : nat -> arb
| B : nat -> list (nat * arb) -> arb.

Fixpoint flatten (a : arb) : list nat :=
  match a with
  | A n => [n]
  | B n l => n :: (fix flatten_list (arbs : list (nat * arb)) : list nat :=
                   match arbs with
                   | [] => []
                   | (n',a')::arbs' => n' :: (flatten a' ++ flatten_list 
arbs')
                end) l
  end.

-------------------------------------------------

Unfortunately, I don't remember the precise rules that make this definition 
okay. It's something along the lines of "l" being structurally smaller than 
"a" and "flatten_list" applying flatten only to arguments that are 
"structurally no greater than y". However, this seems to not be covered by 
relevant section of the current manual: 
https://coq.inria.fr/refman/language/core/inductive.html#id10

Maybe someone can chime in and provide the precise rules making this legal.

By the way, one can also make this slightly more readable by factoring out 
flatten_list. 

-------------------------------------------------

Definition flatten_list (f : arb -> list nat) : list (nat * arb) -> list nat 
:=
  (fix flatten_list (arbs : list (nat * arb)) : list nat :=
     match arbs with
     | [] => []
     | (n',a')::arbs' => n' :: (f a' ++ flatten_list arbs')
     end).

Fixpoint flatten (a : arb) : list nat :=
  match a with
  | A n => [n]
  | B n l => n :: flatten_list flatten l
  end.

-------------------------------------------------

This pattern is used extensively throughout the mathematical components 
library. Note that replacing the definition with the more standard 

Fixpoint flatten_list (f : arb -> list nat) (arbs : list (nat * arb)) := ... 

does *not* work, because this would lead to "flatten" not being applied to 
any arguments in the clause for "B", even after the reduction that is 
happening before checking the guard condition.

Best,
Christian

On 9/14/20 9:28 AM, Tj Barclay wrote:
> Enclosed is an arbritrary example (Coq 8.11.2) of an attempt to show 
> termination of a recursive function on the size of a nested-recursive 
> datatype.

> (* Function in question *)
> Program Fixpoint flatten (a : arb) {measure (size_arb a)}: list nat :=
>   match a with
>   | A n => [n]
>   | B n l => n :: (fix flatten_list (arbs : list (nat * arb)) : list nat :=
>                    match arbs with
>                    | [] => []
>                    | (n',a')::arbs' => n' :: (flatten a' ++ flatten_list 
> arbs')
>                 end) l
>   end.
> Obligation 1.
> (* Example End *)