-- Finite powersets and maximal members of finite families, in ZF.
-- 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.Cardinal.FiniteSubsets
import FiniteImage

defgraph insertSubset (A x : Set) (S ∈ 𝒫(A)) : 𝒫(insert(x, A)) := insert(x, S)
proof
  apply powerset.membership_iff.backward at insert(x, S), insert(x, A)
  have subset := powerset.membership_iff.forward at S, A with *
  settle with Subset, insert.membership

theorem Finite.powerset_insert (A x : Set)
  requires finite : Finite(𝒫(A))
  shows Finite(𝒫(insert(x, A)))
proof
  have function := insertSubset.function at A, x
  have reflexive : 𝒫(A) ⊆ 𝒫(A) by simp
  have image := Finite.function_image with function, finite, reflexive
  have combined := Finite.union with finite, image
  have covered : 𝒫(insert(x, A)) ⊆ 𝒫(A) ∪ functionImage(insertSubset(A, x), 𝒫(A), 𝒫(insert(x, A)))
    intros S member
    have subset := powerset.membership_iff.forward with member
    have alternatives : x ∈ S ∨ ¬(x ∈ S) by tauto
    cases alternatives with present | absent
    . have rest : S ∖ {x} ⊆ A by simp
      have restIn := powerset.membership_iff.backward with rest
      have restored : insert(x, S ∖ {x}) = S
        ext y
        simp
      have value := insertSubset.value at A, x, S ∖ {x} with restIn
      have inImage : S ∈ functionImage(insertSubset(A, x), 𝒫(A), 𝒫(insert(x, A)))
        apply functionImage.membership.backward
        refine ⟨member, S ∖ {x}, restIn, ?_⟩
        cc
      simp
    . have smaller : S ⊆ A
        intros y hy
        have inInsert := subset with y, hy
        simp
      have old := powerset.membership_iff.backward with smaller
      simp
  exact Finite.subset with combined, covered

theorem listSupport.finite_powerset (C : Set) (xs : List(C))
  shows Finite(𝒫(listSupport{C}(xs)))
proof
  induction xs
  | List.nil =>
    rw listSupport
    have bounded : 𝒫(∅) ⊆ {∅}
      intros S member
      have subset := powerset.membership_iff.forward with member
      have reverse := empty.subset at S
      have equal := Subset.antisymmetric with subset, reverse
      exact singleton.membership.backward with equal
    have finite := Finite.singleton at ∅
    exact Finite.subset with finite, bounded
  | List.cons(x, tail) using ih =>
    rw listSupport
    exact Finite.powerset_insert with *

theorem Finite.powerset (A : Set)
  requires finite : Finite(A)
  shows Finite(𝒫(A))
proof
  obtain ⟨xs, list, covers⟩ := Finite.list_cover with finite
  have bound := listSupport.finite_powerset with list
  have included := powerset.monotone with covers
  exact Finite.subset with bound, included

-- Scan a finite family, replacing the current member only by a larger one.
theorem listSupport.maximal_extension (F : Set) (xs : List(F))
  shows ∀ S ∈ F, ∃ M ∈ F, S ⊆ M ∧ (∀ T ∈ listSupport{F}(xs), M ⊆ T → T = M)
proof
  induction xs
  | List.nil =>
    intros S member
    refine ⟨S, member, ?_⟩
    constructor
    . settle with Subset
    . intros T inList contains
      rw listSupport at inList
      exfalso
      exact set.empty with inList
  | List.cons(x, tail) using ih =>
    intros S member
    obtain ⟨M, inFamily, extends, maximal⟩ := ih with S, member
    have alternatives : M ⊆ x ∨ ¬(M ⊆ x) by tauto
    cases alternatives with larger | incomparable
    . have xIn : x ∈ F
        assumption
      have extension := Subset.transitive with extends, larger
      refine ⟨x, xIn, extension, ?_⟩
      intros T inList contains
      rw listSupport at inList
      have casesT := insert.membership.forward with inList
      cases casesT with equal | inTail
      . exact equal
      . have includes := Subset.transitive with larger, contains
        have equal := maximal with T, inTail, includes
        have reverse : x ⊆ M by simp
        have same := Subset.antisymmetric with larger, reverse
        cc
    . refine ⟨M, inFamily, extends, ?_⟩
      intros T inList contains
      rw listSupport at inList
      have casesT := insert.membership.forward with inList
      cases casesT with equal | inTail
      . exfalso
        rw equal at contains
        exact incomparable with contains
      . exact maximal with T, inTail, contains

theorem Finite.maximal_extension (F S : Set)
  requires finite : Finite(F)
  requires member : S ∈ F
  shows ∃ M ∈ F, S ⊆ M ∧ (∀ T ∈ F, M ⊆ T → T = M)
proof
  obtain ⟨xs, list, covers⟩ := Finite.list_cover with finite
  have scan := listSupport.maximal_extension with list
  obtain ⟨M, inFamily, extends, maximal⟩ := scan with S, member
  refine ⟨M, inFamily, extends, ?_⟩
  intros T inFamilyT contains
  have inList := covers with T, inFamilyT
  exact maximal with T, inList, contains