Log*_*ins 24 coq agda dependent-type idris lean
我在Coq的SSReflect扩展中找到了两个公约,这些公约看起来特别有用,但我还没有看到在新的依赖类型语言(Lean,Agda,Idris)中广泛采用的公约.
首先,可能的谓词表示为布尔返回函数,而不是归纳定义的数据类型.这默认带来可判定性,通过计算开辟了更多的证明机会,并通过避免校对引擎携带大量证明条件来提高检查性能.我看到的主要缺点是需要使用反射词来在证明时操纵这些布尔谓词.
其次,具有不变量的数据类型被定义为包含简单数据类型和不变量证明的从属记录.例如,固定长度序列在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.Lean实际上在其标准库中具有等效的SSReflect样式vector,但它也具有Idris样式array,似乎在运行时具有优化的实现.
一本面向SSReflect的书甚至声称Vect n A风格方法是反模式:
依赖类型语言和Coq中的常见反模式特别是将这样的代数属性编码到数据类型和函数本身的定义中(这种方法的规范示例是长度索引列表).虽然这种方法看起来很吸引人,因为它展示了依赖类型捕获它们的数据类型和函数的某些属性的能力,但它本质上是不可扩展的,因为总会有另一个感兴趣的属性,这是设计者没有预见到的.数据类型/函数的数据,因此它必须被编码为外部事实.这就是为什么我们提倡这种方法,其中数据类型和函数被定义为尽可能接近程序员定义的方式,并且它们的所有必要属性都是分开证明的.
因此,我的问题是,为什么没有更广泛地采用这些方法.我缺少哪些缺点,或者它们的优势在具有比Coq更好支持依赖模式匹配的语言中不那么重要？
我可以就第一点提供一些想法（将谓词定义为布尔返回函数）。我用这种方法的最大问题是：从定义上说，该函数不可能有错误，即使事实证明它所计算的不是您想要的。在许多情况下，如果您必须在其定义中包括该谓词的决策过程的实现细节，也会掩盖您对谓词的实际含义。
在数学应用程序中，如果您想定义一个谓词，它通常是无法确定的，即使在您的特定情况下它是可确定的，它也会存在一个问题。我在这里谈论的一个示例是使用给定的演示文稿定义组：在Coq中，定义此组的一种常见方法是setoid，其基础集是生成器中的形式表达式，而等式由“ word”给出等价”。通常，这种关系是不确定的，尽管在许多特定情况下是可以确定的。但是，如果您仅限于使用可确定单词问题的演示文稿来定义组，那么您将无法定义将所有不同示例联系在一起的统一概念，并一般性地证明有关有限表示或有限表示组的事物。另一方面，将单词等价关系定义为抽象Prop 或等效项很简单（如果可能会很长）。
就个人而言，我更喜欢先给谓语最透明的定义，然后在可能的地方提供决策程序（{P} + {~P}在这里，我偏爱返回类型为type的函数，尽管布尔返回函数也可以正常工作）。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.
这在默认情况下带来了可判定性，为通过计算证明提供了更多机会，并通过避免证明引擎携带大量证明项来提高检查性能。
您不必像Edwin Brady 的论文中所描述的那样以“强制优化”的名义携带大量术语。Agda 确实具有影响类型检查的强制（尤其是计算 Universe 的方式是相关的），但我不确定仅在类型检查时使用的东西是否真的在运行时之前被删除。无论如何，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 中比在 Agda 中更容易发现无关性的使用。
SSReflect 方法的一个优点是它允许重用，例如，许多为
seq它们定义的函数和关于它们的证明仍然可以使用tuple（通过在底层 上操作seq），而使用 Idris 的方法函数，如 reverse、append 和 the就像需要为Vect.
如果您无论如何都必须证明属性，并且这些证明与在索引数据上定义的函数具有相同的复杂性，那么这不是真正的重用。这也是不方便做一个统一机械作业，并通过各地明确的证据和适用引理得到length xs ? n来自suc (length xs) ? n（也sym，trans，subst和所有其他引理，一个统一的机器可以节省你在很多情况下）。此外，您会因滥用命题相等xs : List A; length xs ? n + m而失去一些清晰度：使用而不是xs : Vec A (n + m)不会提高上下文的可读性，尤其是当它们很大时，通常就是这种情况。还有另一个问题：有时使用 SSReflect 的方法定义函数更难：你提到reverse过Vect，我挑战您从头开始定义此函数（将reverseforList作为引擎盖下的“重用”部分），然后将您的解决方案Data.Vec与 Agda 标准库中的定义进行比较。如果默认情况下您没有为命题启用无关性（Agda 就是这种情况），那么您还需要证明有关证明的属性，例如，如果您想证明reverse (reverse xs) ? xs这是很多重要的样板文件.
所以SSReflect的做法并不完美。另一个也是。有什么可以改善两者的吗？是的，装饰品（见装饰代数、代数装饰品和装饰品的本质）。你可以很容易地得到Vec来自List通过应用相应的观赏性代数，但我不能说你有多少代码重用从中得到和类型是否将推动你疯了还是不行。我听说人们实际上在某处使用装饰品。
所以并不是说我们有一个理想的 SSReflect 的解决方案而其他人拒绝采用它。只是希望有一种更合适的方法来获得实际的代码重用。
更新
安东Trunov在他们的评论让我意识到我是有点太阿格达头脑和人勒柯克有战术可以简化证明了很多，所以在Coq的证明通常更容易（只要你有喜欢的武器crush从CPDT不是定义书）数据上的函数。好吧，那么我想证明默认情况下无关紧要和繁重的策略机制是使 SSReflect 的方法在 Coq 中有效的原因。