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?

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.

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`

.

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