The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT inria.fr>]

Hi Tj,

> Le 14 sept. 2020 à 09:28, Tj Barclay <tjbarclay AT ku.edu> a écrit :
> 
> 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.
> 
> Is it possible for the obligation generated by the recursive call to 
> 'flatten' inside the nested fix, 'flatten_list', to also generate 
> hypotheses relating the matched list 'l' and the parameter 'arbs'? In 
> particular,  that 'arbs' will always be a sublist of 'l' or that the 
> matched pair '(_,a')' has the property 'In (_,a') l'

[…]

> 
> (* 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 *)


For this to work I think you will need to explicitly pass around a proof 
witness 
that `size arbs <= size l` (or `size arbs < size a`) in the `flatten_list` 
fixpoint,
otherwise there is no (semantic) link between `arbs` in the fixpoint and the 
argument
`l` to which it is applied.

Best, 
— Matthieu