引入假设的战术，然后立即对其采取另一种策略

Question

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

谢谢。

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教程对于初学者来说非常舒适。