1 files changed, 137 insertions, 0 deletions
diff --git a/Nominal/Instances/Abstraction.lean b/Nominal/Instances/Abstraction.lean
new file mode 100644
index 0000000..92385d7
--- /dev/null
+++ b/Nominal/Instances/Abstraction.lean
@@ -0,0 +1,137 @@
+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