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

Question

我感到困惑勒柯克的类型系统对的小时以下的定义证明长期的匹配部分的行为：

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 AB：NAT，一= b - > b = a“。由于返回子句，由于H的类型是x = y，它看起来像匹配将返回类型为b = y - > b = x的项。应用后面的各种术语后，我们得到h的预期类型。

然而，有趣的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

这是非常多的。这种行为是有记录的（在this manual chapter中查找“匹配......与......结束构造”），但理解发生的事情可能有点令人生畏。

首先，回顾一个典型的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会根据从其检查的分支中提取的信息使用更专用的类型。这在做案例分析时，对索引归纳类型，像eq经常发生：（该=符号只是缀语法糖eq）

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

感应型的参数提供给冒号右边在Coq中是特殊的：它们被称为指数。那些出现在左侧（在这种情况下，T和x）被称为参数。参数必须在归纳类型的声明中全部不同，并且必须与所有构造函数的结果中使用的参数完全匹配。例如，请考虑以下违法片段：因为它在eq_refl'构造的结果发现nat而不是T

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

勒柯克拒绝这个实例。

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

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允许匹配的返回类型取决于该索引：匹配的in子句为所有归纳类型的索引提供名称，并且这些名称成为可在return子句中使用的绑定变量。

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

现在Coq的检查了所有分支是正确的，将其分配到整个匹配表达式与e为x取代的类型的索引中的return子句的类型。该变量e的类型为a = b，索引为b，因此得到的类型为b = a（即，x = a，其中b代替x）。

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