本日のC.A.D.
a, b, c がある 3 角形の 3 辺の長さ，ma, mb, mc がその各辺の中点と対頂点との距離（つまり，中線の長さ）ならば
${\displaystyle\frac{3}{4}}(a+b+c) < m_a+m_b+m_c < a+b+c$
8.1 Bottema, et. al. "GEOMETRIC INEQUALITIES"
等式制約は中線定理，非退化 3 角形の存在条件は WLOG で 0＜a, a≦b, b≦c, c＜a+b，そして，a+b+c=1，従って，比の値は ma+mb+mc=x とおけるので，c, mc を消去したのち，parisizemax = 20G で実行すると
? tst12([ex,ex,ex,ex],[x,a,b,ma,mb],andx,"0<a,a<=b,b<=(1-a-b),(1-a-b)<a+b,0<ma,0<mb,0<x-ma-mb,a^2+b^2==2*((x-ma-mb)^2+((1-a-b)/2)^2),b^2+(1-a-b)^2==2*(ma^2+(a/2)^2),(1-a-b)^2+a^2==2*(mb^2+(b/2)^2),0<x");Ans() *** using Lazard's method (MPP17). [mb,4] [ma,6] [b,15] [a,68] [x,1332] time = 3min, 24,355 ms. 5771 984695(168,6317) 869098(224436,1848995) 869111(307784,1653038) 503(0,229566) *** combined adjacent 502 cells. 1[[4*x-3,1] < x < [x-1,1],true,true,true,true] time = 3h, 13min, 15,870 ms.
のようにちょっと大変です．
こうした cell の爆発の回避には，やはり下位の lifting で真理値の定まる制約の採用が効果的なので，求むべきは，x の必要条件です．
ところで，今回の問題の難しさは，2 次式で定義された ma, mb, mc の和を扱うことにありますが，2 乗和であれば
? tst12([ex,ex,ex,ex,ex],[y,a,b,ma,mb,mc],andx,"0<a,a<=b,b<=(1-a-b),(1-a-b)<a+b,0<ma,0<mb,0<mc,a^2+b^2==2*(mc^2+((1-a-b)/2)^2),b^2+(1-a-b)^2==2*(ma^2+(a/2)^2),(1-a-b)^2+a^2==2*(mb^2+(b/2)^2),ma^2+mb^2+mc^2==y,0<y");Ans() *** using Lazard's method (MPP17). [mc,3] [mb,4] [ma,6] [b,14] [a,38] [y,242] time = 9,897 ms. 727 47811(48,910) 30824(13820,74979) 30824(4108,56040) 30824(3392,7928) 114(1292,1748) *** combined adjacent 113 cells. 1[[4*y-1,1] <= y < [8*y-3,1],true,true,true,true,true] time = 4min, 13,126 ms.
のように難しくなく，これにより x の値域の拡大集合が得られます．つまり，この 2 乗和の条件と一般的な 2 乗和と和との関係から
? tst12([ex,ex,ex,ex],[x,y,ma,mb,mc],andx,"0<ma,0<mb,0<mc,ma^2+mb^2+mc^2==y,1/4<=y,y<3/8,ma+mb+mc==x,0<x");Ans() *** using Lazard's method (MPP17). [mc,3] [mb,4] [ma,5] [y,6] [x,7] time = 67 ms. 11 28(0,12) 228(8,16) 924(108,222) 7(62,146) *** combined adjacent 6 cells. 1[[2*x-1,1] < x < [8*x^2-9,2],true,true,true,true] time = 342 ms.
という必要条件が得られ，これを 0＜x の代わりの制約として与えれば
? tst12([ex,ex,ex,ex],[x,a,b,ma,mb],andx,"0<a,a<=b,b<=(1-a-b),(1-a-b)<a+b,0<ma,0<mb,0<x-ma-mb,a^2+b^2==2*((x-ma-mb)^2+((1-a-b)/2)^2),b^2+(1-a-b)^2==2*(ma^2+(a/2)^2),(1-a-b)^2+a^2==2*(mb^2+(b/2)^2),1/2<x,8*x^2-9<0");Ans() *** using Lazard's method (MPP17). [mb,4] [ma,6] [b,15] [a,68] [x,1333] time = 3min, 24,448 ms. 1279 223043(41,1481) 130080(50064,411377) 130080(58236,277036) 503(0,36682) *** combined adjacent 502 cells. 1[[4*x-3,1] < x < [x-1,1],true,true,true,true] time = 37min, 17,195 ms.
といった結果を得ます．
この方法は問題の形に依存していますが，一般に適用可能なものとして，束縛変数のみの制約に対する解集合の各束縛変数の空間への射影を用いる方法が考えられます．例えば，最下位の束縛変数 a の束縛を外し，自由変数とした式を QE すれば
? tst12([ex,ex,ex,ex],[a,b,ma,mb,mc],andx,"0<a,a<=b,b<=(1-a-b),(1-a-b)<a+b,0<ma,0<mb,0<mc,a^2+b^2==2*(mc^2+((1-a-b)/2)^2),b^2+(1-a-b)^2==2*(ma^2+(a/2)^2),(1-a-b)^2+a^2==2*(mb^2+(b/2)^2)");Ans() *** using Lazard's method (MPP17). [mc,2] [mb,2] [ma,2] [b,6] [a,6] time = 97 ms. 9 8(6,9) 8(0,0) 8(0,0) 4(0,0) *** combined adjacent 3 cells. 1[[a,1] < a <= [3*a-1,1],true,true,true,true] time = 23 ms.
という必要条件が得られ，これを 0＜a の代わりの制約として与えれば
? tst12([ex,ex,ex,ex],[x,a,b,ma,mb],andx,"0<a,a<=b,b<=(1-a-b),(1-a-b)<a+b,0<ma,0<mb,0<x-ma-mb,a^2+b^2==2*((x-ma-mb)^2+((1-a-b)/2)^2),b^2+(1-a-b)^2==2*(ma^2+(a/2)^2),(1-a-b)^2+a^2==2*(mb^2+(b/2)^2),1/2<x,8*x^2-9<0,3*a-1<0");Ans() *** using Lazard's method (MPP17). [mb,4] [ma,6] [b,15] [a,68] [x,1333] time = 3min, 23,477 ms. 1279 27839(41,1481) 128801(1220,37978) 128801(55678,269357) 503(0,36678) *** combined adjacent 502 cells. 1[[4*x-3,1] < x < [x-1,1],true,true,true,true] time = 15min, 25,279 ms.
といった結果を得ます．
さて，こうした入出力の組合わせ，書き換え，段階的な QE には，総合環境を目指して開発されている tarski ( https://www.usna.edu/Users/cs/wcbrown/tarski/index.html ) が適しており，以下のような前処理により，処理時間の短縮が可能です．
$ tarski > (version) "tarski version 1.29, Fri Mar 19 16:06:57 EDT 2021":str
まず，qfr ( quantified formula rewriting, https://www.usna.edu/Users/cs/cstech/tr/reports/2007-01.orig.pdf ) を適用して，1 次の等式制約により，mc, c を消去，次に，QEPCADB を段階的に適用して，mb, b を消去します．
> (def F [0<a /\ a<=b /\ b<=c /\ c<a+b /\ 0<ma /\ 0<mb /\ 0<mc /\ a^2+b^2=2(mc^2+(c/2)^2) /\ b^2+c^2=2(ma^2+(a/2)^2) /\ c^2+a^2=2(mb^2+(b/2)^2) /\ ma+mb+mc=x /\ 0<x /\ a+b+c=1]) :void > (def F (qfr[ex c,mc[$F]])) :void > (def F (qepcad-qe[ex mb[$F]])) :void > (def F (qepcad-qe[ex b[$F]])) F :void [a > 0 /\ ma > 0 /\ 3 a - 1 <= 0 /\ x > 0 /\ 4 ma^2 + 2 a - 1 >= 0 /\ 4 ma^2 - 9 a^2 + 8 a - 2 <= 0 /\ 2 ma + a - 1 < 0 /\ 8 x^2 - 16 ma x + 4 ma^2 - 9 a^2 > 0 /\ 16 x^4 - 64 ma x^3 + 80 ma^2 x^2 - 36 a^2 x^2 - 32 ma^3 x + 72 a^2 ma x - 72 a ma^2 + 36 ma^2 + 18 a^3 - 45 a^2 + 36 a - 9 = 0]:tar
ここから先は，+N, +L オプションを付けても "Qepcad failure!":err となります．一方，必要条件は
> (def G [0<a /\ a<=b /\ b<c+a /\ c<a+b /\ 0<ma /\ 0<mb /\ 0<mc /\ a^2+b^2=2(mc^2+(c/2)^2) /\ b^2+c^2=2(ma^2+(a/2)^2) /\ c^2+a^2=2(mb^2+(b/2)^2) /\ ma^2+mb^2+mc^2=y /\ 0<y /\ a+b+c=1]) :void > (def G (qfr[ex c[$G]])) :void > (def G (qepcad-qe[ex a,b,ma,mb,mc[$G]])) G :void [4 y - 1 >= 0 /\ 8 y - 3 < 0]:tar > (def G (qepcad-qe(qfr[ex y,ma,mb,mc[$G /\ 0<ma /\ 0<mb /\ 0<mc /\ ma^2+mb^2+mc^2=y /\ ma+mb+mc=x /\ 0<x]]))) G :void [x > 0 /\ 8 x^2 - 9 < 0 /\ 2 x - 1 > 0]:tar
そして
> (def H [0<a /\ a<=b /\ b<=c /\ c<a+b /\ 0<ma /\ 0<mb /\ 0<mc /\ a^2+b^2=2(mc^2+(c/2)^2) /\ b^2+c^2=2(ma^2+(a/2)^2) /\ c^2+a^2=2(mb^2+(b/2)^2) /\ a+b+c=1]) :void > (def H (qepcad-qe(qfr(exclose H '(a))))) H :void [a > 0 /\ 3 a - 1 <= 0]:tar
となるので，これらの連言を整理，書式の近い redlog に翻訳して
> (syntax 'redlog (normalize [$F /\ $G /\ $H])) "and(a > 0, ma > 0, 3*a - 1 <= 0, 4*ma^2 + 2*a - 1 >= 0, 4*ma^2 - 9*a^2 + 8*a - 2 <= 0, 2*ma + a - 1 < 0, 8*x^2 - 16*ma*x + 4*ma^2 - 9*a^2 > 0, 16*x^4 - 64*ma*x^3 + 80*ma^2*x^2 - 36*a^2*x^2 - 32*ma^3*x + 72*a^2*ma*x - 72*a*ma^2 + 36*ma^2 + 18*a^3 - 45*a^2 + 36*a - 9 = 0, 8*x^2 - 9 < 0, 2*x - 1 > 0)":str
原子式の列をコピペ，tst12 で実行すると
? tst12([ex,ex],[x,a,ma],andx,"a > 0, ma > 0, 3*a - 1 <= 0, 4*ma^2 + 2*a - 1 >= 0, 4*ma^2 - 9*a^2 + 8*a - 2 <= 0, 2*ma + a - 1 < 0, 8*x^2 - 16*ma*x + 4*ma^2 - 9*a^2 > 0, 16*x^4 - 64*ma*x^3 + 80*ma^2*x^2 - 36*a^2*x^2 - 32*ma^3*x + 72*a^2*ma*x - 72*a*ma^2 + 36*ma^2 + 18*a^3 - 45*a^2 + 36*a - 9 = 0, 8*x^2 - 9 < 0, 2*x - 1 > 0");Ans() *** using Lazard's method (MPP17). [ma,6] [a,20] [x,102] time = 854 ms. 103 1508(18,124) 53(8,1123) *** combined adjacent 52 cells. 1[[4*x-3,1] < x < [x-1,1],true,true] time = 3,578 ms.
G, H を付さない場合でも
? tst12([ex,ex],[x,a,ma],andx,"a > 0, ma > 0, 3*a - 1 <= 0, x > 0, 4*ma^2 + 2*a - 1 >= 0, 4*ma^2 - 9*a^2 + 8*a - 2 <= 0, 2*ma + a - 1 < 0, 8*x^2 - 16*ma*x + 4*ma^2 - 9*a^2 > 0, 16*x^4 - 64*ma*x^3 + 80*ma^2*x^2 - 36*a^2*x^2 - 32*ma^3*x + 72*a^2*ma*x - 72*a*ma^2 + 36*ma^2 + 18*a^3 - 45*a^2 + 36*a - 9 = 0");Ans() *** using Lazard's method (MPP17). [ma,6] [a,20] [x,102] time = 849 ms. 317 4184(30,357) 53(60,4430) *** combined adjacent 52 cells. 1[[4*x-3,1] < x < [x-1,1],true,true] time = 11,089 ms.
のように大幅に高速化，「1 人では出来ない（こともないけれど可也しんどい）ことも 2 人居れば何でもない」わけです．
なお，不等式の証明のみであれば，1 人でも何でもありません．
? tst12([ex,ex,ex,ex,ex],[a,b,c,ma,mb,mc],andx,"0<a,a<=b,b<=c,c<a+b,0<ma,0<mb,0<mc,a^2+b^2==2*(mc^2+(c/2)^2),b^2+c^2==2*(ma^2+(a/2)^2),c^2+a^2==2*(mb^2+(b/2)^2),ma+mb+mc<=3/4*(a+b+c)");Ans() *** using Lazard's method (MPP17). [mc,3] [mb,4] [ma,6] [c,18] [b,98] [a,1] time = 1,656 ms. 1 52(0,0) 192(12,80) 192(104,488) 192(0,0) 0(0,0) 1[false] time = 1,358 ms. ? tst12([ex,ex,ex,ex,ex],[a,b,c,ma,mb,mc],andx,"0<a,a<=b,b<=c,c<a+b,0<ma,0<mb,0<mc,a^2+b^2==2*(mc^2+(c/2)^2),b^2+c^2==2*(ma^2+(a/2)^2),c^2+a^2==2*(mb^2+(b/2)^2),ma+mb+mc>=1*(a+b+c)");Ans() *** using Lazard's method (MPP17). [mc,3] [mb,4] [ma,6] [c,16] [b,97] [a,1] time = 1,660 ms. 1 76(0,0) 276(14,100) 276(152,704) 276(0,0) 0(0,0) 1[false] time = 2,007 ms.
