Блог

Я формулирую следующую цель в 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
  

Является ли это стандартной тактикой в такой ситуации? Или есть более простой способ?

 e (FIRST_ASSUM ACCEPT_TAC)
  

делает это.

FIRST_ASSUM применяет тактику теоремы аргументации к предположениям до достижения успеха.

ACCEPT_TAC цель просто доказывается, если мы приводим ту же теорему.

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

(спасибо кому-то на #hol)