diff options
Diffstat (limited to 'Nominal/NameRestriction')
| -rw-r--r-- | Nominal/NameRestriction/Model.lean | 36 |
1 files changed, 25 insertions, 11 deletions
diff --git a/Nominal/NameRestriction/Model.lean b/Nominal/NameRestriction/Model.lean index adefdb4..6195099 100644 --- a/Nominal/NameRestriction/Model.lean +++ b/Nominal/NameRestriction/Model.lean @@ -706,18 +706,16 @@ lemma restrict_supp (f : StepModel 𝔸 X) (a c : 𝔸) : 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 +lemma mem_fresh (f : StepModel 𝔸 X) (a c : 𝔸) : c # f → c ≠ a → c # f.val.val a := 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 + 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 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 + specialize h hcontra + simp only [Set.union_singleton, Set.mem_insert_iff] at h + cases h <;> contradiction noncomputable instance : AlgebraStructure 𝔸 (StepModel 𝔸 X) where bot := ⟨bot 𝔸, inferInstance⟩ @@ -852,7 +850,23 @@ noncomputable instance : AlgebraStructure 𝔸 (StepModel 𝔸 X) where 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 + rw [union_eq] + 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 [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] + rw [show ⸨a,c⸩ • ⟪a⟫ f.val.val b = ⟪a⟫ f.val.val b by + apply NominalSet.fresh_swap_fix + · rw [NameAbstraction.fresh]; right; rfl + · rw [NameAbstraction.fresh]; left + apply mem_fresh 𝔸 f b c hcf hcb] + apply AlgebraStructure.ax_redundant end StepModel |