我对以下h定义中证据术语的匹配部分的Coq类型系统的行为感到困惑:
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,a = b - > b = a".
由于H的类型是x = y,由于return子句,匹配将返回类型为b = y - > b = x的项.应用后面的各种术语后,我们得到h的预期类型.
然而,乐趣HC0:b = x => HC0是类型b = x - > b = x的同一性函数.我不认为有任何强制会迫使b = x - > b = x被识别为b = y - > b = x.
我最好的猜测是H的构造函数,即x = x的@eq_refl nat x,是唯一的.由于H也是x = y类型,因此名称x和y绑定到相同的术语.因此,类型系统决定b = x - > b = x的类型为b = y - > b = x.这很接近吗？这种行为是在某处解释或记录的吗？我看了iota减少,但我不认为这是正确的.
这就是它.记录了这种行为(在手册中查找"匹配...与......结构" ),虽然理解那里发生的事情可能有点令人生畏.
首先,回想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:
Inductive eq (T : Type) (x : T) : T -> Prop :=
| eq_refl : eq T x x.
(=符号只是中缀语法糖eq.)
对于结肠右侧的归纳类型的论证在Coq中是特殊的:它们被称为指数.出现在左边的那些(在这种情况下,T和x)被称为参数.参数在归纳类型的声明中必须全部不同,并且必须与所有构造函数的结果中使用的参数完全匹配.例如,请考虑以下非法代码段:
Inductive eq' (T : Type) (x : T) : T -> Type :=
| eq_refl' : eq nat 4 3.
Coq拒绝这个例子,因为它找到的nat不是构造函数T的结果eq_refl'.
另一方面,索引没有此限制:出现在构造函数的返回类型上的索引可以是适当类型的任何表达式.此外,该表达式可能因我们所在的构造函数而异.因此,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检查了所有分支都是正确的,它为整个匹配表达式分配了return带有e被替换类型的索引的子句的类型x.此变量e具有类型a = b,索引是b,因而所得到的类型是b = a(即,x = a与b取代x).
这个答案提供了关于参数和指数之间差异的更多解释,如果这有帮助的话.