Coq 的类型系统在这个例子中做了什么？

Question

我对 Coq 的类型系统在下面 h 的定义中证明项的匹配部分的行为感到困惑：

Set Implicit Arguments.
Definition h := fun (a b : nat) (e : a = b) =>
(fun (x y : nat)(HC : b = y)(H : x = y) =>
(match H in (_ = y0) return (b = y0 -> b = x) with
| @eq_refl _ _ => fun HC0 : b = x => HC0
end HC)) a b (eq_refl b) e.

检查 h 告诉我们整体类型是 "forall a b : nat, a = b -> b = a"。

由于 H 的类型是 x = y，由于 return 子句，看起来匹配将 return 类型为 b = y -> b = x 的项。在应用了后面的各种项之后，我们得到了 h 的预期类型。

然而，fun HC0 : b = x => HC0 是类型 b = x -> b = x 的恒等函数。我不相信有任何强制将 b = x -> b = x 识别为类型 b = y -> b = x。

我最好的猜测是 H 的构造函数是 @eq_refl nat x 类型 x = x，是唯一的。由于 H 也是类型 x = y，因此名称 x 和 y 绑定到相同的项。因此，类型系统决定 b = x -> b = x 是类型 b = y -> b = x。这很近吗？是否在某处解释或记录了这种行为？我查看了 iota 减少，但我认为这不正确。

Answer 1

差不多就这些了。此行为已记录在案（在 the manual 中查找 "the match...with...end construction"），尽管了解其中发生的事情可能有点令人生畏。

首先，回顾一下典型的 match 在 Coq 中是如何检查的：

Inductive list (T : Type) :=
| nil : list T
| cons : T -> list T -> list T.

Definition tail (T : Type) (l : list T) : list T :=
  match l with 
  | nil       => nil
  | cons x l' => l'
  end.

Coq 检查 (1) list 类型的每个构造函数在 match 中都有对应的分支，以及 (2) 每个分支都具有相同的类型（在本例中，list T) 假设在每个分支中引入的构造函数参数具有适当的类型（这里，假设 x 的类型为 T 并且 l' 的类型为 list T第二个分支）。

在这种简单的情况下，用于检查每个分支的类型与整个匹配表达式的类型完全相同。然而，这并非总是正确的：有时，Coq 根据从正在检查的分支中提取的信息使用更专业的类型。在对 indexed 归纳类型进行案例分析时经常发生这种情况，例如 eq:

Inductive eq (T : Type) (x : T) : T -> Prop :=
| eq_refl : eq T x x.

（= 符号只是 eq 的中缀语法糖。）

给定在冒号右侧的归纳类型的参数在 Coq 中是特殊的：它们被称为 indices。出现在左侧的参数（在本例中为 T 和 x）被称为参数。参数在归纳类型的声明中必须全部不同，并且必须与所有构造函数的结果中使用的参数完全匹配。例如，考虑以下非法片段：

Inductive eq' (T : Type) (x : T) : T -> Type :=
| eq_refl' : eq nat 4 3.

Coq 拒绝此示例，因为它在 eq_refl' 构造函数的结果中找到 nat 而不是 T。

另一方面，

索引没有此限制：出现在 return 类型构造函数上的索引可以是适当类型的任何表达式。此外，该表达式可能会有所不同，具体取决于我们所在的构造函数。正因为如此，Coq 允许每个分支的 return 类型根据每个分支索引的选择而变化。考虑以下原始示例的稍微简化的版本。

Definition h (a b : nat) (e : a = b) : b = a :=
  match e in _ = x return x = a with
  | eq_refl => eq_refl : a = a
  end.

由于 eq 的第二个参数是一个索引，原则上它可能会因所使用的构造函数而异。由于我们只有在查看所使用的构造函数时才知道该索引实际上是什么，因此 Coq 允许匹配的 return 类型依赖于该索引：匹配的 in 子句给出了名称归纳类型的所有索引，这些名称成为可以在 return 子句中使用的绑定变量。

当键入一个分支时，Coq 会找出索引的值，并将这些值替换为 in 子句中声明的变量。该匹配只有一个分支，该分支强制索引等于 e 类型的第二个参数（在本例中为 a）。因此，Coq 试图确保该分支的类型是 a = a（即，x = a 并用 a 代替 x）。因此，我们可以简单地提供 eq_refl : a = a 就完成了。

既然 Coq 检查了所有分支都是正确的，它将 return 子句的类型分配给整个匹配表达式，并用 e 类型的索引替换 x.此变量 e 的类型为 a = b，索引为 b，因此结果类型为 b = a（即 x = a 和 b代替 x).

This answer 提供了有关参数和索引之间差异的更多解释（如果有帮助的话）。

Coq 的类型系统在这个例子中做了什么？

What is Coq's type system doing in this example?

coq