1 files changed, 194 insertions, 0 deletions
diff --git a/Nominal/NameRestriction/Model.lean b/Nominal/NameRestriction/Model.lean
index 9c6103f..adefdb4 100644
--- a/Nominal/NameRestriction/Model.lean
+++ b/Nominal/NameRestriction/Model.lean
@@ -661,4 +661,198 @@ private lemma restrict_req2 {a : 𝔸} {f : StepModel 𝔸 X} : Req2 𝔸 (restr
   rw [show ⸨b,e⸩ • d = d from FPerm.swap_apply_of_ne_of_ne hdb (Ne.symm hed)]
   rw [AlgebraStructure.ax_swap]
 
+noncomputable def restrict : NameAbstraction 𝔸 (StepModel 𝔸 X) → StepModel 𝔸 X :=
+  fun p ↦ ⟨restrict' 𝔸 p,
+  ⟨by
+    suffices ∀ p, Req1 𝔸 (restrict' 𝔸 p) by apply this
+    apply Quotient.ind; intro ⟨a, x⟩
+    apply restrict_req1,
+   by
+    suffices ∀ p, Req2 𝔸 (restrict' 𝔸 p) by apply this
+    apply Quotient.ind; intro ⟨a, x⟩
+    apply restrict_req2⟩⟩
+
+instance : Function.Equivariant 𝔸 (restrict 𝔸 : NameAbstraction 𝔸 (StepModel 𝔸 X) → StepModel 𝔸 X) := by
+  constructor; intro x π
+  apply Subtype.eq; apply Subtype.eq
+  simp only [restrict, restrict', smul_val, PermSet.Finsupp.smul_val]
+  rw [← Function.equivariant]
+
+@[simp] lemma bot_eq {a : 𝔸} :
+    (bot 𝔸 () : StepModel 𝔸 X).val.val a = ⊥[𝔸] := rfl
+
+@[simp] lemma union_eq {f₁ f₂ : StepModel 𝔸 X} {a : 𝔸} :
+    (union 𝔸 (f₁, f₂)).val.val a = f₁.val.val a ∨[𝔸] f₂.val.val a := rfl
+
+lemma restrict_eq' {a : 𝔸} {f : StepModel 𝔸 X} {b : 𝔸} :
+    (restrict 𝔸 (⟪a⟫ f)).val.val b =  ((chooseFresh 𝔸 f a b) \ (⸨a, (chooseFresh 𝔸 f a b)⸩ • f.val).val b) := rfl
+
+lemma restrict_eq {a : 𝔸} {f : StepModel 𝔸 X} {b : 𝔸} :
+    ∀ c, c # f → c ≠ a → c ≠ b →
+      (restrict 𝔸 (⟪a⟫ f)).val.val b =  (c \ (⸨a, c⸩ • f.val).val b) := by
+  intro d hdf hda hdb
+  have ⟨hcf, hca, hcb⟩ := chooseFresh_fresh 𝔸 f a b
+  rw [fresh] at hdf
+  apply Req1.choose_restriction 𝔸 f.val f.prop.left a b _ _ hcf hdf hca hda hcb hdb
+
+lemma restrict_supp (f : StepModel 𝔸 X) (a c : 𝔸) :
+    c # f → c # (restrict 𝔸 (⟪a⟫ f)) := by
+  intro hf hcontra
+  have h : NominalSet.supp 𝔸 (restrict 𝔸 (⟪a⟫ f)) ⊆ NominalSet.supp 𝔸 (⟪a⟫ f) :=
+    Function.Equivariant.supp_subset 𝔸
+  specialize h hcontra
+  simp only [NameAbstraction.supp, supp, Set.mem_diff, Set.mem_singleton_iff] at h
+  have := h.left
+  rw [← supp] at this
+  contradiction
+
+lemma restrict_mem_supp (f : StepModel 𝔸 X) (a b c : 𝔸) :
+    c # f → c ≠ b → c # (restrict 𝔸 (⟪a⟫ f)).val.val b := by
+  intro hf hb hcontra
+  have h₁ : NominalSet.supp 𝔸 ((restrict 𝔸 (⟪a⟫ f)).val.val b) ⊆ NominalSet.supp 𝔸 (restrict 𝔸 (⟪a⟫ f)).val ∪ {b} :=
+    NominalSet.support_subset_supp 𝔸 (((restrict 𝔸 (⟪a⟫ f)).prop.left b)) (by
+      simp only [Set.union_singleton, Set.finite_insert]
+      apply NominalSet.supp_finite)
+  specialize h₁ hcontra
+  simp only [Set.union_singleton, Set.mem_insert_iff] at h₁
+  cases h₁ with
+  | inl h => contradiction
+  | inr h => rw [← supp] at h; exact restrict_supp 𝔸 f a c hf h
+
+noncomputable instance : AlgebraStructure 𝔸 (StepModel 𝔸 X) where
+  bot := ⟨bot 𝔸, inferInstance⟩
+  join := ⟨union 𝔸, inferInstance⟩
+  res := ⟨restrict 𝔸, inferInstance⟩
+  ax_neutral x := by
+    show union 𝔸 (x, (bot 𝔸 ())) = x
+    apply Subtype.eq; apply Subtype.eq; ext a
+    simp [AlgebraStructure.ax_neutral]
+  ax_idempotent x := by
+    show union 𝔸 (x, x) = x
+    apply Subtype.eq; apply Subtype.eq; ext a
+    simp [AlgebraStructure.ax_idempotent]
+  ax_commutative x y := by
+    show union 𝔸 (x, y) = union 𝔸 (y, x)
+    apply Subtype.eq; apply Subtype.eq; ext a
+    simp [AlgebraStructure.ax_commutative]
+  ax_associative x y z := by
+    show union 𝔸 (union 𝔸 (x, y), z) = union 𝔸 (x, union 𝔸 (y, z))
+    apply Subtype.eq; apply Subtype.eq; ext a
+    simp [AlgebraStructure.ax_associative]
+  ax_fresh a f := by
+    intro hfresh
+    show restrict 𝔸 (⟪a⟫ f) = f
+    apply Subtype.eq; apply Subtype.eq; ext b
+    have ⟨hcf, hca, hcb⟩ := chooseFresh_fresh 𝔸 f a b
+    rw [restrict_eq']
+    rw [fresh] at hfresh
+    rw [show ⸨a,chooseFresh 𝔸 f a b⸩ • f.val = f.val from NominalSet.fresh_swap_fix 𝔸 hfresh hcf]
+    apply AlgebraStructure.ax_fresh
+    intro hcontra
+    have h := NominalSet.support_subset_supp 𝔸 (f.prop.left b) (by simp [NominalSet.supp_finite]) hcontra
+    simp only [Set.union_singleton, Set.mem_insert_iff] at h
+    cases h <;> contradiction
+  ax_swap a₁ a₂ f := by
+    show restrict 𝔸 (⟪a₁⟫ (restrict 𝔸 (⟪a₂⟫ f))) = restrict 𝔸 (⟪a₂⟫ (restrict 𝔸 (⟪a₁⟫ f)))
+    apply Subtype.eq; apply Subtype.eq; ext b
+    by_cases heq : a₁ = a₂
+    · rw [heq]
+    · have hinf : (NominalSet.supp 𝔸 f ∪ {a₁} ∪ {a₂} ∪ {b})ᶜ.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 ⟨c₁, hc₁⟩ := hinf.nonempty
+      simp only [Set.compl_union, Set.mem_inter_iff, Set.mem_compl_iff] at hc₁
+      have hc₁f : c₁ # f := hc₁.left.left.left
+      have hc₁a₁ : c₁ ≠ a₁ := hc₁.left.left.right
+      have hc₁a₂ : c₁ ≠ a₂ := hc₁.left.right
+      have hc₁b : c₁ ≠ b := hc₁.right
+      have hinf' : (NominalSet.supp 𝔸 f ∪ {a₁} ∪ {a₂} ∪ {b} ∪ {c₁})ᶜ.Infinite := by
+        apply Set.Finite.infinite_compl
+        rw [Set.finite_union, Set.finite_union, Set.finite_union, Set.finite_union]
+        constructor
+        · constructor
+          · constructor
+            · constructor
+              · apply NominalSet.supp_finite
+              · apply Set.finite_singleton
+            · apply Set.finite_singleton
+          · apply Set.finite_singleton
+        · apply Set.finite_singleton
+      obtain ⟨c₂, hc₂⟩ := hinf'.nonempty
+      simp only [Set.compl_union, Set.mem_inter_iff, Set.mem_compl_iff] at hc₂
+      have hc₂f : c₂ # f := hc₂.left.left.left.left
+      have hc₂a₁ : c₂ ≠ a₁ := hc₂.left.left.left.right
+      have hc₂a₂ : c₂ ≠ a₂ := hc₂.left.left.right
+      have hc₂b : c₂ ≠ b := hc₂.left.right
+      have hc₂c₁ : c₂ ≠ c₁ := hc₂.right
+      have hc₁f' : c₁ # (⸨a₂,c₂⸩ • f) := by
+        intro hcontra
+        rw [Function.equivariant 𝔸 (NominalSet.supp 𝔸)] at hcontra
+        rw [← PermSet.atom_set_swap_ne_ne 𝔸 hc₁a₂ (Ne.symm hc₂c₁)] at hcontra
+        contradiction
+      have hc₂f' : c₂ # (⸨a₁,c₁⸩ • f) := by
+        intro hcontra
+        rw [Function.equivariant 𝔸 (NominalSet.supp 𝔸)] at hcontra
+        rw [← PermSet.atom_set_swap_ne_ne 𝔸 hc₂a₁ hc₂c₁] at hcontra
+        contradiction
+      rw [restrict_eq 𝔸 c₁ (restrict_supp 𝔸 f a₂ c₁ hc₁f) hc₁a₁ hc₁b]
+      rw [← smul_val, ← Function.equivariant 𝔸 (restrict 𝔸), NameAbstraction.smul]
+      rw [show ⸨a₁,c₁⸩ • a₂ = a₂ from FPerm.swap_apply_of_ne_of_ne (Ne.symm heq) (Ne.symm hc₁a₂)]
+      rw [restrict_eq 𝔸 c₂ hc₂f' hc₂a₂ hc₂b]
+      rw [smul_val, PermSet.Finsupp.smul_val, PermSet.Finsupp.smul_val]
+      rw [restrict_eq 𝔸 c₂ (restrict_supp 𝔸 f a₁ c₂ hc₂f) hc₂a₂ hc₂b]
+      rw [← smul_val, ← Function.equivariant 𝔸 (restrict 𝔸), NameAbstraction.smul]
+      rw [show ⸨a₂,c₂⸩ • a₁ = a₁ from FPerm.swap_apply_of_ne_of_ne heq (Ne.symm hc₂a₁)]
+      rw [restrict_eq 𝔸 c₁ hc₁f' hc₁a₁ hc₁b]
+      rw [smul_val, PermSet.Finsupp.smul_val, PermSet.Finsupp.smul_val]
+      rw [AlgebraStructure.ax_swap]
+      rw [← MulAction.mul_smul, ← MulAction.mul_smul]
+      suffices ⸨a₂,c₂⸩ * ⸨a₁,c₁⸩ = ⸨a₁,c₁⸩ * ⸨a₂,c₂⸩ by rw [this]
+      rw [FPerm.mul_swap_eq_swap_mul]
+      rw [FPerm.swap_apply_of_ne_of_ne heq (Ne.symm hc₂a₁)]
+      rw [FPerm.swap_apply_of_ne_of_ne hc₁a₂ (Ne.symm hc₂c₁)]
+  ax_distributive a f g := by
+    show restrict 𝔸 (⟪a⟫ (union 𝔸 (f, g))) = union 𝔸 (restrict 𝔸 (⟪a⟫ f), restrict 𝔸 (⟪a⟫ g))
+    apply Subtype.eq; apply Subtype.eq; ext b
+    rw [union_eq]
+    have hinf : (NominalSet.supp 𝔸 (union 𝔸 (f, g)) ∪ NominalSet.supp 𝔸 f ∪ NominalSet.supp 𝔸 g ∪ {a} ∪ {b})ᶜ.Infinite := by
+      apply Set.Finite.infinite_compl
+      rw [Set.finite_union, Set.finite_union, Set.finite_union, Set.finite_union]
+      constructor
+      · constructor
+        · constructor
+          · constructor
+            · apply NominalSet.supp_finite
+            · apply NominalSet.supp_finite
+          · apply NominalSet.supp_finite
+        · apply Set.finite_singleton
+      · apply Set.finite_singleton
+    obtain ⟨c, hc⟩ := hinf.nonempty
+    simp only [Set.compl_union, Set.mem_inter_iff, Set.mem_compl_iff] at hc
+    have hcfg : c # (union 𝔸 (f, g)) := hc.left.left.left.left
+    have hcf : c # f := hc.left.left.left.right
+    have hcg : c # g := hc.left.left.right
+    have hca : c ≠ a := hc.left.right
+    have hcb : c ≠ b := hc.right
+    rw [restrict_eq 𝔸 c hcfg hca hcb]
+    rw [PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv, union_eq]
+    rw [AlgebraStructure.join_equivariant]
+    rw [AlgebraStructure.ax_distributive]
+    rw [restrict_eq 𝔸 c hcf hca hcb]
+    rw [PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv]
+    rw [restrict_eq 𝔸 c hcg hca hcb]
+    rw [PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv]
+  ax_redundant a f := by
+    show f = union 𝔸 (f, restrict 𝔸 (⟪a⟫ f))
+    apply Subtype.eq; apply Subtype.eq; ext b
+    rw [union_eq, restrict_eq']
+    sorry
+
 end StepModel