-- Relations and equivalence relations
-- 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.Relation.Core
import Algebra.Foundation

predicate RelationOn (r A : Set) := RelationBetween(r, A, A)
predicate IrreflexiveOn (A r : Set) := ∀ x ∈ A, ¬relates(r, x, x)
predicate SymmetricOn (A r : Set) := ∀ x ∈ A, ∀ y ∈ A, relates(r, x, y) → relates(r, y, x)
predicate ConnectedOn (A r : Set) := ∀ x ∈ A, ∀ y ∈ A, x ≠ y → (relates(r, x, y) ∨ relates(r, y, x))
predicate Equivalence (A r : Set) := RelationOn(r, A) ∧ (ReflexiveOn(A, r) ∧ (SymmetricOn(A, r) ∧ TransitiveOn(A, r)))

theorem RelationBetween.bounds (r A B x y : Set)
  requires relation : RelationBetween(r, A, B)
  requires hxy : relates(r, x, y)
  shows x ∈ A ∧ y ∈ B
proof
  unfold RelationBetween at relation
  specialize relation with (x, y), hxy
  obtain ⟨bounded, a, haA, b, hbB, pairShape⟩ := product.membership.forward with relation
  obtain (xEquals, yEquals) := orderedPair.injective with pairShape
  rw [xEquals, yEquals]
  refine ⟨haA, hbB⟩

-- Converse is bounded by the reversed Cartesian product, so it is a set.
def converse (r A B : Set) : Set := { p ∈ B × A | ∃ x ∈ A, ∃ y ∈ B, p = (y, x) ∧ relates(r, x, y) }

theorem converse.relates (r A B x y : Set)
  requires hx : x ∈ A
  requires hy : y ∈ B
  requires hxy : relates(r, x, y)
  shows relates(converse(r, A, B), y, x)
proof
  simp [relates, converse.membership, product.pair]

theorem converse.reflects (r A B x y : Set)
  requires hxy : relates(converse(r, A, B), y, x)
  shows relates(r, x, y)
proof
  unfold relates at hxy
  simp [converse.membership] at hxy
  rcases hxy with ⟨hProduct, a, haA, b, hbB, hPair, hab⟩
  obtain ⟨hyb, hxa⟩ := orderedPair.injective with hPair
  rw ← hxa at hab
  rwa ← hyb at hab

theorem converse.relation (r A B : Set)
  shows RelationBetween(converse(r, A, B), B, A)
proof
  simp [RelationBetween, Subset]

theorem converse.bounds (r A B x y : Set)
  requires hxy : relates(converse(r, A, B), y, x)
  shows y ∈ B ∧ x ∈ A
proof
  unfold relates at hxy
  simp [converse.membership] at hxy
  rcases hxy with ⟨hProduct, a, haA, b, hbB, hPair, hab⟩
  obtain ⟨hyb, hxa⟩ := orderedPair.injective with hPair
  constructor
  rwa hyb
  rwa hxa

theorem Equivalence.relation (A r : Set)
  requires h : Equivalence(A, r)
  shows RelationOn(r, A)
proof
  rcases h with ⟨relation, laws⟩
  exact relation

theorem Equivalence.reflexive (A r : Set)
  requires h : Equivalence(A, r)
  shows ReflexiveOn(A, r)
proof
  simp [Equivalence]

theorem Equivalence.symmetric (A r : Set)
  requires h : Equivalence(A, r)
  shows SymmetricOn(A, r)
proof
  simp [Equivalence]

theorem Equivalence.transitive (A r : Set)
  requires h : Equivalence(A, r)
  shows TransitiveOn(A, r)
proof
  simp [Equivalence]