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：true-> true）。再帰性。H2にHを適用します。

assert (H2 := H (eq_refl true)).また動作します。私はまだよりクリーンなソリューションについて知りたいです。