東ロボくんのこと（７）今年の問題

　http://d.hatena.ne.jp/ehito/20131129/1385725290 に続き
　人間が問題を訳した場合，計算機は本年の東大文科数学の問題をどの程度処理できるか？
の第２問です．http://www.yozemi.ac.jp/nyushi/sokuho/recent/tokyo/zenki/

　出題テーマは「２次曲線の性質を平方根の簡約によって解く」といった所ですが，残念ながらMathematicaは二重根号を外してくれません．また座標平面，２次式の平方なのでQE処理にも厳しいものがあります．

　まずは設定．

P={0,-Sqrt[2]};Q={0,Sqrt[2]};A={a,Sqrt[a^2+1]};

線分の長さは（ビルトインのNormでもよいのですが）内積の非負平方根のまま

Resolve[ForAll[a, 0 <= a <= 1, 
  Sqrt[(A - P).(A - P)] - Sqrt[(Q - A).(Q - A)] == c], Reals]

とします．これは c == 2 と即答です．

　（２）も

defB = Resolve[
  0 <= a <= 1 &&
  Exists[s, 0 <= s, {b1, b2} == (1 - s)*Q + s*A && b2 == Sqrt[2]/8*b1^2], Reals];
B = {b1, b2}; C2 = {b1, 2};

と設定を追加して

Resolve[ForAll[{a, b1, b2}, defB, 
  Sqrt[(A - P).(A - P)] + Sqrt[(B - A).(B - A)] + Sqrt[(C2 - B).(C2 - B)] == c], Reals]

ですが，これは帰って来ません．

　以上では，典型的な設問である「定数であることを示し」という部分を

　定義域Dの関数fは定数関数である　≡　∃c(∀x(x∈D→f(x)=c))

に基いて訳し，値も判るようにcを自由変数として残したわけですが，例えば

Resolve[
 Exists[c, 
  ForAll[a, 0 <= a <= 1, 
   Sqrt[(A - P).(A - P)] - Sqrt[(Q - A).(Q - A)] == c]], Reals]
Sqrt[(A - P).(A - P)] - Sqrt[(Q - A).(Q - A)] /. {a -> 0}

と分けたほうが問題文には忠実です．

　なお，（２）への対応として

・二重根号を外させる
・根号を用いずに表す
・「定数である」の言い換えを工夫する

などが考えられますので，次回以降模索していきます．