Coq项目1.2.10类型转换

Question

不确定Coq手册v8.7.0第1.2.10项中的以下含义:

• 表达式" term:type "是一种类型转换表达式.它强制使用术语类型作为类型.
• " term <:type "在本地设置虚拟机以检查该术语是否具有类型类型.

我的理解是第一个的类型检查是由Coq(某些默认值)完成的,而第二个是由选择的Coq的VM(可能有不同的输入规则)完成的.

我尝试使用以下示例,并且看不出它们的错误消息有任何区别

Check (3 : bool). (* Error: The term "3" has type "nat" while it is expected to have type "bool".*)
Check (3 <: bool). (* same as above*)

我的问题是:可能是默认情况和VM行为相同的情况？

此外,如果有一个":"和"<:"表现不同的例子会很不错,所以人们可能会更加小心地从另一个中选择一个.

Answer 1

据我所知,默认的还原机制和VM减少机制旨在强制执行相同的打字规则.

但是,对于某些计算,验证时间可能具有不同的数量级,因此它们的行为不同.

这是一个例子

Time Check (refl_equal 1 : (10 ^ 200 - 9 * 10 ^ 199) / 10 ^ 199 = 1).
...
Finished transaction in 0.103  secs ...

Time Check (refl_equal 1 <: (10 ^ 200 - 9 * 10 ^ 199) / 10 ^ 199 = 1).
...
Finished transaction in 0.053 secs

这很重要,因为在证明的中间可能会发生大量计算.