-- Derived consequences of Foundation
-- 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.Foundation
import Relation

-- The nth downward membership layer starting from {x}.
def layer (x : Set, n : Nat) → Set
  | x, zero => {x}
  | x, succ(n) => ⋃(layer(x, n))

-- Replacement collects all finite layers; their union is the
-- transitive closure containing x.
def layers (x : Set) : Set := { layer(x, n) | n ∈ ℕ }
def closure (x : Set) : Set := ⋃(layers(x))

-- Membership restricted to a set, represented as a relation set.
def membershipOn (A : Set) : Set := { p ∈ A × A | ∃ x ∈ A, ∃ y ∈ A, x ∈ y ∧ p = (x, y) }

theorem layer.zero (x : Set)
  shows layer(x, 0) = {x}
proof
  simp [layer, nat.zero]

theorem layer.next (x : Set, n : Nat)
  shows layer(x, succ(n)) = ⋃(layer(x, n))
proof
  simp [layer]

theorem omega.natural (n : Set)
  requires hn : n ∈ ℕ
  shows Nat(n)
proof
  simp [nat.omega]

theorem omega.successor (n : Set)
  requires hn : n ∈ ℕ
  shows succ(n) ∈ ℕ
proof
  have hnat := omega.natural with hn
  have infinity := set.infinity
  cases infinity with hzeroIn ∧ hsuccessor
  specialize hsuccessor with n, hn
  have hsucc := nat.succ with hnat
  rwa hsucc

theorem closure.contains (x : Set)
  shows x ∈ closure(x)
proof
  unfold closure
  apply set.union.backward
  witness layer(x, 0)
  constructor
  apply layers.membership.backward
  witness 0
  constructor
  have infinity := set.infinity
  cases infinity with hzeroIn ∧ hsuccessor
  rwa nat.zero
  rfl
  have hzero := layer.zero at x
  rw hzero
  exact singleton.self

theorem closure.transitive (x : Set)
  shows ∀ y ∈ closure(x), ∀ z ∈ y, z ∈ closure(x)
proof
  intros y hy z hz
  unfold closure at hy
  simp [set.union] at hy
  obtain ⟨L, hLy⟩ := hy
  cases hLy with hL ∧ hyL
  simp [layers] at hL
  obtain ⟨n, hnLayer⟩ := hL
  cases hnLayer with hn ∧ hLayer
  unfold closure
  apply set.union.backward
  witness layer(x, succ(n))
  constructor
  apply layers.membership.backward
  witness succ(n)
  constructor
  exact omega.successor with hn
  rfl
  have hnext := layer.next at x, n
  rw [hnext, hLayer]
  exact set.union.backward with ⟨y, hyL, hz⟩

theorem membershipOn.relates (a b A : Set)
  requires ha : a ∈ A
  requires hb : b ∈ A
  shows relates(membershipOn(A), a, b) ↔ a ∈ b
proof
  constructor
  . intro h
    unfold relates at h
    simp [membershipOn] at h
    obtain ⟨hproduct, x, hxA, y, hyA, hxy, hpair⟩ := h
    obtain ⟨hax, hby⟩ := orderedPair.injective with hpair
    rw hax
    rwa hby
  . intro h
    unfold relates
    exact membershipOn.backward with ⟨(product.pair with ha, hb), a, ha, b, hb, h, rfl⟩

theorem membershipOn.relation (A : Set)
  shows RelationBetween(membershipOn(A), A, A)
proof
  simp [RelationBetween, Subset]

theorem membershipOn.wellFounded (A : Set)
  shows wellFoundedOn(membershipOn(A), A)
proof
  intros s hs
  cases hs with hsubset ∧ hnonempty
  obtain ⟨m, hmMinimal⟩ := set.foundation with hnonempty
  cases hmMinimal with hm ∧ hminimal
  witness m
  constructor
  exact hm
  intros y hy hrel
  have hmA := hsubset with hm
  have hyA := hsubset with hy
  have relation := membershipOn.relates with hyA, hmA
  simp [relation] at hrel
  exact hminimal with y, hrel, hy

-- This tiny theorem is a regression test for the derived induction tactic.
theorem membership.induction_reflexive (x : Set)
  shows x = x
proof
  simp

theorem membership.irreflexive (x : Set)
  shows ¬x ∈ x
proof
  induction x using membership
  intros current ih hSelf
  exact ih with hSelf, hSelf