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

以下，表題の証明です．

# g `!s. prime s ==> ~rational (sqrt (&s))` ;;
val it : goalstack = 1 subgoal (1 total)

`!s. prime s ==> ~rational (sqrt (&s))`

まず，全称量化を外し，前件を仮定に廻して，結論を（その１）の定理でリライトします．

# e( GEN_TAC THEN DISCH_TAC THEN
     DISCH_THEN (MP_TAC o (MATCH_MP RATIONAL_COPRIME)) );;
val it : goalstack = 1 subgoal (1 total)

  0 [`prime s`]

`(?p q. &p * &p = sqrt (&s) pow 2 * &q * &q /\ coprime (p,q)) ==> F`

更に根号を外します．

# e( SIMP_TAC [REAL_POS; SQRT_POW_2; REAL_MUL; REAL_INJ] );;
val it : goalstack = 1 subgoal (1 total)

  0 [`prime s`]

`~(?p q. p * p = s * q * q /\ coprime (p,q))`

あとは「dividesにより結論にある等式の左辺はsで割り切れ，仮定によりsは素数なのでPRIME_DIVPRODが使えて，s divides p．再びdividesにより(s * x) * s * x = s * q * qとなり，MULT_AC と PRIME の ~(p = 0) によりMULT_LCANCELが適用できて s * x * x = q * q．従って，pと同様にs divides qとなるが，これはcoprime (p,q)に反する．」

# [divides; PRIME_DIVPROD; MULT_AC; PRIME; MULT_LCANCEL; coprime];;
val it : thm list =
  [|- a divides b <=> (?x. b = a * x);
   |- !p a b. prime p /\ p divides a * b ==> p divides a \/ p divides b;
   |- m * n = n * m /\ (m * n) * p = m * n * p /\ m * n * p = n * m * p;
   |- !p. prime p <=>
          ~(p = 0) /\ ~(p = 1) /\ (!m. 0 < m /\ m < p ==> coprime (p,m));
   |- !a b c. ~(a = 0) /\ a * b = a * c ==> b = c;
   |- coprime (a,b) <=> (!d. d divides a /\ d divides b ==> d = 1)]

という証明をPV9がノーヒントで完成してくれます．

# e( ASM_PV9_TAC it );;
-------- Proof 1 --------

THEOREM PROVED

------ process 5536 exit (max_proofs) ------
CPU time (user): 0.90300000002
val it : goalstack = No subgoals

名前を付けて出来上がり．

# let SQRT_PRIME_NOT_RATIONAL = top_thm();;
val ( SQRT_PRIME_NOT_RATIONAL ) : thm =
  |- !s. prime s ==> ~rational (sqrt (&s))

proveにまとめると

prove
 (`!s. prime s ==> ~rational (sqrt (&s))`,
  GEN_TAC THEN DISCH_TAC THEN
  DISCH_THEN (MP_TAC o (MATCH_MP RATIONAL_COPRIME)) THEN
  SIMP_TAC [REAL_POS; SQRT_POW_2; REAL_MUL; REAL_INJ] THEN
  ASM_PV9_TAC[divides; PRIME_DIVPROD; MULT_AC; PRIME; MULT_LCANCEL; coprime]);;

MESON版

prove
 (`!s. prime s ==> ~rational (sqrt (&s))`,
  GEN_TAC THEN DISCH_TAC THEN
  DISCH_THEN (MP_TAC o (MATCH_MP RATIONAL_COPRIME)) THEN
  SIMP_TAC [REAL_POS; SQRT_POW_2; REAL_MUL; REAL_INJ] THEN STRIP_TAC THEN
  SUBGOAL_TAC "" `s divides p` [ASM_MESON_TAC[divides; PRIME_DIVPROD]] THEN
  FIRST_ASSUM (CHOOSE_TAC o (SIMP_RULE [divides])) THEN
  SUBGOAL_TAC "" `q * q = s * x * x:num`
              [ASM_MESON_TAC[PRIME; MULT_AC; MULT_LCANCEL]] THEN
  ASM_MESON_TAC [divides; PRIME_DIVPROD; PRIME; coprime]);;