prove well-definedness of abs

1 files changed, 85 insertions, 0 deletions

diff --git a/Nominal/NameRestriction/Model.lean b/Nominal/NameRestriction/Model.lean
index d09bebd..a694c05 100644
--- a/Nominal/NameRestriction/Model.lean
+++ b/Nominal/NameRestriction/Model.lean
@@ -908,6 +908,91 @@ private noncomputable def abs' : NameAbstraction 𝔸 X → PermSet.FinsuppFunct
       apply NominalSet.supp_is_support
     · apply NominalSet.supp_finite⟩
 
+private lemma abs_req2 {a : 𝔸} {x : X} : Req2 𝔸 (abs' 𝔸 (⟪a⟫ x)) := by
+  intro b c hcfresh hcb
+  have hinf : (NominalSet.supp 𝔸 x ∪ {a} ∪ {b} ∪ {c})ᶜ.Infinite := by
+    apply Set.Finite.infinite_compl
+    rw [Set.finite_union, Set.finite_union, Set.finite_union]
+    constructor
+    · constructor
+      · constructor
+        · apply NominalSet.supp_finite
+        · apply Set.finite_singleton
+      · apply Set.finite_singleton
+    · apply Set.finite_singleton
+  obtain ⟨d, hd⟩ := hinf.nonempty
+  simp only [Set.compl_union, Set.mem_inter_iff, Set.mem_compl_iff] at hd
+  have hdx : d # x := hd.left.left.left
+  have hda : d ≠ a := hd.left.left.right
+  have hdb : d ≠ b := hd.left.right
+  have hdc : d ≠ c := hd.right
+  have hinf' : (NominalSet.supp 𝔸 (⸨a, d⸩ • x) ∪ NominalSet.supp 𝔸 (abs' 𝔸 (⟪a⟫ x)) ∪ {b} ∪ {d})ᶜ.Infinite := by
+    apply Set.Finite.infinite_compl
+    rw [Set.finite_union, Set.finite_union, Set.finite_union]
+    constructor
+    · constructor
+      · constructor
+        · apply NominalSet.supp_finite
+        · apply NominalSet.supp_finite
+      · apply Set.finite_singleton
+    · apply Set.finite_singleton
+  obtain ⟨e, he⟩ := hinf'.nonempty
+  simp only [Set.compl_union, Set.mem_inter_iff, Set.mem_compl_iff] at he
+  have hex : e # (⸨a, d⸩ • x) := he.left.left.left
+  have hefresh : e # abs' 𝔸 (⟪a⟫ x) := he.left.left.right
+  have heb : e ≠ b := he.left.right
+  have hed : e ≠ d := he.right
+  rw [choose_restriction' 𝔸 (abs' 𝔸 (⟪a⟫ x)) b b _ _ hcfresh hefresh hcb heb hcb heb]
+  simp only [abs', abs'', Quotient.lift_mk, PermSet.Finsupp.smul_val, PermSet.smul_function,
+    FPerm.swap_inv, PermSet.atom_swap, Equiv.swap_apply_left]
+  have ⟨hdx₁, hda₁, hdb₁⟩ := chooseFresh_fresh 𝔸 x a b
+  have ⟨hdx₂, hda₂, hde₂⟩ := chooseFresh_fresh 𝔸 x a e
+  rw [abs_choice 𝔸 _ _ hdx₁ hdx hda₁ hda hdb₁ hdb]
+  rw [abs_choice 𝔸 _ _ hdx₂ hdx hda₂ hda hde₂ (Ne.symm hed)]
+  nth_rw 1 [show e = ⸨b,e⸩ • b by simp]
+  rw [← AlgebraStructure.res_equivariant]
+  nth_rw 6 [← show ⸨e,d⸩ • b = b from FPerm.swap_apply_of_ne_of_ne (Ne.symm heb) (Ne.symm hdb)]
+  rw [← AlgebraStructure.res_equivariant]
+  rw [← MulAction.mul_smul]
+  rw [FPerm.mul_swap_eq_swap_mul, FPerm.swap_apply_right, FPerm.swap_apply_of_ne_of_ne hdb (Ne.symm hed)]
+  rw [MulAction.mul_smul]
+  rw [show ⸨b,e⸩ • (b \ (e \ (⸨a,d⸩ • x))) = (b \ (e \ (⸨a,d⸩ • x))) by
+    apply NominalSet.fresh_swap_fix
+    · show b # AlgebraStructure.res.toFun (⟪b⟫ AlgebraStructure.res (⟪e⟫ ⸨a,d⸩ • x))
+      apply Function.Equivariant.preserve_fresh
+      rw [NameAbstraction.fresh]; right; rfl
+    · show e # AlgebraStructure.res.toFun (⟪b⟫ AlgebraStructure.res (⟪e⟫ ⸨a,d⸩ • x))
+      apply Function.Equivariant.preserve_fresh
+      rw [NameAbstraction.fresh]; left
+      show e # AlgebraStructure.res.toFun (⟪e⟫ ⸨a,d⸩ • x)
+      apply Function.Equivariant.preserve_fresh
+      rw [NameAbstraction.fresh]; right; rfl]
+  rw [AlgebraStructure.ax_swap]
+  nth_rw 3 [AlgebraStructure.res_equivariant]
+  rw [show ⸨b,d⸩ • e = e from FPerm.swap_apply_of_ne_of_ne heb hed]
+  apply AlgebraStructure.ax_redundant
+
+noncomputable def abs : NameAbstraction 𝔸 X → StepModel 𝔸 X :=
+  fun p ↦ ⟨abs' 𝔸 p, by
+    suffices ∀ p, Req2 𝔸 (abs' 𝔸 p) by apply this
+    apply Quotient.ind; intro ⟨a, x⟩
+    apply abs_req2⟩
+
+instance : Function.Equivariant 𝔸 (abs 𝔸 : NameAbstraction 𝔸 X → StepModel 𝔸 X) := by
+  constructor; intro x π
+  apply Subtype.eq; apply Subtype.eq
+  simp only [abs, abs', smul_val, PermSet.Finsupp.smul_val]
+  rw [← Function.equivariant]
+
+lemma abs_eq' {a : 𝔸} {x : X} {b : 𝔸} :
+    (abs 𝔸 (⟪a⟫ x)).val.val b = ⸨b,chooseFresh 𝔸 x a b⸩ • (b \ ⸨a,chooseFresh 𝔸 x a b⸩ • x) := rfl
+
+lemma abs_eq {a : 𝔸} {x : X} {b : 𝔸} :
+    ∀ c, c # x → c ≠ a → c ≠ b →
+      (abs 𝔸 (⟪a⟫ x)).val.val b = ⸨b,c⸩ • (b \ ⸨a,c⸩ • x) := by
+  intro d hdx hda hdb
+  have ⟨hcx, hca, hcb⟩ := chooseFresh_fresh 𝔸 x a b
+  apply abs_choice 𝔸 _ _ hcx hdx hca hda hcb hdb
 
 end StepModel