-- Singletons, pairs, power sets, unions of families, and products:
-- the basic set constructions and their laws
-- 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.Powerset
import Algebra

-- Singletons and pairs

theorem singleton.subset_iff (x A : Set)
  shows {x} ⊆ A ↔ x ∈ A
proof
  constructor
  . intro h
    exact h with x, (singleton.self at x)
  . intros h y hy
    simp [singleton.membership] at hy
    rwa hy

theorem singleton.injective (x y : Set)
  requires h : {x} = {y}
  shows x = y
proof
  have member : x ∈ {y}
    rw ← h
    exact singleton.self
  simpa [singleton.membership] using member

theorem singleton.eq_iff (x y : Set)
  shows {x} = {y} ↔ x = y
proof
  constructor
  . intro h
    exact singleton.injective with h
  . intro h
    rw h
    rfl

theorem subset_singleton.cases (Y x : Set)
  requires h : Y ⊆ {x}
  shows Y = ∅ ∨ Y = {x}
proof
  by_contra neither
  have nonempty : Y ≠ ∅
    intro hY
    apply neither
    left
    exact hY
  obtain ⟨y, hy⟩ := Nonempty.of_ne_empty with nonempty
  have hyx : y ∈ {x} := h with y, hy
  simp [singleton.membership] at hyx
  apply neither
  right
  ext z
  constructor
  . intro hz
    exact h with z, hz
  . intro hz
    simp [singleton.membership] at hz
    rwa [hz, ← hyx]

theorem pair.commutative (x y : Set)
  shows {x, y} = {y, x}
proof
  ext z
  simp

theorem pair.eq_union2 (x y : Set)
  shows {x, y} = {x} ∪ {y}
proof
  ext z
  simp

theorem pair.self (x : Set)
  shows {x, x} = {x}
proof
  ext z
  simp

theorem pair.subset_iff (x y A : Set)
  shows {x, y} ⊆ A ↔ x ∈ A ∧ y ∈ A
proof
  constructor
  . intro h
    constructor
    . exact h with x, (pair.left at x, y)
    . exact h with y, (pair.right at x, y)
  . intros h z hz
    simp at hz
    cases hz with hx | hy
    . rw hx
      exact h.left
    . rw hy
      exact h.right

theorem singleton.subset_pair (x y : Set)
  shows {x} ⊆ {x, y}
proof
  simp

theorem pair.cancel_right (a b c : Set)
  requires h : {a, c} = {b, c}
  shows a = b
proof
  have member : a ∈ {b, c}
    rw ← h
    exact pair.left
  simp at member
  cases member with hab | hac
  . exact hab
  . have other : b ∈ {a, c}
      rw h
      exact pair.left
    simp at other
    cases other with hba | hbc
    . symm
      exact hba
    . rw [hac, hbc]
      rfl

theorem singleton.eq_pair_iff (x a b : Set)
  shows {x} = {a, b} ↔ x = a ∧ x = b
proof
  constructor
  . intro h
    have inA : a ∈ {x}
      rw h
      exact pair.left
    have inB : b ∈ {x}
      rw h
      exact pair.right
    simp [singleton.membership] at inA
    simp [singleton.membership] at inB
    constructor
    . symm
      exact inA
    . symm
      exact inB
  . intro h
    rw [← h.left, ← h.right]
    symm
    exact pair.self

theorem difference.singleton_membership (z A x : Set)
  shows z ∈ A ∖ {x} ↔ z ∈ A ∧ z ≠ x
proof
  simp [difference.membership, singleton.membership]

theorem difference.singleton_of_absent (A x : Set)
  requires h : ¬(x ∈ A)
  shows A ∖ {x} = A
proof
  ext z
  simp [difference.membership, singleton.membership]

-- Power sets

theorem powerset.self (A : Set)
  shows A ∈ 𝒫(A)
proof
  exact powerset.membership_iff.backward with (Subset.reflexive at A)

theorem powerset.empty_member (A : Set)
  shows ∅ ∈ 𝒫(A)
proof
  exact powerset.membership_iff.backward with (empty.subset at A)

theorem powerset.subset_iff (A B : Set)
  shows 𝒫(A) ⊆ 𝒫(B) ↔ A ⊆ B
proof
  constructor
  . intro h
    have member : A ∈ 𝒫(B) := h with A, (powerset.self at A)
    simpa [powerset.membership_iff] using member
  . intro h
    exact powerset.monotone with h

theorem powerset.injective (A B : Set)
  requires h : 𝒫(A) = 𝒫(B)
  shows A = B
proof
  apply Subset.antisymmetric
  . exact powerset.subset_iff.forward with (Subset.of_eq with h)
  . symm at h
    exact powerset.subset_iff.forward with (Subset.of_eq with h)

theorem powerset.intersection (A B : Set)
  shows 𝒫(A ∩ B) = 𝒫(A) ∩ 𝒫(B)
proof
  ext z
  simp [powerset.membership_iff, intersection.membership, Subset.intersection_iff]

theorem powerset.union2_subset (A B : Set)
  shows 𝒫(A) ∪ 𝒫(B) ⊆ 𝒫(A ∪ B)
proof
  intros z hz
  simp [union2.membership, powerset.membership_iff] at hz
  simp [powerset.membership_iff]

theorem powerset.union_subset (A : Set)
  shows A ⊆ 𝒫(⋃(A))
proof
  intros z hz
  simp [powerset.membership_iff]
  intros w hw
  exact union.contains with hz, hw

theorem powerset.union (A : Set)
  shows ⋃(𝒫(A)) = A
proof
  apply Subset.antisymmetric
  . apply union.subset
    intros z hz
    simpa [powerset.membership_iff] using hz
  . intros z hz
    exact union.contains with (powerset.self at A), hz

-- Unions of families

theorem union.membership (x S : Set)
  shows x ∈ ⋃(S) ↔ ∃ A ∈ S, x ∈ A
proof
  simp [set.union]

theorem union.subset_of_member (A S : Set)
  requires h : A ∈ S
  shows A ⊆ ⋃(S)
proof
  intros z hz
  exact union.contains with h, hz

theorem union.monotone (S T : Set)
  requires h : S ⊆ T
  shows ⋃(S) ⊆ ⋃(T)
proof
  apply union.subset
  intros A hA
  exact union.subset_of_member with (h with A, hA)

theorem union.pair (A B : Set)
  shows ⋃({A, B}) = A ∪ B
proof
  apply Subset.antisymmetric
  . apply union.subset
    intros C hC
    simp at hC
    cases hC with hA | hB
    . rw hA
      exact union2.subset_left
    . rw hB
      exact union2.subset_right
  . intros z hz
    simp [union2.membership] at hz
    cases hz with hA | hB
    . exact union.contains with (pair.left at A, B), hA
    . exact union.contains with (pair.right at A, B), hB

theorem union.union2 (S T : Set)
  shows ⋃(S ∪ T) = ⋃(S) ∪ ⋃(T)
proof
  apply Subset.antisymmetric
  . apply union.subset
    intros A hA
    simp [union2.membership] at hA
    cases hA with hS | hT
    . exact union2.subset_of_subset_left with (union.subset_of_member with hS)
    . exact union2.subset_of_subset_right with (union.subset_of_member with hT)
  . apply union2.subset
    . exact union.monotone with (union2.subset_left at S, T)
    . exact union.monotone with (union2.subset_right at S, T)

theorem union.intersection_subset (S T : Set)
  shows ⋃(S ∩ T) ⊆ ⋃(S) ∩ ⋃(T)
proof
  apply Subset.intersection_iff.backward
  constructor
  . exact union.monotone with (intersection.subset_left at S, T)
  . exact union.monotone with (intersection.subset_right at S, T)

theorem union.eq_empty_iff (S : Set)
  shows ⋃(S) = ∅ ↔ ∀ A ∈ S, A = ∅
proof
  constructor
  . intros h A hA
    apply Subset.empty_iff.forward
    rw ← h
    exact union.subset_of_member with hA
  . intro h
    apply Subset.empty_iff.forward
    apply union.subset
    intros A hA
    have empty : A = ∅ := h with A, hA
    rw empty
    exact Subset.reflexive

theorem union.subset_powerset (S A : Set)
  requires h : S ⊆ 𝒫(A)
  shows ⋃(S) ⊆ A
proof
  apply union.subset
  intros B hB
  have member : B ∈ 𝒫(A) := h with B, hB
  simpa [powerset.membership_iff] using member

-- Products

theorem product.pair_membership (x y A B : Set)
  shows (x, y) ∈ A × B ↔ x ∈ A ∧ y ∈ B
proof
  constructor
  . intro h
    simp [product.membership] at h
    obtain ⟨bound, a, ha, b, hb, equation⟩ := h
    obtain ⟨hxa, hyb⟩ := orderedPair.injective with equation
    rw [hxa, hyb]
    constructor
    . exact ha
    . exact hb
  . intro h
    exact product.pair with h.left, h.right

theorem product.left_empty (B : Set)
  shows ∅ × B = ∅
proof
  ext p
  constructor
  . intro hp
    simp [product.membership] at hp
  . intro hp
    exact empty.subset at ∅ × B with p, hp

theorem product.right_empty (A : Set)
  shows A × ∅ = ∅
proof
  ext p
  constructor
  . intro hp
    simp [product.membership] at hp
  . intro hp
    exact empty.subset at A × ∅ with p, hp

theorem product.eq_empty_iff (A B : Set)
  shows A × B = ∅ ↔ A = ∅ ∨ B = ∅
proof
  constructor
  . intro h
    by_contra neither
    have hA : A ≠ ∅
      intro hA
      apply neither
      left
      exact hA
    have hB : B ≠ ∅
      intro hB
      apply neither
      right
      exact hB
    obtain ⟨a, ha⟩ := Nonempty.of_ne_empty with hA
    obtain ⟨b, hb⟩ := Nonempty.of_ne_empty with hB
    have member : (a, b) ∈ A × B := product.pair with ha, hb
    rw h at member
    simpa using member
  . intro h
    cases h with hA | hB
    . rw hA
      exact product.left_empty
    . rw hB
      exact product.right_empty

theorem product.union2_left (A B C : Set)
  shows (A ∪ B) × C = (A × C) ∪ (B × C)
proof
  ext p
  constructor
  . intro hp
    simp [product.membership] at hp
    obtain ⟨bound, a, ha, c, hc, equation⟩ := hp
    rw equation
    simp [union2.membership] at ha
    simp [union2.membership]
    cases ha with hA | hB
    . left
      exact product.pair with hA, hc
    . right
      exact product.pair with hB, hc
  . intro hp
    simp [union2.membership] at hp
    cases hp with hAC | hBC
    . exact product.monotone at A, C, A ∪ B, C with (union2.subset_left at A, B), (Subset.reflexive at C), p, hAC
    . exact product.monotone at B, C, A ∪ B, C with (union2.subset_right at A, B), (Subset.reflexive at C), p, hBC

theorem product.union2_right (A B C : Set)
  shows A × (B ∪ C) = (A × B) ∪ (A × C)
proof
  ext p
  constructor
  . intro hp
    simp [product.membership] at hp
    obtain ⟨bound, a, ha, b, hb, equation⟩ := hp
    rw equation
    simp [union2.membership] at hb
    simp [union2.membership]
    cases hb with hB | hC
    . left
      exact product.pair with ha, hB
    . right
      exact product.pair with ha, hC
  . intro hp
    simp [union2.membership] at hp
    cases hp with hAB | hAC
    . exact product.monotone at A, B, A, B ∪ C with (Subset.reflexive at A), (union2.subset_left at B, C), p, hAB
    . exact product.monotone at A, C, A, B ∪ C with (Subset.reflexive at A), (union2.subset_right at B, C), p, hAC

theorem product.difference_left (A B C : Set)
  shows (A ∖ B) × C = (A × C) ∖ (B × C)
proof
  ext p
  constructor
  . intro hp
    obtain ⟨_, a, ha, c, hc, rfl⟩ := product.membership.forward with hp
    obtain ⟨inA, notInB⟩ := difference.membership.forward with ha
    apply difference.membership.backward
    constructor
    . exact product.pair with inA, hc
    . intro inB
      have coordinates := product.pair_membership.forward with inB
      exact notInB with coordinates.left
  . intro hp
    obtain ⟨inAC, notInBC⟩ := difference.membership.forward with hp
    obtain ⟨_, a, ha, c, hc, rfl⟩ := product.membership.forward with inAC
    have notInB : ¬a ∈ B
      intro inB
      exact notInBC with (product.pair with inB, hc)
    have inDifference := difference.membership.backward with ⟨ha, notInB⟩
    exact product.pair with inDifference, hc

theorem product.symmetricDifference_left (A B C : Set)
  shows (A △ B) × C = (A × C) △ (B × C)
proof
  unfold symmetricDifference
  rw [product.union2_left, product.difference_left, product.difference_left]
  rfl

theorem product.intersection (A B C D : Set)
  shows (A ∩ B) × (C ∩ D) = (A × C) ∩ (B × D)
proof
  ext p
  constructor
  . intro hp
    simp [product.membership] at hp
    obtain ⟨bound, a, ha, c, hc, equation⟩ := hp
    rw equation
    simp [intersection.membership] at ha
    simp [intersection.membership] at hc
    simp [intersection.membership]
    constructor
    . exact product.pair with ha.left, hc.left
    . exact product.pair with ha.right, hc.right
  . intro hp
    simp [intersection.membership] at hp
    obtain ⟨hAC, hBD⟩ := hp
    simp [product.membership] at hAC
    obtain ⟨bound, a, ha, c, hc, equation⟩ := hAC
    rw equation at hBD
    rw equation
    have coordinates := product.pair_membership.forward with hBD
    apply product.pair
    . simp [intersection.membership]
    . simp [intersection.membership]

-- Products with disjoint factors are disjoint.
theorem product.disjoint_of_right (A B C D : Set)
  requires disjoint : Disjoint(B, D)
  shows Disjoint(A × B, C × D)
proof
  have separated := Disjoint.iff.forward with disjoint
  apply Disjoint.iff.backward
  intros p hp hp2
  obtain ⟨bound, x, hx, y, hy, shape⟩ := product.membership.forward with hp
  rw shape at hp2
  have coordinates := product.pair_membership.forward with hp2
  exact separated with y, hy, coordinates.right

theorem product.disjoint_of_left (A B C D : Set)
  requires disjoint : Disjoint(A, C)
  shows Disjoint(A × B, C × D)
proof
  have separated := Disjoint.iff.forward with disjoint
  apply Disjoint.iff.backward
  intros p hp hp2
  obtain ⟨bound, x, hx, y, hy, shape⟩ := product.membership.forward with hp
  rw shape at hp2
  have coordinates := product.pair_membership.forward with hp2
  exact separated with x, hx, coordinates.left

theorem product.subset_of_nonempty (A B C D : Set)
  requires nonempty : Nonempty(A × B)
  requires h : A × B ⊆ C × D
  shows A ⊆ C ∧ B ⊆ D
proof
  obtain ⟨p, hp⟩ := nonempty
  simp [product.membership] at hp
  obtain ⟨bound, a, ha, b, hb, equation⟩ := hp
  constructor
  . intros x hx
    have member : (x, b) ∈ C × D := h with (x, b), (product.pair with hx, hb)
    have coordinates := product.pair_membership.forward with member
    exact coordinates.left
  . intros y hy
    have member : (a, y) ∈ C × D := h with (a, y), (product.pair with ha, hy)
    have coordinates := product.pair_membership.forward with member
    exact coordinates.right

theorem product.singleton (x y : Set)
  shows {x} × {y} = {(x, y)}
proof
  ext p
  constructor
  . intro hp
    simp [product.membership] at hp
    obtain ⟨bound, a, ha, b, hb, equation⟩ := hp
    simp [singleton.membership] at ha
    simp [singleton.membership] at hb
    rw [equation, ha, hb]
    exact singleton.self
  . intro hp
    simp [singleton.membership] at hp
    rw hp
    exact product.pair with (singleton.self at x), (singleton.self at y)