Tactician

　HOL Light の g コマンドによる証明と prove コマンドによる証明との変換ツール Tactician のご紹介です．

http://www.proof-technologies.com/tactician/index.html

　使い方は簡単で，HOL Light のディレクトリに

http://www.proof-technologies.com/tactician/hollight_tactician-2.2.tgz

を解凍して

#use "Tactician/main.ml";;

とロードして

promote_ml_values ();;

と初期化，何か証明した後にtop_thmの証明を表示するには

print_executed_proof ();;

それをTHENを用いない形に変換したものを表示するには

print_flat_proof ();;

それを１つのtacticにしたもの（つまり，proveタイプ）を表示するには

print_thenl_proof ();;

更にALL_TACを用いてTHENLのネストを避けたものを表示するには

print_packaged_proof ();;

とするだけです（なお，これをロードすると search が使えません）．

　例えば．．．

g `!a b s t. &0 <= a ==> &0 <= b ==> &0 <= s ==> &0 <= t ==> s + t = &1 ==> !n. (s * a + t * b) pow n <= s * a pow n + t * b pow n` ;;
e( REPEAT GEN_TAC THEN REPEAT DISCH_TAC THEN INDUCT_TAC );;
e( SIMP_TAC [pow] THEN ASM_REAL_ARITH_TAC );;
e( SIMP_TAC [pow] );;
e( MATCH_MP_TAC REAL_LE_TRANS );;
e( EXISTS_TAC `(s * a + t * b) * (s * a pow n + t * b pow n)` );;
e( CONJ_TAC );;
e( ASM_SIMP_TAC [REAL_LE_ADD;REAL_LE_MUL;REAL_LE_LMUL] );;
e( ONCE_REWRITE_TAC [GSYM REAL_SUB_LE] );;
e( SIMP_TAC [UNDISCH(REAL_FIELD`s + t = &1 ==> (s * a * x + t * b * y) - (s * a + t * b) * (s * x + t * y) = (s * t) * (a - b) * (x - y)`)] );;
e( MATCH_MP_TAC REAL_LE_MUL );;
e( CONJ_TAC );;
e( ASM_SIMP_TAC [REAL_LE_MUL] );;
e( DISJ_CASES_THEN ASSUME_TAC (SPECL[`a:real`;`b:real`]REAL_LE_TOTAL) );;
e( ONCE_REWRITE_TAC [GSYM REAL_NEG_MUL2] THEN SIMP_TAC [REAL_NEG_SUB] );;
e( ASM_SIMP_TAC [REAL_LE_MUL;REAL_SUB_LE;POW_LE] );;
e( ASM_SIMP_TAC [REAL_LE_MUL;REAL_SUB_LE;POW_LE] );;

に対しては

# print_executed_proof ();;

g `!a b s t. &0 <= a ==> &0 <= b ==> &0 <= s ==> &0 <= t ==> s + t = &1 ==> !n. (s * a + t * b) pow n <= s * a pow n + t * b pow n`;;
e (REPEAT GEN_TAC THEN REPEAT DISCH_TAC THEN INDUCT_TAC);;
(* *** Subgoal 1 *** *)
e (SIMP_TAC [pow] THEN ASM_REAL_ARITH_TAC);;
(* *** Subgoal 2 *** *)
e (SIMP_TAC [pow]);;
e (MATCH_MP_TAC REAL_LE_TRANS);;
e (EXISTS_TAC `(s * a + t * b) * (s * a pow n + t * b pow n)`);;
e (CONJ_TAC);;
(* *** Subgoal 2.1 *** *)
e (ASM_SIMP_TAC [REAL_LE_ADD; REAL_LE_MUL; REAL_LE_LMUL]);;
(* *** Subgoal 2.2 *** *)
e (ONCE_REWRITE_TAC [GSYM REAL_SUB_LE]);;
e (SIMP_TAC
     [UNDISCH
        (REAL_FIELD
           `s + t = &1 ==> (s * a * x + t * b * y) - (s * a + t * b) * (s * x + t * y) = (s * t) * (a - b) * (x - y)`)]);;
e (MATCH_MP_TAC REAL_LE_MUL);;
e (CONJ_TAC);;
(* *** Subgoal 2.2.1 *** *)
e (ASM_SIMP_TAC [REAL_LE_MUL]);;
(* *** Subgoal 2.2.2 *** *)
e (DISJ_CASES_THEN ASSUME_TAC (SPECL [`a:real`; `b:real`] REAL_LE_TOTAL));;
(* *** Subgoal 2.2.2.1 *** *)
e (ONCE_REWRITE_TAC [GSYM REAL_NEG_MUL2] THEN SIMP_TAC [REAL_NEG_SUB]);;
e (ASM_SIMP_TAC [REAL_LE_MUL; REAL_SUB_LE; POW_LE]);;
(* *** Subgoal 2.2.2.2 *** *)
e (ASM_SIMP_TAC [REAL_LE_MUL; REAL_SUB_LE; POW_LE]);;

val it : unit = ()
# print_flat_proof ();;

g `!a b s t. &0 <= a ==> &0 <= b ==> &0 <= s ==> &0 <= t ==> s + t = &1 ==> !n. (s * a + t * b) pow n <= s * a pow n + t * b pow n`;;
e (REPEAT GEN_TAC);;
e (REPEAT DISCH_TAC);;
e (INDUCT_TAC);;
(* *** Subgoal 1 *** *)
e (SIMP_TAC [pow]);;
e (ASM_REAL_ARITH_TAC);;
(* *** Subgoal 2 *** *)
e (SIMP_TAC [pow]);;
e (MATCH_MP_TAC REAL_LE_TRANS);;
e (EXISTS_TAC `(s * a + t * b) * (s * a pow n + t * b pow n)`);;
e (CONJ_TAC);;
(* *** Subgoal 2.1 *** *)
e (ASM_SIMP_TAC [REAL_LE_ADD; REAL_LE_MUL; REAL_LE_LMUL]);;
(* *** Subgoal 2.2 *** *)
e (ONCE_REWRITE_TAC [GSYM REAL_SUB_LE]);;
e (SIMP_TAC
     [UNDISCH
        (REAL_FIELD
           `s + t = &1 ==> (s * a * x + t * b * y) - (s * a + t * b) * (s * x + t * y) = (s * t) * (a - b) * (x - y)`)]);;
e (MATCH_MP_TAC REAL_LE_MUL);;
e (CONJ_TAC);;
(* *** Subgoal 2.2.1 *** *)
e (ASM_SIMP_TAC [REAL_LE_MUL]);;
(* *** Subgoal 2.2.2 *** *)
e (DISJ_CASES_THEN ASSUME_TAC (SPECL [`a:real`; `b:real`] REAL_LE_TOTAL));;
(* *** Subgoal 2.2.2.1 *** *)
e (ONCE_REWRITE_TAC [GSYM REAL_NEG_MUL2]);;
e (SIMP_TAC [REAL_NEG_SUB]);;
e (ASM_SIMP_TAC [REAL_LE_MUL; REAL_SUB_LE; POW_LE]);;
(* *** Subgoal 2.2.2.2 *** *)
e (ASM_SIMP_TAC [REAL_LE_MUL; REAL_SUB_LE; POW_LE]);;

val it : unit = ()
# print_thenl_proof ();;

prove
 (`!a b s t. &0 <= a ==> &0 <= b ==> &0 <= s ==> &0 <= t ==> s + t = &1 ==> !n. (s * a + t * b) pow n <= s * a pow n + t * b pow n`,
  REPEAT GEN_TAC THEN
  (REPEAT DISCH_TAC THEN
   (INDUCT_TAC THENL
     [SIMP_TAC [pow] THEN ASM_REAL_ARITH_TAC;
      SIMP_TAC [pow] THEN
      (MATCH_MP_TAC REAL_LE_TRANS THEN
       (EXISTS_TAC `(s * a + t * b) * (s * a pow n + t * b pow n)` THEN
        (CONJ_TAC THENL
          [ASM_SIMP_TAC [REAL_LE_ADD; REAL_LE_MUL; REAL_LE_LMUL];
           ONCE_REWRITE_TAC [GSYM REAL_SUB_LE] THEN
           (SIMP_TAC
              [UNDISCH
                 (REAL_FIELD
                    `s + t = &1 ==> (s * a * x + t * b * y) - (s * a + t * b) * (s * x + t * y) = (s * t) * (a - b) * (x - y)`)] THEN
            (MATCH_MP_TAC REAL_LE_MUL THEN
             (CONJ_TAC THENL
               [ASM_SIMP_TAC [REAL_LE_MUL];
                DISJ_CASES_THEN ASSUME_TAC
                  (SPECL [`a:real`; `b:real`] REAL_LE_TOTAL) THENL
                 [ONCE_REWRITE_TAC [GSYM REAL_NEG_MUL2] THEN
                  (SIMP_TAC [REAL_NEG_SUB] THEN
                   ASM_SIMP_TAC [REAL_LE_MUL; REAL_SUB_LE; POW_LE]);
                  ASM_SIMP_TAC [REAL_LE_MUL; REAL_SUB_LE; POW_LE]]])))])))])));;

val it : unit = ()
# print_packaged_proof ();;

prove
 (`!a b s t. &0 <= a ==> &0 <= b ==> &0 <= s ==> &0 <= t ==> s + t = &1 ==> !n. (s * a + t * b) pow n <= s * a pow n + t * b pow n`,
  REPEAT GEN_TAC THEN REPEAT DISCH_TAC THEN INDUCT_TAC THEN SIMP_TAC [pow] THENL
   [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
  MATCH_MP_TAC REAL_LE_TRANS THEN
  EXISTS_TAC `(s * a + t * b) * (s * a pow n + t * b pow n)` THEN CONJ_TAC THENL
   [ASM_SIMP_TAC [REAL_LE_ADD; REAL_LE_MUL; REAL_LE_LMUL]; ALL_TAC] THEN
  ONCE_REWRITE_TAC [GSYM REAL_SUB_LE] THEN
  SIMP_TAC
    [UNDISCH
       (REAL_FIELD
          `s + t = &1 ==> (s * a * x + t * b * y) - (s * a + t * b) * (s * x + t * y) = (s * t) * (a - b) * (x - y)`)] THEN
  MATCH_MP_TAC REAL_LE_MUL THEN CONJ_TAC THENL
   [ASM_SIMP_TAC [REAL_LE_MUL]; ALL_TAC] THEN
  DISJ_CASES_THEN ASSUME_TAC (SPECL [`a:real`; `b:real`] REAL_LE_TOTAL) THENL
   [ONCE_REWRITE_TAC [GSYM REAL_NEG_MUL2] THEN SIMP_TAC [REAL_NEG_SUB];
    ALL_TAC] THEN
  ASM_SIMP_TAC [REAL_LE_MUL; REAL_SUB_LE; POW_LE]);;

val it : unit = ()

となります．

　実のところ g タイプから prove タイプへの変換だけなら難しくなく，私もエディターのマクロで実装していますが，このツールは証明の構造を分析しており，非常に柔軟な処理が可能となっています．なお，print_thenl_proof は何故か上記のサイトで紹介されていません．また，より簡潔にした print_optimal_proof は http://proofgeneral.inf.ed.ac.uk/releases/ProofGeneral-4.2/hol-light/TacticRecording/INSTRUCTIONS に生き残っています．