From 502188498eca3e076b10aaa7a0a1763f624abe8d Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Sun, 11 Jan 2026 23:45:55 +0100 Subject: prove some more axioms --- Nominal/NameRestriction/Model.lean | 194 +++++++++++++++++++++++++++++++++++++ 1 file changed, 194 insertions(+) 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 -- cgit v1.3.1