## Stream: Coq users

### Topic: Termination Checker for Nested Lists

#### Josh Cohen (Apr 19 2024 at 19:57):

Hello, I am confused about the behavior of Coq's termination checker on nested lists. Namely, in the following example, termination checking fails:

``````Fixpoint map2' {A B C: Type} (f : A -> B -> C) (l1 : list A) (l2: list B) : list C :=
match l1, l2 with
| x1 :: t1, x2 :: t2 => f x1 x2 :: map2' f t1 t2
| _, _ => nil
end.

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

Fail Fixpoint tree_eqb1 (t1 t2: tree) {struct t1} : bool :=
match t1, t2 with
| Leaf n1, Leaf n2 => Nat.eqb n1 n2
| Node l1, Node l2 => Nat.eqb (length l1) (length l2) &&
forallb id (map2' tree_eqb1 l1 l2)
| _, _ => false
end.
``````

It fails with message "Recursive call to tree_eqb1 has not enough arguments".

But if I write `map2` in a more unusual (but equivalent) way, termination checking succeeds:

``````Definition map2 {A B C: Type} :=
fun (f: A -> B -> C) =>
fix map2 (l1: list A) : list B -> list C :=
match l1 with
| nil => fun l2 => nil
| x1 :: t1 =>
fun l2 =>
match l2 with
| nil => nil
| x2 :: t2 => f x1 x2 :: map2 t1 t2
end
end.

Fixpoint tree_eqb2 (t1 t2: tree) {struct t1} : bool :=
match t1, t2 with
| Leaf n1, Leaf n2 => Nat.eqb n1 n2
| Node l1, Node l2 => Nat.eqb (length l1) (length l2) &&
forallb id (map2 tree_eqb2 l1 l2)
| _, _ => false
end.
``````

Does anyone know why this is the case?

#### Guillaume Melquiond (Apr 20 2024 at 03:43):

You don't need to make `map2` so ugly. The only thing that matters here is that its argument `f` be outside the fixed point (i.e., be visibly constant across the iterations of `map2`). Other than that, you can write `map2` the usual way. (In particular, if you were using `Section` to lift `f`, it would be written exactly the usual way.) As to why the termination checker does not support this case, I am not quite sure.

#### Dominique Larchey-Wendling (Apr 20 2024 at 06:21):

There is indeed a very subtle aspect of the guard checker. It already manifests itself already on the simpler case of `map` on rose trees below

``````Require Import List.

Fixpoint map_int {X Y} (f : X -> Y) l :=
match l with
| nil  => nil
| x::l => f x :: map_int f l
end.

Definition map_ext {X Y} (f : X -> Y) :=
fix loop l :=
match l with
| nil  => nil
| x::l => f x :: loop l
end.

Inductive tree X :=
| node : X -> list (tree X) -> tree X.

Arguments node {_}.

Fixpoint map_ext_tree {X Y} (f : X -> Y) t :=
match t with
| node x l => node (f x) (map_ext (map_ext_tree f) l)
end.

Fail Fixpoint map_int_tree {X Y} (f : X -> Y) t { struct t } :=
match t with
| node x l => node (f x) (map_int (map_int_tree f) l)
end.
``````

The terms `map_int` and `map_ext` look nearly interchangeable, but they are not from the guard-checker point of view. Indeed:

• in `map_ext_tree`, the sub-term `map_ext (map_ext_tree f)` can be reduced to `fix loop l := match l with nil => nil | x::l => map_ext_tree f x :: loop l end` because `map_ext` is a `Definition`. And this type-checks as a nested-fixpoint;
• in `map_int_tree`, the sub-term `map_int (map_ext_tree f) l` cannot be reduced further because `map_int` is a `Fixpoint` and its `struct` argument, hence `l` here, must first be reduced to a term with a head constructor to further reduce the fixpoint. Not the case in the code of `map_int_tree`.

#### Pierre-Marie Pédrot (Apr 20 2024 at 06:48):

FTR I think that this discrepancy would be fixed by https://github.com/coq/coq/pull/17986 whose purpose is precisely to check guard as if the parameters were extruded.

Last updated: Jun 13 2024 at 19:02 UTC