import Nominal.Permutations
import Nominal.Support

/-!
# Instances

This file contains common instances of (FPerm 𝔸)-sets and nominal sets.
-/

variable (𝔸 : Type)

/-!
## Atoms

The set 𝔸 of atoms itself is a nominal set, where supp a = {a}.
-/
section Atoms

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

instance : NominalSet 𝔸 𝔸 where
  fin_supp := by
    intro a
    use {a}
    exact ⟨NominalSet.supp_atoms' 𝔸, Set.finite_singleton a⟩

lemma NominalSet.supp_atoms [Infinite 𝔸] [DecidableEq 𝔸] {a : 𝔸} : supp 𝔸 a = {a} := by
  ext b; constructor
  · apply support_subset_supp
    · apply NominalSet.supp_atoms'
    · apply Set.finite_singleton
  · suffices a ∈ supp 𝔸 a by simp; intro h; rwa [h]
    intro S ⟨hsuppS, hfinS⟩
    by_contra ha
    -- Show that we can find a fresh c with (a c) ∈ fix S
    obtain ⟨c, hc⟩ := Infinite.exists_notMem_finset ({a} ∪ hfinS.toFinset)
    simp at hc
    have hfix : ⸨a, c⸩ ∈ PermSet.fix 𝔸 S := by
      intro d hd
      apply Equiv.Perm.supp_notin
      simp [FPerm.swap, Equiv.Perm.supp_swap, Ne.symm hc.left]
      exact ⟨ne_of_mem_of_not_mem hd ha, ne_of_mem_of_not_mem hd hc.right⟩
    have h₁ : ⸨a, c⸩ • a = c := by simp [show ⸨a,c⸩ • a = (Equiv.swap a c) a from rfl]
    have h₂ : ⸨a, c⸩ • a = a := by apply hsuppS; assumption
    rw [h₁] at h₂
    exact hc.left h₂

end Atoms

/-!
## Discrete Nominal Sets

Every set can be made into a discrete nominal set, where supp x = ∅.
-/
section Discrete

def NominalSet.discrete (X : Type) : DiscreteNominalSet 𝔸 X where
  smul π x := x
  one_smul := by intro; rfl
  mul_smul := by intro _ _ _; rfl
  is_discrete := by intro _ _; rfl
  fin_supp := by
    intro x
    use {}
    constructor
    · intro π hπ; simp [PermSet.fix']; rfl
    · exact Set.finite_empty

lemma NominalSet.supp_discrete {X : Type} [DiscreteNominalSet 𝔸 X] {x : X} : supp 𝔸 x = ∅ := by
  rw [← Set.subset_empty_iff]
  apply Set.sInter_subset_of_mem
  constructor
  · intro π hπ; simp [PermSet.fix', DiscreteNominalSet.is_discrete]
  · exact 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 Discrete