Coq中的哪些形式的目标被认为是"真实的"？

Question

当我证明一些定理时,我的目标随着我应用越来越多的策略而演变.一般来说,目标往往分为子目标,子目标更简单.在最后一点,Coq决定目标得到证实.这个"经证实"的目标可能如何？这些目标似乎很好:

a = a.                       (* Any object is identical to itself (?) *)
myFunc x y = myFunc x y.     (* Result of the same function with the same params
                                is always the same (?) *)

还有什么可以在这里或者可能是例子从根本上是错误的？

换句话说,当我最终申请时reflexivity,Coq只是说** Got it **没有任何解释.有没有办法获得更多关于它实际上做了什么的细节或者为什么它决定目标被证明了？

Answer 1

你实际上面对的是一个看似不那么普遍的非常普遍的概念,因为Coq有一些用户友好的设施,特别是平等的推理.

一般来说,Coq接受一个目标,只要它收到一个类型是目标类型的术语:它已经确信命题是真的,因为它已经确信这个命题描述的类型是有人居住的,以及说服了什么这是你在证明中帮助建立的实际见证人.

对于归纳数据类型的特定情况,您将能够证明命题的两种方式P a b c是:

• 通过构造一个类型的术语P a b c,使用归纳类型的构造函数P,并提供所有必要的参数.

• 或者通过重复使用您可以匹配的类型的环境中的现有证明或公理P a b c.

对于更具体的等式证明情况(相等只是 Coq中的归纳数据类型),我在上面列出的两种方式退化为:

• 平等的唯一构造者是eq_refl,并且要应用它,你需要表明双方在法官上是平等的.在大多数情况下,这对应于看起来像的目标T a b c = T a b c,但它实际上是一个稍微宽泛的平等概念(见下文).对于这些,您所要做的就是应用eq_refl构造函数.简而言之,就是reflexivity这样!

• 第二种情况包括证明平等成立,因为你在你的背景中有其他的平等,这里没什么特别的.

现在问题的一部分是:Coq何时接受平等的两个方面是否反身？

如果我没有弄错的话,答案是当平等的两边是αβδιζ-可兑换的时候.这大概意味着有一种方法可以通过重复应用来使它们在语法上相等:

• α:理智地重命名非自由变量
• β:计算可简化的表达式
• δ:展开定义
• ι:简化匹配
• ζ:扩展let-bound表达式

[如果有更多规则适用或我错了,请有人纠正我]

例如,这些规则未捕获的一些内容是:

• 以不同方式执行或多或少相同的函数的相等性:

  (fun x => 0 + x) = (fun x => x + 0)
  quicksort = mergesort
  

• 保持减少但相等的术语平等:

  forall n, 0 + n = n + 0