coq - `ssreflect` 的 `move=>` 的替代策略

Question

我喜欢在目标是暗示的情况下（例如 A -> B）使用库中的move=>策略ssreflect，以使前提成为假设，并使结论成为新目标。但是，我并不总是想使用ssreflect.

是否有另一种 Coq 策略可以在不使用 的情况下做同样的事情ssreflect？

Answer 1

您始终可以使用intros:intros pat大致相当于move=> pat. 不幸的是，Coq 和 ssreflect 对引入模式使用不同的语法，因此两者不可互换。

请注意，现在 ssreflect 是 Coq 发行版的一部分，因此您可以通过简单地使用策略语言From Coq Require Import ssreflect.，而无需安装单独的库。