Докажите цель с предположением в HOL - PullRequest
Новая
       14

Докажите цель с предположением в HOL

1 голос
/ 28 марта 2019

Я ставлю следующую цель в 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

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

1 Ответ

1 голос
/ 28 марта 2019 
e (FIRST_ASSUM ACCEPT_TAC)

делает это.

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

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

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

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

...