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

幾何的に考えるまでもなく，等比数列と１の６乗根を用いればよいでしょう．数学としては位数６の巡回群の生成元を地道に求めさせる問題です．

まずは帰納法で一般項を準備します．

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

主要部分の処理は，様々な方法がありますが，COMPLEX_RING のお力を得て．．．

g `c pow 6 = Cx(&1) /\ (!i j. i < 6 ==> j < i ==> ~(c pow j = c pow i)) <=>
   c pow 2 - c + Cx(&1) = Cx(&0)` ;;
e( SIMP_TAC[RIGHT_FORALL_IMP_THM]  );;
e( CONV_TAC(REDEPTH_CONV EXPAND_CASES_CONV) THEN SIMP_TAC[complex_pow] );;
e( CONV_TAC COMPLEX_RING );;

あとは問題の表現に合わせるだけです．

let lem02 = SIMP_RULE [MESON[]`(!i j. i < 6 ==> j < i ==> ~p j i) <=>
                               ~(?i j. i < j /\ j < 6 /\ p i j)`] (top_thm ()) ;;

let lem03 = SIMP_RULE[GSYM COMPLEX_TRAD; COMPLEX_POW_II_2; CX_POW; MESON[REAL_POW_DIV; SQRT_POW_2; ARITH_RULE `&2 pow 2 = &4 /\ &0 <= &3` ] ` &3/ &4= (sqrt(&3)/ &2) pow 2`; GSYM CX_MUL; GSYM REAL_NEG_MINUS1]
(COMPLEX_FIELD `Cx(sqrt(&3)/ &2) pow 2 = Cx(&3/ &4) /\ ii pow 2 = --Cx(&1) ==>(c pow 2 - c + Cx(&1) = Cx(&0) <=> c = Cx(&1/ &2) + ii * Cx(sqrt (&3)/ &2) \/ c = Cx(&1/  &2) + ii * Cx(-- &1) * Cx(sqrt (&3)/ &2))`) ;;

let lem04 = GEN_ALL(DISCH_ALL(SIMP_RULE[UNDISCH_ALL lem01; lem03]lem02));;

let lem05 = SIMP_RULE[GSYM PAIR_EQ; complex_mul; COMPLEX_EQ; CX_DEF; RE; IM](SPECL[`\n:num. complex(x n,y n)`; `complex(a,b)`]lem04);;

let lem20130408 = EQT_ELIM(SIMP_CONV[REAL_ADD_SYM; EQ_SYM_EQ; lem05]
`!a b P x y. (!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))`);;