The Coq mailing list

[Tj Barclay <tjbarclay AT ku.edu>]

On Mon, Sep 14, 2020 at 11:41 AM Christian Doczkal <christian.doczkal AT inria.fr> wrote:

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:

Christian is right here. I was so focused on the nested fix aspect of my made up example that I neglected to add another twist to the example that actually results in it not being syntactically structurally recursive.

(* Size of arb lists *)

Fixpoint size_arb_list (al : list arb) : nat :=
  match al with
  | [] => 0
  | a::al' => size_arb a + size_arb_list al'
  end.

(* flatten function for list of arb *)

 Fixpoint flatten (al : list arb) {measure (size_arb_list al)}: list nat :=
  match al 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
  | a::al' => flatten [a] ++ flatten al'
  end.

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

I really appreciate your, and all the others, feedback on this problem.

Best,

TJ