Coq 项目 1.2.10 类型转换
Coq item 1.2.10 Type cast
不确定以下在 Coq 手册 v8.7.0 中的含义 item 1.2.10:
- 表达式“term : type”是一个类型转换表达式。它强制 term 的类型为 type.
- “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 行为相同的情况吗？
此外，最好有一个示例，其中“:”和“<:”的行为不同，这样人们可以更加谨慎地从另一个中选择一个。
据我所知，默认缩减机制和 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
这很重要，因为在证明过程中可能会发生大量计算。
不确定以下在 Coq 手册 v8.7.0 中的含义 item 1.2.10:
- 表达式“term : type”是一个类型转换表达式。它强制 term 的类型为 type.
- “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 行为相同的情况吗？
此外，最好有一个示例，其中“:”和“<:”的行为不同，这样人们可以更加谨慎地从另一个中选择一个。
据我所知，默认缩减机制和 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
这很重要，因为在证明过程中可能会发生大量计算。