diff options
| -rw-r--r-- | Nominal/NameRestriction/Finsupp.lean | 13 | ||||
| -rw-r--r-- | Nominal/NameRestriction/Model.lean | 315 |
2 files changed, 199 insertions, 129 deletions
diff --git a/Nominal/NameRestriction/Finsupp.lean b/Nominal/NameRestriction/Finsupp.lean index 3059bba..4311bee 100644 --- a/Nominal/NameRestriction/Finsupp.lean +++ b/Nominal/NameRestriction/Finsupp.lean @@ -64,6 +64,19 @@ instance {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] : PermSet 𝔸 (X → Y) abbrev FinsuppFunction (X Y : Type) [PermSet 𝔸 X] [PermSet 𝔸 Y] : Type := Finsupp 𝔸 (X → Y) +lemma FinsuppFunction.supp_image {X Y : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y] (f : PermSet.FinsuppFunction 𝔸 X Y) : + ∀ x, PermSet.HasSupport 𝔸 (f.val x) (NominalSet.supp 𝔸 f ∪ NominalSet.supp 𝔸 x) := by + intro x π hπ + have hπ₁ : π ∈ PermSet.fix 𝔸 (NominalSet.supp 𝔸 f) := by + apply PermSet.fix_antitone_mem 𝔸 hπ; exact Set.subset_union_left + have hπ₂ : π ∈ PermSet.fix 𝔸 (NominalSet.supp 𝔸 x) := by + apply PermSet.fix_antitone_mem 𝔸 hπ; exact Set.subset_union_right + suffices (π • f).val (π • x) = f.val x by + simp at this + exact this + rw [show π • f = f from NominalSet.supp_is_support 𝔸 hπ₁] + rw [show π • x = x from NominalSet.supp_is_support 𝔸 hπ₂] + variable (X Y : Type) [NominalSet 𝔸 X] [NominalSet 𝔸 Y] namespace Finsupp diff --git a/Nominal/NameRestriction/Model.lean b/Nominal/NameRestriction/Model.lean index 6195099..d09bebd 100644 --- a/Nominal/NameRestriction/Model.lean +++ b/Nominal/NameRestriction/Model.lean @@ -208,15 +208,18 @@ 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 supp_image {X : Type} [NominalSet 𝔸 X] (f : PermSet.FinsuppFunction 𝔸 𝔸 X) : + ∀ a, PermSet.HasSupport 𝔸 (f.val a) (NominalSet.supp 𝔸 f ∪ {a}) := by + intro a + have := PermSet.FinsuppFunction.supp_image 𝔸 f a + rw [NominalSet.supp_atom] at this + exact this -lemma Req1.choose_restriction +lemma choose_restriction' {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] (f : PermSet.FinsuppFunction 𝔸 𝔸 X) : - Req1 𝔸 f → ∀ (a b c d : 𝔸), c # f → d # f → c ≠ a → d ≠ a → c ≠ b → d ≠ b → + ∀ (a b c d : 𝔸), c # f → d # f → c ≠ a → d ≠ a → c ≠ b → d ≠ b → (c \ (⸨a, c⸩ • f).val b) = (d \ (⸨a, d⸩ • f).val b) := by - intro hreq a b c d hcfresh hdfresh hca hda hcb hdb + intro a b c d hcfresh hdfresh hca hda hcb hdb by_cases heq : b = a · nth_rw 1 [← show ⸨c, d⸩ • f = f from NominalSet.fresh_swap_fix 𝔸 hcfresh hdfresh] simp only [heq, PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv, @@ -242,7 +245,7 @@ lemma Req1.choose_restriction 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]) + have h := NominalSet.support_subset_supp 𝔸 (supp_image 𝔸 f d) (by simp [NominalSet.supp_finite]) specialize h hc simp only [Set.union_singleton, Set.mem_insert_iff] at h cases h @@ -263,7 +266,7 @@ lemma Req1.choose_restriction · rw [NameAbstraction.fresh]; right; rfl · rw [NameAbstraction.fresh]; left rw [NominalSet.IsFresh]; intro hcontra - have h := NominalSet.support_subset_supp 𝔸 (hreq b) (by simp [NominalSet.supp_finite]) hcontra + have h := NominalSet.support_subset_supp 𝔸 (supp_image 𝔸 f b) (by simp [NominalSet.supp_finite]) hcontra simp only [Set.union_singleton, Set.mem_insert_iff] at h cases h <;> contradiction] rw [show ⸨a,d⸩ • ⟪a⟫ f.val b = ⟪a⟫ f.val b by @@ -271,7 +274,7 @@ lemma Req1.choose_restriction · rw [NameAbstraction.fresh]; right; rfl · rw [NameAbstraction.fresh]; left rw [NominalSet.IsFresh]; intro hcontra - have h := NominalSet.support_subset_supp 𝔸 (hreq b) (by simp [NominalSet.supp_finite]) hcontra + have h := NominalSet.support_subset_supp 𝔸 (supp_image 𝔸 f b) (by simp [NominalSet.supp_finite]) hcontra simp only [Set.union_singleton, Set.mem_insert_iff] at h cases h <;> contradiction] @@ -280,7 +283,7 @@ def Req2 {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] (f : PermSet.F ∀ 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 | Req1 𝔸 f ∧ Req2 𝔸 f } + { f : PermSet.FinsuppFunction 𝔸 𝔸 X | Req2 𝔸 f } def StepModel (X : Type) [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] : Type := permissibleFunctions 𝔸 X @@ -289,17 +292,6 @@ namespace StepModel variable {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] -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 @@ -326,10 +318,7 @@ private lemma permissibleFunctions_req2 simp instance : Set.Equivariant 𝔸 (permissibleFunctions 𝔸 X) := by - constructor; intro f π hf - constructor - · exact permissibleFunctions_req1 𝔸 f π hf.left - · exact permissibleFunctions_req2 𝔸 f π hf.right + constructor; exact permissibleFunctions_req2 𝔸 instance : NominalSet 𝔸 (StepModel 𝔸 X) := Subtype.instNominalSetElem 𝔸 @@ -345,6 +334,13 @@ instance instValEquivariant : Function.Equivariant 𝔸 (Subtype.val : StepModel @[simp] lemma fresh {a : 𝔸} {f : StepModel 𝔸 X} : a # f ↔ a # f.val := Subtype.fresh 𝔸 +lemma choose_restriction (f : StepModel 𝔸 X) : + ∀ (a b c d : 𝔸), c # f → d # f → c ≠ a → d ≠ a → c ≠ b → d ≠ b → + (c \ (⸨a, c⸩ • f.val).val b) = (d \ (⸨a, d⸩ • f.val).val b) := by + intro a b c d hcf hdf hca hda hcb hdb + rw [fresh] at hcf hdf + exact choose_restriction' 𝔸 f.val a b c d hcf hdf hca hda hcb hdb + private def bot' : PermSet.FinsuppFunction 𝔸 𝔸 X := ⟨fun _ ↦ ⊥[𝔸], by use ∅; constructor @@ -352,10 +348,6 @@ private def bot' : PermSet.FinsuppFunction 𝔸 𝔸 X := 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'] @@ -364,7 +356,7 @@ private lemma bot_req2 : Req2 𝔸 (bot' 𝔸 : PermSet.FinsuppFunction 𝔸 rw [AlgebraStructure.ax_idempotent] def bot : Unit → StepModel 𝔸 X := - fun _ ↦ ⟨bot' 𝔸, ⟨bot_req1 𝔸, bot_req2 𝔸⟩⟩ + fun _ ↦ ⟨bot' 𝔸, bot_req2 𝔸⟩ instance : Function.Equivariant 𝔸 (bot 𝔸 : Unit → StepModel 𝔸 X) := by constructor; intro _ π @@ -387,24 +379,6 @@ private def union' : (StepModel 𝔸 X × StepModel 𝔸 X) → PermSet.FinsuppF 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 @@ -424,7 +398,7 @@ private lemma union_req2 {f g : StepModel 𝔸 X} : Req2 𝔸 (union' 𝔸 (f, g 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 a c d hcfresh hdfresh hca hda hca hda + have h := choose_restriction' 𝔸 (union' 𝔸 (f, g)) a a c d hcfresh hdfresh hca hda 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, @@ -441,14 +415,14 @@ private lemma union_req2 {f g : StepModel 𝔸 X} : Req2 𝔸 (union' 𝔸 (f, g 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 + have hf := f.prop a d hdf hda + have hg := g.prop 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 𝔸⟩⟩ + fun (f, g) ↦ ⟨union' 𝔸 (f, g), union_req2 𝔸⟩ instance : Function.Equivariant 𝔸 (union 𝔸 : (StepModel 𝔸 X × StepModel 𝔸 X) → StepModel 𝔸 X) := by constructor; intro x π @@ -457,17 +431,17 @@ instance : Function.Equivariant 𝔸 (union 𝔸 : (StepModel 𝔸 X × StepMode rw [show (π • x.fst, π • x.snd) = π • x by ext <;> simp] rw [← Function.equivariant] -private noncomputable def chooseFresh (f : StepModel 𝔸 X) (a b : 𝔸) : 𝔸 := - have hinf : (NominalSet.supp 𝔸 f ∪ {a} ∪ {b})ᶜ.Infinite := by +private noncomputable def chooseFresh {X : Type} [NominalSet 𝔸 X] (x : X) (a b : 𝔸) : 𝔸 := + have hinf : (NominalSet.supp 𝔸 x ∪ {a} ∪ {b})ᶜ.Infinite := by apply Set.Finite.infinite_compl - simp only [supp, Set.union_singleton, Set.finite_insert] + simp only [Set.union_singleton, Set.finite_insert] apply NominalSet.supp_finite Classical.choose hinf.nonempty -private lemma chooseFresh_fresh (f : StepModel 𝔸 X) (a b : 𝔸) : - chooseFresh 𝔸 f a b # f.val ∧ chooseFresh 𝔸 f a b ≠ a ∧ chooseFresh 𝔸 f a b ≠ b := by - have h : chooseFresh 𝔸 f a b ∈ (NominalSet.supp 𝔸 f ∪ {a} ∪ {b})ᶜ := Classical.choose_spec _ - simp only [supp, Set.union_singleton, Set.mem_compl_iff, Set.mem_insert_iff, not_or] at h +private lemma chooseFresh_fresh {X : Type} [NominalSet 𝔸 X] (x : X) (a b : 𝔸) : + chooseFresh 𝔸 x a b # x ∧ chooseFresh 𝔸 x a b ≠ a ∧ chooseFresh 𝔸 x a b ≠ b := by + have h : chooseFresh 𝔸 x a b ∈ (NominalSet.supp 𝔸 x ∪ {a} ∪ {b})ᶜ := Classical.choose_spec _ + simp only [Set.union_singleton, Set.mem_compl_iff, Set.mem_insert_iff, not_or] at h exact ⟨h.right.right, h.right.left, h.left⟩ private noncomputable def restrict'' : NameAbstraction 𝔸 (StepModel 𝔸 X) → 𝔸 → X := Quotient.lift @@ -482,7 +456,7 @@ private noncomputable def restrict'' : NameAbstraction 𝔸 (StepModel 𝔸 X) | inl h => rw [h.left, h.right] | inr h => simp only - have hinf : (NominalSet.supp 𝔸 f₁.val ∪ NominalSet.supp 𝔸 f₂.val ∪ {a₁} ∪ {a₂} ∪ {b})ᶜ.Infinite := by + have hinf : (NominalSet.supp 𝔸 f₁ ∪ NominalSet.supp 𝔸 f₂ ∪ {a₁} ∪ {a₂} ∪ {b})ᶜ.Infinite := by apply Set.Finite.infinite_compl rw [Set.finite_union, Set.finite_union, Set.finite_union, Set.finite_union] constructor @@ -496,15 +470,15 @@ private noncomputable def restrict'' : NameAbstraction 𝔸 (StepModel 𝔸 X) · 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 hcf₁ : c # f₁.val := hc.left.left.left.left - have hcf₂ : c # f₂.val := hc.left.left.left.right + have hcf₁ : c # f₁ := hc.left.left.left.left + have hcf₂ : c # f₂ := hc.left.left.left.right have hca₁ : c ≠ a₁ := hc.left.left.right have hca₂ : c ≠ a₂ := hc.left.right have hcb : c ≠ b := hc.right have ⟨hfreshf₁, hfresha₁, hfreshb₁⟩ := chooseFresh_fresh 𝔸 f₁ a₁ b have ⟨hfreshf₂, hfresha₂, hfreshb₂⟩ := chooseFresh_fresh 𝔸 f₂ a₂ b - rw [Req1.choose_restriction 𝔸 f₁.val f₁.prop.left a₁ b _ c hfreshf₁ hcf₁ hfresha₁ hca₁ hfreshb₁ hcb] - rw [Req1.choose_restriction 𝔸 f₂.val f₂.prop.left a₂ b _ c hfreshf₂ hcf₂ hfresha₂ hca₂ hfreshb₂ hcb] + rw [choose_restriction 𝔸 f₁ a₁ b _ c hfreshf₁ hcf₁ hfresha₁ hca₁ hfreshb₁ hcb] + rw [choose_restriction 𝔸 f₂ a₂ b _ c hfreshf₂ hcf₂ hfresha₂ hca₂ hfreshb₂ hcb] rw [h.right.right] suffices ⸨a₂,c⸩ • f₂.val = ⸨a₁,c⸩ • (⸨a₁,a₂⸩ • f₂).val by rw [this] rw [smul_val, ← MulAction.mul_smul] @@ -520,7 +494,9 @@ private noncomputable def restrict'' : NameAbstraction 𝔸 (StepModel 𝔸 X) contradiction · simp [*] at * · simp [*] at * - · simp [*] at * + · rw [← supp] at hd + rw [hdc] at hd + contradiction · simp only [Subgroup.coe_mul, Equiv.Perm.coe_mul, Function.comp_apply] rw [FPerm.swap_apply_of_ne_of_ne hda₂ hdc] rw [FPerm.swap_apply_of_ne_of_ne hda₁ hda₂] @@ -535,9 +511,9 @@ instance : Function.Equivariant 𝔸 (restrict'' 𝔸 : NameAbstraction 𝔸 (St nth_rw 2 [PermSet.smul_function] have ⟨hcf, hca, hcb⟩ := chooseFresh_fresh 𝔸 (π • f) (π • a) b have ⟨hdf, hda, hdb⟩ := chooseFresh_fresh 𝔸 f a (π⁻¹ • b) - have hcf' : π⁻¹ • chooseFresh 𝔸 (π • f) (π • a) b # f.val := by + have hcf' : π⁻¹ • chooseFresh 𝔸 (π • f) (π • a) b # f := by nth_rw 2 [show f = π⁻¹ • π • f by simp] - rw [← StepModel.fresh, ← Rel.equivariant 𝔸 NominalSet.IsFresh, StepModel.fresh] + rw [← Rel.equivariant 𝔸 NominalSet.IsFresh] exact hcf have hca' : π⁻¹ • chooseFresh 𝔸 (π • f) (π • a) b ≠ a := by intro hcontra @@ -549,7 +525,7 @@ instance : Function.Equivariant 𝔸 (restrict'' 𝔸 : NameAbstraction 𝔸 (St have h : π • π⁻¹ • chooseFresh 𝔸 (π • f) (π • a) b = π • π⁻¹ • b := by rw [hcontra] rw [smul_inv_smul, smul_inv_smul] at h contradiction - have h := Req1.choose_restriction 𝔸 f.val f.prop.left a (π⁻¹ • b) _ _ hdf hcf' hda hca' hdb hcb' + have h := choose_restriction 𝔸 f a (π⁻¹ • b) _ _ hdf hcf' hda hca' hdb hcb' rw [PermSet.Finsupp.smul_val] at h rw [h, AlgebraStructure.res_equivariant, smul_inv_smul] rw [← MulAction.mul_smul] @@ -568,48 +544,9 @@ private noncomputable def restrict' : NameAbstraction 𝔸 (StepModel 𝔸 X) apply NominalSet.supp_is_support · apply NominalSet.supp_finite⟩ -private lemma restrict_req1 {a : 𝔸} {f : StepModel 𝔸 X} : Req1 𝔸 (restrict' 𝔸 (⟪a⟫ f)) := by - intro b π hπ - have hπ₁ : π ∈ PermSet.fix 𝔸 (NominalSet.supp 𝔸 (restrict' 𝔸 (⟪a⟫ f))) := by - apply PermSet.fix_antitone_mem 𝔸 hπ; exact Set.subset_union_left - have hπ₂ : π • b = b := by - apply hπ; apply Set.mem_union_right; rfl - show π • (chooseFresh 𝔸 f a b \ (⸨a,chooseFresh 𝔸 f a b⸩ • f.val).val b) = (restrict' 𝔸 (⟪a⟫ f)).val b - rw [AlgebraStructure.res_equivariant] - rw [PermSet.Finsupp.smul_val] - rw [show π • (⸨a,chooseFresh 𝔸 f a b⸩ • f.val.val) b = (π • ⸨a,chooseFresh 𝔸 f a b⸩ • f.val.val) (π • b) by simp] - rw [← MulAction.mul_smul] - rw [FPerm.mul_swap_eq_swap_mul] - rw [show ⸨π a,π (chooseFresh 𝔸 f a b)⸩ = ⸨π • a,π • (chooseFresh 𝔸 f a b)⸩ from rfl] - rw [MulAction.mul_smul] - let d := chooseFresh 𝔸 (π • f) (π • a) (π • b) - have ⟨hcf, hca, hcb⟩ := chooseFresh_fresh 𝔸 f a b - have ⟨hdf, hda, hdb⟩ := chooseFresh_fresh 𝔸 (π • f) (π • a) (π • b) - have hcf' : π • chooseFresh 𝔸 f a b # (π • f).val := by - rw [← StepModel.fresh, ← Rel.equivariant 𝔸 NominalSet.IsFresh, StepModel.fresh] - exact hcf - have hca' : π • chooseFresh 𝔸 f a b ≠ π • a := by - intro hcontra - have h : π⁻¹ • π • chooseFresh 𝔸 f a b = π⁻¹ • π • a := by rw [hcontra] - rw [inv_smul_smul, inv_smul_smul] at h; contradiction - have hcb' : π • chooseFresh 𝔸 f a b ≠ π • b := by - intro hcontra - have h : π⁻¹ • π • chooseFresh 𝔸 f a b = π⁻¹ • π • b := by rw [hcontra] - rw [inv_smul_smul, inv_smul_smul] at h; contradiction - have h := Req1.choose_restriction 𝔸 (π • f).val (π • f).prop.left (π • a) (π • b) _ _ hcf' hdf hca' hda hcb' hdb - rw [smul_val, PermSet.Finsupp.smul_val, PermSet.Finsupp.smul_val] at h - rw [h] - rw [show (d \ (⸨π • a,d⸩ • π • f.val).val (π • b)) = (restrict' 𝔸 (π • ⟪a⟫ f)).val (π • b) from rfl] - rw [show restrict' 𝔸 (π • ⟪a⟫ f) = π • restrict' 𝔸 (⟪a⟫ f) by - apply Subtype.eq - simp only [restrict', PermSet.Finsupp.smul_val] - rw [Function.equivariant 𝔸 (restrict'' 𝔸)]] - rw [show π • restrict' 𝔸 (⟪a⟫ f) = restrict' 𝔸 (⟪a⟫ f) from NominalSet.supp_is_support 𝔸 hπ₁] - rw [hπ₂] - private lemma restrict_req2 {a : 𝔸} {f : StepModel 𝔸 X} : Req2 𝔸 (restrict' 𝔸 (⟪a⟫ f)) := by intro b c hcfresh hcb - have hinf : (NominalSet.supp 𝔸 f.val ∪ {a} ∪ {b} ∪ {c})ᶜ.Infinite := by + have hinf : (NominalSet.supp 𝔸 f ∪ {a} ∪ {b} ∪ {c})ᶜ.Infinite := by apply Set.Finite.infinite_compl rw [Set.finite_union, Set.finite_union, Set.finite_union] constructor @@ -621,7 +558,7 @@ private lemma restrict_req2 {a : 𝔸} {f : StepModel 𝔸 X} : Req2 𝔸 (restr · 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 hdf : d # f.val := hd.left.left.left + have hdf : d # f := 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 @@ -641,16 +578,16 @@ private lemma restrict_req2 {a : 𝔸} {f : StepModel 𝔸 X} : Req2 𝔸 (restr have hefresh : e # restrict' 𝔸 (⟪a⟫ f) := he.left.left.right have heb : e ≠ b := he.left.right have hed : e ≠ d := he.right - rw [Req1.choose_restriction 𝔸 (restrict' 𝔸 (⟪a⟫ f)) (restrict_req1 𝔸) b b _ _ hcfresh hefresh hcb heb hcb heb] + rw [choose_restriction' 𝔸 (restrict' 𝔸 (⟪a⟫ f)) b b _ _ hcfresh hefresh hcb heb hcb heb] simp only [restrict', restrict'', Quotient.lift_mk] nth_rw 3 [PermSet.Finsupp.smul_val] rw [PermSet.smul_function] simp only [FPerm.swap_inv, PermSet.atom_swap, Equiv.swap_apply_left] have ⟨hdf₁, hda₁, hdb₁⟩ := chooseFresh_fresh 𝔸 f a b have ⟨hdf₂, hda₂, hde₂⟩ := chooseFresh_fresh 𝔸 f a e - rw [Req1.choose_restriction 𝔸 f.val f.prop.left a b _ _ hdf₁ hdf hda₁ hda hdb₁ hdb] - rw [Req1.choose_restriction 𝔸 f.val f.prop.left a e _ _ hdf₂ hdf hda₂ hda hde₂ (Ne.symm hed)] - have h := (⸨a,d⸩ • f).prop.right b e hef heb + rw [choose_restriction 𝔸 f a b _ _ hdf₁ hdf hda₁ hda hdb₁ hdb] + rw [choose_restriction 𝔸 f a e _ _ hdf₂ hdf hda₂ hda hde₂ (Ne.symm hed)] + have h := (⸨a,d⸩ • f).prop b e hef heb simp only [smul_val, PermSet.Finsupp.smul_val] at h nth_rw 3 [PermSet.smul_function] at h simp only [FPerm.swap_inv, PermSet.atom_swap, Equiv.swap_apply_left] at h @@ -662,15 +599,10 @@ private lemma restrict_req2 {a : 𝔸} {f : StepModel 𝔸 X} : Req2 𝔸 (restr 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 + fun p ↦ ⟨restrict' 𝔸 p, by suffices ∀ p, Req2 𝔸 (restrict' 𝔸 p) by apply this apply Quotient.ind; intro ⟨a, x⟩ - apply restrict_req2⟩⟩ + apply restrict_req2⟩ instance : Function.Equivariant 𝔸 (restrict 𝔸 : NameAbstraction 𝔸 (StepModel 𝔸 X) → StepModel 𝔸 X) := by constructor; intro x π @@ -692,8 +624,7 @@ lemma restrict_eq {a : 𝔸} {f : StepModel 𝔸 X} {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 + apply choose_restriction 𝔸 f a b _ _ hcf hdf hca hda hcb hdb lemma restrict_supp (f : StepModel 𝔸 X) (a c : 𝔸) : c # f → c # (restrict 𝔸 (⟪a⟫ f)) := by @@ -710,7 +641,7 @@ lemma mem_fresh (f : StepModel 𝔸 X) (a c : 𝔸) : c # f → c ≠ a → c # intro hf hb hcontra rw [fresh] at hf have h : NominalSet.supp 𝔸 (f.val.val a) ⊆ NominalSet.supp 𝔸 f.val ∪ {a} := - NominalSet.support_subset_supp 𝔸 (f.prop.left a) (by + NominalSet.support_subset_supp 𝔸 (supp_image 𝔸 f.val a) (by simp only [Set.union_singleton, Set.finite_insert] apply NominalSet.supp_finite) specialize h hcontra @@ -742,13 +673,13 @@ noncomputable instance : AlgebraStructure 𝔸 (StepModel 𝔸 X) where 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] + rw [restrict_eq', ← smul_val] + rw [show ⸨a,chooseFresh 𝔸 f a b⸩ • f = f 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 + have h := NominalSet.support_subset_supp 𝔸 (supp_image 𝔸 f.val b) (by simp [NominalSet.supp_finite]) hcontra simp only [Set.union_singleton, Set.mem_insert_iff] at h + rw [← supp] at h cases h <;> contradiction ax_swap a₁ a₂ f := by show restrict 𝔸 (⟪a₁⟫ (restrict 𝔸 (⟪a₂⟫ f))) = restrict 𝔸 (⟪a₂⟫ (restrict 𝔸 (⟪a₁⟫ f))) @@ -854,11 +785,11 @@ noncomputable instance : AlgebraStructure 𝔸 (StepModel 𝔸 X) where by_cases heq : a = b · rw [heq, restrict_eq'] have ⟨hcf, hcb, _⟩ := chooseFresh_fresh 𝔸 f b b - exact f.prop.right b _ hcf hcb + rw [fresh] at hcf + exact f.prop b _ hcf hcb · rw [restrict_eq'] let c := chooseFresh 𝔸 f a b have ⟨hcf, hca, hcb⟩ := chooseFresh_fresh 𝔸 f a b - rw [← fresh] at hcf rw [PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv] rw [show ⸨a,c⸩ • b = b from FPerm.swap_apply_of_ne_of_ne (Ne.symm heq) (Ne.symm hcb)] rw [show ⟪c⟫ ⸨a,c⸩ • f.val.val b = ⸨a,c⸩ • ⟪a⟫ f.val.val b by simp] @@ -869,4 +800,130 @@ noncomputable instance : AlgebraStructure 𝔸 (StepModel 𝔸 X) where apply mem_fresh 𝔸 f b c hcf hcb] apply AlgebraStructure.ax_redundant +private lemma abs_choice {x : X} {a b : 𝔸} : + ∀ (c d : 𝔸), c # x → d # x → c ≠ a → d ≠ a → c ≠ b → d ≠ b → + ⸨b,c⸩ • (b \ (⸨a,c⸩ • x)) = ⸨b,d⸩ • (b \ (⸨a,d⸩ • x)) := by + intro c d hcx hdx hca hda hcb hdb + by_cases heq : c = d + · rw [heq] + · rw [AlgebraStructure.res_equivariant, AlgebraStructure.res_equivariant] + simp only [PermSet.atom_swap, Equiv.swap_apply_left] + suffices ⟪c⟫ ⸨b,c⸩ • ⸨a,c⸩ • x = ⟪d⟫ ⸨b,d⸩ • ⸨a,d⸩ • x by rw [this] + rw [NameAbstraction.eq_iff_cases]; right + constructor + · exact heq + · constructor + · rw [← show ⸨b,d⸩ • c = c from FPerm.swap_apply_of_ne_of_ne hcb heq] + rw [← Rel.equivariant 𝔸 NominalSet.IsFresh] + rw [← show ⸨a,d⸩ • c = c from FPerm.swap_apply_of_ne_of_ne hca heq] + rw [← Rel.equivariant 𝔸 NominalSet.IsFresh] + exact hcx + . nth_rw 2 [← MulAction.mul_smul] + rw [FPerm.mul_swap_eq_swap_mul, FPerm.swap_apply_right, FPerm.swap_apply_of_ne_of_ne (Ne.symm hcb) (Ne.symm hdb)] + rw [MulAction.mul_smul] + nth_rw 3 [← MulAction.mul_smul] + rw [FPerm.mul_swap_eq_swap_mul, FPerm.swap_apply_right, FPerm.swap_apply_of_ne_of_ne (Ne.symm hca) (Ne.symm hda)] + rw [MulAction.mul_smul] + rw [show ⸨c,d⸩ • x = x from NominalSet.fresh_swap_fix 𝔸 hcx hdx] + +private noncomputable def abs'' : NameAbstraction 𝔸 X → 𝔸 → X := Quotient.lift + (fun ⟨a, x⟩ b ↦ + let c := chooseFresh 𝔸 x a b + ⸨b,c⸩ • (b \ (⸨a,c⸩ • x))) + (by + intro ⟨a, x⟩ ⟨a', x'⟩ haeq + ext b + simp only + rw [← NameAbstraction.eq_iff_alpha_eq 𝔸 X, NameAbstraction.eq_iff_cases] at haeq + cases haeq with + | inl h => rw [h.left, h.right] + | inr h => + have hinf : (NominalSet.supp 𝔸 x ∪ NominalSet.supp 𝔸 x' ∪ {a} ∪ {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 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 hcx : c # x := hc.left.left.left.left + have hcx' : c # x' := hc.left.left.left.right + have hca : c ≠ a := hc.left.left.right + have hca' : c ≠ a' := hc.left.right + have hcb : c ≠ b := hc.right + have ⟨hdx, hda, hdb⟩ := chooseFresh_fresh 𝔸 x a b + rw [abs_choice 𝔸 _ _ hdx hcx hda hca hdb hcb] + have ⟨hex', hea', heb⟩ := chooseFresh_fresh 𝔸 x' a' b + rw [abs_choice 𝔸 _ _ hex' hcx' hea' hca' heb hcb] + suffices ⸨a,c⸩ • x = ⸨a',c⸩ • x' by rw [this] + rw [h.right.right, ← MulAction.mul_smul] + rw [FPerm.mul_swap_eq_swap_mul, FPerm.swap_apply_left, FPerm.swap_apply_of_ne_of_ne (Ne.symm h.left) (Ne.symm hca')] + rw [MulAction.mul_smul, FPerm.swap_comm] + nth_rw 2 [NominalSet.fresh_swap_fix 𝔸] + · exact h.right.left + · exact hcx') + +instance : Function.Equivariant 𝔸 (abs'' 𝔸 : NameAbstraction 𝔸 X → 𝔸 → X) := by + constructor + apply Quotient.ind + intro ⟨a, x⟩ π + ext b + simp only [abs'', NameAbstraction.smul, Quotient.lift_mk, PermSet.smul_function] + have ⟨hcx, hca, hcb⟩ := chooseFresh_fresh 𝔸 (π • x) (π • a) b + have ⟨hdx, hda, hdb⟩ := chooseFresh_fresh 𝔸 x a (π⁻¹ • b) + have hcx' : π⁻¹ • chooseFresh 𝔸 (π • x) (π • a) b # x := by + nth_rw 2 [show x = π⁻¹ • π • x by simp] + rw [← Rel.equivariant 𝔸 NominalSet.IsFresh] + exact hcx + have hca' : π⁻¹ • chooseFresh 𝔸 (π • x) (π • a) b ≠ a := by + intro hcontra + have h : π • π⁻¹ • chooseFresh 𝔸 (π • x) (π • a) b = π • a := by rw [hcontra] + rw [smul_inv_smul] at h + contradiction + have hcb' : π⁻¹ • chooseFresh 𝔸 (π • x) (π • a) b ≠ π⁻¹ • b := by + intro hcontra + have h : π • π⁻¹ • chooseFresh 𝔸 (π • x) (π • a) b = π • π⁻¹ • b := by rw [hcontra] + rw [smul_inv_smul, smul_inv_smul] at h + contradiction + rw [abs_choice 𝔸 _ _ hdx hcx' hda hca' hdb hcb'] + nth_rw 2 [← MulAction.mul_smul] + rw [show π * ⸨π⁻¹ • b,π⁻¹ • chooseFresh 𝔸 (π • x) (π • a) b⸩ = ⸨π • π⁻¹ • b,π • π⁻¹ • chooseFresh 𝔸 (π • x) (π • a) b⸩ * π from FPerm.mul_swap_eq_swap_mul] + rw [smul_inv_smul, smul_inv_smul, MulAction.mul_smul] + nth_rw 2 [AlgebraStructure.res_equivariant] + rw [smul_inv_smul] + nth_rw 2 [← MulAction.mul_smul] + rw [show π * ⸨a,π⁻¹ • chooseFresh 𝔸 (π • x) (π • a) b⸩ = ⸨π • a,π • π⁻¹ • chooseFresh 𝔸 (π • x) (π • a) b⸩ * π from FPerm.mul_swap_eq_swap_mul] + rw [smul_inv_smul, MulAction.mul_smul] + +private noncomputable def abs' : NameAbstraction 𝔸 X → PermSet.FinsuppFunction 𝔸 𝔸 X := + fun p ↦ ⟨abs'' 𝔸 p, by + use NominalSet.supp 𝔸 p; constructor + · apply Function.Equivariant.preserve_support + apply NominalSet.supp_is_support + · apply NominalSet.supp_finite⟩ + + end StepModel + +private noncomputable def ModelBundle (X : Type) [NominalSet 𝔸 X] : ℕ → ((T : Type) × ((_ : NominalSet 𝔸 T) × AlgebraStructure 𝔸 T)) +| 0 => ⟨BaseModel 𝔸 X, inferInstance, inferInstance⟩ +| n + 1 => + let ⟨Y, _, _⟩ := ModelBundle X n + ⟨StepModel 𝔸 Y, inferInstance, inferInstance⟩ + +def Model (X : Type) [NominalSet 𝔸 X] (n : ℕ) := (ModelBundle 𝔸 X n).fst + +namespace Model + +variable {X : Type} [NominalSet 𝔸 X] {n : ℕ} + +noncomputable instance : NominalSet 𝔸 (Model 𝔸 X n) := (ModelBundle 𝔸 X n).snd.fst +noncomputable instance : AlgebraStructure 𝔸 (Model 𝔸 X n) := (ModelBundle 𝔸 X n).snd.snd + +end Model |