终止检查器何时减少记录访问器

Question

我对 Coq 的终止检查器的行为感到困惑，我无法向自己解释。考虑：

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.

第一个和第二个例子表明，当试图理解一个固定点是否正在终止时，Coq 能够解析记录访问器，基本上评估我们在 tree_P1 中写入的内容与我们在 [=12] 中写入的内容=].

但这似乎只有在本地构建记录时才有效 (let tree_C :=…)，如果它是使用 Definition.

定义的则无效

但是Fixpoint可以很好地查看其他定义，例如通过 list_P。那么记录有什么特别之处，我可以让 Coq 接受 tree_P3?

Answer 1

对于问题1。我相信在tree_P1中，class实例的定义在fix构造中，并在终止检查时减少。

正如您正确指出的那样，以下定义被拒绝。

Fixpoint tree_P1' {a} `{C a} (t : tree a) : bool :=
    let tree_C := Build_C _ tree_P1' in
    match t with Node _ x ts => orb (P x) (@P _ (* mark *) _ ts) end.

在此定义中，注释 (* mark *) 之后所需的 class 实例由您在第 7 行的定义填充。但此定义存在于 fix 构造之外并且不会以相同的方式被终止检查器减少。因此，未应用于任何树参数的 tree_P1' 的出现将保留在代码中，并且终止检查器将无法确定此出现仅用于小于参数的参数初始参数。

这是一个大胆的猜测，因为我们看不到被拒绝的函数的主体。

Answer 2

在阅读了 Coq 中的终止检查器之后，我想我找到了解决方案：

终止检查器将始终展开局部定义和 beta-reduce。这就是 tree_P1 起作用的原因。

终止检查器还将在必要时展开调用的定义（如 list_C'、P、existsb），这就是 tree_P2 起作用的原因。

但是，终止检查器不会展开出现在 match … with 子句中的定义，例如 list_C。这是一个最小的例子：

(* 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.

原始代码的解决方法是确保调用所有定义（而不是模式匹配），以确保终止检查器将展开它们。我们可以通过切换到连续传递样式来做到这一点：

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.

这甚至适用于类型 classes，因为类型 class 分辨率与这些问题无关：

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.

终止检查器何时减少记录访问器

When does the termination checker reduce a record accessor

coq

termination