8.1 The goalstack (2)

　今回は，量化，論理結合，対称式を含んだ

# g `!x y:real. &0 < x * y ==> (&0 < x <=> &0 < y)`;;
val it : goalstack = 1 subgoal (1 total)

`!x y. &0 < x * y ==> (&0 < x <=> &0 < y)`

を場合分けを用いて証明します．なお，証明自体は，REAL_FIELDでは

# REAL_FIELD `!x y. &0 < x*y ==> (&0 &0

と失敗しますが，MESONに

# REAL_LT_MUL_EQ;;
val it : thm =
|- (!x y. &0 < x ==> (&0 < x * y <=> &0 < y)) /\
(!x y. &0 < y ==> (&0 < x * y <=> &0 < x))

（探し方は後述）を参照させると

# MESON [REAL_LT_MUL_EQ] `!x y. &0 < x*y ==> (&0 &0 (&0 < y <=> &0 < x)

のように処理してくれます．

　ではまず，可能な限り繰り返しの tactic を生成する REPEAT(: tactic -> tactic = ) で，全称量化除去（下向きなら導入）の tactic GEN_TAC を評価して e で展開すると

# e ( REPEAT GEN_TAC );;
val it : goalstack = 1 subgoal (1 total)

`&0 < x * y ==> (&0 < x <=> &0 < y)`

なので，前件を仮定にまわすと

# e ( DISCH_TAC );;
val it : goalstack = 1 subgoal (1 total)

0 [`&0 < x * y`]

`&0 < x <=> &0 < y`

となります．なお，STRIP_TAC は subgoalの形に応じて，GEN_TAC，CONJ_TAC(連言の分解)，DISCH_TAC を実行しますので，次のようにもできます．

...
`!x y. &0 < x * y ==> (&0 < x <=> &0 < y)`
# e ( REPEAT STRIP_TAC );;
val it : goalstack = 1 subgoal (1 total)

0 [`&0 < x * y`]

`&0 < x <=> &0 < y`

　次に，EQ_TAC で equivalent を2つの implies に分解します．

# e ( EQ_TAC ) ;;
val it : goalstack = 2 subgoals (2 total)

0 [`&0 < x * y`]

`&0 < y ==> &0 < x`

0 [`&0 < x * y`]

`&0 < x ==> &0 < y`

　subgoalsが2個になりましたが，e 関数は，表示されている最も下のsubgoalに対して作用しますので，その証明を考えましょう．
　普通ならy=(x*y)/xですが，今回は場合分けの紹介なので，yの符号についての場合分けで行きます．つまり

# REAL_ARITH `&0 < y \/ &0 <= --y`;;
val it : thm = |- &0 < y \/ &0 <= --y

というtheoremを，theoremを引数に取るtheorem tacticである，場合分けの DISJ_CASES_TAC(: thm_tactic = )に与えて，分解すると

# e ( DISJ_CASES_TAC ( REAL_ARITH `&0 < y \/ &0 <= --y` ) );;
val it : goalstack = 2 subgoals (3 total)

0 [`&0 < x * y`]
1 [`&0 <= --y`]

`&0 < x ==> &0 < y`

0 [`&0 < x * y`]
1 [`&0 < y`]

`&0 < x ==> &0 < y`

となりますが，下側の結論はその仮定より直ちに得られるので

# e ( ASM_REWRITE_TAC[] ) ;;
val it : goalstack = 1 subgoal (2 total)

0 [`&0 < x * y`]
1 [`&0 <= --y`]

`&0 < x ==> &0 < y`

に絞れます．
　ところが，仮定の`&0 <= --y`から結論の後件`&0 < y`を得るのはどう見ても無理です．困りましたね（笑）．
　お判りのように，この２つの仮定と結論の前件の連言は F なので，任意の p に対して |- F ==> p という話で，普通に言えば「この場合は起こり得ないので」ということです．
　実際に連言が F であることを示すには

# TAUT `( p ==> ( q ==> r ) ) <=> ( ( p /\ q ) ==> r )` ;;
val it : thm = |- p ==> q ==> r <=> p /\ q ==> r

および，==> が右結合であることから

p1 ==> p2 ==> ... ==> pn ==> q(n+1)

が

( p1 /\ p2 /\ ... /\ pn ) ==> q(n+1)

と等価であることに注意しながら，`&0q と B |- p に遡る MP_TAC(: thm_tactic = )を用いるわけですが，このMP_TACは，既存のtheorem B |- p を引数にとる theorem-tactic と呼ばれるもので，証明図の分解・結合を実現するタイプです．ここで，B は {B}⊆(現在の goalstack の仮定の集合) を満たすものであればよく，空（つまりpが定理）である必要はないことに注意します．

# e ( MP_TAC (ASSUME`&0<= --y`) );;
val it : goalstack = 1 subgoal (2 total)

0 [`&0 < x * y`]
1 [`&0 <= --y`]

`&0 <= --y ==> &0 < x ==> &0 < y`

# e ( MP_TAC (ASSUME`&0 &0 <= --y ==> &0 < x ==> &0 < y`

# e( MP_TAC ( SPECL [ `x:real` ; `--y` ] REAL_LE_MUL ) ) ;;
val it : goalstack = 1 subgoal (2 total)

0 [`&0 < x * y`]
1 [`&0 <= --y`]

`(&0 <= x /\ &0 <= --y ==> &0 <= x * --y)
==> &0 < x * y
==> &0 <= --y
==> &0 < x
==> &0 < y`

# e( MP_TAC ( REAL_ARITH `&0 &0<=x` ) ) ;;
val it : goalstack = 1 subgoal (2 total)

0 [`&0 < x * y`]
1 [`&0 <= --y`]

`(&0 < x ==> &0 <= x)
==> (&0 <= x /\ &0 <= --y ==> &0 <= x * --y)
==> &0 < x * y
==> &0 <= --y
==> &0 < x
==> &0 < y`

# e( MP_TAC ( REAL_ARITH `&0 ~(&0<=x*(--y))` ) ) ;;
val it : goalstack = 1 subgoal (2 total)

0 [`&0 < x * y`]
1 [`&0 <= --y`]

`(&0 < x * y ==> ~(&0 <= x * --y))
==> (&0 < x ==> &0 <= x)
==> (&0 <= x /\ &0 <= --y ==> &0 <= x * --y)
==> &0 < x * y
==> &0 <= --y
==> &0 < x
==> &0 < y`

　これで結論の &0

# e ( MESON_TAC [] );;
0..0..solved at 2
0..0..solved at 3
0..0..solved at 2
0..0..solved at 3
0..0..solved at 2
0..0..solved at 3
0..0..solved at 2
0..0..solved at 3
0..0..solved at 2
0..0..solved at 2
0..0..solved at 2
0..0..solved at 2
val it : goalstack = 1 subgoal (1 total)

0 [`&0 < x * y`]

`&0 < y ==> &0 < x`

　上のtheorem REAL_LE_MULを見つけるには，search(: term list -> (string * thm) list = )コマンドを使って，`&0<=x`と`&0<=x*y`（変数は自動的に置きかえられる）を含むtheoremを探せばよく

# search[ `&0<=x` ; `&0<=x*y` ];;
val it : (string * thm) list =
[("REAL_LE_MUL", |- !x y. &0 <= x /\ &0 <= y ==> &0 <= x * y);
("REAL_LE_MUL_EQ",
|- (!x y. &0 < x ==> (&0 <= x * y <=> &0 <= y)) /\
(!x y. &0 < y ==> (&0 <= x * y <=> &0 <= x)));
("REAL_LE_SQUARE", |- !x. &0 <= x * x);
("REAL_MUL_POS_LE",
|- !x y.
&0 <= x * y <=>
x = &0 \/ y = &0 \/ &0 < x /\ &0 < y \/ x < &0 /\ y < &0)]

引数のリストの要素は，name"theoremの名前の一部"や omit`除外するterm` も使えます．