MMA 中，如何指定某些假设（条件）成立？
本帖最后由 uk702 于 2022-12-27 20:22 编辑如下的一道几何题：
Rt△ABC 中，∠ABC=90°，直线 l 交 BC、CA 及 BA 的延长线于 D、E、F，若 DE=DC=AB，求证：AF+EF=BD。
以下的 MMA 代码是对问题的简单 “直译”：
ClearAll["Global`*"];
b={0,0}; a={0,u}; d={v,0}; c={u+v, 0}; (* 令 AB=u, BD=v，则 BC=u+v *)
(* E 在 AC 上且 DE=DC=u *)
e = {x, y} /. Simplify@First@Solve[{{x,y} \ InfiniteLine[{a, c}] && EuclideanDistance[{x,y}, d] == u && 0 < x < v}, {x, y}];
(* 求直线{e, d} 和 直线{b, a} 的交点 *)
f = {x, y} /. Simplify@First@Solve . (#2 - {x, y}) == 0 & @@@ {{e, d}, {b, a}}, {x, y}];
lenAfAndFe = (EuclideanDistance + EuclideanDistance) // Simplify;
Print["AF+FE = ", lenAfAndFe, " , BD = v，两者当相等"]
结果显示：
AF+FE = v if u>0&&v>0 , BD = v，两者当相等
故命题得证。
其中，求解 E有坐标时，MMA 返回
\( \left\{\fbox{$\frac{v^2 (u+v)}{2 u^2+2 v u+v^2}\text{ if }u>0\land v>0$},\fbox{$\frac{2 u^2 (u+v)}{2 u^2+2 v u+v^2}\text{ if }u>0\land v>0$}\right\} \)
求助各位专家，不知是否有办法让 MMA 知道 u>0 和 v>0 这两个假设已经作为预置条件总是成立的？
本帖最后由 uk702 于 2022-12-27 20:44 编辑
经实验将代码改为如下可行，求大佬们提供更好的写法（多处都要加 Assuming[{u > 0, v > 0}, xxx] 挺烦人的）：
ClearAll["Global`*"];
b={0,0}; a={0,u}; d={v,0}; c={u+v, 0}; (* 令 AB=u, BD=v，则 BC=u+v *)
(* E 在 AC 上且 DE=DC=u *)
e = {x, y} /. Simplify@First@Assuming[{u > 0, v > 0}, Solve[{{x,y} \ InfiniteLine[{a, c}] && EuclideanDistance[{x,y}, d] == u && 0 < x < v}, {x, y}]];
Print["e = ", e];
(* 求直线{e, d} 和 直线{b, a} 的交点 *)
f = {x, y} /. Simplify@First@Solve . (#2 - {x, y}) == 0 & @@@ {{e, d}, {b, a}}, {x, y}];
Print["f = ", f];
lenAfAndFe = Assuming[{u > 0, v > 0}, FullSimplify[(EuclideanDistance + EuclideanDistance)]];
Print["AF+FE = ", lenAfAndFe, " , BD = v，两者当相等"]
经实验，可以将 Assuming[{u > 0, v > 0} 放到最外层，让整个代码都包裹进这个假设里，这样就可以避免多处重复写这段代码：
```
ClearAll["Global`*"];
Assuming[{u > 0, v > 0},
b={0,0}; a={0,u}; d={v,0}; c={u+v, 0}; (* 令 AB=u, BD=v，则 BC=u+v *)
(* E 在 AC 上且 DE=DC=u *)
e = {x, y} /. Simplify@First@ Solve[{{x,y} \ InfiniteLine[{a, c}] && EuclideanDistance[{x,y}, d] == u && 0 < x < v}, {x, y}];
Print["e = ", e];
(* 求直线{e, d} 和 直线{b, a} 的交点 *)
f = {x, y} /. Simplify@First@Solve . (#2 - {x, y}) == 0 & @@@ {{e, d}, {b, a}}, {x, y}];
Print["f = ", f];
lenAfAndFe = FullSimplify[(EuclideanDistance + EuclideanDistance)];
Print["AF+FE = ", lenAfAndFe, " , BD = v，两者当相等"]
]
``` 我只会做具体的题目，可以这样(恒等式)。
\(AB=\sin(\theta),BD=\cos(\theta)-\sin(\theta),AE=1-\sin(2\theta)\)
\(\frac{AF+EF}{BD}=\frac{(1-\sin(2\theta))(\cos(\theta)+\sin(\theta))/cos(2\theta)}{\cos(\theta)-\sin(\theta)}=1\) $Assumptions=u>0; CD=AB → Rt△ABD≌Rt△CDG
所以BC=BD-CD=BH-AB=AH=AF+FH=AF+EF
页:
[1]