The Coq mailing list

[Jim Fehrle <jim.fehrle AT gmail.com>]

>  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.

Hi Gert,

How about submitting an issue mentioning these points?  And mentioning why the Giménez reference should be removed.  Or, if you know the information needed to update the documentation, consider submitting a pull request.  Your observations are very likely to be overlooked otherwise.

Jim

On Mon, Sep 14, 2020 at 11:16 AM Gert Smolka <smolka AT ps.uni-saarland.de> wrote:

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.