-- Foundational set mathematics
-- 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.Core
import Hierarchy

-- The public root of Cumulus set theory: extensional mathematics,
-- classes, relations, Foundation, ordinals, rank, and the cumulative hierarchy.
predicate Nonempty (A : Set) := ∃ x, x ∈ A
predicate Disjoint (A B : Set) := A ∩ B = ∅

theorem Subset.transitive (A B C : Set)
  requires hAB : A ⊆ B
  requires hBC : B ⊆ C
  shows (A ⊆ C)
proof
  simp

theorem Subset.antisymmetric (A B : Set)
  requires hAB : A ⊆ B
  requires hBA : B ⊆ A
  shows A = B
proof
  ext y
  simp

theorem empty.subset (A : Set)
  shows (∅ ⊆ A)
proof
  simp

theorem union2.subset (A B C : Set)
  requires hA : A ⊆ C
  requires hB : B ⊆ C
  shows (A ∪ B ⊆ C)
proof
  simp

theorem union2.subset_left (A B : Set)
  shows (A ⊆ A ∪ B)
proof
  simp

theorem union2.subset_right (A B : Set)
  shows (B ⊆ A ∪ B)
proof
  simp

theorem union.contains (x A S : Set)
  requires hA : A ∈ S
  requires hx : x ∈ A
  shows x ∈ ⋃(S)
proof
  simp [set.union]

theorem union.subset (S B : Set)
  requires h : ∀ A ∈ S, (A ⊆ B)
  shows (⋃(S) ⊆ B)
proof
  intros x hx
  simp [set.union] at hx
  obtain ⟨A, hAS, hxA⟩ := hx
  exact h with A, hAS, x, hxA

theorem intersection.subset_right (A B : Set)
  shows (A ∩ B ⊆ B)
proof
  simp

theorem intersection.greatest (A B C : Set)
  requires hA : C ⊆ A
  requires hB : C ⊆ B
  shows (C ⊆ A ∩ B)
proof
  simp

theorem difference.subset_left (A B : Set)
  shows (A ∖ B ⊆ A)
proof
  simp

theorem powerset.membership_iff (A B : Set)
  shows A ∈ 𝒫(B) ↔ (A ⊆ B)
proof
  simp

theorem powerset.monotone (A B : Set)
  requires h : A ⊆ B
  shows (𝒫(A) ⊆ 𝒫(B))
proof
  simp [Subset, set.powerset]

theorem Nonempty.singleton (x : Set)
  shows Nonempty({x})
proof
  simp [Nonempty]

theorem Nonempty.ne_empty (A : Set)
  requires inhabited : Nonempty(A)
  shows A ≠ ∅
proof
  intro equal
  obtain ⟨x, member⟩ := inhabited
  rw equal at member
  exact set.empty with member

-- The converse needs only classical logic and extensionality.
theorem Nonempty.of_ne_empty (A : Set)
  requires different : A ≠ ∅
  shows Nonempty(A)
proof
  by_contra absent
  apply different
  ext x
  constructor
  . intro member
    exfalso
    apply absent
    unfold Nonempty
    refine ⟨x, member⟩
  . intro member
    exfalso
    exact set.empty with member

theorem Nonempty.iff_ne_empty (A : Set)
  shows Nonempty(A) ↔ A ≠ ∅
proof
  simp [Nonempty.ne_empty, Nonempty.of_ne_empty]

theorem Disjoint.symmetric (A B : Set)
  requires h : Disjoint(A, B)
  shows Disjoint(B, A)
proof
  unfold Disjoint at h
  unfold Disjoint
  rwa intersection.commutative

theorem singleton.ne_empty (x : Set)
  shows {x} ≠ ∅
proof
  intro singletonEmpty
  have self := singleton.self at x
  rw singletonEmpty at self
  simp