import Mathlib.Tactic
import Nominal.Permutations
import Nominal.Helpers.Finset
/-!
# Basic Definitions

This file provides basic definitions for nominal sets.
-/

/-!
## (FPerm 𝔸)-Sets

Sets equipped with a permutation operation.
-/
section PermSet

variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]

/-- A set X equipped with a group action •: (FPerm 𝔸) × X → X. -/
class PermSet (X : Type) extends MulAction (FPerm 𝔸) X

/-- The set of atoms itself forms a (FPerm 𝔸)-Set. -/
instance : PermSet 𝔸 𝔸 where
  smul π a := π a
  one_smul := by intro; rfl
  mul_smul := by intro _ _ _; rfl

/-- The set of finite permutations forms a (FPerm 𝔸)-Set. -/
instance : PermSet 𝔸 (FPerm 𝔸) where
  smul π τ := π * τ
  one_smul := by intro; rfl
  mul_smul := by intro _ _ _; rfl

class DiscretePermSet (X : Type) extends PermSet 𝔸 X where
  is_discrete : ∀ (x : X) (π : FPerm 𝔸), π • x = x

/-- A discrete (FPerm 𝔸)-Set where permutations do not change anything. -/
def PermSet.discrete (X : Type) : DiscretePermSet 𝔸 X where
  smul π x := x
  one_smul := by intro; rfl
  mul_smul := by intro _ _ _; rfl
  is_discrete := by intro _ _; rfl

/-- We consider Unit a discrete (FPerm 𝔸)-Set. -/
instance : DiscretePermSet 𝔸 Unit := PermSet.discrete 𝔸 Unit

/-- We consider Bool a discrete (FPerm 𝔸)-Set. -/
instance : DiscretePermSet 𝔸 Bool := PermSet.discrete 𝔸 Bool

end PermSet

/-!
## Support Definitions

We can define the notion of "supports" on elements of (FPerm 𝔸)-Sets as the atoms which need to be left unchanged to also fix the element.
-/
section Support

variable (𝔸 : Type) {X : Type} [PermSet 𝔸 X]

namespace PermSet

/-- The permutations that leave an element x unchanged. -/
def fix' (x : X) : Set (FPerm 𝔸) :=
  { π : FPerm 𝔸 | π • x = x }

/-- The permutations that leave all elements in A unchanged. -/
def fix (A : Set X) : Set (FPerm 𝔸) :=
  { π : FPerm 𝔸 | ∀ x ∈ A, π • x = x }

/-- A set S ⊆ 𝔸 is a support for x if every permutation that fixes S also leaves x unchanged. -/
def HasSupport (x : X) (S : Set 𝔸) : Prop :=
  fix 𝔸 S ⊆ fix' 𝔸 x

@[simp]
lemma support_iff {x : X} {S : Set 𝔸} : HasSupport 𝔸 x S ↔ ∀ (π : FPerm 𝔸), (∀ x ∈ S, π x = x) → π ∈ fix' 𝔸 x := by
  constructor
  · intro hsupp π hπ
    aesop
  · intro hsupp π hπ
    aesop

lemma support_subset {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S ⊆ T → HasSupport 𝔸 x T := by
  intro hS hsub π hπ
  apply hS
  intro a
  aesop

lemma support_inter {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S.Finite → HasSupport 𝔸 x T → T.Finite → HasSupport 𝔸 x (S ∩ T) := by
  sorry

lemma support_sInter {x : X} {C : Set (Set 𝔸)}: C.Finite → C.Nonempty → (∀ S ∈ C, HasSupport 𝔸 x S ∧ S.Finite) → HasSupport 𝔸 x (⋂₀ C) := by
  suffices (C : Finset (Set 𝔸)) : C.Nonempty → (∀ S ∈ C, HasSupport 𝔸 x S ∧ S.Finite) → HasSupport 𝔸 x (⋂₀ C.toSet) ∧ (⋂₀ C.toSet).Finite
  · intro hfin
    rw [show C = hfin.toFinset.toSet by simp]
    intro hne h
    exact (this hfin.toFinset hne h).left
  · have : DecidableEq (Set 𝔸) := Classical.typeDecidableEq (Set 𝔸)
    apply Finset.Nonempty.induction
    · intro S hS
      rw [show ⋂₀ ({S} : Finset (Set 𝔸)).toSet = S by simp]
      apply hS
      simp
    · intro S C' hS hC' hsing
      rw [show (⋂₀ (insert S C' : Finset (Set 𝔸))) = S ∩ (⋂₀ C') by aesop]
      have hother : (∀ S ∈ C', HasSupport 𝔸 x S ∧ S.Finite) := by
        intro S' hS'
        apply hsing
        exact Finset.mem_insert_of_mem hS'
      specialize hC' hother
      specialize hsing S (by simp)
      constructor
      · apply support_inter 𝔸 hsing.left hsing.right hC'.left hC'.right
      · apply Set.Finite.inter_of_left
        exact hsing.right

end PermSet

end Support

/-!
## Basic Nominal Set Definition

Nominal sets are then just (FPerm 𝔸)-Sets where all elements are finitely supported.
-/
section NominalSet

variable (𝔸 : Type)

/-- An (FPerm 𝔸)-Set X is nominal if every x ∈ X is finitely supported. -/
class NominalSet (X : Type) extends PermSet 𝔸 X where
  finsupp : ∀ (x : X), ∃ (S : Set 𝔸), PermSet.HasSupport 𝔸 x S ∧ S.Finite

namespace NominalSet

variable {X : Type} [nom : NominalSet 𝔸 X]

/-- For every element x of a nominal set, there exists a least finite support, denoted "supp x". --/
def supp (x : X) : Set 𝔸 :=
  ⋂₀ { S : Set 𝔸 | PermSet.HasSupport 𝔸 x S ∧ S.Finite }

/-- The least finite support in a nominal set is always finite. -/
lemma supp_finite {x : X} : (supp 𝔸 x).Finite := by
  unfold supp
  obtain ⟨S, ⟨hsuppS, hfinS⟩⟩ := nom.finsupp x
  apply Set.Finite.subset
  · exact hfinS
  · grind

/-- The least finite support is itself a support. -/
lemma supp_is_support {x : X} : PermSet.HasSupport 𝔸 x (supp 𝔸 x) := by
  obtain ⟨S, ⟨hsuppS, hfinS⟩⟩ := nom.finsupp x
  have suppf : (supp 𝔸 x = ⋂₀ { T : Set 𝔸 | T ⊆ S ∧ PermSet.HasSupport 𝔸 x T ∧ T.Finite }) := by
    unfold supp; ext a
    constructor
    · intro h T hT
      apply h
      exact hT.out.right
    · intro h T hT
      suffices : a ∈ S ∩ T
      · apply Set.mem_of_mem_inter_right; assumption
      · apply h
        constructor
        · exact Set.inter_subset_left
        · constructor
          · exact PermSet.support_inter 𝔸 hsuppS hfinS hT.out.left hT.out.right
          · apply Set.Finite.inter_of_left; assumption
  rw [suppf]
  apply PermSet.support_sInter
  · apply Set.Finite.subset
    · apply Set.Finite.powerset
      exact hfinS
    · intro T hT
      exact hT.out.left
  · use S
    exact ⟨by rfl, ⟨hsuppS, hfinS⟩⟩
  · intro T hT
    exact hT.right

lemma support_subset_supp {x : X} {S : Set 𝔸} : PermSet.HasSupport 𝔸 x S → S.Finite → supp 𝔸 x ⊆ S := by
  intro hsupp hfin
  apply Set.sInter_subset_of_mem
  exact ⟨hsupp, hfin⟩

end NominalSet

private lemma NominalSet.supp_atoms' {a : 𝔸} : PermSet.HasSupport 𝔸 a {a} := by
  simp [PermSet.fix']

/-- The set of atoms is a nominal set, where supp a = {a}. -/
instance : NominalSet 𝔸 𝔸 where
  finsupp := by
    intro a
    use {a}
    constructor
    · exact NominalSet.supp_atoms' 𝔸
    · simp

lemma NominalSet.supp_atoms [Infinite 𝔸] [DecidableEq 𝔸] {a : 𝔸} : supp 𝔸 a = {a} := by
  ext b; constructor
  · apply support_subset_supp
    · apply NominalSet.supp_atoms'
    · simp
  · suffices : a ∈ supp 𝔸 a
    -- TODO: Shorten
    · simp; intro h; rw [h]; assumption
    · intro S ⟨hsuppS, hfinS⟩
      by_contra
      have hfin : ({a} ∪ S).Finite := by
        apply Set.finite_union.mpr; simp [hfinS]
      obtain ⟨c, hc⟩ := Infinite.exists_notMem_finset hfin.toFinset
      have h₁ : c ≠ a := by aesop
      have h₂ : c ∉ S := by aesop
      have h₃ : ⸨a, c⸩ ∈ PermSet.fix 𝔸 S := by
        intro d hd
        rw [show ⸨a,c⸩ • d = (Equiv.swap a c) d from rfl]
        apply Equiv.Perm.supp_notin
        rw [Equiv.Perm.supp_swap]
        aesop
      have h₄ : ⸨a, c⸩ • a = c := by
        simp [show ⸨a,c⸩ • a = (Equiv.swap a c) a from rfl]
      unfold PermSet.HasSupport at hsuppS
      specialize hsuppS h₃
      simp [PermSet.fix'] at hsuppS
      aesop

class DiscreteNominalSet (X : Type) extends NominalSet 𝔸 X, DiscretePermSet 𝔸 X

private lemma NominalSet.supp_discrete' {X : Type} [disc : DiscretePermSet 𝔸 X] {x : X} : PermSet.HasSupport 𝔸 x ∅ := by
  intro π hπ
  simp [PermSet.fix']
  exact DiscretePermSet.is_discrete x π

/-- Every set can be made into a discrete nominal set where every element has empty support. -/
def NominalSet.discrete (X : Type) : DiscreteNominalSet 𝔸 X :=
{ PermSet.discrete 𝔸 X with
  finsupp := by
    intro x
    use {}
    constructor
    · intro π hπ; simp [PermSet.fix']; rfl
    · simp
}

lemma NominalSet.supp_discrete {X : Type} [DiscreteNominalSet 𝔸 X] {x : X} : supp 𝔸 x = ∅ := by
  rw [← Set.subset_empty_iff]
  apply Set.sInter_subset_of_mem
  exact ⟨NominalSet.supp_discrete' 𝔸, Set.finite_empty⟩

/-- We consider Unit a discrete nominal set. -/
instance : DiscreteNominalSet 𝔸 Unit := NominalSet.discrete 𝔸 Unit

/-- We consider Bool a discrete nominal set. -/
instance : DiscreteNominalSet 𝔸 Bool := NominalSet.discrete 𝔸 Bool

end NominalSet