11.1 Irrationality of Sqrt[2]
今回は
# g( `!p q. p*p=2*q*q ==> q=0` );;
val it : goalstack = 1 subgoal (1 total)`!p q. p * p = 2 * q * q ==> q = 0`
をpについての wellfounded induction で証明します．方針は，p*p=2*q*qならばpは偶数，p=2r従って2*r*r=q*qと表せて仮定が使える，というものですが，一つ注意があります．それは，例えばp>0のときp*p=2*q*qからq=0が導けるのか？と言う点です．勿論導けませんが，それどころか以下の証明を見れば判るようにp*p=2*q*qからp=0が導けてしまうのです．つまり，今回のwellfounded inductionの利用は，積み上げが目的ではなく，p>0では不合理であることを示すためなのです．
# e ( MATCH_MP_TAC num_WF );;
val it : goalstack = 1 subgoal (1 total)`!p. (!m. m < p ==> (!q. m * m = 2 * q * q ==> q = 0))
==> (!q. p * p = 2 * q * q ==> q = 0)`
まず
# RIGHT_IMP_FORALL_THM;;
val it : thm = |- !P Q. P ==> (!x. Q x) <=> (!x. P ==> Q x)
により，全称記号を左にまとめておきます．冠頭標準形prenex normal formla までは必要ありませんが，これをやらないと，後で!m q.に対するSPECLの置換先が見つからないと叱られます．
# e ( REWRITE_TAC[RIGHT_IMP_FORALL_THM] );;
val it : goalstack = 1 subgoal (1 total)`!p q.
(!m q. m < p ==> m * m = 2 * q * q ==> q = 0)
==> p * p = 2 * q * q
==> q = 0`# e( REPEAT STRIP_TAC );;
val it : goalstack = 1 subgoal (1 total)0 [`!m q. m < p ==> m * m = 2 * q * q ==> q = 0`]
1 [`p * p = 2 * q * q`]`q = 0`
では，仮定1からpが偶数であることを導きましょう．それには，FIRST_ASSUM により，仮定のうち，その辺々を
# EVEN;;
val it : thm = |- (EVEN 0 <=> T) /\ (!n. EVEN (SUC n) <=> ~EVEN n)
で定まるEVEN:num->boolで評価できる最初のもの，つまり，仮定1の辺々に AP_TERM `EVEN` として EVEN を結合させて，MP_TAC で結論の implies の前件に据えます．
# e( FIRST_ASSUM( MP_TAC o AP_TERM `EVEN` ) );;
val it : goalstack = 1 subgoal (1 total)0 [`!m q. m < p ==> m * m = 2 * q * q ==> q = 0`]
1 [`p * p = 2 * q * q`]`(EVEN (p * p) <=> EVEN (2 * q * q)) ==> q = 0`
この前件を
# EVEN_MULT;;
val it : thm = |- !m n. EVEN (m * n) <=> EVEN m \/ EVEN n
および，ARITHを参照してREWRITEすると
# e( REWRITE_TAC[EVEN_MULT;ARITH] );;
val it : goalstack = 1 subgoal (1 total)0 [`!m q. m < p ==> m * m = 2 * q * q ==> q = 0`]
1 [`p * p = 2 * q * q`]`EVEN p ==> q = 0`
となるので，具体化する為
# EVEN_EXISTS;;
val it : thm = |- !n. EVEN n <=> (?m. n = 2 * m)
を続けて参照すると
# e( REWRITE_TAC[EVEN_EXISTS] );;
val it : goalstack = 1 subgoal (1 total)0 [`!m q. m < p ==> m * m = 2 * q * q ==> q = 0`]
1 [`p * p = 2 * q * q`]`(?m. p = 2 * m) ==> q = 0`
となり，前件のmとしてr:numを復元して，全ての p を 2*r に置き換えます．なお，SUBST_ALL_TAC(: thm -> tactic =
# e ( DISCH_THEN( X_CHOOSE_THEN `r:num` SUBST_ALL_TAC ) );;
val it : goalstack = 1 subgoal (1 total)0 [`!m q. m < 2 * r ==> m * m = 2 * q * q ==> q = 0`]
1 [`(2 * r) * 2 * r = 2 * q * q`]`q = 0`
後は，仮定0のm，qをそれぞれq，rとSPECLしたもので結論を導けば，全称の仮定からも導けるので十分です．仮定0は再利用しませんので，FIRST_X_ASSUMで取り出します．
# e( FIRST_X_ASSUM( MP_TAC o SPECL[`q:num`;`r:num`] ) );;
val it : goalstack = 1 subgoal (1 total)0 [`(2 * r) * 2 * r = 2 * q * q`]
`(q < 2 * r ==> q * q = 2 * r * r ==> r = 0) ==> q = 0`
この仮定0があればq * q = 2 * r * rは不要です．実際
# e( ONCE_REWRITE_TAC[ARITH_RULE`q*q=2*r*r<=>(2*r)*(2*r)=2*q*q`] THEN ASM_SIMP_TAC[] );;
val it : goalstack = 1 subgoal (1 total)0 [`(2 * r) * 2 * r = 2 * q * q`]
`(q < 2 * r ==> r = 0) ==> q = 0`
得られた前件は~(q<2*r)\/ r=0つまり2*r<=q\/r=0となりますが，r=0==>2*r<=qなので
# e( REWRITE_TAC[ARITH_RULE`(q < 2 * r ==> r = 0) <=> 2*r<=q`] );;
val it : goalstack = 1 subgoal (1 total)0 [`(2 * r) * 2 * r = 2 * q * q`]
`2 * r <= q ==> q = 0`
にまとめられます．実は，この前件の形を見越して，仮定0を書き換えなかったわけで，この前件と
# LE_MULT2;;
val it : thm = |- !m n p q. m <= n /\ p <= q ==> m * p <= n * q
により(2 * r) * 2 * r <= q * q，仮定0を用いて 2 * q * q <= q * q，ARITH_RULE で導ける |- 2*x<=x <=> x=0 を参照して q * q =0，最後に
# MULT_EQ_0;;
val it : thm = |- !m n. m * n = 0 <=> m = 0 \/ n = 0
によりq=0となります．
# e( ASM_MESON_TAC[LE_MULT2;ARITH_RULE`2*x<=x <=> x=0`;MULT_EQ_0] );;
0..0..1..3..9..22..48..204..698..2758..solved at 8153
val it : goalstack = No subgoals
以上をまとめると
prove( `!p q. p*p=2*q*q==>q=0` ,
MATCH_MP_TAC num_WF THEN
REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN
REPEAT STRIP_TAC THEN
FIRST_ASSUM( MP_TAC o AP_TERM `EVEN` ) THEN
REWRITE_TAC[EVEN_MULT;ARITH;EVEN_EXISTS] THEN
DISCH_THEN( X_CHOOSE_THEN `r:num` SUBST_ALL_TAC ) THEN
FIRST_X_ASSUM( MP_TAC o SPECL[`q:num`;`r:num`] ) THEN
ONCE_REWRITE_TAC[ARITH_RULE`q*q=2*r*r<=>(2*r)*(2*r)=2*q*q`] THEN
ASM_SIMP_TAC[] THEN
REWRITE_TAC[ARITH_RULE`(q<2*r==>r=0)<=>2*r<=q`] THEN
ASM_MESON_TAC[LE_MULT2;ARITH_RULE`2*x<=x<=>x=0`;MULT_EQ_0] );;
となりますが
ONCE_REWRITE_TAC[ARITH_RULE`q*q=2*r*r<=>(2*r)*(2*r)=2*q*q`] THEN ASM_SIMP_TAC[] THEN REWRITE_TAC[ARITH_RULE`(q<2*r==>r=0)<=>2*r<=q`] THEN
の部分をARITH_RULEに任せて
ASM_SIMP_TAC
[ARITH_RULE
`((q < 2 * r ==> q * q = 2 * r * r ==> r = 0))
<=>((2 * r) * 2 * r = 2 * q * q ==> 2 * r <= q)`] THEN
とすることも，また，sos.mlをロードすれば
# prove( `!p q. p*p=2*q*q==>q=0` ,
MATCH_MP_TAC num_WF THEN
REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN
REPEAT STRIP_TAC THEN
FIRST_ASSUM( MP_TAC o AP_TERM `EVEN` ) THEN
REWRITE_TAC[EVEN_MULT;ARITH;EVEN_EXISTS] THEN
DISCH_THEN( X_CHOOSE_THEN `r:num` SUBST_ALL_TAC ) THEN
FIRST_X_ASSUM( MP_TAC o SPECL[`q:num`;`r:num`] ) THEN
FIRST_X_ASSUM( MP_TAC ) THEN
CONV_TAC( SOS_RULE ) );;
Searching with depth limit 0
Searching with depth limit 1
Translating proof certificate to HOL
Searching with depth limit 0
Searching with depth limit 1
Translating proof certificate to HOL
Searching with depth limit 0
Searching with depth limit 1
Translating proof certificate to HOL
Searching with depth limit 0
Searching with depth limit 1
Translating proof certificate to HOL
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Translating proof certificate to HOL
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Translating proof certificate to HOL
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Translating proof certificate to HOL
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Translating proof certificate to HOL
val it : thm = |- !p q. p * p = 2 * q * q ==> q = 0
ともできます．
