well-definedness of union

1 files changed, 248 insertions, 35 deletions

diff --git a/Nominal/NameRestriction/Model.lean b/Nominal/NameRestriction/Model.lean
index 8ef60fe..7cc0df6 100644
--- a/Nominal/NameRestriction/Model.lean
+++ b/Nominal/NameRestriction/Model.lean
@@ -31,7 +31,7 @@ private abbrev AlgebraStructure.join' {X : Type} [NominalSet 𝔸 X] [AlgebraStr
 
 notation "⊥[" A "]" => AlgebraStructure.bot' A ()
 notation:60 x " ∨[" A "] " y => AlgebraStructure.join' A (x, y)
-infixl:60 " \\ " => fun a x => AlgebraStructure.res (⟪a⟫ x)
+notation:60 a " \\ " x => AlgebraStructure.res (⟪a⟫ x)
 
 namespace AlgebraStructure
 
@@ -43,6 +43,15 @@ lemma bot_supp : NominalSet.supp 𝔸 (⊥[𝔸] : X) = ∅ := by
   grw [Function.Equivariant.supp_subset]
   simp
 
+lemma bot_fresh {a : 𝔸} : a # (⊥[𝔸] : X) := by
+  simp [NominalSet.IsFresh, bot_supp]
+
+lemma bot_equivariant {π : FPerm 𝔸} : π • (⊥[𝔸] : X) = ⊥[𝔸] := by
+  show π ∈ PermSet.fix' 𝔸 (bot' 𝔸 ())
+  apply NominalSet.supp_is_support
+  rw [bot_supp]
+  intro a ha; contradiction
+
 lemma join_equivariant {x y : X} {π : FPerm 𝔸} : π • (x ∨[𝔸] y) = (π • x) ∨[𝔸] (π • y) := by
   show π • (join' 𝔸).toFun (x, y) = (join' 𝔸).toFun (π • (x, y))
   rw [← Function.equivariant]
@@ -86,7 +95,6 @@ def union : (BaseModel 𝔸 X × BaseModel 𝔸 X) → BaseModel 𝔸 X := PermS
 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⟩)
@@ -200,11 +208,59 @@ end BaseModel
 
 -- Step Model: \bar{M₁} X
 
+def Req1 {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] (f : PermSet.FinsuppFunction 𝔸 𝔸 X) :=
+  -- Support for individual atoms may only additionally add that atom
+  ∀ a, PermSet.HasSupport 𝔸 (f.val a) (NominalSet.supp 𝔸 f ∪ {a})
+
+lemma Req1.choose_restriction
+    {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] (f : PermSet.FinsuppFunction 𝔸 𝔸 X) :
+    Req1 𝔸 f → ∀ (a c d : 𝔸), c # f → d # f → c ≠ a → d ≠ a →
+      (c \ (⸨a, c⸩ • f).val a) = (d \ (⸨a, d⸩ • f).val a) := by
+  intro hreq a c d hcfresh hdfresh hca hda
+  nth_rw 1 [← show ⸨c, d⸩ • f = f from NominalSet.fresh_swap_fix 𝔸 hcfresh hdfresh]
+  simp only [PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv, PermSet.atom_swap,
+    Equiv.swap_apply_left]
+  rw [show ⟪d⟫ ⸨a,d⸩ • f.val d = ⟪⸨a, d⸩ • a⟫ ⸨a,d⸩ • f.val d by simp]
+  rw [show ⟪⸨a, d⸩ • a⟫ ⸨a,d⸩ • f.val d = ⸨a, d⸩ • ⟪a⟫ f.val d by simp]
+  rw [show ⟪c⟫ ⸨a,c⸩ • ⸨c, d⸩ • f.val d = ⟪⸨a, c⸩ • a⟫ ⸨a,c⸩ • ⸨c, d⸩ • f.val d by simp]
+  rw [show ⟪⸨a, c⸩ • a⟫ ⸨a,c⸩ • ⸨c, d⸩ • f.val d = ⸨a, c⸩ • ⟪a⟫ ⸨c, d⸩ • f.val d by simp]
+  nth_rw 2 [show a = ⸨c, d⸩ • a by
+    symm; apply FPerm.swap_apply_of_ne_of_ne
+    · symm; exact hca
+    · symm; exact hda]
+  rw [show ⟪⸨c, d⸩ • a⟫ ⸨c,d⸩ • f.val d = ⸨c, d⸩ • ⟪a⟫ f.val d by simp]
+  suffices ⸨a,c⸩ • ⸨c,d⸩ • ⟪a⟫ f.val d = ⸨a,d⸩ • ⟪a⟫ f.val d by rw [this]
+  rw [← MulAction.mul_smul]
+  apply PermSet.support_permutations_eq 𝔸 (NominalSet.supp_is_support 𝔸)
+  intro b hb
+  by_cases hba : b = a <;> by_cases hbc : b = c <;> by_cases hbd : b = d
+  · simp [*] at *
+  · simp [*] at *
+  · simp [*] at *
+  · simp [*] at *
+  · rw [← hbc, ← hbd]; simp
+  · rw [hbc] at hb
+    suffices c ∉ NominalSet.supp 𝔸 (⟪a⟫ f.val d) by contradiction
+    suffices c ∉ NominalSet.supp 𝔸 (f.val d) by simp [this]
+    intro hc
+    have h := NominalSet.support_subset_supp 𝔸 (hreq d) (by simp [NominalSet.supp_finite])
+    specialize h hc
+    simp only [Set.union_singleton, Set.mem_insert_iff] at h
+    cases h
+    · simp [*] at *
+    · contradiction
+  · simp [*] at *
+  · simp only [Subgroup.coe_mul, Equiv.Perm.coe_mul, Function.comp_apply]
+    rw [FPerm.swap_apply_of_ne_of_ne hbc hbd]
+    rw [FPerm.swap_apply_of_ne_of_ne hba hbc]
+    rw [FPerm.swap_apply_of_ne_of_ne hba hbd]
+
+def Req2 {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] (f : PermSet.FinsuppFunction 𝔸 𝔸 X) :=
+  -- Traces for all atoms include those from bound traces
+  ∀ a c, c # f → c ≠ a → f.val a = f.val a ∨[𝔸] (c \ (⸨a, c⸩ • f).val a)
+
 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) }
+  { f : PermSet.FinsuppFunction 𝔸 𝔸 X | Req1 𝔸 f ∧ Req2 𝔸 f }
 
 def StepModel (X : Type) [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] : Type :=
   permissibleFunctions 𝔸 X
@@ -213,37 +269,47 @@ 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,
+private lemma permissibleFunctions_req1
+    (f : PermSet.FinsuppFunction 𝔸 𝔸 X) (π : FPerm 𝔸) : Req1 𝔸 f → Req1 𝔸 (π • f) := by
+  intro hf a
+  specialize hf (π⁻¹ • a)
+  rw [show NominalSet.supp 𝔸 (π • f) = π • NominalSet.supp 𝔸 f from Function.equivariant _ _ _ _]
+  rw [show ({a} : Set 𝔸) = π • {π⁻¹ • a} by simp]
+  rw [← Set.smul_set_union]
+  rw [PermSet.Finsupp.smul_val, PermSet.smul_function]
+  rw [← Rel.equivariant 𝔸 (PermSet.HasSupport 𝔸)]
+  exact hf
+
+private lemma permissibleFunctions_req2
+    (f : PermSet.FinsuppFunction 𝔸 𝔸 X) (π : FPerm 𝔸) : Req2 𝔸 f → Req2 𝔸 (π • f) := by
+  intro hf a c hcf hca
+  specialize hf (π⁻¹ • a) (π⁻¹ • 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)
+  simp only [PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv, PermSet.atom_swap,
+    Equiv.swap_apply_left]
+  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 : Set.Equivariant 𝔸 (permissibleFunctions 𝔸 X) := by
+  constructor; intro f π hf
   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
+  · exact permissibleFunctions_req1 𝔸 f π hf.left
+  · exact permissibleFunctions_req2 𝔸 f π hf.right
 
 instance : NominalSet 𝔸 (StepModel 𝔸 X) := Subtype.instNominalSetElem 𝔸
 
@@ -259,6 +325,153 @@ instance instValEquivariant : Function.Equivariant 𝔸 (Subtype.val : StepModel
 @[simp] lemma fresh {a : 𝔸} {f : StepModel 𝔸 X} : a # f ↔ a # f.val :=
   Subtype.fresh 𝔸
 
+private def bot' : PermSet.FinsuppFunction 𝔸 𝔸 X :=
+  ⟨fun _ ↦ ⊥[𝔸], by
+    use ∅; constructor
+    · intro π hπ; ext a
+      simp [AlgebraStructure.bot_equivariant]
+    · exact Set.finite_empty⟩
 
+private lemma bot_req1 : Req1 𝔸 (bot' 𝔸 : PermSet.FinsuppFunction 𝔸 𝔸 X) := by
+  intro a π _
+  apply AlgebraStructure.bot_equivariant
+
+private lemma bot_req2 : Req2 𝔸 (bot' 𝔸 : PermSet.FinsuppFunction 𝔸 𝔸 X) := by
+  intro a c _ _
+  simp only [PermSet.Finsupp.smul_val, PermSet.smul_function, bot']
+  rw [AlgebraStructure.bot_equivariant]
+  rw [AlgebraStructure.ax_fresh c (⊥[𝔸]) (AlgebraStructure.bot_fresh 𝔸)]
+  rw [AlgebraStructure.ax_idempotent]
+
+def bot : Unit → StepModel 𝔸 X :=
+  fun _ ↦ ⟨bot' 𝔸, ⟨bot_req1 𝔸, bot_req2 𝔸⟩⟩
+
+instance : Function.Equivariant 𝔸 (bot 𝔸 : Unit → StepModel 𝔸 X) := by
+  constructor; intro _ π
+  apply Subtype.eq; ext a
+  simp [bot, bot', AlgebraStructure.bot_equivariant]
+
+private def union'' : (StepModel 𝔸 X × StepModel 𝔸 X) → 𝔸 → X :=
+  fun (f, g) ↦ fun a ↦ f.val.val a ∨[𝔸] g.val.val a
+
+instance : Function.Equivariant 𝔸 (union'' 𝔸 : (StepModel 𝔸 X × StepModel 𝔸 X) → 𝔸 → X) := by
+  constructor; intro (f, g) π
+  ext a
+  simp only [union'', smul_val, PermSet.Finsupp.smul_val, PermSet.smul_function]
+  rw [AlgebraStructure.join_equivariant]
+
+private def union' : (StepModel 𝔸 X × StepModel 𝔸 X) → PermSet.FinsuppFunction 𝔸 𝔸 X :=
+  fun p ↦ ⟨union'' 𝔸 p, by
+    use NominalSet.supp 𝔸 p; constructor
+    · apply Function.Equivariant.preserve_support
+      apply NominalSet.supp_is_support
+    · apply NominalSet.supp_finite⟩
+
+private lemma union_req1 {f g : StepModel 𝔸 X} : Req1 𝔸 (union' 𝔸 (f, g)) := by
+  intro a π hπ
+  have hπ₁ : π ∈ PermSet.fix 𝔸 (NominalSet.supp 𝔸 (union' 𝔸 (f, g))) := by
+    apply PermSet.fix_antitone_mem 𝔸 hπ; exact Set.subset_union_left
+  have hπ₂ : π • a = a := by
+    apply hπ; apply Set.mem_union_right; rfl
+  show π • (f.val.val a ∨[𝔸] g.val.val a) = (union' 𝔸 (f, g)).val a
+  rw [AlgebraStructure.join_equivariant]
+  rw [show π • f.val.val a = (π • f).val.val (π • a) by simp]
+  rw [show π • g.val.val a = (π • g).val.val (π • a) by simp]
+  rw [show ((π • f).val.val (π • a) ∨[𝔸] (π • g).val.val (π • a)) = (union' 𝔸 (π • f, π • g)).val (π • a) from rfl]
+  suffices union' 𝔸 (π • f, π • g) = π • union' 𝔸 (f, g) by
+    rw [this]
+    rw [show π • union' 𝔸 (f, g) = union' 𝔸 (f, g) from NominalSet.supp_is_support 𝔸 hπ₁]
+    rw [hπ₂]
+  ext b
+  simp [union', union'', AlgebraStructure.join_equivariant]
+
+private lemma union_req2 {f g : StepModel 𝔸 X} : Req2 𝔸 (union' 𝔸 (f, g)) := by
+  intro a c hcfresh hca
+  have hinf : (NominalSet.supp 𝔸 (union' 𝔸 (f, g)) ∪ NominalSet.supp 𝔸 f ∪ NominalSet.supp 𝔸 g ∪ {a})ᶜ.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 NominalSet.supp_finite
+    · apply Set.finite_singleton
+  obtain ⟨d, hd⟩ := hinf.nonempty
+  simp only [supp, Set.compl_union, Set.mem_inter_iff, Set.mem_compl_iff] at hd
+  have hdfresh : d # union' 𝔸 (f, g) := hd.left.left.left
+  have hdf : d # f.val := hd.left.left.right
+  have hdg : d # g.val := hd.left.right
+  have hda : d ≠ a := hd.right
+  simp only [PermSet.Finsupp.smul_val]
+  have h := Req1.choose_restriction 𝔸 (union' 𝔸 (f, g)) (union_req1 𝔸) a c d hcfresh hdfresh hca hda
+  simp only [PermSet.Finsupp.smul_val] at h
+  rw [h]
+  simp only [union', union'', PermSet.smul_function, FPerm.swap_inv, PermSet.atom_swap,
+    Equiv.swap_apply_left]
+  nth_rw 1 [show d = ⸨a, d⸩ • a by simp]
+  rw [← AlgebraStructure.res_equivariant]
+  rw [AlgebraStructure.ax_distributive]
+  rw [AlgebraStructure.join_equivariant]
+  rw [AlgebraStructure.res_equivariant]
+  rw [AlgebraStructure.res_equivariant]
+  rw [AlgebraStructure.ax_associative]
+  nth_rw 3 [AlgebraStructure.ax_commutative]
+  rw [AlgebraStructure.ax_associative]
+  rw [← AlgebraStructure.ax_associative]
+  nth_rw 4 [AlgebraStructure.ax_commutative]
+  rw [show ⸨a, d⸩ • a = d by simp]
+  have hf := f.prop.right a d hdf hda
+  have hg := g.prop.right a d hdg hda
+  simp only [PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv, PermSet.atom_swap,
+    Equiv.swap_apply_left] at hf hg
+  rw [← hf, ← hg]
+
+def union : (StepModel 𝔸 X × StepModel 𝔸 X) → StepModel 𝔸 X :=
+  fun (f, g) ↦ ⟨union' 𝔸 (f, g), ⟨union_req1 𝔸, union_req2 𝔸⟩⟩
+
+instance : Function.Equivariant 𝔸 (union 𝔸 : (StepModel 𝔸 X × StepModel 𝔸 X) → StepModel 𝔸 X) := by
+  constructor; intro x π
+  apply Subtype.eq; ext a
+  simp only [union, union', Prod.mk.eta, smul_val, PermSet.Finsupp.smul_val]
+  rw [show (π • x.fst, π • x.snd) = π • x by ext <;> simp]
+  rw [← Function.equivariant]
+
+private noncomputable def chooseFresh (f : StepModel 𝔸 X) (a : 𝔸) : 𝔸 :=
+  have hinf : (NominalSet.supp 𝔸 f ∪ {a})ᶜ.Infinite := by
+    apply Set.Finite.infinite_compl
+    simp only [supp, Set.union_singleton, Set.finite_insert]
+    apply NominalSet.supp_finite
+  Classical.choose hinf.nonempty
+
+private lemma chooseFresh_fresh (f : StepModel 𝔸 X) (a : 𝔸) :
+    chooseFresh 𝔸 f a # f.val ∧ chooseFresh 𝔸 f a ≠ a := by
+  have h : chooseFresh 𝔸 f a ∈ (NominalSet.supp 𝔸 f ∪ {a})ᶜ := Classical.choose_spec _
+  simp only [supp, Set.union_singleton, Set.mem_compl_iff, Set.mem_insert_iff, not_or] at h
+  exact ⟨h.right, h.left⟩
+
+private noncomputable def restrict'' : NameAbstraction 𝔸 (StepModel 𝔸 X) → 𝔸 → X := Quotient.lift
+  (fun ⟨a, f⟩ ↦
+    let c := chooseFresh 𝔸 f a
+    fun b ↦ if a = b then (c \ (⸨a, c⸩ • f.val).val a) else f.val.val b)
+  (by
+    intro ⟨a₁, f₁⟩ ⟨a₂, f₂⟩ haeq
+    ext b
+    rw [← NameAbstraction.eq_iff_alpha_eq 𝔸 (StepModel 𝔸 X), NameAbstraction.eq_iff_cases] at haeq
+    cases haeq with
+    | inl h => rw [h.left, h.right]
+    | inr h =>
+      simp only [PermSet.Finsupp.smul_val]
+      by_cases h₁ : a₁ = b <;> by_cases h₂ : a₂ = b <;> simp only [h₁, h₂, ↓reduceIte]
+      · rw [← h₂] at h₁
+        have hcontra := h.left
+        contradiction
+      ·
+        sorry
+      · rw [h.right.right, ← h₂]
+        simp only [smul_val, PermSet.Finsupp.smul_val]
+        have heq := Req1.choose_restriction 𝔸 f₂.val f₂.prop.left
+        sorry
+      · sorry)
 
 end StepModel