32 lines
1.5 KiB
Markdown
32 lines
1.5 KiB
Markdown
# Перевод геометрических свойств в координаты
|
|
## Ссылка на видеоразбор
|
|
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;; |