Tiểu luận Cơ sở Groebner và chứng minh định lý hình học bằng máy tính

dạng tham số thì Maple sẽ đưa ra một thông báo là hai điểm đó phải là hai điểm phân biệt (tức là chúng ta phải đưa ra câu lệnh giả thiết rằng hai điểm đó là phân biệt trước khi khai báo đường thẳng). Với mỗi thủ tục đó khi thực hiện phép tính sẽ rất phức tạp mà nhiều khi chưa chắc đã làm được. Do vậy, vấn đề xây dựng một gói công cụ mới dựa trên ngôn ngữ lập trình Maple để giải quyết vấn đề trên là không thể thiếu được. Sau đây là các câu lệnh để đưa ra hệ phương trình giả thiết và kết luận của định lý: Ta tiến hành khai báo các điểm: [> A:=Point(0, 0): B:=Point(u1, 0): C:=Point(u2, u3): D_:=Point(x1, x2): N:=Point(x3, x4): Hình 3.4 Các biến u1, u2, u3 là các biến độc lập, còn các biến x1, x2, x3, x4 là các biến phụ thuộc và nó bị ràng buộc bởi điều kiện ABCD là hình thoi và N là giao điểm của hai đường chéo. Từ giả thiết AB = AD và ,N AC N BD  ta có các phương trình: [> sqrdist(A, B ) - sqrdist(A, D_) = 0; 2 2 2 1 1 2 0u x x   [> on_line(N, pp_line(B, D_)) = 0; 2 3 4 1 4 1 2 1 0x x x x x u x u    23 [> on_line(N, pp_line(A, C)) = 0; 3 3 2 4 0u x u x  Từ giả thiết AD // CB và CD // AB ta có các phương trình: [> is_parallel(pp_line(A, D_), pp_line(C, B)) = 0; 2 2 2 1 1 3 0x u x u x u   [> is_parallel(pp_line(C, D_), pp_line(A, B)) = 0; 3 2 0u x  Từ kết luận AC BD và N là trung điểm của AC, BD ta có: [> is_orthogonal(pp_line(C, A), pp_line(D_, B)) = 0; 2 3 2 1 2 1 0x u u x u u   [> sqrdist(N, B) - sqrdist(N, D_) = 0; 2 2 2 1 1 3 1 1 3 2 2 42 2 2 0u u x x x x x x x      [> sqrdist(N, A) - sqrdist(N, C) = 0; 2 2 2 2 3 3 3 42 2 0u u x u u x     Như vậy định lý trên được chia thành hai bài toán vì định lý có hai kết luận riêng biệt. Ta sẽ dùng cơ sở Groebner để kiểm định từng kết luận: Giả thiết 1: Cho hệ phương trình: 2 2 2 1 1 1 2 2 2 2 2 1 1 3 3 3 2 0 0 0 f u x x f x u x u x u f u x               Kết luận 1: Khi đó mọi nghiệm thực của nó phải thoả mãn hệ phương trình: 1 2 3 2 1 2 1 0g x u u x u u    (nghĩa là AC BD ) Giả thiết 2: Cho hệ phương trình: 2 2 2 1 1 1 2 2 2 2 2 1 1 3 3 3 2 4 2 3 4 1 4 1 2 1 5 3 3 2 4 0 0 0 0 0 f u x x f x u x u x u f u x f x x x x x u x u f u x u x                          Kết luận 2: Khi đó mọi nghiệm thực của nó phải thoả mãn hệ phương trình: 24 2 2 2 2 1 1 3 1 1 3 2 2 4 2 2 3 2 2 3 3 3 4 2 2 2 0 2 2 0 g u u x x x x x x x g u u x u u x                (N là trung điểm của AC và BD) Bây giờ ta sử dụng phần mềm Maple đối với iđêan I1 để kiểm định kết luận thứ nhất g1: 𝐼1 = (𝑓1, 𝑓2, 𝑓3, 𝑧𝑔1 − 1) ⊂ ℝ[𝑢1, 𝑢2, 𝑢3, 𝑥1, 𝑥2, 𝑧] theo thứ tự từ điển với 1 2 1 2 3z x x u u u     , ta được có sở Groebner sau: [>  2 2 21 1 1 2 2 2 2 1 1 3 2 3 2 3 2 1 2 1: , , , 1 :L u x x x u x u x u x u x u u x u u z            [>  2 1 2 1 2 3: , , , , , :L z x x u u u Ta tìm đa thức dư của đa thức 1 khi chia cho các đa thức trong danh sách L1 đối với thứ tự từ điển trên: [> normalf(1, L1, plex(L2)); 1 Ta thấy đa thức dư là 1, do vậy kết luận g1 chưa đúng. Để xem định lý suy biến trong trường hợp nào ta hãy tìm cơ sở Groebner G của I1 và tìm iđêan khử 𝐼1 ′ : [> G:= gbasis(L1, plex(L2));  3 2 1 1 2 1: , , ,2 1G u x x u zu u   Dựa trên cơ sở Groebner trên, ta khai báo các biến phụ thuộc vào danh sách L3 và sử dụng các câu lệnh của Maple để đưa ra 𝐼1 ′ : [>  3 1 2: , , :L z x x [> for j from 1 to nops(G) do k[j]:= degree(leadterm(G[j], plex(L3)), {L3}): if k[j] = 0 then print(G[j]); fi; od; 3u Như vậy, ta tìm được iđêan khử 𝐼1 ′ = (𝑢3). Trường hợp suy biến của định lý ứng với nghiệm của phương trình 3 0u  , tức là điểm C có toạ độ  2 ,0u hay nói cách khác điểm C nằm trên trục hoành của hệ trục tọa độ đã chọn và khi đó hình thoi suy biến thành một đường thẳng. Ta tiếp tục kiểm định đối với kết luận g2: 25 𝐼2 = (𝑓1, 𝑓2, 𝑓3, 𝑓4, 𝑓5, 𝑧𝑔2 − 1) ⊂ ℝ[𝑢1, 𝑢2, 𝑢3, 𝑥1, 𝑥2, 𝑥3, 𝑥4, 𝑧] theo thứ tự từ điển với 1 2 3 4 1 2 3z x x x x u u u       , ta được có sở Groebner sau: [> ' 1 :L  [ 2 2 2 1 1 2 2 2 2 1 1 3 2 3, , ,u x x x u x u x u x u      2 3 4 1 4 1 2 1,x x x x x u x u   2 3 4 1 4 1 2 1,x x x x x u x u    2 2 21 1 3 1 1 3 2 2 42 2 2 1u u x x x x x x x z      ]: [>  '2 1 2 3 4 1 2 3: , , , , , , , :L z x x x x u u u [> normalf(1, L1, plex(𝐿2 ′ )); 1 [> G:= gbasis(𝐿1 ′ , plex(𝐿2 ′ ));  3 4 2 1 1 1 3: , , , ,4 1G u x x x u zu x   Dựa trên cơ sở Groebner trên, ta khai báo các biến phụ thuộc vào danh sách 𝐿3 ′ và sử dụng các câu lệnh của Maple để đưa ra iđêan khử 𝐼2 ′ : [>  '3 1 2 3 4: , , , , :L z x x x x [> for j from 1 to nops(G) do k[j]:= degree(leadterm(G[j], plex(𝐿3 ′ )), {𝐿3 ′ }): if k[j] = 0 then print(G[j]); fi; od; 3u Như vậy, ta tìm được iđêan khử 𝐼2 ′ = (𝑢3). Trường hợp suy biến của định lý ứng với nghiệm của phương trình 3 0u  , tức là hình thoi suy biến thành một đường thẳng. Kiểm định tương tự cho kết luận g3 ta cũng có kết quả tương tự. 3.3. CHỨNG MINH MỘT SỐ ĐỊNH LÝ HÌNH HỌC Sau đây chúng tôi trình bày phương pháp chứng minh một số định lý hình học sơ cấp bằng máy tính. Phần mềm Maple sẽ đưa ra kết luận về tính đúng sai của định lý hình học. Sau khi có kết quả từ máy tính, chúng tôi sẽ chứng minh định lý đó bằng toán học và phát triển thêm các bài toán khác. 26 Định lý 1. (Đường thẳng Ơle) Gọi O, H, G lần lượt là tâm của đường tròn ngoại tiếp, trực tâm và trọng tâm của ABC cho trước. Khi đó, ba điểm O, H, G thẳng hàng và điểm G chia đoạn thẳng OH theo tỉ số 1:3. Trước tiên, trong hệ tọa độ Đề-các vuông góc ta tiến hành khai báo tọa độ của các điểm như sau: [> A:=Point(a1, a2): B:=Point(b1, b2): C:=Point(c1, c2): [> O_:=intersection_point(p_bisector(A, B), p_bisector(B, C)); M:=[( –b2a22 + b2c22 + b2c12 – b2a12 – c22a2 – c12a2 + b22a2 – b22c2 + c2a22 + c2a12 + b12a2 – b12c2)/(2(c2a1 – a1b2 – b1c2 + b2c1 + a2b1 – c1a2)), –(a1c22 + a1b22 + a1b12 – a1c12 + b1c22 + b1c12 – b1a22 – b1a12 – c1b22 + c1a22 + c1a12 – c1b12)/(2(c2a1 – a1b2 – b1c2 + b2c1 + a2b1 – c1a2))] [> H:=intersection_point(altitude(A, B, C),altitude(B, C, A)); H:=[( –c2a22 + c22a2 + b2a22 + a1a2b1 – a1c1a2 + c1a1c2 – b22a2 – b2c22 + b22c2 – b1c1c2 + b1b2c1 – b1a1b2)/(c2a1 – a1b2 – b1c2 + b2c1 + a2b1 – c1a2), (b2a2b1 – b2b1c2 – c1b12 + a1b12 + b2c1c2 + b1c12 – a2c2c1 – a1c12 + a2c2a1 – a2a1b2 – b1a12 + c1a12)/(c2a1 – a1b2 – b1c2 + b2c1 + a2b1 – c1a2))] [> G:=intersection_point(median(A, B, C),median(B, C, A)); 𝐺 ≔ [ 𝑏1 3 + 𝑎1 3 + 𝑐1 3 , 𝑎2 3 + 𝑏2 3 + 𝑐2 3 ] Để kiểm tra các kết luận của định lý, ta sử dụng câu lệnh sau đây: [> is_collinear(O_, H, G); 0 [> sqrdist(G,varpoint(O_, H, 1/3)); 0 Cả hai câu lệnh trên đều cho kết quả bằng 0. Điều đó có nghĩa là định lý trên là đúng. Bây giờ ta chứng minh bằng toán học như sau: Chứng minh. Gọi A’, B’, C’ lần lượt là trung điểm của các cạnh BC, CA, AB. Ta chứng minh giao điểm của đường thẳng HO và đường thẳng AA’ chính là trọng tâm G của ABC. Thật vậy, ta có: HA = 2OA' và HA // OA' ⇒ 𝐺𝐴 𝐺𝐴′ = 𝐻𝐴 𝑂𝐴′ = 2, suy ra G là trọng tâm ABC. Từ đó ta suy ra H, G, O thẳng hàng. 27 Hình 3.5 Hơn nữa, nếu gọi O9 là tâm đường tròn Ơle của ABC hay O9 là tâm đường tròn ngoại tiếp A’B’C’ thì ta có O, G, O9 thẳng hàng (theo chứng minh trên với điểm G là trọng tâm A’B’C’ và điểm O là trực tâm của A’B’C’). Đặc biệt, bốn điểm H, G, O và O9 lập thành một hàng điểm điều hoà với 𝐺𝑂⃗⃗⃗⃗ ⃗ = −2𝐺𝑂9⃗⃗ ⃗⃗ ⃗⃗ ⃗ và 𝐺𝐻⃗⃗⃗⃗⃗⃗ = −2𝐺𝑂⃗⃗⃗⃗ ⃗. Định lý 2. (Đường tròn Ơle) Trong tam giác ba trung điểm của ba cạnh, ba chân các đường cao, ba trung điểm của ba đoạn thẳng nối trực tâm với các đỉnh của tam giác là 9 điểm nằm trên một đường tròn với tâm O9 là trung điểm của đoạn thẳng OH. Đường tròn này được gọi là đường tròn Ơle. Trong hệ tọa độ Đề-các vuông góc ta có thể chọn tọa độ các điểm với A là gốc tọa độ và trục Ox với đơn vị là điểm B. Điểm C là điểm tùy ý. [> A:=Point(0, 0): B:=Point(u1, 0): C:=Point(u2, u3) : Gọi O9 là trung điểm của đoạn thẳng OH. Ta xác định tọa độ của các điểm O, H và O9 như sau: [> O_:=intersection_point(p_bisector(A, B), p_bisector(B, C)); 𝑂_ ≔ [ 𝑢1 2 ,− −𝑢3 2 − 𝑢2 2 + 𝑢1𝑢2 2𝑢3 ] [> H:=intersection_point(altitude(A, B, C), altitude(B, C, A)); 28 𝐻 ≔ [𝑢2, (𝑢1 − 𝑢2)𝑢2 𝑢3 ] [> O9:=midpoint(O_, H); 𝑂9 ≔ [ 𝑢2 2 + 𝑢1 4 , 𝑢1𝑢2 − 𝑢2 2 + 𝑢3 2 4𝑢3 ] Ta chỉ ra điểm O9 là tâm của đường tròn đi qua 9 điểm trên như sau: [> sqrdist(O9, midpoint(A, B)) - sqrdist(O9, midpoint(B, C)); 0 [> sqrdist(O9, midpoint(A, B)) - sqrdist(O9, midpoint(H, C)); 0 [> D_:=intersection_point(pp_line(A, B), pp_line(H, C)); 𝐷_ ≔ [𝑢2, 0] [> sqrdist(O9, midpoint(A, B)) - sqrdist(O9, D_); 0 Biểu thức cuối cùng trả lại kết quả bằng 0 chứng tỏ rằng kết luận trong định lý là đúng hay nói cách khác định lý được chứng minh. Sau đây là chứng minh toán học của định lý. Chứng minh. Giả sử ABC có H là trực tâm. Gọi D, E, F, P, L, T lần lượt là trung điểm của các đoạn thẳng BC, CA, AB, AH, HB, HC. Gọi K, M, N lần lượt là chân của các đường cao của ABC. Gọi (O) là đường tròn ngoại tiếp DEF. Hình 3.6 29 Ta có DK = EF = 2 AB và KE // DF nên DEKF là hình thang cân. Do đó, ta có điểm K thuộc đường tròn (O). Do DL // AK, DF // BC và BC  AK nên ta có LDF = 900. Tương tự, ta có LEF = 900. Suy ra tứ giác EFDL nội tiếp hay điểm L thuộc đường tròn (O). Chứng minh tương tự ta có bốn điểm T, P, N, M cũng thuộc đường tròn (O). Định lý 3. Có bốn giao điểm được tạo thành bởi ba cặp các đường phân giác trong và ngoài của ABC cho trước. Các điểm này là tâm đường tròn nội tiếp và tâm các đường tròn bàng tiếp của tam giác. Chọn tọa độ của các điểm với hai biến độc lập là u1, u2 (tọa độ của điểm C): [> A:=Point(0, 0): B:=Point(1, 0): C:=Point(u1, u2): P:=Point(x1, x2): Điểm P khai báo ở trên là giao điểm của ba đường phân giác nếu và chỉ nếu hệ đa thức sau có kết quả bằng 0 với x1, x2 là các số không xác định được lấy hệ số trên trường ℚ(𝑢1, 𝑢2). [> polys:={on_bisector(P, A, B, C), on_bisector(P, B, C, A), on_bisector(P, C, A, B)}; polys:= {–2x2 + 2u1x2 + 2x2x1 – 2x2u1x1 – u2x22 + u2 – 2u2x1 + u2x12, –2u1x2u22 – u23 – u2u12 + 2u22x2 + 2x2u12 – u2x22 – 2u13x2 + 2u23x1 + u2x12 + 2u1x22u2 + 2u2x1u12 – 2u2x12u1 – 2u22x1x2 – 2x2u1x1 + 2u12x2x1, 2x2u1x1 – u2x12 + u2x22} Tiếp theo ta tính cơ sở Groebner bằng câu lệnh sau: [> TO:=plex(x1, x2): [> gb:=gbasis(polys, TO); gb:=[4u2x24 – 8x23u22 – 8x23u12 + 8x23u1 – 4u1x22u2 + 4u2x22u12 – 4u2x22 – u23 + 4u23x22 + 4u22x2, –u22x1 + 2x23u2 – 2u22x22 – 4u12x22 + 2u2x2u1 + 4x22u1 – 2u12u2x2 – u1u22 + 2u1u22x1 + u22 – 2u2x2] Từ kết quả trên ta thấy phương trình của biểu thức thứ nhất có 4 nghiệm với x2 và mỗi phương trình với x1 được rút ra từ phương trình của biểu thức thứ hai. Vì vậy, phương trình có 4 nghiệm ứng với 4 giao điểm. Nghiệm tổng quát liên quan đến phương trình bậc 4 trên trường ℚ(𝑢1, 𝑢2). 30 Thật khó để biểu diễn qua căn thức các giá trị này, vì cần đến nhiều tính toán với biểu thức suy ra từ kết quả của lệnh RootOf trong Maple được biết đến như là đa thức tối tiểu. Vì trong tình huống này x2 là khoảng cách từ điểm P đến đường thẳng AB, chúng ta có thể chứng minh mỗi một điểm trong 4 điểm này có khoảng cách bằng nhau đến ba cạnh của tam giác ABC, nghĩa là những điểm này là tâm của đường tròn nội tiếp và 3 đường tròn bàng tiếp tam giác. Ta tính khoảng cách giữa chúng bằng câu lệnh sau: [> con:=[sqrdist_pl(P, pp_line(A, C)) - sqrdist_pl(P, pp_line(A, B)), sqrdist_pl(P, pp_line(B, C)) - sqrdist_pl(P, pp_line(A, B))]; 𝑐𝑜𝑛 ≔ [ (−𝑢1𝑥2+𝑢2𝑥1) 2 𝑢2 2+𝑢1 2 − 𝑥2 2, 𝑢2 2−2𝑢2𝑥2+2𝑢2𝑥2𝑢1−2𝑢2 2𝑥1+𝑥2 2−2𝑥2 2𝑢1+2𝑢2𝑥2𝑥1+𝑢1 2𝑥2 2−2𝑢2𝑥1𝑢1+𝑢2 2𝑥1 2 (1−2𝑢1+𝑢1 2+𝑢2 2)−𝑥2 2 ] Tử số của mỗi trong hai biểu thức trên có thể đơn giản bằng 0 với một số giá trị đặc biệt của x1, x2. Điều này có thể kiểm chứng việc tính dạng chuẩn tắc ứng với cơ sở Groebner nói trên: [> map(u->normalf(numer(u), gb, TO), con); [0, 0] Ta cũng có thể chứng minh định lý trên như sau: Bắt đầu với A, B và giao điểm P của các đường phân giác qua A và B. Khi đó AC và BC đối xứng với AB tương ứng qua AP và BP và điểm P phải nằm trên các đường phân giác: [> A:=Point(0, 0): B:=Point(1, 0): P:=Point(u1, u2): [> l1:=pp_line(A, B): [> l2:=sym_line(l1, pp_line(A, P)); l2:=[–2u1u2, –u22 + u12, 0] [> l3:=sym_line(l1, pp_line(B, P)); l3:=[–2(u1 – 1)u2, –u22 + 1 – 2u1 + u12, 2(u1 – 1)u2] [> on_bisector(P, A, B, intersection_point(l2, l3)); 0 Biểu thức cuối cùng được đơn giản bằng 0 và vì vậy định lý được chứng minh bằng máy tính. 31 Hình 3.7 Định lý 4. (Định lý Ptô-lê-mê) Điều kiện cần và đủ để một tứ giác lồi ABCD nội tiếp được là tích hai đường chéo của nó bằng tích các cạnh đối diện. Ta xác định tọa độ các điểm trong hệ tọa độ Đề-các vuông góc như sau: [> A:=Point(a1, a2): B:=Point(b1, b2); C:=Point(c1, c2): D_:=Point(d1, d2): Bốn điểm A, B, C, D thuộc cùng một đường tròn tương đương với điều kiện sau: [> p4:=on_circle(D_, p3_circle(A, B, C)); p4:= –a1b2c22 + c1a2d22 + c1a2d12 + b1c2d22 + b1c2d12 – a2b1d22 – a2b1d12 + d1c2a12 + d1c2a22 – d1b22c2 + d1b22a2 – d1c12a2 – d1c22a2 – d1b2a12 + d1b2c12 + d1b2c22 – d1b2a22 + a1b2d22 + a1b2d12 – b2c1d22 – b2c1d12 – c2a1d22 – c2a1d12 – d2b1c22 – d2b1c12 + d2a1c22 + d2a1c12 – d2a1b22 – d2a1b12 + d2c1b22 + d2c1b12 – d2c1a22 + d2b1a22 – d2c1a12 + d2b1a12 – d1b12c2 + d1b12a2 – a12b1c2 – c1a2b22 – c1a2b12 – a1b2c12 + a2b1c22 – a22b1c2 + a2b1c12 + a12b2c1 + c2a1b12 + c2a1b22 + a22b2c1 A B C P 32 Tương tự ta cũng nhận được đa thức có bậc tương tự như trên nếu chúng ta phát biểu dưới dạng định lý về góc định hướng: [> u:=l2_angle(pp_line(A, D_), pp_line(B, D_)): [> v:=l2_angle(pp_line(A, C), pp_line(B, C)): [> w:=normal(numer(u)*denom(v) - denom(u)*numer(v)); w:= a1b2c22 – c1a2d22 – c1a2d12 – b1c2d22 – b1c2d12 + a2b1d22 + a2b1d12 – d1c2a12 – d1c2a22 + d1b22c2 – d1b22a2 + d1c12a2 + d1c22a2 + d1b2a12 – d1b2c12 – d1b2c22 + d1b2a22 – a1b2d22 – a1b2d12 + b2c1d22 + b2c1d12 + c2a1d22 + c2a1d12 + d2b1c22 + d2b1c12 – d2a1c22 – d2a1c12 + d2a1b22 + d2a1b12 – d2c1b22 – d2c1b12 + d2c1a22 – d2b1a22 + d2c1a12 – d2b1a12 + d1b12c2 – d1b12a2 + a12b1c2 + c1a2b22 + c1a2b12 + a1b2c12 – a2b1c22 + a22b1c2 – a2b1c12 – a12b2c1 – c2a1b12 – c2a1b22 – a22b2c1 [> w + p4; 0 Điều kiện này cũng tương đương với định lý Ptô-lê-mê trình bày ở trên. Biểu thức cuối cùng được đơn giản bằng 0 và vì