#!/usr/bin/env python3
"""A relation is a set of pairs, a function is a relation with one property, a graph is a relation drawn.

Run:  python3 relations_and_functions.py

Everything here is a set of ordered pairs. 'Divides' on {1, ..., 6} is
one; its domain and range are read off the pairs; 'is a function' is a
property a set of pairs has or lacks; composition is a product of
relations; a graph is a relation drawn as arrows. The program builds each
object as a Python set of tuples and checks the textbook claims on every
relation over a small base set, where the check is a proof.
"""

from itertools import product

BASE = (1, 2, 3)
PAIRS = [(x, y) for x in BASE for y in BASE]
RELATIONS = [frozenset(p for p, keep in zip(PAIRS, bits) if keep) for bits in product((True, False), repeat=9)]
TWO = [(x, y) for x in (1, 2) for y in (1, 2)]
RELATIONS2 = [frozenset(p for p, keep in zip(TWO, bits) if keep) for bits in product((True, False), repeat=4)]


def dom(r):
    return {x for x, y in r}


def ran(r):
    return {y for x, y in r}


def inverse(r):
    return frozenset((y, x) for x, y in r)


def compose(r, s):
    """The relation product ρσ of Simovici and Djeraba: first ρ, then σ.
    Jech and Kunen write the same thing as σ ∘ ρ."""
    return frozenset((x, z) for x, y in r for y2, z in s if y == y2)


def is_function(r):
    """Jech, Kunen, Simovici: (x, y) ∈ f and (x, z) ∈ f imply y = z."""
    return all(y == z for x, y in r for x2, z in r if x == x2)


def one_to_one(r):
    return all(x == x2 for x, y in r for x2, y2 in r if y == y2)


def show(r):
    return "{" + ", ".join(f"({x}, {y})" for x, y in sorted(r)) + "}" if r else "∅"


def main() -> None:
    print("1. A RELATION IS A SET OF ORDERED PAIRS")
    six = range(1, 7)
    divides = frozenset((m, n) for m in six for n in six if n % m == 0)
    print(f"   'm divides n' on {{1, ..., 6}} is the set of {len(divides)} pairs")
    print("   " + show(divides))
    print(f"   2 divides 6?  (2, 6) ∈ δ: {(2, 6) in divides}     4 divides 6?  (4, 6) ∈ δ: {(4, 6) in divides}")
    print(f"   dom(δ) = {sorted(dom(divides))}   ran(δ) = {sorted(ran(divides))}")
    print("   'x ρ y' is just a way of writing (x, y) ∈ ρ; the relation IS the set.")
    print()

    print("2. A FUNCTION IS A RELATION WITH ONE PROPERTY")
    sq = frozenset((x, x * x) for x in range(-3, 4))
    root = inverse(sq)
    print(f"   square = {show(sq)}")
    print(f"   is a function: {is_function(sq)}   (each x has one square)")
    print(f"   root = square⁻¹ = {show(root)}")
    print(f"   is a function: {is_function(root)}   (4 has partners 2 and -2)")
    print("   f(x) means 'the unique y with (x, y) ∈ f'; a Python dict is the same")
    print(f"   object:  dict(square) = {dict(sorted(sq))}")
    print()

    print("3. FUNCTIONS, ONE-TO-ONE RELATIONS, INVERSES: EVERY RELATION ON {1, 2, 3}")
    funcs = [r for r in RELATIONS if is_function(r)]
    total = [r for r in funcs if dom(r) == set(BASE)]
    inj = [r for r in total if one_to_one(r)]
    sur = [r for r in total if ran(r) == set(BASE)]
    bij = [r for r in inj if ran(r) == set(BASE)]
    print(f"   relations on {{1, 2, 3}}: {len(RELATIONS)}   functions (partial): {len(funcs)}   with domain all of {{1, 2, 3}}: {len(total)} = 3^3")
    print(f"   injections: {len(inj)}   surjections: {len(sur)}   bijections: {len(bij)} = 3!   (on a finite set, injective = surjective = bijective: {inj == sur})")
    thm = all(is_function(r) == one_to_one(inverse(r)) for r in RELATIONS)
    print(f"   ρ is a function  iff  ρ⁻¹ is one-to-one, all {len(RELATIONS)} relations: {thm}   (Simovici–Djeraba, Theorem 1.37)")
    inv = all(inverse(inverse(r)) == r and dom(inverse(r)) == ran(r) for r in RELATIONS)
    print(f"   (ρ⁻¹)⁻¹ = ρ and dom(ρ⁻¹) = ran(ρ): {inv}")
    print()

    print("4. COMPOSITION IS A PRODUCT OF RELATIONS")
    r = frozenset({(1, 2), (2, 3)})
    s = frozenset({(2, 10), (3, 20)})
    print(f"   ρ = {show(r)}, σ = {show(s)}:  ρσ = {show(compose(r, s))}   ('first ρ, then σ')")
    assoc = all(compose(compose(a, b), c) == compose(a, compose(b, c)) for a in RELATIONS2 for b in RELATIONS2 for c in RELATIONS2)
    invp = all(inverse(compose(a, b)) == compose(inverse(b), inverse(a)) for a in RELATIONS2 for b in RELATIONS2)
    fn = all((not (is_function(a) and is_function(b))) or is_function(compose(a, b)) for a in RELATIONS2 for b in RELATIONS2)
    print(f"   on all {len(RELATIONS2)} relations on {{1, 2}}:  (ρσ)τ = ρ(στ): {assoc}   (ρσ)⁻¹ = σ⁻¹ρ⁻¹: {invp}   product of functions is a function: {fn}")
    print("   Jech and Kunen write σ ∘ ρ for Simovici's ρσ: same set, letters swapped.")
    print()

    print("5. A GRAPH IS A RELATION DRAWN AS ARROWS")
    likes = frozenset({("a", "a"), ("b", "c"), ("c", "b"), ("d", "c")})
    print(f"   'x likes y' from the quantifiers lesson: {show(likes)}")
    for x in "abcd":
        out = sorted(y for x2, y in likes if x2 == x)
        print(f"     {x} → {', '.join(out) if out else '(nobody)'}")
    sym = likes == inverse(likes)
    print(f"   symmetric (an undirected graph): {sym};  an undirected graph is a relation equal to its inverse,")
    print("   or a set of two-element sets {x, y}. A membership table x ∈ y is a directed graph too:")
    print("   Kunen's Exercise I.2.1 draws seven of them, and the axiom katas page evaluates the axioms on each.")
    print()

    print("6. A FUNCTION IS ITS PAIRS, NOT ITS FORMULA")
    f = frozenset((x, x * x) for x in range(-2, 3))
    g = frozenset((x, abs(x) ** 2) for x in range(-2, 3))
    h = frozenset((x, (x * x) % 7) for x in range(-2, 3))
    print(f"   y = x² and y = |x|² on {{-2, ..., 2}}: same set of pairs: {f == g}   so one function, by extensionality")
    print(f"   y = x² and y = x² mod 7 on {{-2, ..., 2}}: {f == h}   (they differ nowhere here) ")
    print("   Two formulas that agree on every input define one function; a function")
    print("   is the table of its values, which is why a table in a database is one.")
    print()

    print("7. IMAGES OF SETS UNDER A RELATION: HRBACEK AND JECH, EXERCISES 2.3 AND 2.4")
    print("   R[A] = {y : x R y for some x in A}; R⁻¹[B] = {x : x R y for some y in B}.")

    def image(r, a):
        return {y for x, y in r if x in a}

    subsets = [frozenset(c) for r_ in range(4) for c in __import__("itertools").combinations(BASE, r_)]
    a_ = all(image(r, a | b) == image(r, a) | image(r, b) for r in RELATIONS for a in subsets for b in subsets)
    b_ = all(image(r, a & b) <= image(r, a) & image(r, b) for r in RELATIONS for a in subsets for b in subsets)
    c_ = all(image(r, a - b) >= image(r, a) - image(r, b) for r in RELATIONS for a in subsets for b in subsets)
    print(f"   2.3(a) R[A ∪ B] = R[A] ∪ R[B]: {a_}    (b) R[A ∩ B] ⊆ R[A] ∩ R[B]: {b_}    (c) R[A − B] ⊇ R[A] − R[B]: {c_}")
    strict = next((r, a, b) for r in RELATIONS for a in subsets for b in subsets if image(r, a & b) != image(r, a) & image(r, b))
    r, a, b = strict
    print(f"   2.3(d) ⊆ is not =: R = {show(r)}, A = {set(a)}, B = {set(b)}:")
    print(f"          R[A ∩ B] = {image(r, a & b) or '∅'} but R[A] ∩ R[B] = {image(r, a) & image(r, b)}")
    e_ = all(image(inverse(r), image(r, a)) >= a & dom(r) for r in RELATIONS for a in subsets)
    print(f"   2.3(f) R⁻¹[R[A]] ⊇ A ∩ dom R, all {len(RELATIONS) * len(subsets)} cases: {e_}")
    d_ = all(image(r, frozenset(BASE)) == ran(r) and image(inverse(r), frozenset(BASE)) == dom(r) for r in RELATIONS)
    f_ = all(compose(r, inverse(r)) >= {(x, x) for x in dom(r)} for r in RELATIONS)
    print(f"   2.4(a) R[X] = ran R and R⁻¹[Y] = dom R: {d_}    2.4(e) R ∘ R⁻¹ ⊇ Id on dom R: {f_}")
    print("   A relation can merge, so the image of an intersection can be smaller")
    print("   than the intersection of the images; a one-to-one relation cannot, and")
    print("   for it (b) and (c) become equalities (Simovici–Djeraba, Theorem 1.62).")
    print()

    print("8. SULLIVAN'S FOUR PICTURES OF A FUNCTION, ONE TEST FOR ALL")
    print("   Precalculus 2.1 shows a function as a mapping diagram, a set of pairs, an")
    print("   equation and a machine. Each is the same set of pairs, and is_function")
    print("   asks one thing of it: no two pairs with the same first member.")
    examples = [
        ("Fig. 6, substance → specific heat",
         {("air", 1.00), ("lead", 0.128), ("graphite", 0.711), ("copper", 0.387), ("water", 4.18)}),
        ("year → price of a stamp, 2018",
         {(2018, 0.49), (2018, 0.50)}),
        ("Fig. 8, menu item → price",
         {("Cheeseburger", 1), ("McChicken", 1), ("Bacon McDouble", 2), ("Triple Cheeseburger", 3), ("Happy Meal", 3)}),
        ("Fig. 10, gestation → life expectancy",
         {(122, 5), (201, 8), (284, 15), (240, 12), (240, 20)}),
        ("Example 3(a)", {(1, 4), (2, 5), (3, 6), (4, 7)}),
        ("Example 3(b)", {(1, 4), (2, 4), (3, 5), (6, 10)}),
        ("Example 3(c)", {(-3, 9), (-2, 4), (0, 0), (1, 1), (-3, 8)}),
        ("Example 4, y = 2x − 5 on x = −2..2", {(x, 2 * x - 5) for x in range(-2, 3)}),
        ("Example 5, x² + y² = 1 on a grid",
         {(x / 4, y / 4) for x in range(-4, 5) for y in range(-4, 5) if x * x + y * y == 16}),
    ]
    for name, r in examples:
        verdict = "a function" if is_function(r) else "not a function"
        extra = ""
        rs = sorted(r, key=lambda pair: (str(pair[0]), str(pair[1])))
        if not is_function(r):
            x = next(x for x, y in rs for x2, z in rs if x == x2 and y != z)
            extra = f": {x} has two partners"
        elif not one_to_one(r):
            y = next(y for x, y in rs for x2, y2 in rs if y == y2 and x != x2)
            extra = f", and two inputs share the output {y}, which is allowed"
        print(f"   {name:<38} {verdict}{extra}")
    print("   The machine picture is the same test read aloud: one output per input.")
    print("   'y = f(x)' names the unique partner of x, and the WARNING in the book,")
    print("   that f(x) is not f times x, is the warning that f is a set, not a number.")


if __name__ == "__main__":
    main()