the definition of structurally smaller · Coq devs & plugin devs

Hi coq devs! In presence of impredicativity, the "structurally smaller" rule for acceptable inductive calls become tricky. See for example agda issue https://github.com/agda/agda/issues/3883 where termination checker sees x as a syntactic subterm of b x and thus decides x Bad bad is "structurally smaller" than b x. Coq rightfully rejects this definition, what's the magic? Is there any pointer to something describing this case of termination checking?

Lapinot (May 10 2023 at 15:45):

We had in mind marking some arguments of constructors as "recursive positions" and restricting the syntactic check to these. But there is trouble with "nested" or layered definitions.

Lapinot (May 10 2023 at 15:49):

Guillaume Melquiond (May 10 2023 at 16:23):

I am not sure what you mean with "deep". The argument of the constructor b does not syntactically have type Bad, so it does not qualify as a subterm. There is no advanced analysis at work here, as far as Coq is concerned.

Lapinot (May 10 2023 at 19:30):

By deep i mean that in the following definition, l does not qualify as a subterm of ListCon l, but xs qualifies as a subterm of the deep pattern ListCon (Right (x , xs)). So the analysis of which places qualify as subterms doesn't take place on patterns but on deep patterns.

Variant sum (A B : Type) : Type :=
| Left (a : A) : sum A B
| Right (b : B) : sum A B
.
Inductive list (A : Type) : Type :=
| ListCon (l : sum A (A * list A) : list A

In the linked slides, it is hinted that there is a definition-time analysis of Inductive constructions which marks which of the variables of these deep patterns are valid subterms. Is this right? Slide 7 hints at an analysis on deep patterns.

Your answer seem to hint more to an other idea we had, which would be a usage-time criterion (at the time of checking validity of a recursive definition). This criterion is harder to put simply and seems less principled, but amount to: in a pattern branch, if i'm trying to call myself recursively on an argument who's head of the spine is a variable x bound as an argument of some (possibly deep) pattern, the rightmost element of the telescope of its type has to be convertible (before application of the telescope to arguments) to the type we are doing induction on.

On top of this being already hard to state, there are question marks in the case of inductive families (most likely we want the type parameters to match also, but the family indices could be different), and it seems like we would miss some valid definitions in case of mutual induction. So I'd be happier with the definition-time analysis of which variables of deep patterns are considered subterms.

Gaëtan Gilbert (May 10 2023 at 20:00):

  Rec{(Mrec[foo.list, 0],
        (Norec,
          Rec{(Nested[foo.sum, 0], (Norec, (Norec)),
                (Norec,
                  Rec{(Nested[Coq.Init.Datatypes.prod, 0],
                        (Norec, (Norec), #2,0))}))}))}

I don't really understand this type but it certainly looks like an analysis of the nested structure

Guillaume Melquiond (May 11 2023 at 07:58):

To be clear, I was not hinting at all at a usage-time criterion. The fact that the argument of the constructor b is syntactically non-recursive is a definition-time criterion.

Lapinot (May 12 2023 at 12:07):

Thanks to you two for the answers! We are in the process of understanding the use of regular trees and their construction. @Gaëtan Gilbert is there a debug flag to get the content of mind_recargs for a given def? (or a file) Thanks again!

Gaëtan Gilbert (May 12 2023 at 12:41):

Lapinot (May 12 2023 at 13:06):

Matthieu Sozeau (May 27 2023 at 05:15):

@Lapinot indeed the regular trees handle nested inductive occurrences and one has to find syntactic occurrences of the (possibly mutual) inductive type in the constructor’s types under an of instantiation of the regular tree for the nested inductive type with the parameters used in the toplevel definition. At least that’s how I understand it. You can see that it’s an inductive definition-time analysis as it is not possible to write useful recursive defs on list rose for example.

Stream: Coq devs & plugin devs

Topic: the definition of structurally smaller

Lapinot (May 10 2023 at 15:41):