coq - 在 Coq 中丢弃重言式前提

Question

我在本地上下文中有一个假设，我们称其H为true=true -> conclusion. 我可以使用哪种策略来放弃前提而只保留结论？

Answer 1

这将前提断言为子目标，然后尝试使用琐碎的策略来证明它以及带有 H 的结论的原始目标。

lapply H; trivial.

Answer 2

使用specialize策略：http ://coq.inria.fr/doc/Reference-Manual011.html#@tactic35

specialize (H (eq_refl true)).

Answer 3

我想出了以下内容。这些工作中的任何一个：

断言（H2：结论）。应用 H. 自反性。

断言（H2：真->真）。反身性。在 H2 中应用 H。

assert (H2 := H (eq_refl true)).也有效。我仍然想了解更清洁的解决方案。