logo标签列表

Coq中的相等性和Awodey论文中的相等性

coqtype-theory
4
在论文《同一性作为逻辑原理》中，Awodey在第7页上写道：
让我们考虑内涵类型理论和外延类型理论的例子。外延理论具有明显“更强”的相等概念，因为它允许人们在所有情况下简单地将相等的东西替换为相等的东西。相比之下，内涵系统中，一个可以有a = b以及一个关于a的语句Φ(a)，但却没有Φ(b)。
我不理解这一点，因为我认为这是相等性的基本属性。
此外，在Coq中，人们可以简单地证明：
Theorem subs: forall (T:Type)(a b:T)(p:a=b)(P:T-> Prop), P a -> P b. 
intros.
rewrite <- p.
assumption.
Qed.
1
在我的看法中，源代码中似乎存在错误，对于任何命题等式概念，subs必须是可证明的。 - András Kovács
1
也许 Steve 的意思是你需要使用显式的“重写”步骤来得出Φ(b)的结论。我想最好直接问他！ - ejgallego
2个回答
3
如果我没记错，Awodey的论文中，符号Φ(a)表示将Φ中的某个隐含自由变量替换为表达式a。
在我的回答中，我将使用下面更明确的符号（对应于论文中的Φ(a)）：
Φ[z ⟼ a]

这意味着在表达式 Φ 中，自由变量 z 将被表达式 a 替换。

例如：

(x = z)[z ⟼ a]

结果是

(x = a)

现在，我假设您已经熟悉了类型理论的常规演示方式，即通过推理规则，例如在HoTT Book的附录A.2中所述。
类型理论使用两种相等的概念。 恒等类型：通常使用符号=在推理规则中书写。为了得出类似于a = b这样的语句，我们需要提供一个证明项。例如，让我们看一下恒等类型的引入规则：
      a : A 
---------------- (=)-INTRO
 refl a : a = a

在这里，refl a 充当了证明项或证据，证明了我们声称的a = a成立（即，refl a代表微不足道的或自反性证明）。因此，像p: a = b这样的语句表达了由证据p可以确定a和b是相同的。 定义相等：通常使用符号≡在推理规则中书写。语句a ≡ b表示a和b是可互换的，在任何地方都可以替换，或者是替换等价的。这种相等性捕捉到像“根据定义”，“通过计算”，“通过简化”这样的概念。这种类型的相等性没有随之带有一个证明项，即它不是一个类型声明。这是Coq在您使用simpl和compute策略时隐含使用的相等性。例如，让我们看一下≡的自反性规则：
  a : A
--------- (≡)-REFLE
  a ≡ a

请注意，a ≡ a 左侧没有证明项（与上面的 (=)-INTRO 规则进行比较）。在这种情况下，证明系统将 a ≡ a 视为一个事实，即某些东西可以无需明确说明其理由而成立，因为证明系统中 ≡ 的唯一用途是重写表达式。
在其他推理规则中也可以发现 ≡ 仅用于简化表达式，例如，≡ 的类型保持规则。
   a : A     A ≡ B
 ------------------ (≡)-TYPE-PRESERV
        a : B

换句话说，如果你从类型A的术语a开始，并且你知道类型A和B是可互换的，那么术语a也具有类型B。请注意（这将在以后非常重要！！）证明术语或证据对于B没有改变，它仍然是用于A的相同证明术语。
现在我们可以进入问题。
Extensional Type Theory（ETT）与Intensional Type Theory（如HoTT或CoC）的区别在于它们处理身份类型和定义平等的方式。
ETT通过添加以下推理规则使身份类型和定义平等可互换：
 p : a = b
----------- (=)-EXT
   a ≡ b

换句话说，证明标识的证据 p 变得无关紧要，我们在证明系统中将 a 和 b 视为可互换的（感谢诸如 (≡)-TYPE-PRESERV 等类似规则）。
在 ETT 中，从假设 p：a = b 和 a：A 开始，我们可以执行以下操作：
  a : A                    p : a = b
--------- (≡)-REFLE      ----------- (=)-EXT
  a ≡ a                      a ≡ b 
------------------------------------- (=)-CONG        (*1)
            (a = a) ≡ (a = b)

其中，(=)-CONG是一个同余规则（即，定义等价的术语产生定义等价的身份类型），我将这个推导称为(*1)。

利用(*1)，我们可以推导出：

     a : A                           
----------------- (=)-INTRO    -------------------- (*1)
 refl a : a = a                 (a = a) ≡ (a = b)
-------------------------------------------------- (≡)-TYPE-PRESERV
                    refl a : a = b

我们需要在(*1)中插入我们上面推导的内容。

换句话说，如果我们忽略假设 a：A 和中间步骤，实际上就好像我们进行了以下推论：

p : a = b            refl a : a = a
-------------------------------------
          refl a : a = b

由于ETT将a和b视为可互换的（这要归功于假设p：a=b和(=)-EXT规则），因此对于a=a的证明refl a也可以被视为a=b的证明。 因此，在ETT中，拥有类似a=b的恒等性的证明足以替换涉及a的任何语句中的某些或全部出现的a为b。

那么，在内涵类型理论（ITT）中会发生什么呢？

在ITT中，不假定(=)-EXT规则。 因此，我们无法执行上面的推导(*1)，特别地，以下推论是无效的：

p : a = b            refl a : a = a
-------------------------------------
          refl a : a = b

这是一个例子，我们有一个标识p：a = b，但从语句(refl a: a = z)[z ⟼ a]，我们不能得出语句(refl a: a = z)[z ⟼ b]。我认为这是Awodey论文所提到的内容之一。
为什么这是无效推理？因为refl a：a = b强制a和b在定义上相等（即引入refl a到推导中的唯一方法是通过(=)-INTRO规则），但这并不一定从假设p：a = b中成立。例如，在HoTT中，区间类型I（在HoTT Book的第6.3节中）有两个项0：I和1：I，它们在定义上不相等，但我们有一个证明seg：0 = 1。
存在其他身份证明，而不是平凡或自反性证明，正是意图类型理论具有丰富性的原因。例如，这使得HoTT具有Univalence和Higher Inductive Types。
那么，在ITT中，我们可以从假设p：a = b和refl a：a = a中得出什么结论？
在你的问题中，你在Coq中证明的定理在HoTT中称为“transport”函数（在HoTT Book的第2.3节中）。使用你的定理（删除隐含参数），你将能够进行以下推导：
  p : a = b               refl a : a = a
------------------------------------------
   subs p (λx => a = x) (refl a) : a = b

换句话说，我们可以得出结论 a = b，但是我们的证明术语已经改变了！在ETT中，我们只是进行了一次替换（因为a和b是可互换的），从而使我们能够在结论中使用相同的证据（即refl a）。但在ITT中，由于恒等类型的丰富性，我们不能将a和b视为替换等价物。为了反映这个意图，我们需要将假设的证明组合起来，以建立我们在结论中的新证据。
因此，从 (refl a : a = z)[z ⟼ a]，我们不能得出 (refl a : a = z)[z ⟼ b] 的结论，但我们可以得出 subs p (λx => a = x) (refl a) : a = b 的结论，这不是像ETT中那样从假设中进行简单替换的结果。
-2
在 Coq 中，rewrite 策略可能会失败 - 它可能会生成一个类型不正确的术语。
如果我记得正确，有时可以通过一些小心的操作来避免这种情况，但是如果您通过（隐式或显式）引入额外的公理（例如函数扩展性或 JMeq_eq），那么第一个目标不再仅仅是从第二个目标推导出来的。
我看不出你的回答与我的问题有什么关系。 - Cryptostasis
由于重写并不总是有效的，这是由于Coq中的类型问题而不是简单的错误所导致的，这就解释了为什么在Coq的逻辑中，Φ(a)并不一定意味着如果a=b，则Φ(b)。 - Robin Green
我的问题恰恰相反。在COQ中，它通常有效，但Awodey说它通常无效... - Cryptostasis
不，它在 Coq 中通常不起作用。你的定理并没有表达出你想要表达的意思。我的意思是它看起来像是这样，但它只是在逻辑上是一个定理，而不是在元逻辑中。Awodey 是在元逻辑层面上发言。 - Robin Green
网页内容由stack overflow 提供, 点击上面的
可以查看英文原文，
原文链接