relations_test.py

"""
relations_test.py - Test file specifically for Problem 3: The three medians of a triangle are concurrent

This file tests the formalization of Problem 3: "The three medians of a triangle are concurrent"
using the geometric predicates defined in relations.py.

Problem 3 Formalization:
Given a triangle ABC, let:
- MAB be the midpoint of AB
- MBC be the midpoint of BC
- MAC be the midpoint of AC

The three medians AMAB, BMB, and CMC are concurrent (meet at a single point G, the centroid).

Formal statement using predicates:
Given: Triangle ABC
Let: MAB, MBC, MAC be midpoints
Then: There exists a point G such that col(A, MBC, G), col(B, MAC, G), col(C, MAB, G)
"""

from relations import predicate, geometric

def test_formalization_of_midpoints(x1,y1,x2,y2,x3,y3):
    # instantiate points
    A = geometric.Point(name="A", x=x1, y=y1)
    B = geometric.Point(name="B", x=x2, y=y2)
    C = geometric.Point(name="C", x=x3, y=y3)
    MAB = geometric.Point(name="MAB", x=(A.x + B.x) / 2, y=(A.y + B.y) / 2)
    MBC = geometric.Point(name="MBC", x=(B.x + C.x) / 2, y=(B.y + C.y) / 2)
    MAC = geometric.Point(name="MAC", x=(A.x + C.x) / 2, y=(A.y + C.y) / 2)
    G = geometric.Point(name="G", x = (A.x + B.x + C.x) / 3, y = (A.y + B.y + C.y) / 3) # Centroid
    # formalize given
    given = [
       predicate.Col(G, MAB, C),
       predicate.Col(G, MAC, B),
       predicate.Midp(MAB, A, B),
       predicate.Midp(MBC, B, C),   
       predicate.Midp(MAC, A, C)
    ]
    # formalize conclusion
    conclusion = [predicate.Col(G, MBC, A)]
    # return all statements
    return given, conclusion