import Mathlib
import Nominal.Support
import Nominal.Equivariance
import Nominal.Category
import Nominal.Permutations
import Nominal.Instances.Basic

/-!
# Name Abstractions

Given a nominal set X, we define the set `[𝔸]X` of abstractions as pairs in 𝔸 × X modulo alpha-equivalence.
-/

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

/-!
## Raw Structure

We first define the raw type of name abstractions as a pair (𝔸, X).

This structure, along with the obvious permutation action, forms a nominal set where supp (a, x) = supp x ∪ {a}.
-/
section RawStructure

variable (X : Type) [NominalSet 𝔸 X]

/-- The structure forming a name abstraction. -/
structure NameAbstraction' where
  /-- The atom that is abstracted away. -/
  atom : 𝔸
  /-- The body from which the atom is abstracted. -/
  body : X

attribute [ext] NameAbstraction'

namespace NameAbstraction'

instance : SMul (FPerm 𝔸) (NameAbstraction' 𝔸 X) where
  smul π x := .mk (π x.atom) (π • x.body)

@[simp] lemma smul_atom (π : FPerm 𝔸) (x : NameAbstraction' 𝔸 X) : (π • x).atom = π x.atom := rfl

@[simp] lemma smul_body (π : FPerm 𝔸) (x : NameAbstraction' 𝔸 X) : (π • x).body = π • x.body := rfl

instance : PermSet 𝔸 (NameAbstraction' 𝔸 X) where
  smul π x := .mk (π x.atom) (π • x.body)
  one_smul := by intro _; ext <;> simp [one_smul]
  mul_smul := by intro _ _ _; ext <;> simp [mul_smul]

instance : NominalSet 𝔸 (NameAbstraction' 𝔸 X) where
  fin_supp := sorry

@[simp] lemma supp {x : NameAbstraction' 𝔸 X} : NominalSet.supp 𝔸 x = NominalSet.supp 𝔸 x.body ∪ {x.atom} := by sorry

@[simp] lemma fresh {a : 𝔸} {x : NameAbstraction' 𝔸 X} : a # x ↔ a ≠ x.atom ∧ a # x.body := by
  simp [NominalSet.IsFresh]

end NameAbstraction'

end RawStructure

/-!
## Alpha-Equivalence

We continue to define alpha-equivalence on this structure.
-/
section AlphaEquivalence

namespace NameAbstraction

variable {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] {X : Type} [NominalSet 𝔸 X]

/-- (a, x) ≈ (b, y) if (c a) x = (c b) y for some fresh c. -/
def AlphaEq (x y : NameAbstraction' 𝔸 X) : Prop :=
  И c, ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body

lemma alpha_eq_iff_exists {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ ∃ c, c # x ∧ c # y ∧ ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body := by sorry

lemma alpha_eq_iff_all {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ ∀ c, c # x ∧ c # y → ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body := by sorry

lemma alpha_eq_iff_cases {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ (x.atom = y.atom ∧ x.body = y.body) ∨ (x.atom ≠ y.atom ∧ x.atom # y ∧ x.body = ⸨x.atom, y.atom⸩ • y.body) := by sorry

private lemma alpha_eq_refl (x : NameAbstraction' 𝔸 X) : AlphaEq x x := by sorry

private lemma alpha_eq_symm {x y : NameAbstraction' 𝔸 X} : AlphaEq x y → AlphaEq y x := by sorry

private lemma alpha_eq_trans {x y z : NameAbstraction' 𝔸 X} : AlphaEq x y → AlphaEq y z → AlphaEq x z := by sorry

lemma alpha_eq_equivariant : EquivariantRelation 𝔸 (AlphaEq : NameAbstraction' 𝔸 X → NameAbstraction' 𝔸 X → Prop) := by sorry

end NameAbstraction

end AlphaEquivalence

/-!
## Quotient Type

We then define `NameAbstraction` as the quotient type of this structure modulo alpha-equivalence.
-/
section Quotient

variable (X : Type) [NominalSet 𝔸 X]

/-- Associate the name abstraction structure with alpha-equivalence. -/
instance NameAbstraction.setoid : Setoid (NameAbstraction' 𝔸 X) where
  r := AlphaEq
  iseqv := ⟨alpha_eq_refl, alpha_eq_symm, alpha_eq_trans⟩

/-- Define name abstractions as the quotient set (𝔸 × X)/≈. -/
def NameAbstraction := Quotient (NameAbstraction.setoid 𝔸 X)

/-- The equivalence class of a name abstraction (a, x), often written `⟪a⟫ x` -/
def NameAbstraction.mk {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] {X : Type} [NominalSet 𝔸 X] (a : 𝔸) (x : X) : NameAbstraction 𝔸 X :=
  Quotient.mk (setoid 𝔸 X) (.mk a x)

/-- We write `⟪a⟫ x` instead of the usual `⟨a⟩ x` because `⟨⟩` is already heavily used in Lean for constructors. -/
notation "⟪" a "⟫ " t => NameAbstraction.mk a t

end Quotient

/-!
## Nominal Set Instance

The equivalence classes of name abstractions form a nominal set where supp (⟪a⟫ x) = supp x \ {a}.
-/
section NominalSet

end NominalSet

/-!
## Abstraction Functor

Name abstraction can also be considered as a functor `Nom → Nom`.
-/
section Functor

end Functor