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}
    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
    · simp; intro h; rw [h]; assumption
    · intro S ⟨hsuppS, hfinS⟩
      by_contra ha
      obtain ⟨c, hc⟩ := Infinite.exists_notMem_finset ({a} ∪ hfinS.toFinset)
      simp at hc
      have hfix : ⸨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
        simp [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 ha₁ : ⸨a, c⸩ • a = c := by
        simp [show ⸨a,c⸩ • a = (Equiv.swap a c) a from rfl]
      have ha₂ : ⸨a, c⸩ • a = a := by
        specialize hsuppS hfix
        simpa [PermSet.fix']
      rw [ha₁] at ha₂
      exact hc.left ha₂

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
    · 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
  constructor
  · intro π hπ
    simp [PermSet.fix']
    exact DiscreteNominalSet.is_discrete x π
  · 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