我在 HOL4 中陈述了以下目标:
set_goal([``A:bool``,``B:bool``], ``B:bool``);
导致证明状态
val it =
Proof manager status: 1 proof.
1. Incomplete goalstack:
Initial goal:
B
------------------------------------
0. B
1. A
: proofs
我试图找到使用这些假设的适当策略。我想出了ASM_MESON_TAC
:
e (mesonLib.ASM_MESON_TAC [])
它证明了目标:
OK..
Meson search level: ..
val it =
Initial goal proved.
[..] ⊢ B: proof
这是在这种情况下的标准策略吗?或者,有没有更简单的?