为什么Coq不能统一目标和假设？

Question

经过一番练习，我达到了以下证明状态。

(尾巴1是一个nat列表模式生成器, lng 笼统的)

1 subgoal
n' : nat
IH_n' : forall lng : nat, lng > n' -> nth n' (update (tail1 lng) 0 1) 9 = 1
lng : nat
H : S lng > S n'
______________________________________(1/1)
nth (S n') (update (tail1 (S lng)) 0 1) 9 = 1

使用 apply IH_n' 失败，出现以下错误。

无法将 "nth n'(update (tail1 ?M1305) 0 1) 9 = 1 "与 "nth (S n') (update (tail1 (S lng))0 1) 9 = 1 "统一起来。

• 是否是......是......是......是......是......是......是......是......是......是......是......是......是......是......是......是......是......是......是......是......是.......是......是......是......是.......是......"。?M1305 - (S lng) 不能统一的对?
• 什么是 ?M1305 究竟是什么？
• 是否可以从这里继续前进？

Answer 1

这里的问题是，你正试图将一个假设应用于 n' 对于 S n'而n'在IH_n'中没有被量化。

只有当你的假设是，它才会有效。

IH_n' : forall n' lng : nat, lng > n' -> nth n' (update (tail1 lng) 0 1) 9 = 1

回答你的另一个问题： ?_ 是存在的变量，如果你的假设适用的话，这个变量就会被替换掉，因为变量lng在假设中被量化了。

如果你想得到一些关于如何证明这个目标的帮助，你可以分享一下代码吗？（尽管我认为你应该做 unfold nth, update; simpl 看看你是否能在某处应用你的假设。

Answer 2

假设 IH_n' 是普遍量化的 lng:nat. 要将其应用到目标上，Coq需要将其实例化。?M1305 的值的名称。lng 它还没有找到。

该错误信息不一定意味着 ?M1305 和 (S lng) 不能统一。问题可能来自于其他地方。例如，你的目标始于 nth (S n')，而假设的起点是 nth n'. 很明显 (S n') 和 n' 不能统一。

你的第一步，假设目标是可以证明的，就是要确保它的起点是 nth n'. 要做到这一点，你需要第二个参数，即 nth 拟为 (cons foo bar).