-- The coordinates of an ordered pair, read back from the pair
-- 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.Tuple
import Core
import Relation

-- A structure bundled as a nested pair is read back through fst and snd:
-- fst((x, y)) = x and snd((x, y)) = y.
def fstCandidates (p : Set) : Set := { x ∈ ⋃ p | ∃ y, p = (x, y) }
def sndCandidates (p : Set) : Set := { y ∈ ⋃ p | ∃ x, p = (x, y) }
def fst (p : Set) : Set := ⋃ fstCandidates(p)
def snd (p : Set) : Set := ⋃ sndCandidates(p)

theorem orderedPair.first_in_union (x y : Set)
  shows x ∈ ⋃ (x, y)
proof
  have inSingleton : x ∈ {x} := singleton.self at x
  have singletonIn : {x} ∈ (x, y) by simp [orderedPair, singleton, pair.membership]
  exact union.contains with singletonIn, inSingleton

theorem orderedPair.second_in_union (x y : Set)
  shows y ∈ ⋃ (x, y)
proof
  have inPair : y ∈ {x, y} := pair.right at x, y
  have pairIn : {x, y} ∈ (x, y) by simp [orderedPair, singleton, pair.membership]
  exact union.contains with pairIn, inPair

theorem fstCandidates.pair (x y : Set)
  shows fstCandidates((x, y)) = {x}
proof
  ext z
  constructor
  . intro member
    obtain ⟨bounded, w, shape⟩ := fstCandidates.membership.forward with member
    have same : x = z := orderedPair.first with shape
    rw ← same
    exact singleton.self at x
  . intro member
    have same : z = x := singleton.membership.forward with member
    have inUnion : x ∈ ⋃ (x, y) := orderedPair.first_in_union at x, y
    rw same
    apply fstCandidates.membership.backward
    refine ⟨inUnion, y, rfl⟩

theorem sndCandidates.pair (x y : Set)
  shows sndCandidates((x, y)) = {y}
proof
  ext z
  constructor
  . intro member
    obtain ⟨bounded, w, shape⟩ := sndCandidates.membership.forward with member
    obtain ⟨sameFirst, same⟩ := orderedPair.injective with shape
    rw ← same
    exact singleton.self at y
  . intro member
    have same : z = y := singleton.membership.forward with member
    have inUnion : y ∈ ⋃ (x, y) := orderedPair.second_in_union at x, y
    rw same
    apply sndCandidates.membership.backward
    refine ⟨inUnion, x, rfl⟩

theorem fst.pair (x y : Set)
  shows fst((x, y)) = x
proof
  simp [fst, fstCandidates.pair, union.singleton]

theorem snd.pair (x y : Set)
  shows snd((x, y)) = y
proof
  simp [snd, sndCandidates.pair, union.singleton]