coq - 引入假设然后立即对其执行另一种策略的策略

Question

当我的证明状态是这种形式时， H -> goal 我经常使用 intros H. *some tactic* H. 一些策略可能是“反转”或“应用 _ in”等的模式。如果有一些策略将这两个步骤结合起来会很好，即引入最高假设，然后对其应用特定的策略。我在 ssreflect 文档中查看了 move，因为 move 可以做类似的有用的事情，但没有找到任何东西。有这样的战术吗？

谢谢。

Answer 1

如前所述 ssreflect 可以移动变量，例如使用 ssreflect 如果变量位于堆栈顶部，您甚至不需要引入变量。

Lemma blah : H -> Goal                  Lemma blah : H -> Goal 
intro H. induction H.           ~       elim.

Lemma blahh : P -> H -> Goal            Lemma blah : P -> H -> Goal 
intros P H. induction H.         ~      move=> P; elim. or shorten intros;elim : H.
intro P H. apply P in H.         ~      apply : P.

我推荐一个 ssreflect 教程对初学者来说很舒服。