diff options
Diffstat (limited to 'Nominal/NameRestriction/Model.lean')
| -rw-r--r-- | Nominal/NameRestriction/Model.lean | 85 |
1 files changed, 85 insertions, 0 deletions
diff --git a/Nominal/NameRestriction/Model.lean b/Nominal/NameRestriction/Model.lean index d09bebd..a694c05 100644 --- a/Nominal/NameRestriction/Model.lean +++ b/Nominal/NameRestriction/Model.lean @@ -908,6 +908,91 @@ private noncomputable def abs' : NameAbstraction 𝔸 X → PermSet.FinsuppFunct apply NominalSet.supp_is_support · apply NominalSet.supp_finite⟩ +private lemma abs_req2 {a : 𝔸} {x : X} : Req2 𝔸 (abs' 𝔸 (⟪a⟫ x)) := by + intro b c hcfresh hcb + have hinf : (NominalSet.supp 𝔸 x ∪ {a} ∪ {b} ∪ {c})ᶜ.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 ⟨d, hd⟩ := hinf.nonempty + simp only [Set.compl_union, Set.mem_inter_iff, Set.mem_compl_iff] at hd + have hdx : d # x := 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 + have hinf' : (NominalSet.supp 𝔸 (⸨a, d⸩ • x) ∪ NominalSet.supp 𝔸 (abs' 𝔸 (⟪a⟫ x)) ∪ {b} ∪ {d})ᶜ.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 Set.finite_singleton + · apply Set.finite_singleton + obtain ⟨e, he⟩ := hinf'.nonempty + simp only [Set.compl_union, Set.mem_inter_iff, Set.mem_compl_iff] at he + have hex : e # (⸨a, d⸩ • x) := he.left.left.left + have hefresh : e # abs' 𝔸 (⟪a⟫ x) := he.left.left.right + have heb : e ≠ b := he.left.right + have hed : e ≠ d := he.right + rw [choose_restriction' 𝔸 (abs' 𝔸 (⟪a⟫ x)) b b _ _ hcfresh hefresh hcb heb hcb heb] + simp only [abs', abs'', Quotient.lift_mk, PermSet.Finsupp.smul_val, PermSet.smul_function, + FPerm.swap_inv, PermSet.atom_swap, Equiv.swap_apply_left] + have ⟨hdx₁, hda₁, hdb₁⟩ := chooseFresh_fresh 𝔸 x a b + have ⟨hdx₂, hda₂, hde₂⟩ := chooseFresh_fresh 𝔸 x a e + rw [abs_choice 𝔸 _ _ hdx₁ hdx hda₁ hda hdb₁ hdb] + rw [abs_choice 𝔸 _ _ hdx₂ hdx hda₂ hda hde₂ (Ne.symm hed)] + nth_rw 1 [show e = ⸨b,e⸩ • b by simp] + rw [← AlgebraStructure.res_equivariant] + nth_rw 6 [← show ⸨e,d⸩ • b = b from FPerm.swap_apply_of_ne_of_ne (Ne.symm heb) (Ne.symm hdb)] + rw [← AlgebraStructure.res_equivariant] + rw [← MulAction.mul_smul] + rw [FPerm.mul_swap_eq_swap_mul, FPerm.swap_apply_right, FPerm.swap_apply_of_ne_of_ne hdb (Ne.symm hed)] + rw [MulAction.mul_smul] + rw [show ⸨b,e⸩ • (b \ (e \ (⸨a,d⸩ • x))) = (b \ (e \ (⸨a,d⸩ • x))) by + apply NominalSet.fresh_swap_fix + · show b # AlgebraStructure.res.toFun (⟪b⟫ AlgebraStructure.res (⟪e⟫ ⸨a,d⸩ • x)) + apply Function.Equivariant.preserve_fresh + rw [NameAbstraction.fresh]; right; rfl + · show e # AlgebraStructure.res.toFun (⟪b⟫ AlgebraStructure.res (⟪e⟫ ⸨a,d⸩ • x)) + apply Function.Equivariant.preserve_fresh + rw [NameAbstraction.fresh]; left + show e # AlgebraStructure.res.toFun (⟪e⟫ ⸨a,d⸩ • x) + apply Function.Equivariant.preserve_fresh + rw [NameAbstraction.fresh]; right; rfl] + rw [AlgebraStructure.ax_swap] + nth_rw 3 [AlgebraStructure.res_equivariant] + rw [show ⸨b,d⸩ • e = e from FPerm.swap_apply_of_ne_of_ne heb hed] + apply AlgebraStructure.ax_redundant + +noncomputable def abs : NameAbstraction 𝔸 X → StepModel 𝔸 X := + fun p ↦ ⟨abs' 𝔸 p, by + suffices ∀ p, Req2 𝔸 (abs' 𝔸 p) by apply this + apply Quotient.ind; intro ⟨a, x⟩ + apply abs_req2⟩ + +instance : Function.Equivariant 𝔸 (abs 𝔸 : NameAbstraction 𝔸 X → StepModel 𝔸 X) := by + constructor; intro x π + apply Subtype.eq; apply Subtype.eq + simp only [abs, abs', smul_val, PermSet.Finsupp.smul_val] + rw [← Function.equivariant] + +lemma abs_eq' {a : 𝔸} {x : X} {b : 𝔸} : + (abs 𝔸 (⟪a⟫ x)).val.val b = ⸨b,chooseFresh 𝔸 x a b⸩ • (b \ ⸨a,chooseFresh 𝔸 x a b⸩ • x) := rfl + +lemma abs_eq {a : 𝔸} {x : X} {b : 𝔸} : + ∀ c, c # x → c ≠ a → c ≠ b → + (abs 𝔸 (⟪a⟫ x)).val.val b = ⸨b,c⸩ • (b \ ⸨a,c⸩ • x) := by + intro d hdx hda hdb + have ⟨hcx, hca, hcb⟩ := chooseFresh_fresh 𝔸 x a b + apply abs_choice 𝔸 _ _ hcx hdx hca hda hcb hdb end StepModel |