在 Coq 中，术语“?T@{x:=t}”或带有问号和 at 符号的类型是什么意思？

Question

我正在尝试编写一个从列表中删除零的函数。这是我实现的第一次尝试。

Require Import Nat.
Require Import List.
Fixpoint shrink (x : list nat) list nat := (* Mistake! Needs a : list nat *)
  match x with
  | nil    => nil
  | h :: t => if h =? 0 then shrink t else (h :: shrink t)
  end.

但是，我得到这个错误：

Error:
In environment
shrink : forall (x : Datatypes.list Datatypes.nat) 
           (list0 : ?T) (nat : ?T0@{list:=list0}),
         Datatypes.list ?T1@{x:=x; list:=list0; x1:=x}
x : list nat
list : ?T
nat : ?T0
h : Datatypes.nat
t : Datatypes.list Datatypes.nat
The term "shrink t" has type
 "forall (list0 : ?T@{x:=t}) (nat : ?T0@{x:=t; list:=list0}),
  Datatypes.list ?T1@{x:=t; list:=list0; x1:=t}"
while it is expected to have type "Datatypes.list ?T1@{x1:=h :: t}".

正确的函数实现是这样的：

Fixpoint shrink (x : list nat) : list nat :=
  match x with
  | nil    => nil
  | h :: t => if h =? 0 then shrink t else (h :: shrink t)
  end.

但是我应该如何解释错误，尤其是 (list0 : ?T@{x:=t})？特别是，

为什么是 list0 而不是 list？
? 前面的 T 是什么意思？
T后面的@{ ... }是什么意思？

Answer 1

对于你的第一点，这只是一个打印的东西，但本质上局部变量名称只是 Coq 的提示，它可能不会尊重它们以避免混淆。这里可能是因为后面看到的list := list0

?前面的字母是存在变量或evar，用于统一。它不知道 list0 的类型应该是什么，因为你没有给出任何类型，但它知道它必须是 something。所以现在它是?T，稍后它会通过查看它的用途来尝试弄清楚它应该是什么。

对于 nat 它是相同的，但它也知道它可能依赖于某些 list 并且在这种情况下它的值应该是 list0 所以它会实例化 ?T0{list:=list0}.此符号用于 evars 中的替换。

我邀请您查看documentation of evars in the manual以了解更多信息。

在 Coq 中，术语“?T@{x:=t}”或带有问号和 at 符号的类型是什么意思？

What does the term "?T@{x:=t}", or a type with a question mark and at sign surrounding it mean in Coq?

coq