2013年東京大学理科前期第１問 by SIMPLE_COMPLEX_ARITH.

needs "Multivariate/transcendentals.ml";;
needs "Examples/prover9_win.ml";;
needs "Examples/sos_win.ml";;

let lem01 = prove
 (`z 0 = Cx(&1) /\ (!n. z (SUC n) = c * z n) ==> (!n. z n  = c pow n)`,
  STRIP_TAC THEN INDUCT_TAC THEN ASM_SIMP_TAC[complex_pow] );;

let lem02 = SIMP_RULE[IN_ELIM_THM](AP_THM(SIMP_RULE[ARITH](SPEC`6`COMPLEX_ROOTS_UNITY))`c:complex`);;

let lem03 = SIMP_RULE[REAL_MUL](SIMPLE_COMPLEX_ARITH`Cx (&p) * a * b * ii * Cx (&j / &6) = a * b * ii * Cx ((&p * &j) / &6)`);; 

let lem04 = ARITH_RULE`(0 < 1 /\ 1 < 6 /\ 1 * 0 = 0 * 6 + 0 * 0) /\
(0 < 3 /\ 3 < 6 /\ 3 * 2 = 1 * 6 + 0 * 2) /\
(0 < 2 /\ 2 < 6 /\ 2 * 3 = 1 * 6 + 0 * 3) /\
(0 < 3 /\ 3 < 6 /\ 3 * 4 = 2 * 6 + 0 * 4) /\
(j < 6 <=> j = 0 \/ j = 1 \/ j = 2 \/ j = 3 \/ j = 4 \/ j = 5)`;;

g `j < 6 /\ ~(?s t. (s < t /\ t < 6) /\ (t * j == s * j) (mod 6)) <=> j = 1 \/ j = 5`;;
e( EQ_TAC );;
e( PV9_TAC [CONG_CASES; lem04]  );;
e( SIMP_TAC [ARITH_RULE `j = 1 \/ j = 5 ==> j < 6`] );;
e( DISCH_TAC THEN STRIP_TAC THEN POP_ASSUM MP_TAC );;
e( ASM_SIMP_TAC[CONG_MULT_RCANCEL_EQ; MESON[COPRIME_BEZOUT; ARITH_RULE`6*1-5*1=1`; COPRIME_1]`(j = 1 \/ j = 5) ==> coprime(j,6)`; LT_IMP_LE; CONG_LE] THEN STRIP_TAC );;
e( DISJ_CASES_THEN (fun t -> MP_TAC t THEN ASM_ARITH_TAC) (ARITH_RULE `q=0 \/ 1<=q`) );;
let lem05 = top_thm () ;;

g `!z c.  z 0 = Cx(&1) ==> (!n. z (SUC n) = c * z n) ==> (z 6 = z 0 /\ ~(?s t. (s<t /\ t < 6) /\ z t = z s) <=> (?j. c=cexp (Cx (&2) * Cx pi * ii * Cx (&j / &6)) /\ (j=1\/j=5)))`;;

let lem_1 = end_itlist CONJ 
[MESON [] `j<6 /\ c = cexp w /\ p c <=> c = cexp w /\ j<6 /\ p (cexp w)`;
 MESON [] `(?j. j < 6 /\ p j) /\ q <=> (?j. j < 6 /\ p j /\ q)`];;

e( REPEAT STRIP_TAC THEN ASM_SIMP_TAC [lem01; lem02; lem_1; ] );;
e( SIMP_TAC [GSYM CEXP_N; lem03; ARITH; COMPLEX_ROOT_UNITY_EQ; lem05 ]);;
let lem06 = top_thm () ;;

 (* cos sin *) 
 (* 100/constructible.ml に COS_TRIPLE，COS_PI3 もありますが，SOSが簡潔でしょう *)

g`!x.cos (x+x+x)= &4*cos(x) pow 3- &3*cos (x)`;;
e( GEN_TAC THEN SIMP_TAC [COS_ADD; SIN_ADD] );;
e( MP_TAC (SPEC_ALL SIN_CIRCLE) THEN CONV_TAC REAL_RING );;
let COS_3 = top_thm();;

let lem0c=MP(MP(REAL_SOSFIELD `&0 < cos(pi / &3) ==> -- &1 = &4 * cos (pi / &3) pow 3 - &3 * cos (pi / &3) ==> cos(pi / &3)= &1/ &2`)(MATCH_MP COS_POS_PI2(MP(REAL_ARITH `&0 < pi ==> &0 < pi / &3 /\ pi / &3 < pi / &2`)PI_POS))) (SIMP_RULE [REAL_ARITH `pi / &3 + pi / &3 + pi / &3 = pi`; COS_PI] (SPEC`pi/ &3`COS_3));;

let lem0s=SIMP_RULE [lem03_4] (CONV_RULE REAL_RAT_REDUCE_CONV (SIMP_RULE [lem0c; ] (MATCH_MP SIN_COS_SQRT(MESON[MATCH_MP SIN_POS_PI2(MP(REAL_ARITH `&0 < pi ==> &0 < pi / &3 /\ pi / &3 < pi / &2`)PI_POS);REAL_LT_LE]`&0<=sin(pi/ &3)`))));;

let lem1c = MESON[COS_PERIODIC; COS_NEG; REAL_ARITH `(--(pi / &3)) + &2 * pi = pi* &5 / &3`; lem0c]`cos(pi * &5 / &3)= &1 / &2`;;

let lem1s = MESON[SIN_PERIODIC; SIN_NEG; REAL_ARITH `(--(pi / &3)) + &2 * pi = pi* &5 / &3`; lem0s]`sin(pi * &5 / &3)= -- (sqrt (&3) / &2)`;;

let lem2c = PV9[COMPLEX_TRAD; GSYM CEXP_EULER; GSYM lem0c; GSYM lem0s; CX_COS; CX_SIN; SIMPLE_COMPLEX_ARITH ` Cx (&2) * Cx pi * ii * Cx (&1 / &6) = ii * Cx (pi / &3)`;] `complex (&1 / &2,sqrt (&3) / &2) = cexp (Cx (&2) * Cx pi * ii * Cx (&1 / &6))` ;;

let lem2s = PV9[COMPLEX_TRAD; GSYM CEXP_EULER; GSYM lem1c; GSYM lem1s; CX_COS; CX_SIN; SIMPLE_COMPLEX_ARITH ` Cx (&2) * Cx pi * ii * Cx (&5 / &6) = ii * Cx (pi* &5 / &3)`;] `complex (&1 / &2,--(sqrt (&3) / &2)) = cexp (Cx (&2) * Cx pi * ii * Cx (&5 / &6))` ;;

 (*  *) 

let lem07 = REWRITE_RULE
[MESON[] `~(?s t. p s t /\ q s t) <=> (!i j. p i j ==> ~(q i j))`;
 MESON[]`(?j. p j /\ (j=1 \/ j=5))<=>(p 1 \/ p 5)`;
 GSYM lem2c; GSYM lem2s; ]
lem06;;

g `(!n. P n = x n,y n) ==> (x 0,y 0 = &1,&0) ==>
   (!n. x (SUC n),y (SUC n) = a * x n - b * y n,b * x n + a * y n)
   ==> (P 0 = P 6 /\ (!i j. i < j /\ j < 6 ==> ~(P i = P j)) <=>
        a,b = &1 / &2,sqrt (&3) / &2 \/
        a,b = &1 / &2,--(sqrt (&3) / &2))`;;
e( MP_TAC (SPECL[`\n:num. complex(x n,y n)`; `complex(a,b)`]lem07) );;
e( SIMP_TAC[REAL_ADD_SYM; PAIR_EQ; complex_mul; COMPLEX_EQ; CX_DEF; RE; IM; EQ_SYM_EQ]);;
let lem20130406_2= GEN_ALL(top_thm ()) ;;

val lem20130406_2 : thm =
  |- !x y P a b.
         (!n. P n = x n,y n)
         ==> x 0,y 0 = &1,&0
         ==> (!n. x (SUC n),y (SUC n) = a * x n - b * y n,b * x n + a * y n)
         ==> (P 0 = P 6 /\ (!i j. i < j /\ j < 6 ==> ~(P i = P j)) <=>
              a,b = &1 / &2,sqrt (&3) / &2 \/
              a,b = &1 / &2,--(sqrt (&3) / &2))