基于解线性方程组的导角算法

hbghlyj · 发表于 2022-5-28 11:54

本帖最后由 hbghlyj 于 2022-5-28 20:22 编辑

未命名1.pdf (7.44 KB, 下载次数: 218)
Mathematica Notebook:

two circle parallel chords.nb (11.64 KB, 下载次数: 0) Screenshot 2022-04-24 055320.png

输出为 $\left\{l_{\{\text{E},\text{F}\}}=l_{\{\text{A},\text{B}\}},l_{\{\text{B},\text{D},\text{F}\}}=l_{\{\text{A},\text{B}\}}+l_{\{\text{C},\text{D}\}}-l_{\{\text{A},\text{C},\text{E}\}}\right\}$
所以直线EF与AB平行.

(将第$i$条直线的倾斜角定义为$l_i$)

hbghlyj · 发表于 2022-5-28 13:14

本帖最后由 hbghlyj 于 2022-5-28 15:23 编辑

未命名1.svg (8.41 KB, 下载次数: 173)
把前两行改为

linestr = "A,F,B;B,D,C;C,E,A;D,G;E,G;F,G";
circlestr = "A,E,F,G;B,D,F,G";

重新运行:

输出为
$\left\{l_{\{\text{E},\text{G}\}}=l_{\{\text{D},\text{G}\}}+l_{\{\text{C},\text{E},\text{A}\}}-l_{\{\text{B},\text{D},\text{C}\}},l_{\{\text{F},\text{G}\}}=l_{\{\text{D},\text{G}\}}+l_{\{\text{A},\text{F},\text{B}\}}-l_{\{\text{B},\text{D},\text{C}\}}\right\}$
这里的第一个等式$l_{\{\text{E},\text{G}\}}=l_{\{\text{D},\text{G}\}}+l_{\{\text{C},\text{E},\text{A}\}}-l_{\{\text{B},\text{D},\text{C}\}}$等价于$CDEG$共圆.

再举一个例子:

未命名1.svg (11.1 KB, 下载次数: 97) 把前两行改为

linestr = "A,B,E;B,C,F;C,D,G;A,H;D,H;E,I;F,I;G,I;H,I";
circlestr = "A,E,H,I;B,E,F,I;C,F,G,I;D,G,H,I";

重新运行:

从第一个等式$l_{\{\text{D},\text{H}\}}=l_{\{\text{A},\text{H}\}}$就得出ADH共线.

hbghlyj · 发表于 2022-5-28 13:49

本帖最后由 hbghlyj 于 2022-5-28 17:16 编辑 为每个svg创建section元素,然后挂载shadow DOM元素,再把svg填进去,就可以避免id冲突了.
我在Firefox和Chrome上都试过了,1层和2层的图可以正常显示

async function startconvert(num){
const url = $('attach_'+num).firstElementChild.href;
var has_fetched=false;
var contentType,response;
do{
if(has_fetched){console.error('attach_'+num+' failed, retry...')};
response = await fetch(url);
contentType = response.headers.get('content-type');
has_fetched=true;
}while(!contentType||!contentType.includes('application/octet-stream'))
console.info('attach_'+num+' succeeded!');
const decoder = new TextDecoder();
const reader = response.body.getReader();
let str = '';
while (true) {
const { value, done } = await reader.read();
if (done) break;
str += decoder.decode(value);
}
let sec=document.createElement('section');
$('attach_'+num).parentNode.replaceWith(sec);
let shadow=sec.attachShadow({mode: 'open'});
let mydiv=document.createElement('div');
shadow.appendChild(mydiv);
mydiv.innerHTML=str;
}
startconvert(11766);

复制代码

注1:
11766是attachment id

注2:
有的时候会Discuz database error

所以让它自动retry. 控制台大概会输出这样的信息:
QQ图片20220401132641.png

hbghlyj · 发表于 2022-5-28 14:14

本帖最后由 hbghlyj 于 2022-5-28 16:11 编辑

未命名1.svg (7.27 KB, 下载次数: 119) 把前两行改为

linestr = "A,E,B;B,F,C;A,C,D;D,E,F;A,G;B,G;C,G;D,G;E,G;F,G";
circlestr = "A,B,C,G;A,D,E,G";

并把最后一行改为

rules = Solve[eqns][[1]] /. (Subscript[l, _?ListQ] -> _) :> Nothing /. Subscript[l, a_?NumberQ] :> Subscript[l, lineset[[a]]]

并且在最后添加一行:

Subscript[l, {"B", "G"}] - Subscript[l, {"E", "G"}] - Subscript[l, {"B", "F", "C"}] + Subscript[l, {"D", "E", "F"}] /. rules

Screenshot 2022-05-27 at 18-12-23 测试.png

$l_{\{\text{B},\text{G}\}}+l_{\{\text{D},\text{E},\text{F}\}}-l_{\{\text{B},\text{F},\text{C}\}}-l_{\{\text{E},\text{G}\}}$使用rules的代换以后化为0,这样就证明了BEFG共圆.

再举一例:

未命名1.svg (7.49 KB, 下载次数: 92) 把前两行改为

linestr = "A,K;M,L;A,M,B;B,L,C;M,P;B,P;P,L,K";
circlestr = "A,B,C,K,P;B,L,M,P";

第一个等式是$l_{\{\text{M},\text{L}\}}=l_{\{\text{A},\text{K}\}}$,这样就证明了ML与AK平行.

hbghlyj · 发表于 2022-5-28 14:25

未命名2.svg (8.52 KB, 下载次数: 106) 把前两行改为

linestr = "A,B;B,C;C,D;D,A;M,N;N,P;P,Q;Q,M;A,M;B,N;C,P;D,Q";
circlestr = "A,B,C,D;A,B,M,N;B,C,N,P;C,D,P,Q;D,A,Q,M";

和4楼一样,修改最后一行,然后加上

Subscript[l, {"M", "N"}] + Subscript[l, {"P", "Q"}] - Subscript[l, {"Q", "M"}] - Subscript[l, {"N", "P"}] /. rules

$l_{\{\text{M},\text{N}\}}+l_{\{\text{P},\text{Q}\}}-l_{\{\text{Q},\text{M}\}}-l_{\{\text{N},\text{P}\}}$使用rules代换以后化为0,这就证明了MNPQ共圆.

math.stackexchange.com/questions/2540283/proof-of-miquels-six-circle-theorem
baike.baidu.com/item/%E5%85%AD%E8%BF%9E%E7%8E%AF/18895082

hbghlyj · 发表于 2022-5-28 15:23

本帖最后由 hbghlyj 于 2022-5-28 18:42 编辑 其实这个小程序只是使用了$l_{AB}-l_{BC}=l_{AD}-l_{DC}$这一条规则

而且用到的圆都是circleset里面的圆,没有自动把由导角导出的新的圆添加到circleset中(但是可以手动添加然后重新运行)

而且需要手动加辅助线(添加到lineset中).如果lineset里的直线少的话,有可能rules是空集(因为方程少的话,Solve出来可能就只有l_{_?listQ}类型的,所以都被(l_{_?listQ}->_)->Nothing的那步过滤掉了)
应该不能证明Miquel五圆定理的.因为Miquel五圆定理里面用到了ABCD,ABCE共圆⇒ ABDE共圆这条规则.
但或许可以? 嘿嘿, 可以在lineset里多加几条直线试试...

补充一些资料:(就连他们所称的naive的方法也比我的小程序高级多了

)

Automated Generation of Readable Proofs with
Geometric Invariants II. Theorem Proving With Full-Angles

Open Geo prover
Java Geometry Expert

arxiv上2022年1月的新论文:A Method for the Automated Discovery of Angle Theorems
(也是线性方程组)
话说,文章中的figure4的定理好像不对啊??
QQ图片20220401132641.png

hbghlyj · 发表于 2022-5-28 23:56

下面的例子来自Evan chan的有向角讲义第6-7页的Example 4.1 (NIMO Winter 2014, Adapted)

未命名2.svg (9.73 KB, 下载次数: 81) 把前两行改为

linestr = "B,M,C;C,Q,A;A,P,B;P,H,R;Q,H,S;S,M;R,M;A,H;B,H;C,H;M,H";
circlestr = "P,B,S,M,H;C,Q,R,M,H";

并且把最后改为

AppendTo[eqns, 
  Subscript[l, 8] - Subscript[l, 1] == 
   Subscript[l, 9] - Subscript[l, 2] == 
   Subscript[l, 10] - Subscript[l, 3]]; 
rules = Solve[eqns][[1]]

注: 因为$H$是垂心, 所以$l_8-l_1=l_9-l_2=l_{10}-l_3$(都是直角).

QQ图片20220401132641.png

$l_6-l_7$使用rules代换以后化为0,这就证明了SMR共线.

hbghlyj · 发表于 2022-5-29 00:47

那个findline的返回值是i,但是我发现没有单独使用i的地方(凡是用到i的地方,i都是出现在Subscript[l, i]里面),所以改为return Subscript[l, i]的话更方便,但上面各楼层已经发了,我就不作修改了

(我把1楼的notebook和图片都改了.如果您是从1楼下载的notebook文件,应该是已经改好了的)

只需改两处,一个是在findline的定义的最后一行,把i改为Subscript[l, i],另一处是eqns的定义里,findline[Subscript[l,a]]改为findline[a]
这样输入条件的时候就可以只输入直线上的两个点,让程序去找那条直线的编号:
Screenshot 2022-04-24 055320.png

下面的例子来自Evan chan的有向角讲义第7页的 Example 4.2 (European Girl’s MO 2012, Problem 7)

cropped.svg (42.59 KB, 下载次数: 59) (我定义了angle,使输入更方便)
这次修改比较大,直接上传notebook吧

现在可以通过导角找到共线信息然后更新lineset了!
在这个例子中,程序通过导角发现$L,H_C,E'$共线,然后把lineset中的$LH_C,H_CE',LE'$这三条直线合并成一条,然后重新解方程组的
这次需要输入的已知条件是题目条件“点$K,L$和$H,H_C$关于直线AB对称”,“点$K,M$和$H,H_A$关于直线BC对称”的推论:(比较奇怪的是,没有用到高线垂直于对应边的条件,就可以证明出来...)

 eqns = eqns~Join~
   {findline[{"HC", "B"}] + findline[{"H", "B"}] == findline[{"B", "K"}] + findline[{"B", "L"}] == findline[{"H", "K"}] + findline[{"HC", "L"}] == 2 findline[{"A", "B"}], 
    findline[{"HA", "B"}] + findline[{"H", "B"}] == findline[{"HA", "M"}] + findline[{"H", "K"}] == findline[{"B", "M"}] + findline[{"B", "K"}] == 2 findline[{"B", "C"}]};

欧洲女子数奥.nb (27.88 KB, 下载次数: 1) Screenshot 2022-04-24 055320.png

最后angle["L", "HC", "B"] - angle["E'", "HC", "B"]经过rules代换得到0,所以$L,E',B,H_C$共圆.

hbghlyj · 发表于 2022-5-29 03:34

留个坑:
如何可以通过导角找到共圆信息然后更新circleset

(如果可以的话,就可以证明Miquel五圆定理了,正如6层所说的)

		自动登录	找回密码
密码			快速注册