在HOL中用假设证明目标

Question

我在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

这是这种情况下的标准策略吗？或者，有没有更简单的方法？

Answer 1

e (FIRST_ASSUM ACCEPT_TAC)

就是这样。

FIRST_ASSUM在假设上应用论证定理策略，直到成功。

如果我们提供相同的定理，ACCEPT_TAC只是简单地证明了一个目标。

ACCEPT_TAC: thm -> tactic
FIRST_ASSUM: (thm -> tactic) -> tactic

(感谢#hol上的某人)