时间戳

首页 > 解决方案 > 用 HOL 中的假设证明目标

theorem-proving - 用 HOL 中的假设证明目标

问题描述

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

解决方案

e (FIRST_ASSUM ACCEPT_TAC)

可以。

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

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

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

（感谢#hol上的某人）

推荐阅读