小编Zhe*_*eng的帖子

假设采用战术有子目标清单T：

______________________________________(1/10)
A
______________________________________(2/10)
A'
______________________________________(3/10)
A''

并且假设我们知道引理L可以用来证明A，A''但不能 A'。

我的问题是，我们是否可以T根据的应用结果进行测序，而结果L只剩下一个子目标A'？

我尝试T;apply L.没有成功，因为排序似乎需要所有分支/子目标都经过证明。

我还通过使用by T;apply L.SSReflect 尝试了受控自动化，这是本文的建议。不幸的是，Coq也陷入困境，并报告Ltac calls to ... last call failed.

不确定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行为相同的情况？

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