√素数が有理数でないこと（その１）

前回の性質を少し一般化したものの tactics による証明です．

まず（その１）として，有理数が既約分数で表せることを定理にしておきます．

# g `!x. rational x ==> (?p q. &p * &p = x pow 2 * &q * &q /\ coprime (p,q))`;;
val it : goalstack = 1 subgoal (1 total)

`!x. rational x ==> (?p q. &p * &p = x pow 2 * &q * &q /\ coprime (p,q))`

rational の定義は整数によるものですが，ここでは自然数による

# RATIONAL_ALT;;
val it : thm = |- !x. rational x <=> (?p q. ~(q = 0) /\ abs x = &p / &q)

で簡約します．

# e( SIMP_TAC [RATIONAL_ALT] THEN REPEAT STRIP_TAC );;
val it : goalstack = 1 subgoal (1 total)

  0 [`~(q = 0)`]
  1 [`abs x = &p / &q`]

`?p q. &p * &p = x pow 2 * &q * &q /\ coprime (p,q)`

この仮定のp,qをgcd (p,q)で割ったものを結論に用いればcoprime (p,q)なので証明が完成する流れです．

要になる既存の定理は

# GCD_COPRIME_EXISTS;;
val it : thm =
  |- !a b.
         ~(gcd (a,b) = 0)
         ==> (?a' b'.
                  a = a' * gcd (a,b) /\ b = b' * gcd (a,b) /\ coprime (a',b'))

ですので

# e( SUBGOAL_TAC "" `~(gcd (p,q) = 0)` [ASM_MESON_TAC [GCD_ZERO]] );;
0..0..1..solved at 4
val it : goalstack = 1 subgoal (1 total)

  0 [`~(q = 0)`]
  1 [`abs x = &p / &q`]
  2 [`~(gcd (p,q) = 0)`]

`?p q. &p * &p = x pow 2 * &q * &q /\ coprime (p,q)`

のように前件を用意（ここでMESONに参照させたのは

# GCD_ZERO;;
val it : thm = |- !a b. gcd (a,b) = 0 <=> a = 0 /\ b = 0

です）して，MATCH_MPで後件を仮定に加えます（多重の特称量化の消去はCHOOSE_TACでは面倒ですので，MP_TAC で導入してシステムに STRIP させます）．

# e( FIRST_ASSUM (MP_TAC o (MATCH_MP GCD_COPRIME_EXISTS)) THEN STRIP_TAC );;
val it : goalstack = 1 subgoal (1 total)

  0 [`~(q = 0)`]
  1 [`abs x = &p / &q`]
  2 [`~(gcd (p,q) = 0)`]
  3 [`p = a' * gcd (p,q)`]
  4 [`q = b' * gcd (p,q)`]
  5 [`coprime (a',b')`]

`?p q. &p * &p = x pow 2 * &q * &q /\ coprime (p,q)`

ここまでくれば，結論のp,qとして仮定のa',b'が使えることは，計算で判りますが，その計算が実は面倒です．

つまり，結論にある等式は実数についてのもの，仮定0,2,3,4にある等式は自然数ついてのものなので，それらを同時には処理できないのです．このような場合には，まず自然数から実数への単射 & を施した実数についての等式を REAL_FIELD などで証明し，更に

# [REAL_POW2_ABS; REAL_INJ; REAL_MUL];;
val it : thm list =
  [|- !x. abs x pow 2 = x pow 2; |- !m n. &m = &n <=> m = n;
   |- !m n. &m * &n = &(m * n)]

を参照させて SIMP_RULE で簡約すれば

let lem1 = SIMP_RULE [REAL_POW2_ABS; REAL_INJ; REAL_MUL]
(REAL_FIELD `~(&q = &0) ==> abs x = &p / &q ==> ~(&(gcd (p,q)) = &0)
 ==> &p = &a' * &(gcd (p,q)) ==> &q = &b' * &(gcd (p,q))
 ==> &a' * &a' = abs x pow 2 * &b' * &b'`);;
2 basis elements and 0 critical pairs
...
17 basis elements and 0 critical pairs
val lem1 : thm =
  |- ~(q = 0)
     ==> abs x = &p / &q
     ==> ~(gcd (p,q) = 0)
     ==> p = a' * gcd (p,q)
     ==> q = b' * gcd (p,q)
     ==> &(a' * a') = x pow 2 * &(b' * b')

が得られます．最後の&(a' * a'),&(b' * b')はREAL_MULの副作用で，同値の両辺を入れ替えた GSYM REAL_MUL を参照させ，もう一度簡約すれば &a' * &a',&b' * &b'に出来ますが，それは最後にMESONに任せましょう．

後はこのlem1の前件たちが現在のサブゴールの仮定を満たしていることをUNDISCH_ALL により HOL Light に判らせれば，MP_TAC でも ASSUME_TAC でも

# e( MP_TAC (UNDISCH_ALL lem1) );;
val it : goalstack = 1 subgoal (1 total)

  0 [`~(q = 0)`]
  1 [`abs x = &p / &q`]
  2 [`~(gcd (p,q) = 0)`]
  3 [`p = a' * gcd (p,q)`]
  4 [`q = b' * gcd (p,q)`]
  5 [`coprime (a',b')`]

`&(a' * a') = x pow 2 * &(b' * b')
 ==> (?p q. &p * &p = x pow 2 * &q * &q /\ coprime (p,q))`

のように後件が導入でき，先ほどの簡約の補正も含め，MESONに託せば

# e( ASM_MESON_TAC [REAL_MUL] );;
0..0..2..5..13..26..44..73..103..144..208..303..428..614..833..solved at 101
7
val it : goalstack = No subgoals

となります．

# let RATIONAL_COPRIME = top_thm () ;;
val ( RATIONAL_COPRIME ) : thm =
  |- !x. rational x ==> (?p q. &p * &p = x pow 2 * &q * &q /\ coprime (p,q))

まとめれば

# let RATIONAL_COPRIME = prove
   (`!x. rational x ==> (?p q. &p * &p = x pow 2 * &q * &q /\ coprime (p,q))`,
    SIMP_TAC [RATIONAL_ALT] THEN REPEAT STRIP_TAC THEN
    SUBGOAL_TAC "" `~(gcd (p,q) = 0)` [ASM_MESON_TAC [GCD_ZERO]] THEN
    FIRST_ASSUM (MP_TAC o (MATCH_MP GCD_COPRIME_EXISTS)) THEN STRIP_TAC THEN
    MP_TAC (UNDISCH_ALL lem1) THEN
    ASM_MESON_TAC [REAL_MUL]);;
0..0..1..solved at 4
0..0..2..5..13..26..44..73..103..144..208..303..428..614..833..solved at 1017
val ( RATIONAL_COPRIME ) : thm =
  |- !x. rational x ==> (?p q. &p * &p = x pow 2 * &q * &q /\ coprime (p,q))

となります．

なお，MESONでは難しいですが，Prover9 ならこの程度はノーヒントで証明してくれます．

# [REAL_EQ_RDIV_EQ; REAL_NZ_IMP_LT; REAL_MUL; REAL_INJ; REAL_MUL_AC;
   REAL_EQ_RMUL_IMP; POW_2; REAL_POW2_ABS];;
val it : thm list =
  [|- !x y z. &0 < z ==> (x = y / z <=> x * z = y);
   |- !n. ~(n = 0) ==> &0 < &n; |- !m n. &m * &n = &(m * n);
   |- !m n. &m = &n <=> m = n;
   |- m * n = n * m /\ (m * n) * p = m * n * p /\ m * n * p = n * m * p;
   |- !x y z. ~(z = &0) /\ x * z = y * z ==> x = y; |- !x. x pow 2 = x * x;
   |- !x. abs x pow 2 = x pow 2]
# let lem1 = PV9 [REAL_EQ_RDIV_EQ; REAL_NZ_IMP_LT; REAL_MUL; REAL_INJ;
                  REAL_MUL_AC; REAL_EQ_RMUL_IMP; POW_2; REAL_POW2_ABS]
`~(q = 0) ==> abs x = &p / &q ==> ~(gcd (p,q) = 0) ==> p = a' * gcd (p,q)
 ==> q = b' * gcd (p,q) ==> &a' * &a' = x pow 2 * &b' * &b'`;;
-------- Proof 1 --------

THEOREM PROVED

------ process 4804 exit (max_proofs) ------
CPU time (user): 12.187
val lem1 : thm =
  |- ~(q = 0)
     ==> abs x = &p / &q
     ==> ~(gcd (p,q) = 0)
     ==> p = a' * gcd (p,q)
     ==> q = b' * gcd (p,q)
     ==> &a' * &a' = x pow 2 * &b' * &b'

# let RATIONAL_COPRIME =
PV9 [RATIONAL_ALT; GCD_ZERO; GCD_COPRIME_EXISTS; REAL_MUL; lem1]
`!x. rational x ==> (?p q. &p * &p = x pow 2 * &q * &q /\ coprime (p,q))`;;
-------- Proof 1 --------

THEOREM PROVED

------ process 5676 exit (max_proofs) ------
CPU time (user): 32.764
val ( RATIONAL_COPRIME ) : thm =
  |- !x. rational x ==> (?p q. &p * &p = x pow 2 * &q * &q /\ coprime (p,q))

結局のところ，定理自動証明システムのパフォーマンスは，preproved theoremsの質と量，そしてそれを扱うproverの処理能力で定まる訳です．