Termination when encoding mutual recursion with polymorphism · Coq users

It is possible to encode mutually recursive types without directly using mutual recursion by using polymorphism instead, as in the following strange definition of rose trees:

Inductive forest' A := | Fnil | Fcons : A -> forest' A -> forest' A.
Inductive tree := | Node : nat -> forest' tree -> tree.
Definition forest := forest' tree.

But then we can't write any functions about them because they fail Coq's termination checker (in this example, the call to tree_sum is ill-formed).

Fail Fixpoint tree_sum (t: tree) : nat :=
  match t with
  | Node n f => n + forest_sum f
  end
with forest_sum (f: forest) : nat :=
  match f with
  | Fnil _ => 0
  | Fcons _ t f => tree_sum t + forest_sum f
  end.
End Poly.

If Coq did allow definitions like these (if, say, it noted that the "t" parameter is in fact a subterm of f), would anything bad happen?
That is, would we be able to write nonterminating functions? Or is this just a limitation of the checker?

Thomas Lamiaux (May 18 2024 at 23:01):

Your definition of forest' is actually just the usual definition of list. So your definition can be rewritten as

Require Import List.

Inductive tree :=
| Node : nat -> list tree -> tree.

Thomas Lamiaux (May 18 2024 at 23:02):

It is a valid notion on inductive types named "nested inductive types" because you nest the recrusive call with another inductive type, here list.

Thomas Lamiaux (May 18 2024 at 23:04):

But then you can't write a function on it using mutual induction because it is not mutual inductive. What you can do instead is use higher order functional programming like the following

Fixpoint tree_sum (t : tree) : nat :=
  match t with
  | Node n ltree => n + fold_right (fun t s => s + tree_sum t) 0 ltree
  end.

Josh Cohen (May 18 2024 at 23:06):

Yes, this was just a small example. I know that this is not a good way of representing rose trees. I am wondering more generally about this method of "tricking" Coq into accepting mutually recursive definitions that are not explicitly defined to be mutually recursive, and if we allowed functions on these types, would there be a problem?

Naively, I would think that such a definition might indeed pass the termination checker, since in forest_sum, both "t" and "f" are subterms of the original "f". So the Coq termination checker is doing something different, and I am wondering why. Is there some possible unsoundness that results if "t" is considered a subterm for termination checking (in general)?

Thomas Lamiaux (May 18 2024 at 23:29):

Fixpoint tree_sum' (t : tree) : nat :=
  match t with
  | Node n ltree =>
      let fix sum_list (l : list tree) : nat :=
      match l with
      | nil => 0
      | cons t' l' => tree_sum' t' + sum_list l'
      end in
      n + sum_list ltree
  end.

and the guard condition is defined such that it can go through nested match and see syntatically that is is indeed smaller, but already that it is not that simple and historically a slightly different version of that was incompatible with PropExt.

Thomas Lamiaux (May 18 2024 at 23:37):

I don't know enough about the mutual cases, but if you accepted generic definition as above maybe you could replicate a similar bug ?

Thomas Lamiaux (May 19 2024 at 00:23):

Dominique Larchey-Wendling (May 19 2024 at 09:15):

FTR, the Kruskal-Trees library was specifically designed to handle nested rose trees with various forms of nesting (list, vectors ...). The data-type you are discussing here is to be found in ltree.v. There you will find suitable recursors (aka induction principle), finite quantification, weight computation and decidability.

You can easily simulate recursors that look like mutual recursors (one for tree with one for list tree) by deriving them from the nested recursor. However, they are usually less convenient to apply because you need to state the property you want to prove for tree and also for list tree.

Josh Cohen (May 19 2024 at 16:03):

Thank you everyone for the replies. My use case is not really about rose trees, and the more I have thought about it, the more I realized that my question is actually related to #Coq users > Mutually recursive Fixpoint strange behavior . Namely, why does Coq not allow you to define mutually recursive functions on types that are not explicitly defined as mutually recursive? Is there a theoretical reason for this (as in, it could lead to nonterminating functions), or is it just a case of Coq being conservative?

Thomas Lamiaux (May 19 2024 at 16:52):

I don't have an answer on whether it is possible or not, but I see a reason why not to do so.
Naively, it seems to me that there are two cases where you would define mutual functions on non mutual recursive definitions:

Thomas Lamiaux (May 19 2024 at 16:54):

Require Import List.
From Equations Require Import Equations.

Inductive tree :=
| Node : nat -> list tree -> tree.

Definition forest := list tree.

Equations tree_sum (t : tree) : nat :=
tree_sum (Node n f) => n + forest_sum f

where forest_sum (l : forest) : nat :=
forest_sum nil => 0;
forest_sum (cons t l) => tree_sum t + forest_sum l.

Stefan Monnier (May 19 2024 at 18:40):

IIRC the recursive call of a fixpoint needs not only to pass an argument that's a subterm but also that this subterm be syntactically recognized as a recursive subterm in the definition of the inductive type.

This extra condition is needed because of impredicativity, an example of a problematic case would be:

Inductive Foo : Prop := foo : (forall A : Prop, A -> A) -> Foo.
Fixpoint oops (x : Foo) : False :=
  match x with foo f => oops (f Foo (foo f))
  end.

Gaëtan Gilbert (May 19 2024 at 19:13):

Josh Cohen (May 19 2024 at 20:55):

Thanks everyone for all the helpful responses, especially the above counterexample and github issues

Stream: Coq users

Topic: Termination when encoding mutual recursion with polymorphism

Josh Cohen (May 18 2024 at 22:27):