1 files changed, 264 insertions, 0 deletions
diff --git a/Nominal/NameRestriction/Model.lean b/Nominal/NameRestriction/Model.lean
new file mode 100644
index 0000000..8ef60fe
--- /dev/null
+++ b/Nominal/NameRestriction/Model.lean
@@ -0,0 +1,264 @@
+import Mathlib
+import Nominal.Support
+import Nominal.Equivariance
+import Nominal.Category
+import Nominal.Permutations
+import Nominal.Instances.Basic
+import Nominal.Instances.Abstraction
+import Nominal.NameRestriction.Finsupp
+
+variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
+
+-- M₀ algebra structure: Equivariant join semilattices with name restriction
+
+class AlgebraStructure (X : Type) [NominalSet 𝔸 X] where
+  bot : Unit →ₑ[𝔸] X
+  join : (X × X) →ₑ[𝔸] X
+  res : NameAbstraction 𝔸 X →ₑ[𝔸] X
+  ax_neutral : ∀ x, join (x, bot ()) = x
+  ax_idempotent : ∀ x, join (x, x) = x
+  ax_commutative : ∀ x y, join (x, y) = join (y, x)
+  ax_associative : ∀ x y z, join (join (x, y), z) = join (x, join (y, z))
+  ax_fresh : ∀ a x, a # x → res (⟪a⟫ x) = x
+  ax_swap : ∀ a b x, res (⟪a⟫ res (⟪b⟫ x)) = res (⟪b⟫ res (⟪a⟫ x))
+  ax_distributive : ∀ a x y, res (⟪a⟫ join (x, y)) = join (res (⟪a⟫ x), res (⟪a⟫ y))
+  ax_redundant : ∀ a x, x = join (x, res (⟪a⟫ x))
+
+private abbrev AlgebraStructure.bot' {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] :=
+  (AlgebraStructure.bot : Unit →ₑ[𝔸] X)
+private abbrev AlgebraStructure.join' {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] :=
+  (AlgebraStructure.join : (X × X) →ₑ[𝔸] X)
+
+notation "⊥[" A "]" => AlgebraStructure.bot' A ()
+notation:60 x " ∨[" A "] " y => AlgebraStructure.join' A (x, y)
+infixl:60 " \\ " => fun a x => AlgebraStructure.res (⟪a⟫ x)
+
+namespace AlgebraStructure
+
+variable {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X]
+
+lemma bot_supp : NominalSet.supp 𝔸 (⊥[𝔸] : X) = ∅ := by
+  rw [← Set.subset_empty_iff]
+  show NominalSet.supp 𝔸 ((bot' 𝔸).toFun ()) ⊆ ∅
+  grw [Function.Equivariant.supp_subset]
+  simp
+
+lemma join_equivariant {x y : X} {π : FPerm 𝔸} : π • (x ∨[𝔸] y) = (π • x) ∨[𝔸] (π • y) := by
+  show π • (join' 𝔸).toFun (x, y) = (join' 𝔸).toFun (π • (x, y))
+  rw [← Function.equivariant]
+
+lemma res_equivariant {a : 𝔸} {x : X} {π : FPerm 𝔸} : π • (a \ x) = (π • a) \ (π • x) := by
+  show π • res.toFun (⟪a⟫ x) = res.toFun (π • (⟪a⟫ x))
+  rw [← Function.equivariant]
+
+end AlgebraStructure
+
+-- Base Model: M₀ X
+
+def BaseModel (X : Type) [NominalSet 𝔸 X] : Type :=
+  PermSet.FinSet 𝔸 X
+
+namespace BaseModel
+
+variable {X : Type} [NominalSet 𝔸 X]
+
+instance : NominalSet 𝔸 (BaseModel 𝔸 X) := PermSet.FinSet.instNominalSet 𝔸
+instance : EmptyCollection (BaseModel 𝔸 X) := PermSet.FinSet.instEmptyCollection 𝔸
+instance : Union (BaseModel 𝔸 X) := PermSet.FinSet.instUnion 𝔸
+instance : Inter (BaseModel 𝔸 X) := PermSet.FinSet.instInter 𝔸
+instance : SDiff (BaseModel 𝔸 X) := PermSet.FinSet.instSDiff 𝔸
+
+@[simp] lemma empty_val : (∅ : BaseModel 𝔸 X).val = ∅ := rfl
+@[simp] lemma union_val {S₁ S₂ : BaseModel 𝔸 X} : (S₁ ∪ S₂).val = S₁.val ∪ S₂.val := rfl
+@[simp] lemma inter_val {S₁ S₂ : BaseModel 𝔸 X} : (S₁ ∩ S₂).val = S₁.val ∩ S₂.val := rfl
+@[simp] lemma sdiff_val {S₁ S₂ : BaseModel 𝔸 X} : (S₁ \ S₂).val = S₁.val \ S₂.val := rfl
+@[simp] lemma smul_val {L : BaseModel 𝔸 X} {π : FPerm 𝔸} : (π • L).val = π • L.val := rfl
+
+def bot : Unit → BaseModel 𝔸 X :=
+  fun _ ↦ ∅
+
+instance : Function.Equivariant 𝔸 (bot 𝔸 : Unit → BaseModel 𝔸 X) := by
+  constructor; intro _ π
+  apply Subtype.eq; simp [bot]
+
+def union : (BaseModel 𝔸 X × BaseModel 𝔸 X) → BaseModel 𝔸 X := PermSet.FinSet.union 𝔸
+
+instance : Function.Equivariant 𝔸 (union 𝔸 : (BaseModel 𝔸 X × BaseModel 𝔸 X) → BaseModel 𝔸 X) :=
+  PermSet.FinSet.instEquivariantProdUnion 𝔸
+
+
+def restrict : NameAbstraction 𝔸 (BaseModel 𝔸 X) → BaseModel 𝔸 X := Quotient.lift
+  (fun ⟨a, S⟩ ↦ ⟨{x ∈ S.val | a # x}, by
+    apply Set.Finite.subset S.prop; simp⟩)
+  (by
+    intro ⟨a₁, S₁⟩ ⟨a₂, S₂⟩ haeq
+    apply Subtype.eq
+    simp only
+    rw [← NameAbstraction.eq_iff_alpha_eq 𝔸 (BaseModel 𝔸 X), NameAbstraction.eq_iff_cases] at haeq
+    cases haeq with
+    | inl h => rw [h.left, h.right]
+    | inr h =>
+      ext x; constructor
+      · intro ⟨hx, ha₁⟩
+        have hx' : ⸨a₁, a₂⸩ • x ∈ S₂.val := by
+          rw [← Set.mem_inv_smul_set_iff, FPerm.swap_inv]
+          show x ∈ (⸨a₁, a₂⸩ • S₂).val
+          rw [← h.right.right]; exact hx
+        have ha₂ := h.right.left
+        rw [PermSet.FinSet.fresh] at ha₂
+        specialize ha₂ (⸨a₁, a₂⸩ • x) hx'
+        nth_rw 1 [show a₁ = ⸨a₁, a₂⸩ • a₂ by simp] at ha₂
+        rw [← Rel.equivariant 𝔸 NominalSet.IsFresh] at ha₂
+        constructor
+        · rw [← show ⸨a₁, a₂⸩ • x = x from NominalSet.fresh_swap_fix 𝔸 ha₁ ha₂]
+          exact hx'
+        · exact ha₂
+      · intro ⟨hx, ha₂⟩
+        have hx' : ⸨a₁, a₂⸩ • x ∈ S₁.val := by
+          rw [← Set.mem_inv_smul_set_iff, FPerm.swap_inv]
+          show x ∈ (⸨a₁, a₂⸩ • S₁).val
+          rw [h.right.right, ← MulAction.mul_smul, FPerm.swap_mul_self, MulAction.one_smul]
+          exact hx
+        have ha₁ := h.right.left
+        rw [PermSet.FinSet.fresh] at ha₁
+        specialize ha₁ x hx
+        rw [← show ⸨a₁, a₂⸩ • x = x from NominalSet.fresh_swap_fix 𝔸 ha₁ ha₂] at hx'
+        rw [← MulAction.mul_smul, FPerm.swap_mul_self, MulAction.one_smul] at hx'
+        exact ⟨hx', ha₁⟩)
+
+instance : Function.Equivariant 𝔸 (restrict 𝔸 : NameAbstraction 𝔸 (BaseModel 𝔸 X) → BaseModel 𝔸 X) := by
+  constructor
+  apply Quotient.ind
+  intro ⟨a, S⟩ π
+  apply Subtype.eq
+  simp only [restrict, NameAbstraction.smul, Quotient.lift_mk, smul_val]
+  ext x; constructor
+  · intro ⟨hx, hfresh⟩
+    rw [Set.mem_smul_set_iff_inv_smul_mem]; constructor
+    · rw [← Set.mem_smul_set_iff_inv_smul_mem]; exact hx
+    · rw [show a = π⁻¹ • π • a by simp, ← Rel.equivariant 𝔸 NominalSet.IsFresh]
+      exact hfresh
+  · rw [Set.mem_smul_set_iff_inv_smul_mem]
+    intro ⟨hx, hfresh⟩; constructor
+    · rw [Set.mem_smul_set_iff_inv_smul_mem]; exact hx
+    · rw [show x = π • π⁻¹ • x by simp, ← Rel.equivariant 𝔸 NominalSet.IsFresh]
+      exact hfresh
+
+lemma restrict_eq {a : 𝔸} {S : BaseModel 𝔸 X} :
+    (restrict 𝔸 (⟪a⟫ S)).val = {x ∈ S.val | a # x} := rfl
+
+instance : AlgebraStructure 𝔸 (BaseModel 𝔸 X) where
+  bot := ⟨bot 𝔸, inferInstance⟩
+  join := ⟨union 𝔸, inferInstance⟩
+  res := ⟨restrict 𝔸, inferInstance⟩
+  ax_neutral x := by
+    apply Subtype.eq
+    show x.val ∪ ∅ = x.val
+    simp
+  ax_idempotent x := by
+    apply Subtype.eq
+    show x.val ∪ x.val = x.val
+    simp
+  ax_commutative x y := by
+    apply Subtype.eq
+    show x.val ∪ y.val = y.val ∪ x.val
+    apply Set.union_comm
+  ax_associative x y z := by
+    apply Subtype.eq
+    show (x.val ∪ y.val) ∪ z.val = x.val ∪ (y.val ∪ z.val)
+    apply Set.union_assoc
+  ax_fresh a S := by
+    intro hfresh
+    show restrict 𝔸 (⟪a⟫ S) = S
+    apply Subtype.eq
+    rw [restrict_eq]
+    rw [PermSet.FinSet.fresh] at hfresh
+    ext x; constructor
+    · intro ⟨hS, _⟩; exact hS
+    · intro hS; exact ⟨hS, hfresh x hS⟩
+  ax_swap a b S := by
+    show restrict 𝔸 (⟪a⟫ restrict 𝔸 (⟪b⟫ S)) = restrict 𝔸 (⟪b⟫ restrict 𝔸 (⟪a⟫ S))
+    apply Subtype.eq
+    ext x
+    simp only [restrict_eq, Set.mem_setOf_eq]
+    ac_nf
+  ax_distributive a S₁ S₂ := by
+    show restrict 𝔸 (⟪a⟫ S₁ ∪ S₂) = restrict 𝔸 (⟪a⟫ S₁) ∪ restrict 𝔸 (⟪a⟫ S₂)
+    apply Subtype.eq
+    simp [restrict_eq]
+  ax_redundant a S := by
+    show S = S ∪ restrict 𝔸 (⟪a⟫ S)
+    apply Subtype.eq; ext x
+    simp only [union_val, restrict_eq, Set.mem_union, Set.mem_setOf_eq, iff_self_or, and_imp]
+    intro h _; exact h
+
+@[simp] lemma bot_eq : (⊥[𝔸] : BaseModel 𝔸 X) = ∅ := rfl
+@[simp] lemma join_eq {S₁ S₂ : BaseModel 𝔸 X} : (S₁ ∨[𝔸] S₂) = S₁ ∪ S₂ := rfl
+@[simp] lemma res_eq {a : 𝔸} {S : BaseModel 𝔸 X} : (a \ S) = restrict 𝔸 (⟪a⟫ S) := rfl
+
+end BaseModel
+
+-- Step Model: \bar{M₁} X
+
+def permissibleFunctions (X : Type) [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] :=
+  { f : PermSet.FinsuppFunction 𝔸 𝔸 X |
+    ∀ a,
+      PermSet.HasSupport 𝔸 (f.val a) (NominalSet.supp 𝔸 f ∪ {a}) ∧
+      ∀ c, c # f → c ≠ a → f.val a = f.val a ∨[𝔸] (c \ (⸨a, c⸩ • f).val a) }
+
+def StepModel (X : Type) [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] : Type :=
+  permissibleFunctions 𝔸 X
+
+namespace StepModel
+
+variable {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X]
+
+instance : Set.Equivariant 𝔸 (permissibleFunctions 𝔸 X) := by
+  constructor; intro f π hf a
+  simp only [PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv,
+    PermSet.atom_swap, Equiv.swap_apply_left]
+  constructor
+  · have hf₁ := (hf (π⁻¹ • a)).left
+    rw [show NominalSet.supp 𝔸 (π • f) = π • NominalSet.supp 𝔸 f from Function.equivariant _ _ _ _]
+    rw [show ({a} : Set 𝔸) = π • {π⁻¹ • a} by simp]
+    rw [← Set.smul_set_union]
+    rw [← Rel.equivariant 𝔸 (PermSet.HasSupport 𝔸)]
+    exact hf₁
+  · intro c hcf hca
+    have hf₂ := (hf (π⁻¹ • a)).right (π⁻¹ • c)
+    specialize hf₂ (by
+      rw [show f = π⁻¹ • π • f by simp]
+      rw [← Rel.equivariant 𝔸 NominalSet.IsFresh]
+      exact hcf)
+    specialize hf₂ (by
+      intro hcontra
+      have : π • π⁻¹ • c = π • π⁻¹ • a := by rw [hcontra]
+      simp only [smul_inv_smul] at this
+      exact hca this)
+    nth_rw 1 [hf₂]
+    rw [AlgebraStructure.join_equivariant, AlgebraStructure.res_equivariant]
+    simp only [smul_inv_smul, PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv,
+      PermSet.atom_swap, Equiv.swap_apply_left]
+    suffices π • ⸨π⁻¹ • a,π⁻¹ • c⸩ • f.val (π⁻¹ • c) = ⸨a, c⸩ • π • f.val (π⁻¹ • c) by rw [this]
+    rw [← MulAction.mul_smul, ← MulAction.mul_smul]
+    suffices π * ⸨π⁻¹ • a,π⁻¹ • c⸩ = ⸨a,c⸩ * π by rw [this]
+    rw [FPerm.mul_swap_eq_swap_mul, show π⁻¹ • a = π⁻¹ a from rfl, show π⁻¹ • c = π⁻¹ c from rfl]
+    simp
+
+instance : NominalSet 𝔸 (StepModel 𝔸 X) := Subtype.instNominalSetElem 𝔸
+
+@[simp] lemma smul_val (π : FPerm 𝔸) (f : StepModel 𝔸 X) : (π • f).val = π • f.val :=
+  Subtype.smul_val 𝔸 π f
+
+instance instValEquivariant : Function.Equivariant 𝔸 (Subtype.val : StepModel 𝔸 X → PermSet.FinsuppFunction 𝔸 𝔸 X) :=
+  Subtype.instValEquivariant 𝔸
+
+@[simp] lemma supp {f : StepModel 𝔸 X} : NominalSet.supp 𝔸 f = NominalSet.supp 𝔸 f.val :=
+  Subtype.supp 𝔸
+
+@[simp] lemma fresh {a : 𝔸} {f : StepModel 𝔸 X} : a # f ↔ a # f.val :=
+  Subtype.fresh 𝔸
+
+
+
+end StepModel