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

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

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

/-- We consider Bool a discrete (FPerm 𝔸)-Set. -/
instance : PermSet 𝔸 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 G-Sets where all elements are finitely supported.
-/
section NominalSet

variable (𝔸 : Type)

/-- A G-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". --/
noncomputable 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

end NominalSet

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

-- TODO: Prove supp a = {a}

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

-- TODO: Prove supp x = ∅

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

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

end NominalSet