-- Set-theoretic relations and functions
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Set.Relation
import Finite

-- (x, y) is the Kuratowski ordered pair.  The maplet alias x ↦ y is
-- reserved for entries of function-like graphs; both elaborate to orderedPair.
notation infixr 72 "↦" => orderedPair

-- A generous set bound containing every Kuratowski pair drawn from A and B.
-- Separation then cuts out the Cartesian product.
def productBound (A B : Set) : Set := 𝒫(𝒫(A ∪ B))
def product (A B : Set) : Set := { p ∈ productBound(A, B) | ∃ x ∈ A, ∃ y ∈ B, p = (x, y) }
notation infixl 65 "×" => product

-- Every coordinate occurring in a Kuratowski pair in r lies in union(union(r)).
def coordinateBound (r : Set) : Set := ⋃(⋃(r))
def domain (r : Set) : Set := { x ∈ coordinateBound(r) | ∃ y, (x, y) ∈ r }
def range (r : Set) : Set := { y ∈ coordinateBound(r) | ∃ x, (x, y) ∈ r }
def restrict (r A : Set) : Set := { p ∈ r | ∃ x ∈ A, ∃ y, p = (x, y) }

predicate RelationBetween (r A B : Set) := (r ⊆ A × B)
predicate Functional (r : Set) := ∀ x, ∀ y, relates(r, x, y) → ∀ z, relates(r, x, z) → y = z
predicate FunctionBetween (r A B : Set) := RelationBetween(r, A, B) ∧ Functional(r) ∧ (∀ x ∈ A, ∃ y ∈ B, relates(r, x, y))

-- A function from A to B is written f : A → B.
notation mixfix "_ : _ → _" => FunctionBetween

theorem product.pair (x y A B : Set)
  requires hx : x ∈ A
  requires hy : y ∈ B
  shows (x, y) ∈ A × B
proof
  apply product.membership.backward
  constructor
  . unfold productBound
    apply set.powerset.backward
    intros z hz
    apply set.powerset.backward
    intros w hw
    simp [orderedPair, pair.membership] at hz
    cases hz with hsingle | hpair
    . rw hsingle at hw
      simp [pair.membership] at hw
      cases hw with hwx | hwx2
      . rw hwx
        simp
      . rw hwx2
        simp
    . rw hpair at hw
      simp [pair.membership] at hw
      cases hw with hwx | hwy
      . rw hwx
        simp
      . rw hwy
        simp
  . refine ⟨x, hx, y, hy, rfl⟩

theorem product.monotone (A B C D : Set)
  requires hAC : A ⊆ C
  requires hBD : B ⊆ D
  shows (A × B ⊆ C × D)
proof
  intros p hp
  obtain ⟨bounded, x, hxA, y, hyB, pairShape⟩ := product.membership.forward with hp
  specialize hAC with x, hxA
  specialize hBD with y, hyB
  have pairIn := product.pair with hAC, hBD
  rwa pairShape

theorem RelationBetween.monotone (r A B C D : Set)
  requires relation : RelationBetween(r, A, B)
  requires hAC : A ⊆ C
  requires hBD : B ⊆ D
  shows RelationBetween(r, C, D)
proof
  unfold RelationBetween at relation
  unfold RelationBetween
  have productSubset := product.monotone with hAC, hBD
  intros p hp
  specialize relation with p, hp
  exact productSubset with p, relation

theorem orderedPair.first (a b c d : Set)
  requires h : (a, b) = (c, d)
  shows a = c
proof
  simp [orderedPair] at h
  have firstA := pair.left at {a, a}, {a, b}
  rw h at firstA
  simp [pair.membership] at firstA
  cases firstA with haa | hab
  have cMember := pair.left at c, c
  rw ← haa at cMember
  simp [pair.membership] at cMember
  cases cMember with hca | hca2
  simp
  simp
  have cMember := pair.left at c, d
  rw ← hab at cMember
  simp [pair.membership] at cMember
  cases cMember with hca | hca2
  simp
  simp

theorem orderedPair.injective (a b c d : Set)
  requires h : (a, b) = (c, d)
  shows a = c ∧ b = d
proof
  constructor
  exact orderedPair.first with h
  have first := orderedPair.first with h
  rw first at h
  simp [orderedPair] at h
  have outer := pair.cancel_left with h
  exact pair.cancel_left with outer

theorem range.contains (x y r : Set)
  requires hPair : (x, y) ∈ r
  shows y ∈ range(r)
proof
  apply range.membership.backward
  constructor
  unfold coordinateBound
  apply set.union.backward
  witness {x, y}
  constructor
  apply set.union.backward
  witness (x, y)
  constructor
  exact hPair
  simp [orderedPair, pair.membership]
  exact pair.right
  witness x
  exact hPair

theorem range.empty
  shows range(∅) = ∅
proof
  ext y
  simp [range.membership, set.empty]

theorem range.singleton_pair (x y : Set)
  shows range({(x, y)}) = {y}
proof
  ext z
  constructor
  intro hz
  simp [range.membership] at hz
  cases hz with hBound ∧ hWitness
  obtain ⟨source, hPair⟩ := hWitness
  have hOnlyPair := singleton.membership.forward with hPair
  have hCoordinates := orderedPair.injective with hOnlyPair
  cases hCoordinates with hSource ∧ hValue
  apply singleton.membership.backward
  exact hValue
  intro hz
  have hValue := singleton.membership.forward with hz
  rw hValue
  have hPair := singleton.self at (x, y)
  exact range.contains with hPair

theorem range.pair_of_pairs (a b c d : Set)
  shows range({(a, b), (c, d)}) = {b, d}
proof
  ext z
  constructor
  . intro hz
    simp [range.membership] at hz
    obtain ⟨hBound, source, hPair⟩ := hz
    simp [pair.membership] at hPair
    cases hPair with hFirst | hSecond
    . obtain ⟨hSource, hValue⟩ := orderedPair.injective with hFirst
      rw hValue
      exact pair.left
    . obtain ⟨hSource, hValue⟩ := orderedPair.injective with hSecond
      rw hValue
      exact pair.right
  . intro hz
    simp [pair.membership] at hz
    cases hz with hFirst | hSecond
    . rw hFirst
      exact range.contains with (pair.left at (a, b), (c, d))
    . rw hSecond
      exact range.contains with (pair.right at (a, b), (c, d))