用 HOL 中的假设证明目标答案

【问题标题】：Prove a goal with an assumption in HOL用 HOL 中的假设证明目标
【发布时间】：2019-03-28 14:21:22
【问题描述】：

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

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

【问题讨论】：

标签： theorem-proving hol

【解决方案1】：

e (FIRST_ASSUM ACCEPT_TAC)

会的。

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

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

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

（感谢#hol 上的某个人）

【讨论】：