coq - 为什么较新的依赖类型语言没有采用 SSReflect 的方法？

Question

我在 Coq 的 SSReflect 扩展中发现了两个约定，它们看起来特别有用，但我还没有在较新的依赖类型语言(Lean、Agda、Idris)中看到它们被广泛采用。

首先，在可能的情况下，谓词被表示为返回 bool 值的函数，而不是归纳定义的数据类型。这在默认情况下带来了可判定性，为通过计算证明提供了更多机会，并通过避免证明引擎携带大量证明项来提高检查性能。我看到的主要缺点是在证明时需要使用反射引理来操纵这些 bool 谓词。

其次，具有不变量的数据类型被定义为包含简单数据类型和不变量证明的依赖记录。例如，固定长度序列在 SSReflect 中定义如下:

Structure tuple_of : Type := Tuple {tval :> seq T; _ : size tval == n}.

A seq并且证明该序列的长度是某个值。这与例如Idris 定义了这种类型:

data Vect : (len : Nat) -> (elem : Type) -> Type 

一种依赖类型的数据结构，其中不变量是其类型的一部分。 SSReflect 方法的一个优点是它允许重用，例如为 seq 定义的许多函数并且关于它们的证明仍然可以用于 tuple (通过对底层 seq 进行操作)，而使用 Idris 的方法，函数类似于 reverse , append等需要为Vect重写.精益实际上在其标准库中具有等效的 SSReflect 样式，vector ，但它也有一个 Idris 风格的 array这似乎在运行时有一个优化的实现。

一 SSReflect-oriented book甚至声称 Vect n A样式方法是一种反模式:

A common anti-pattern in dependently-typed languages and Coq in particular is to encode such algebraic properties into the definitions of the datatypes and functions themselves (a canonical example of such approach are length-indexed lists). While this approach looks appealing, as it demonstrates the power of dependent types to capture certain properties of datatypes and functions on them, it is inherently non-scalable, as there will be always another property of interest, which has not been foreseen by a designer of the datatype/function, so it will have to be encoded as an external fact anyway. This is why we advocate the approach, in which datatypes and functions are defined as close to the way they would be defined by a programmer as possible, and all necessary properties of them are proved separately.

因此，我的问题是，为什么没有更广泛地采用这些方法。是否有我遗漏的缺点，或者它们的优点在对依赖模式匹配的支持比 Coq 更好的语言中不那么重要？

Answer 1

我可以提供关于第一点的一些想法(将谓词定义为返回 bool 值的函数)。我对这种方法的最大问题是:那么根据定义，函数不可能有错误，即使结果它计算的不是你想要计算的。在许多情况下，如果您必须在其定义中包含谓词的决策过程的实现细节，它也会模糊您对谓词的实际含义。

在数学应用中，如果您想定义一个谓词，该谓词是一般不可判定的事物的特化，即使它恰好在您的特定情况下是可判定的，也会出现问题。我在这里谈论的一个例子是用给定的表示定义组:在 Coq 中，定义它的一种常用方法是 setoid，底层集合是生成器中的形式表达式，以及由“word”给出的等式等价”。通常，这种关系是不可判定的，尽管在许多特定情况下是可判定的。但是，如果您仅限于定义具有可判定词问题的表示的组，那么您将无法定义将所有不同示例联系在一起的统一概念，并无法对有限表示或有限表示组进行一般性证明。另一方面，将单词等价关系定义为抽象Prop或等价物很简单(如果可能有点长)。

就我个人而言，我更喜欢先给出最透明的谓词定义，然后在可能的情况下提供决策过程(返回 {P} + {~P} 类型的值的函数在这里是我的首选，尽管返回 bool 值的函数也能很好地工作)。 Coq 的类型类机制可以提供一种方便的方式来注册这样的决策过程；例如:

Class Decision (P : Prop) : Set :=
decide : {P} + {~P}.
Arguments decide P [Decision].

Instance True_dec : Decision True := left _ I.
Instance and_dec (P Q : Prop) `{Decision P} `{Decision Q} :
  Decision (P /\ Q) := ...

(* Recap standard library definition of Forall *)
Inductive Forall {A : Type} (P : A->Prop) : list A -> Prop :=
| Forall_nil : Forall P nil
| Forall_cons : forall h t, P h -> Forall P t -> Forall P (cons h t).
(* Or, if you prefer:
Fixpoint Forall {A : Type} (P : A->Prop) (l : list A) : Prop :=
match l with
| nil => True
| cons h t => P h /\ Forall P t
end. *)

Program Fixpoint Forall_dec {A : Type} (P : A->Prop)
  `{forall x:A, Decision (P x)} (l : list A) :
  Decision (Forall P l) :=
  match l with
  | nil => left _ _
  | cons h t => if decide (P h) then
                  if Forall_dec P t then
                    left _ _
                  else
                    right _ _
                else
                  right _ _
  end.
(* resolve obligations here *)
Existing Instance Forall_dec.