-- Basic set theory
-- 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.Basic

namespace Set

def singleton (x : Set) : Set := pair(x, x)
def union2 (A B : Set) : Set := ⋃(pair(A, B))
def intersection (A B : Set) : Set := { x ∈ A | x ∈ B }
def difference (A B : Set) : Set := { x ∈ A | ¬x ∈ B }
predicate Subset (A B : Set) := ∀ x ∈ A, x ∈ B
notation infix 50 "⊆" => Subset
notation infixl 60 "∪" => union2
notation infixl 65 "∩" => intersection
notation infixl 65 "∖" => difference

theorem pair.left (x y : Set)
  shows x ∈ {x, y}
proof
  simp

theorem pair.right (x y : Set)
  shows y ∈ {x, y}
proof
  simp

theorem pair.cancel_left (a b c : Set)
  requires h : {a, b} = {a, c}
  shows b = c
proof
  have hb := pair.right at a, b
  rw h at hb
  simp [pair.membership] at hb
  cases hb with hba | hbc
  have hc := pair.right at a, c
  rw ← h at hc
  simp [pair.membership] at hc
  cases hc with hca | hcb
  simp
  simp
  exact hbc

theorem singleton.self (x : Set)
  shows x ∈ {x}
proof
  simp [singleton, pair.membership]

theorem union2.left (x A B : Set)
  requires x ∈ A
  shows x ∈ A ∪ B
proof
  simp [union2, set.union, pair.membership]

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

theorem union.singleton (A : Set)
  shows ⋃({A}) = A
proof
  ext y
  simp [set.union, singleton, pair.membership]

theorem intersection.commutative (A B : Set)
  shows A ∩ B = B ∩ A
proof
  ext y
  simp

theorem Subset.reflexive (A : Set)
  shows (A ⊆ A)
proof
  simp

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

theorem intersection.idempotent (A : Set)
  shows A ∩ A = A
proof
  ext y
  simp

end Set

export open Grace.Cumulus.Set.Basic.Set