東ロボくんのこと（12）VS on RedLog

　これまでの http://d.hatena.ne.jp/ehito/20131206 および http://d.hatena.ne.jp/ehito/20131208/1386469586 では，前回の（１）を利用した訳ですが，以下では（２），つまり，まず，その「定数」をaのサンプルに対する関数値として得た後，任意のaに対して関数値がそれと等しいことを示す，という方針でやってみます．

　まず，aが0のときの長さの和を調べます．式としては仮定に a == 0 を追加するだけ

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[ForAll[{sq2, a, b, x, y, s, L1, L2, L3}, asm && a == 0, k == L1 + L2 + L3], k, Reals]

ですが．．．帰って来ません．

　式が式ですので，今回はあきらめず，VS（Virtual Substitution http://d.hatena.ne.jp/ehito/20110627/1309162725）を使うよう指示します．

SetSystemOptions[
 "InequalitySolvingOptions" -> {"QuadraticQE" -> True, "QVSPreprocessor" -> True}];
Reduce[ForAll[{sq2, a, b, x, y, s, L1, L2, L3}, asm && a == 0, k == L1 + L2 + L3], k, Reals]

今度は k==4+Sqrt[2] と即答です．そこで，一般のaについて

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

と問う訳ですが．．．帰って来ません（上記の VS のオプションをデフォルトに戻しても当然駄目）．

　しかし，諦めるのはまだ早い．VS といえば RedLog，RedLog といえば VS ですから，上記の asm を RedLog の書式にコンバートして Reduce に入力すると，以下のような期待した結果が得られます．

Redfront 3.2, built 07-Sep-2013 ...
Reduce (Free CSL version), 07-Sep-13 ...

1: load qepcad;on rlnzden,rladdcond;off nat;



4: rlqe all({sq,b,L1,L2,L3,a,x,y,s},and(sq^2=2,0<sq,b^2=a^2+1,0<=b,L1^2 = a^2 + (sq + b)^2, x= a* s, (2 - y)^2 = L3^2 , y = sq*(1 - s) + b*s, y = x^2/(4*sq), (-a + x)^2 + (-b + y)^2 = L2^2, 0 <= a, 0<= L1, 0 <= L2, 0 <= L3, 0 <= s, a <= 1, a=0) impl k=L1+L2+L3);

k - 4 >= 0 and k**2 - 8*k + 14 = 0$

5: rlqe all({sq,b,L1,L2,L3,a,x,y,s,k},and(sq^2=2,0<sq,b^2=a^2+1,0<=b,L1^2 = a^2 + (sq + b)^2, x= a* s, (2 - y)^2 = L3^2 , y = sq*(1 - s) + b*s, y = x^2/(4*sq), (-a + x)^2 + (-b + y)^2 = L2^2, 0 <= a, 0<= L1, 0 <= L2, 0 <= L3, 0 <= s, a <= 1) and ws impl k=L1+L2+L3);

true$