diff --git a/Сивочуб Алексей/README.md b/Сивочуб Алексей/README.md new file mode 100644 index 0000000..5432b7d --- /dev/null +++ b/Сивочуб Алексей/README.md @@ -0,0 +1,18 @@ +# Теорема о квадрате +## Ссылка на видеоразбор +https://youtu.be/0Yp5sgddlko +## Код из сайта + START_INTERACTIVE;; + let coordinations = + ["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>>];; + #Square theorem + + (grobner_decide ** originate) + < lengths_eq(a,b,b,c)>>;; + END_INTERACTIVE; \ No newline at end of file diff --git a/Сивочуб Алексей/square.rkt b/Сивочуб Алексей/square.rkt new file mode 100644 index 0000000..007abc9 --- /dev/null +++ b/Сивочуб Алексей/square.rkt @@ -0,0 +1,35 @@ +#lang racket/base + +(define (square x) (* x x)) + +(define (lengths_eq x1 y1 x2 y2 x3 y3 x4 y4) +(if (equal? (+ (square(- x1 x2)) (square(- y1 y2))) +(+ (square(- x3 x4)) (square(- y3 y4)))) +(displayln "Lines (1,2) and (3,4) have the same length.") +(displayln "Lines (1,2) and (3,4) do not have the same length."))) + +(define (perpendicular x1 y1 x2 y2 x3 y3 x4 y4) +(if (equal? (+ (* (- x1 x2) (- x3 x4)) (* (- y1 y2) (- y3 y4))) 0 ) +#t #f +)) + +(define (is_midpoint x1 y1 x2 y2 x3 y3) +(if (and (equal? (* 2 x1) (+ x2 x3)) (equal? (* 2 y1) (+ y2 y3))) +(displayln "Point 1 is the midpoint of line (2,3).") +(displayln "Point 1 is not the midpoint of line (2,3).") +)) + + +(define (grobner_decide_mid a_x a_y b_x b_y c_x c_y d_x d_y m_x m_y) +(if (and (is_midpoint m_x m_y a_x a_y c_x c_y) + (perpendicular a_x a_y c_x c_y m_x m_y b_x b_y)) + (begin + (lengths_eq a_x a_y b_x b_y b_x b_y c_x c_y) + (displayln "This is a square.") + ) + (displayln "This is not a square.") +)) + + + +(grobner_decide_mid 0 0 0 2 2 2 2 0 1 1) \ No newline at end of file