-- Finite set constructions
-- 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.Finite
import Basic

namespace FiniteSet

def insert (x A : Set) : Set := {x} ∪ A
def doubleton (x y : Set) : Set := {x} ∪ {y}

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

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

theorem union2.right (x A B : Set)
  requires hx : x ∈ B
  shows x ∈ A ∪ B
proof
  simp

theorem union2.commutative (A B : Set)
  shows A ∪ B = B ∪ A
proof
  ext y
  simp

theorem union2.idempotent (A : Set)
  shows A ∪ A = A
proof
  ext y
  simp

theorem union2.associative (A B C : Set)
  shows (A ∪ B) ∪ C = A ∪ (B ∪ C)
proof
  ext y
  simp

theorem insert.membership (x y A : Set)
  shows x ∈ insert(y, A) ↔ (x = y ∨ x ∈ A)
proof
  simp [insert, union2.membership, singleton.membership]

theorem insert.self (x A : Set)
  shows x ∈ insert(x, A)
proof
  simp

theorem insert.contains (x y A : Set)
  requires hx : x ∈ A
  shows x ∈ insert(y, A)
proof
  simp

theorem doubleton.membership (x a b : Set)
  shows x ∈ doubleton(a, b) ↔ (x = a ∨ x = b)
proof
  simp [doubleton, union2.membership, singleton.membership]

theorem insert.restore (V x : Set)
  requires member : x ∈ V
  shows insert(x, V ∖ {x}) = V
proof
  ext y
  simp

end FiniteSet

export open Grace.Cumulus.Set.Finite.FiniteSet