summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Nominal/NameRestriction/Model.lean283
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
generated by cgit v1.3.1 (git 2.54.0) at 2026-11-10 10:48:59 +0000