8.1 The goalstack (1)
前回述べたように，HOL Lightでは，goalの集まりであるgoalstackを用いて対話的に証明が作成できます．具体的には，*_TAC の名前を持つ，tactic（戦略関数) を，必要に応じてやり直し・訂正を加えながら，goalstackに段階的に適用することで，その中にある自明でないgoalを消していくわけです．
まず，g (goal) 関数(: term -> goalstack =
# g ( `2 <= n /\ n <= 2 ==> f(2,2) + n < f(n,n) + 7` );;
Warning: Free variables in goal: f, n
val it : goalstack = 1 subgoal (1 total)`2 <= n /\ n <= 2 ==> f (2,2) + n < f (n,n) + 7`
これで改めて g を使うまで，このtermが証明の対象として固定されました．1 subgoal (1 total) は，今表示しているsubgoalの個数，および，表示していないものも含めたsubgoalの個数を表しています．
以下，e (expand) 関数(: tactic -> goalstack =
とりあえず，p==>q の形なので，|- p==>q から p |- q に上る（証明では下る）tactic である DISCH_TAC (discharge) を用いてみます．
# e ( DISCH_TAC );;
val it : goalstack = 1 subgoal (1 total)0 [`2 <= n /\ n <= 2`]
`f (2,2) + n < f (n,n) + 7`
いわゆる証明論を知っていれば，この書式からHOL Lightは自然演繹に基づくシステムであり，今の処理は，最後に落ちる仮定を復元するステップだとわかるでしょう．
しかし，よく見ると（笑），まず前件を等式にconvした方が良さそうですから，ワンステップ下り，元に戻しましょう．それには，b() ( back up ) 関数を用いて
# b();;
val it : goalstack = 1 subgoal (1 total)`2 <= n /\ n <= 2 ==> f (2,2) + n < f (n,n) + 7`
とします．
で，conversion から，それをsubgoalに適用する tactic を生成する CONV_TAC という関数(: conv -> tactic =
# search[ `a<=b /\ b<=a` ];;
val it : (string * thm) list =
[("LE_ANTISYM", |- !m n. m <= n /\ n <= m <=> m = n)]
がありますので，これをREWRITE_CONVで参照するtactic CONV_TAC ( REWRITE_CONV [LE_ANTISYM] ) を e で評価してみると
# e ( CONV_TAC ( REWRITE_CONV [LE_ANTISYM] ) );;
val it : goalstack = 1 subgoal (1 total)`2 = n ==> f (2,2) + n < f (n,n) + 7`
となります．
この利用法はよくあるので (CONV_TAC o REWRITE_CONV) は REWRITE_TAC(: thm list -> tactic =
# b();;
val it : goalstack = 1 subgoal (1 total)`2 <= n /\ n <= 2 ==> f (2,2) + n < f (n,n) + 7`
# e ( REWRITE_TAC [LE_ANTISYM] ) ;;
val it : goalstack = 1 subgoal (1 total)`2 = n ==> f (2,2) + n < f (n,n) + 7`
ともできます．
次に，2とnが等しいことから，f(2,2)とf(n,n)も等しいことを示します．それには先のDISCH_TACにより`2=n`を仮定にまわし，仮定を参照に加えるASM_REWRITE_TAC(: thm list -> tactic =
# e ( DISCH_TAC ) ;;
val it : goalstack = 1 subgoal (1 total)0 [`2 = n`]
`f (2,2) + n < f (n,n) + 7`
# e ( ASM_REWRITE_TAC [] ) ;;
val it : goalstack = 1 subgoal (1 total)0 [`2 = n`]
`f (n,n) + n < f (n,n) + 7`
おっと，可笑しなsubgoalが出てきましたね．お判りのように，仮定は`2=n`なので，subgoalの全ての2がnに書き換えられてしまったのです．
ということで，２ステップ下って
# b();;
val it : goalstack = 1 subgoal (1 total)0 [`2 = n`]
`f (2,2) + n < f (n,n) + 7`
# b();;
val it : goalstack = 1 subgoal (1 total)`2 = n ==> f (2,2) + n < f (n,n) + 7`
とし，`2=n`を`n=2`にrewriteしましょう．
# search[ `a=b <=> b=a` ];;
Warning: inventing type variables
val it : (string * thm) list = [("EQ_SYM_EQ", |- !x y. x = y <=> y = x)]
# e ( REWRITE_TAC [EQ_SYM_EQ] );;
val it : goalstack = 1 subgoal (1 total)`n = 2 ==> f (2,2) + n < f (n,n) + 7`
そして先ほどと同じく
# e ( DISCH_TAC ) ;;
val it : goalstack = 1 subgoal (1 total)0 [`n = 2`]
`f (2,2) + n < f (n,n) + 7`
# e ( ASM_REWRITE_TAC[] ) ;;
val it : goalstack = 1 subgoal (1 total)0 [`n = 2`]
`f (2,2) + 2 < f (2,2) + 7`
このsubgoalをARITH_RULEで証明できれば，結果がtrueとなり，証明全体も完成します．
ところが，ARITH_RULEは，tmを受け取り|- tmを返す，proverなので，まず
(EQT_INTRO o ARITH_RULE)
のように，|- tm =(<=>) tm'を返す，conversionにして，CONV_TACに渡さなくてはなりません．
ところが有難いことに，CONV_TACは，proverにも適用可能であり
# e ( CONV_TAC ( ARITH_RULE ) ) ;;
val it : goalstack = No subgoals
となり，このCONV_TAC (ARITH_RULE) は ARITH_TAC としても定義されています．同様に，proverである MESON を CONV_TAC で tactic にしたMESON_TAC，更に仮定も参照する ASM_MESON_TAC[] もあります．
No subgoalsとは，示すべき目標が全て証明されて残っていません，つまり，証明完了ということです．得られたtheoremは
# top_thm();;
val it : thm = |- 2 <= n /\ n <= 2 ==> f (2,2) + n < f (n,n) + 7
のように参照できます．
なお，上記では，`n=2`を仮定にまわしましたが，subgoalの中で処理することもできます．
...
`2 <= n /\ n <= 2 ==> f (2,2) + n < f (n,n) + 7`# e ( SIMP_TAC [ LE_ANTISYM ; EQ_SYM_EQ ] );;
val it : goalstack = 1 subgoal (1 total)`n = 2 ==> f (2,2) + 2 < f (2,2) + 7`
このSIMP_TAC(: thm list -> tactic =
以上を一気に書くと
g ( `2 <= n /\ n <= 2 ==> f (2,2) + n < f (n,n) + 7` );;
e ( SIMP_TAC [ LE_ANTISYM ; EQ_SYM_EQ ] );;
e ( ARITH_TAC );;
let th1 = top_thm();;
となり，これは，e 関数の tactics は THEN により一つの tactic に結合して
g ( `2 <= n /\ n <= 2 ==> f (2,2) + n < f (n,n) + 7` );;
e ( SIMP_TAC [ LE_ANTISYM ; EQ_SYM_EQ ] THEN
ARITH_TAC );;
let th1 = top_thm();;
ともできます．この書式は単なる略記ではなく，各tacticを複数のsubgoalの全てに作用させる働きがあります．また，THENのようにtacticを返す関数を一般にtacticalといい，conversionに対するconversionalと同じ位置付けになります．
更に prove(: term * tactic -> thm =
# let th1 = prove( `2 <= n /\ n <= 2 ==> f (2,2) + n < f (n,n) + 7` , SIMP_TAC [ LE_ANTISYM ; EQ_SYM_EQ ] THEN ARITH_TAC );;
val th1 : thm = |- 2 <= n /\ n <= 2 ==> f (2,2) + n < f (n,n) + 7
ともできます．
