I am stumbling about behavior of Coq’s termination checker that I cannot explain to myself. Consider:
Require Import Coq.Lists.List.
Record C a := { P : a -> bool }.
Arguments P {_}.
Definition list_P {a} (a_C : C a) : list a -> bool := existsb (P a_C).
Definition list_C {a} (a_C : C a) : C (list a) := {| P := list_P a_C |}.
(* Note that *)
Eval cbn in fun a C => (P (list_C C)).
(* evaluates to: fun a C => list_P C *)
Inductive tree a := Node : a -> list (tree a) -> tree a.
(* Works, using a local record *)
Fixpoint tree_P1 {a} (a_C : C a) (t : tree a) : bool :=
let tree_C := Build_C _ (tree_P1 a_C) in
let list_C' := Build_C _ (list_P tree_C) in
match t with Node _ x ts => orb (P a_C x) (P list_C' ts) end.
(* Works too, using list_P directly *)
Fixpoint tree_P2 {a} (a_C : C a) (t : tree a) : bool :=
let tree_C := Build_C _ (tree_P2 a_C) in
match t with Node _ x ts => orb (P a_C x) (list_P tree_C ts) end.
(* Does not work, using a globally defined record. Why not? *)
Fixpoint tree_P3 {a} (a_C : C a) (t : tree a) : bool :=
let tree_C := Build_C _ (tree_P3 a_C) in
match t with Node _ x ts => orb (P a_C x) (P (list_C tree_C) ts) end.
The first and second example show that, when trying to understand whether a fixpoint is terminating, Coq is able to resolve record accessors, basically evaluating what we wrote in tree_P1 to what we wrote in tree_P2.
But this seems to only work if the record is built locally (let tree_C :=…), not if it is defined using Definition.
But Fixpoint can look through other definitions just fine, e.g. through list_P. So what is special about records, and can I make Coq accept tree_P3?
After some reading of the termination checker in Coq, I think I found the solution:
The termination checker will always unfold local definitions, and beta-reduce. That is why tree_P1 works.
The termination checker will also, if necessary, unfold definitions that are called (like list_C', P, existsb), that is why tree_P2 works.
Ther termination checker will, however, not unfold definitions that apppear in a match … with clause, such as list_C. Here is a minimal example for that:
(* works *)
Fixpoint foo1 (n : nat) : nat :=
let t := Some True in
match Some True with | Some True => 0
| None => foo1 n end.
(* works *)
Fixpoint foo2 (n : nat) : nat :=
let t := Some True in
match t with | Some True => 0
| None => foo2 n end.
(* does not work *)
Definition t := Some True.
Fixpoint foo3 (n : nat) : nat :=
match t with | Some True => 0
| None => foo3 n end.
A work-around for the original code is to make sure that all definitions are called (and not pattern-matched against), to ensure that the termination checker will unfold them. We can do that by switching to a continuation passing style:
Require Import Coq.Lists.List.
Record C_dict a := { P' : a -> bool }.
Definition C a : Type := forall r, (C_dict a -> r) -> r.
Definition P {a} (a_C : C a) : a -> bool :=
a_C _ (P' _).
Definition list_P {a} (a_C : C a) : list a -> bool := existsb (P a_C).
Definition list_C {a} (a_C : C a) : C (list a) :=
fun _ k => k {| P' := list_P a_C |}.
Inductive tree a := Node : a -> list (tree a) -> tree a.
(* Works now! *)
Fixpoint tree_P1 {a} (a_C : C a) (t : tree a) : bool :=
let tree_C := fun _ k => k (Build_C_dict _ (tree_P1 a_C)) in
match t with Node _ x ts => orb (P a_C x) (P (list_C tree_C) ts) end.
This even works with type classes, as type class resolution is indepenent of these issues:
Require Import Coq.Lists.List.
Record C_dict a := { P' : a -> bool }.
Definition C a : Type := forall r, (C_dict a -> r) -> r.
Existing Class C.
Definition P {a} {a_C : C a} : a -> bool := a_C _ (P' _).
Definition list_P {a} `{C a} : list a -> bool := existsb P.
Instance list_C {a} (a_C : C a) : C (list a) :=
fun _ k => k {| P' := list_P |}.
Inductive tree a := Node : a -> list (tree a) -> tree a.
(* Works now! *)
Fixpoint tree_P1 {a} (a_C : C a) (t : tree a) : bool :=
let tree_C : C (tree a) := fun _ k => k (Build_C_dict _ (tree_P1 a_C)) in
match t with Node _ x ts => orb (P x) (P ts) end.