東ロボくんのこと（９）根号を使わない

　現在のいわゆるSymbolic QEで扱えるのは原理的に多項式のみです（Mathematicaのような根号を受け付けてくれるものでも内部で書き直しています）．

　なら入力の時点から多項式にしておきましょう．という方針でやってみます．問題は http://www.yozemi.ac.jp/nyushi/sokuho/recent/tokyo/zenki/ の文科第２問（２）でした．

　まず，P,Q,Aですが，いきなり根号があるので，新たな変数を導入して

sq2^2 == 2, 0 < sq2, P = {0, -sq2}, 
Q = {0, sq2},
b^2 == a^2 + 1, 0 <= b, A = {a, b}, 0 <= a <= 1

とします．次にBですが，これは「Qを端点としAを通る半直線」と「放物線y=(√2)/8 x^2」との交点なので

0 <= s, {x, y} == (1 - s)*Q + s*A, y == sq2/8*x^2, B = {x, y}

Cについては座標軸に垂直な超平面（直線）への正射影なので，Bの座標を受け継いで

C2 = {B[[1]], 2}

最後に各線分の長さを根号を用いずに

L1^2 == (A - P).(A - P), L2^2 == (B - A).(B - A), L3^2 == (C2 - B).(C2 - B),
0 <= L1, 0 <= L2, 0 <= L3

とします．

　後は以上全ての連言を X，以上全ての変数の列をv，更に

k == L1 + L2 + L3

を Y として ∃k(∀v(X→Y)) が True であること見れば良いのですが，現在のシステムでの変数のドメインはRゆえ，R^2をドメインとするP,Q,A,B,C2（つまり，点）は量化できないので，これらはMathematica側のグローバル変数として定義します（つまり，その部分は全て評価（代入）されたものを扱う）．

　まとめると

P = {0, -sq2}; Q = {0, sq2}; A = {a, b}; B = {x, y}; C2 = {B[[1]], 2};
asm = 
 LogicalExpand[
  And[sq2^2 == 2, 0 < sq2, b^2 == a^2 + 1, 0 <= b, 0 <= a <= 1,
   {x, y} == (1 - s)*Q + s*A, 0 <= s, y == sq2/8*x^2,
   L1^2 == (A - P).(A - P), L2^2 == (B - A).(B - A), 
   L3^2 == (C2 - B).(C2 - B), 0 <= L1, 0 <= L2, 0 <= L3]];

のもとで，前々回に述べた定数関数の定義に従うなら

Reduce[Exists[k,ForAll[{sq2, a, b, x, y, s, L1, L2, L3}, asm, k == L1 + L2 + L3]], Reals]

k の値も同時に得たいなら

Reduce[ForAll[{sq2, a, b, x, y, s, L1, L2, L3}, asm, k == L1 + L2 + L3], k, Reals]

とする訳ですが，やはり両者とも帰って来ません．