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

Question

在Coq的SSReflect扩展中，我发现了两种约定，它们似乎特别有用，但我没有看到它们被广泛采用于新的依赖类型语言（如Lean、Agda、Idris）。首先，尽可能使用返回布尔值的函数来表示谓词，而不是归纳定义数据类型。这默认带来可决定性，为计算证明提供了更多机会，并通过避免证明引擎携带大型证明项来提高检查性能。我看到的主要缺点是，在证明时需要使用反射引理来操作这些布尔谓词。其次，具有不变量的数据类型被定义为包含简单数据类型和不变量证明的依赖记录。例如，固定长度序列在SSReflect中的定义方式为：

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

一个序列和该序列长度为特定值的证明。这与例如Idris定义此类型的方式相反：

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

一种依赖类型数据结构，其中不变量是其类型的一部分。 SSReflect方法的一个优点是它允许重用，因此例如对于seq定义的许多函数和关于它们的证明仍可以与tuple一起使用（通过操作底层的seq），而在Idris的方法中，像reverse，append之类的函数需要为Vect重新编写。 Lean实际上在其标准库中具有SSReflect风格的等效物vector，但它也具有类似于Idris的array，后者在运行时似乎具有优化实现。

甚至有一本SSReflect导向的书声称Vect n A风格的方法是反模式：

“依赖类型语言，尤其是Coq中常见的反模式是将这些代数属性编码到数据类型和函数本身的定义中（这种方法的一个典型例子是长度索引列表）。虽然这种方法看起来很有吸引力，因为它展示了依赖类型捕捉数据类型和函数的某些属性的能力，但它本质上是不可扩展的，因为总会有另一个感兴趣的属性，这个属性没有被数据类型/函数的设计者预见到，因此它仍然必须作为外部事实进行编码。这就是为什么我们倡导一种方法，即尽可能靠近程序员定义数据类型和函数，并单独证明它们的所有必要属性。”

我的问题是，为什么这些方法没有被更广泛地采用。我是否忽略了一些缺点，或者它们的优点在支持依赖模式匹配比Coq更好的语言中不那么显著？

- LogicChains

Answer 1

我可以对第一个观点（将谓词定义为返回布尔值的函数）提供一些想法。 我最大的问题是：根据定义，即使它计算的结果不是您想要计算的结果，该函数也不可能出现错误。 在许多情况下，如果您必须在谓词的定义中包含决策过程的实现细节，则也会掩盖您实际上所指的谓词。

在数学应用中，如果您想定义一个特定于一般情况下无法判定的东西的谓词，即使在您的特定情况下可以判定，也会有问题。 这里我谈论的一个例子是定义具有给定表示的群：在Coq中，定义这个群的常见方法是底层集合为生成器中的形式表达式的等价关系的setoid，并且由“单词等价性”给出相等性。 通常，尽管在许多特定情况下可以判定此关系，但总体而言，这种关系是不可判定的。 但是，如果您只能定义具有可判定单词问题的演示文稿组，则失去了定义将所有不同示例绑在一起并一般地证明有限演示或有限呈现组的能力。 另一方面，将单词等价关系定义为抽象的Prop或等效形式是简单明了的（如果可能有点长）。

就个人而言，我更喜欢首先给出谓词最透明的定义，然后在可能的情况下提供决策过程（这里我更喜欢返回类型为{P} + {~P}的值的函数，虽然返回布尔值函数也可以很好地工作）。 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.

- Daniel Schepler

Answer 2

这样做可以默认带来可决定性，为计算证明打开更多机会，并通过避免证明引擎携带大型证明项来提高检查性能。您不必像Edwin Brady的论文中描述的那样携带大型术语以实现“强制优化”。Agda确实具有影响类型检查的强制性（特别是如何计算宇宙是相关的），但我不确定仅在类型检查时间使用的东西是否在运行时之前真正被删除。无论如何，Agda有两个不相关的概念：.(eq : p ≡ q)是通常的不相关性（意味着eq在类型检查时间是不相关的，因此在该类型的任何其他术语方面定义上等同），而..(x : A)是脊柱不相关性（不确定是否是正确的术语。我认为Agda源将这种事情称为“非严格不相关性”），其字面上是用于擦除计算上不相关但不完全不相关的术语。所以你可以定义

data Vec {α} (A : Set α) : ..(n : ℕ) -> Set α where
  [] : Vec A 0
  _∷_ : ∀ ..{n} -> A -> Vec A n -> Vec A (suc n)

在运行时之前，n 将被清除。至少看起来是这样设计的，但很难确定，因为 Agda 有许多文档不完善的功能。

你可以在 Coq 中编写那些零成本证明，只是因为它也实现了 Prop 中的无关性。但是，在 Coq 的理论中，无关性已经深入内部，而在 Agda 中，它是一个单独的功能，因此可以理解为什么人们更容易在 Coq 中使用无关性。

SSReflect 的方法的一个优点是它允许重用，因此例如对于 seq 定义的许多函数和关于它们的证明仍然可以与 tuple 一起使用（通过操作基础的 seq），而使用 Idris 的方法则需要为 Vect 重新编写像 reverse、append 等函数。

如果您必须证明的属性与针对索引数据定义的函数具有相同的复杂度，那么重用实际上并不是真正的重用。而且，要做一个统一机器的工作并传递显式证明以及应用引理来从 suc (length xs) ≡ n 推导出 length xs ≡ n（以及 sym、trans、subst 和所有其他统一机器可以在许多情况下为您节省的引理）也很不方便。此外，通过滥用命题等式，您会失去一些清晰度：在上下文中具有 xs : List A; length xs ≡ n + m 而不是 xs : Vec A (n + m) 并不会提高可读性，特别是如果它们很大，这种情况经常发生。还有另一个问题：有时使用SSReflect的方法定义函数更加困难：您提到了 Vect 的 reverse，我向您挑战，从零开始定义此函数（使用 List 的 reverse 作为底层“重用”部分），然后将您的解决方案与 Agda 标准库中 Data.Vec 的定义进行比较。如果您没有默认启用命题的不相关性（这是 Agda 的情况），那么如果您想证明 reverse (reverse xs) ≡ xs 等属性，则还需要证明有关证明的属性，这是很多非平凡样板文件。

所以 SSReflect 的方法并不完美，另一个方法也是如此。有没有什么东西可以改进两者？是的，有装饰（见 Ornamental Algebras, Algebraic Ornaments 和 The essence of ornaments）。你可以通过应用相应的装饰代数轻松地从 List 获取 Vec，但我无法说你能从中获得多少代码重用以及类型是否会让你烦恼。我听说有人实际上在某个地方使用装饰。

因此，并不是我们拥有理想的 SSReflect 解决方案，而其他人拒绝采用它。只是希望有更合适的方式来实现实际的代码重用。

更新

Anton Trunov在他的评论中让我意识到我有点太过于Agda思维，而Coq中的人们有可以简化证明的策略，因此在Coq中进行证明通常比对数据定义的函数进行定义更容易（前提是您拥有像CPDT书中的crush这样的武器）。好吧，那么我想默认的证明不相关性和繁重的策略机制就是使SSReflect方法在Coq中有效的原因。

- effectfully

---

定义reverse函数很容易：Definition trev T n (t : n.-tuple T) := [tuple of rev t]。在这里，我们重用了列表的rev函数（在ssr中称为seq）。证明trev是自反的也很容易：Lemma trevK T n : involutive (@trev T n). Proof. by move=>t; apply: val_inj; rewrite /= revK. Qed.在这里，我们再次重用了列表的revK，并使用了非平凡部分的证明不可知性引理val_inj。 - Anton Trunov

@AntonTrunov，很有趣，谢谢。您能否详细说明证明的工作原理？ - effectfully

我使用了mathcomp的线性时间rev。 - Anton Trunov

我提供的证明依赖于val_inj引理来剥离_：size tval == n部分。在SSReflect中，==表示布尔可决等式，我们操作nat，因此val_inj移除了元组的无关证明部分，并让我们处理底层列表，以便我们可以重用列表引理。这里是一个包含所有导入的gist。 - Anton Trunov

我刚刚注意到你的编辑，我想说SSReflect构建证明的方法与CPDT相反。在这里，我们不使用任何聪明的Ltac技巧（只是rewrite和apply），但可决性肯定起着重要作用。 - Anton Trunov