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

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内容tree_P2.

但是,这似乎只有在本地(let tree_C :=…)创建记录时才有效,而不是在使用时定义Definition.

但是Fixpoint可以通过其他定义来查看,例如通过list_P.那么记录有什么特别之处,我可以让Coq接受tree_P3吗？

Answer 1

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

\n\n

终止检查器将始终展开本地定义和 beta-reduce。这就是为什么tree_P1有效。

\n\n

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

\n\n

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

\n\n

(* works *)\nFixpoint foo1 (n : nat) : nat :=\n  let t := Some True in \n  match Some True with | Some True => 0\n                       | None => foo1 n end.\n\n(* works *)\nFixpoint foo2 (n : nat) : nat :=\n  let t := Some True in \n  match t with | Some True => 0\n               | None => foo2 n end.\n\n(* does not work *)\nDefinition t := Some True.\n\nFixpoint foo3 (n : nat) : nat :=\n  match t with | Some True => 0\n               | None => foo3 n end.\n

\n\n

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

\n\n

Require Import Coq.Lists.List.\n\nRecord C_dict a := {  P' : a -> bool }.\n\nDefinition C a : Type := forall r, (C_dict a -> r) -> r.\n\nDefinition P {a} (a_C : C a) : a -> bool :=\n  a_C _ (P' _).\n\nDefinition list_P {a} (a_C : C a) : list a -> bool := existsb (P a_C).\n\nDefinition list_C  {a} (a_C : C a) : C (list a) :=\n   fun _ k => k {| P' := list_P a_C |}.\n\nInductive tree a := Node : a -> list (tree a) -> tree a.\n\n(* Works now! *)\nFixpoint tree_P1 {a} (a_C : C a) (t : tree a) : bool :=\n    let tree_C := fun _ k => k (Build_C_dict _ (tree_P1 a_C)) in\n    match t with Node _ x ts => orb (P a_C x) (P (list_C tree_C) ts) end.\n

\n\n

这甚至适用于类型类，因为类型类解析与这些问题无关：

\n\n

Require Import Coq.Lists.List.\n\nRecord C_dict a := {  P' : a -> bool }.\n\nDefinition C a : Type := forall r, (C_dict a -> r) -> r.\nExisting Class C.\n\nDefinition P {a} {a_C : C a} : a -> bool := a_C _ (P' _).\n\nDefinition list_P {a} `{C a} : list a -> bool := existsb P.\n\nInstance list_C  {a} (a_C : C a) : C (list a) :=\n   fun _ k => k {| P' := list_P |}.\n\nInductive tree a := Node : a -> list (tree a) -> tree a.\n\n(* Works now! *)\nFixpoint tree_P1 {a} (a_C : C a) (t : tree a) : bool :=\n    let tree_C : C (tree a) := fun _ k => k (Build_C_dict _ (tree_P1 a_C)) in\n    match t with Node _ x ts => orb (P x) (P ts) end.\n

\n