8.1 The goalstack (3)

　前回残した

...
val it : goalstack = 1 subgoal (1 total)

0 [`&0 < x * y`]

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

は，先のsubgoalのx,yを交換したものなので，同様に

# e ( DISJ_CASES_TAC ( REAL_ARITH `&0 &0 < x`

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

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

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

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

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

と展開すればよいのですが，ここからは少し手を代えてみましょう．
その１）前回は，仮定を前件にまわすために

e ( MP_TAC ( ASSUME `&0 < x * y` ) ) ;;
...

としましたが，前件に追加するtheoremsも仮定に加え，それらをまとめて前件にまわしてみます．

# e ( ASSUME_TAC ( REAL_ARITH `&0 &0<=y` ) );;
val it : goalstack = 1 subgoal (1 total)

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

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

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

0 [`&0 < x * y`]
1 [`&0 <= --x`]
2 [`&0 < y ==> &0 <= y`]
3 [`&0 <= --x /\ &0 <= y ==> &0 <= --x * y`]

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

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

0 [`&0 < x * y`]
1 [`&0 <= --x`]
2 [`&0 < y ==> &0 <= y`]
3 [`&0 <= --x /\ &0 <= y ==> &0 <= --x * y`]
4 [`&0 < x * y ==> ~(&0 <= --x * y)`]

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

そして，仮定の中で適用可能なものに theorem-tactic ttmを施し，その仮定を除去する(除去しない版は FIRST_ASSUM) tactic を生成する FIRST_X_ASSUM(: thm_tactic -> tactic = ) を繰り返し実行すれば

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

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

# e ( MESON_TAC [] );;
0..0..solved at 2
0..0..solved at 2
0..0..solved at 2
0..0..solved at 2
0..0..solved at 2
0..0..solved at 2
0..0..solved at 2
0..0..solved at 2
0..0..solved at 2
0..0..solved at 2
0..0..solved at 2
0..0..solved at 2
val it : goalstack = No subgoals

となります．
その２）最後のsubgoalもREAL_ARITH_TACで評価するなら

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

で十分なので，REAL_LE_MULのみをMP_TACで導入して

...
val it : goalstack = 1 subgoal (1 total)

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

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

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

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

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

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

# e ( REAL_ARITH_TAC ) ;;
val it : goalstack = No subgoals

つまり

...
val it : goalstack = 1 subgoal (1 total)

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

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

# e ( REPEAT ( FIRST_X_ASSUM MP_TAC ) THEN
MP_TAC ( SPECL [ `--x` ; `y:real` ] REAL_LE_MUL ) THEN REAL_ARITH_TAC
) ;;
val it : goalstack = No subgoals

ともできます．
その３）一般に

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

であり，&0<= --x は ~(&0

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

で良いわけです．さらに，==> の結合を明記すると，この式は

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

なので，initial goal の本体

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

の半分が

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

のみから得られることが判ります．これにより，場合分けを用いない全体の証明として

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

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

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

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

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

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

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

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

# e ( REAL_ARITH_TAC );;
val it : goalstack = No subgoals

まとめて

# prove ( `!x y. &0 < x * y ==> (&0 < x <=> &0 < y)` ,
( REPEAT GEN_TAC ) THEN
( MP_TAC ( SPECL [ `x:real` ; `--y` ] REAL_LE_MUL ) ) THEN
( MP_TAC ( SPECL [ `--x` ; `y:real` ] REAL_LE_MUL ) ) THEN
( REAL_ARITH_TAC ) );;
val it : thm = |- !x y. &0 < x * y ==> (&0 < x <=> &0 < y)

を得ます．