-- Finite sets of permutations and their inversion sets (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.Permutations
import FiniteSubsets
import Enumeration
import Product

def permutations (I : Set) : Set := {p ∈ 𝒫(I × I) | BijectiveBetween(p, I, I)}

def inversions (I p : Set) : Set :=
  {q ∈ I × I | ∃ i ∈ I, ∃ j ∈ I, q = (i, j) ∧ i ∈ j ∧ p(j) ∈ p(i)}

theorem permutations.mem_iff (I p : Set)
  shows p ∈ permutations(I) ↔ BijectiveBetween(p, I, I)
proof
  constructor
  . intro member
    simp
  . intro bijective
    have injective := Bijective.injective with bijective
    have function := Injective.function with injective
    have relation := FunctionBetween.relation with function
    unfold RelationBetween at relation
    have bound := powerset.membership_iff.backward with relation
    simp

theorem permutations.finite (I : Set)
  requires finite : Finite(I)
  shows Finite(permutations(I))
proof
  have product := Finite.product with finite, finite
  have powers := Finite.powerset with product
  have bounded : permutations(I) ⊆ 𝒫(I × I) by simp [Subset, permutations]
  exact Finite.subset with powers, bounded

theorem inversions.finite (I p : Set)
  requires finite : Finite(I)
  shows Finite(inversions(I, p))
proof
  have product := Finite.product with finite, finite
  have bounded : inversions(I, p) ⊆ I × I by simp [Subset, inversions]
  exact Finite.subset with product, bounded

theorem inversions.empty (p : Set)
  shows inversions(∅, p) = ∅
proof
  ext y
  simp [inversions, set.empty]

theorem permutations.empty
  shows permutations(∅) = {∅}
proof
  have emptyFunction : ∅ : ∅ → ∅ by exact FunctionBetween.empty at ∅
  have emptyBijective : BijectiveBetween(∅, ∅, ∅)
    constructor
    . unfold InjectiveBetween
      refine ⟨emptyFunction, ?_⟩
      intros u impossible
      exfalso
      exact set.empty with impossible
    . unfold SurjectiveBetween
      refine ⟨emptyFunction, ?_⟩
      intros u impossible
      exfalso
      exact set.empty with impossible
  ext p
  constructor
  . intro member
    have bijective := permutations.mem_iff.forward with member
    have injective := Bijective.injective with bijective
    have function := Injective.function with injective
    have relation := FunctionBetween.relation with function
    have equal : p = ∅
      ext q
      constructor
      . intro hq
        unfold RelationBetween at relation
        have pair := relation with q, hq
        obtain ⟨bound, i, hi, j, hj, shape⟩ := product.membership.forward with pair
        exfalso
        exact set.empty with hi
      . intro impossible
        exfalso
        exact set.empty with impossible
    rw equal
    simp
  . intro member
    have equal := singleton.membership.forward with member
    rw equal
    exact permutations.mem_iff.backward with emptyBijective