The Coq mailing list

[Gert Smolka <smolka AT cs.uni-saarland.de>]

> On 14. Sep 2020, at 18:42, Christian Doczkal <christian.doczkal AT inria.fr> 
> wrote:
> 
> 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.

Smiley!  What you are referring to is the guard condition, which was extended 
over the years but never documented.
Anyway, nested inductive types (e.g., rose trees) are impossible without the 
extended guard condition.

BTW, someone should delete the reference to Giménez in the reference Manual:
"Before accepting a fixpoint definition as being correctly typed, we check 
that the definition is “guarded”. A precise analysis of this notion can be 
found in [Gimenez94].”
At this point there was only a minimal guard condition.

I’m intrigued by Dominique’s idea to define the eliminator for rose trees 
with ACC.  Below is a minimal version.  
It shows that the extended guard condition can be quite nice.

Cheers, Gert


Inductive tree := T (A: list tree).
Implicit Type s t: tree.

Definition dst s t := let (A) := t in In s A.

Fixpoint tree_Acc t: Acc dst t.
Proof.
  destruct t as [A].
  constructor.
  induction A as [| t A IH]; cbn.
  - intros t [].
  - intros s [[]|H].
    + apply tree_Acc.
    + apply IH, H.
Defined.

Eval cbv -[dst] in tree_Acc.



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