Перевод геометрических свойств в координаты

Ковтун Богдан/README.md

@@ -0,0 +1,32 @@
+# Перевод геометрических свойств в координаты
+## Ссылка на видеоразбор
+https://youtu.be/Nu43zpDrWuM
+## Код из книги
+    let coordinations =
+    ["collinear", (** Points 1, 2 and 3 lie on a common line **)
+    <<(1_x - 2_x) * (2_y - 3_y) = (1_y - 2_y) * (2_x - 3_x)>>;
+    "parallel", (** Lines (1,2) and (3,4) are parallel **)
+    <<(1_x - 2_x) * (3_y - 4_y) = (1_y - 2_y) * (3_x - 4_x)>>;
+    "perpendicular", (** Lines (1,2) and (3,4) are perpendicular **)
+    <<(1_x - 2_x) * (3_x - 4_x) + (1_y - 2_y) * (3_y - 4_y) = 0>>;
+    "lengths_eq", (** Lines (1,2) and (3,4) have the same length **)
+    <<(1_x - 2_x)^2 + (1_y - 2_y)^2 = (3_x - 4_x)^2 + (3_y - 4_y)^2>>;
+    "is_midpoint", (** Point 1 is the midpoint of line (2,3) **)
+    <<2 * 1_x = 2_x + 3_x /\ 2 * 1_y = 2_y + 3_y>>;
+    "is_intersection", (** Lines (2,3) and (4,5) meet at point 1 **)
+    <<(1_x - 2_x) * (2_y - 3_y) = (1_y - 2_y) * (2_x - 3_x) /\
+     (1_x - 4_x) * (4_y - 5_y) = (1_y - 4_y) * (4_x - 5_x)>>;
+    "=", (** Points 1 and 2 are the same **)
+    <<(1_x = 2_x) /\ (1_y = 2_y)>>];;
+
+    let coordinate = onatoms
+    (fun (R(a,args)) ->
+    let xtms,ytms = unzip
+     (map (fun (Var v) -> Var(v^"_x"),Var(v^"_y")) args) in
+    let xs = map (fun n -> string_of_int n^"_x") (1--length args)
+    and ys = map (fun n -> string_of_int n^"_y") (1--length args) in
+    subst (fpf (xs @ ys) (xtms @ ytms)) (assoc a coordinations));;
+
+    START_INTERACTIVE;;
+    coordinate <<collinear(a,b,c) ==> collinear(b,a,c)>>;;
+    END_INTERACTIVE;;