diff options
Diffstat (limited to 'Nominal')
| -rw-r--r-- | Nominal/Instances/Abstraction.lean | 54 |
1 files changed, 30 insertions, 24 deletions
diff --git a/Nominal/Instances/Abstraction.lean b/Nominal/Instances/Abstraction.lean index 76cb360..269e80f 100644 --- a/Nominal/Instances/Abstraction.lean +++ b/Nominal/Instances/Abstraction.lean @@ -278,6 +278,7 @@ lemma eq_iff_cases {a b : 𝔸} {x y : X} : (⟪a⟫ x) = (⟪b⟫ y) ↔ (a = b @[simp] lemma supp {a : 𝔸} {x : X} : NominalSet.supp 𝔸 (⟪a⟫ x) = NominalSet.supp 𝔸 x \ {a} := by + -- XXX: This is rather ugly... have hswap : ∀ (b : 𝔸) (y : X), (⟪a⟫ x) = (⟪b⟫ y) → NominalSet.supp 𝔸 (⟨b, y⟩ : NameAbstraction' 𝔸 X) = {b} ∪ (NominalSet.supp 𝔸 x \ {a}) := by intro b y heq rw [eq_iff_cases] at heq @@ -297,21 +298,32 @@ lemma supp {a : 𝔸} {x : X} : NominalSet.supp 𝔸 (⟪a⟫ x) = NominalSet.su rw [mk, Quotient.supp] ext b constructor - · contrapose; intro h - simp only [NameAbstraction'.supp, Set.union_singleton, Set.mem_insert_iff, Set.mem_setOf_eq, Classical.not_imp, not_forall, not_or] - have hfin : (NominalSet.supp 𝔸 x).Finite := NominalSet.supp_finite 𝔸 - obtain ⟨c, hc⟩ := Infinite.exists_notMem_finset (hfin.toFinset ∪ {a, b}) - simp only [Finset.union_insert, Finset.union_singleton, Finset.mem_insert, Set.Finite.mem_toFinset, not_or] at hc - use ⟨c, ⸨a, c⸩ • x⟩ - constructor - · apply Quotient.exact - rw [← mk, ← mk, eq_iff_cases] - right - exact ⟨hc.left, hc.right.right, by rw [FPerm.swap_comm]⟩ - · constructor - · exact Ne.symm hc.right.left - · simp - sorry + · by_cases h_eq : a = b + · contrapose; intro h + subst h_eq + simp only [NameAbstraction'.supp, Set.union_singleton, Set.mem_insert_iff, Set.mem_setOf_eq, Classical.not_imp, not_forall, not_or] + have hfin : (NominalSet.supp 𝔸 x).Finite := NominalSet.supp_finite 𝔸 + obtain ⟨c, hc⟩ := Infinite.exists_notMem_finset (hfin.toFinset ∪ {a}) + simp only [Finset.union_singleton, Finset.mem_insert, Set.Finite.mem_toFinset, not_or] at hc + use ⟨c, ⸨a, c⸩ • x⟩ + have haeq : (⟪c⟫ ⸨a, c⸩ • x) = (⟪a⟫ x) := by + rw [eq_iff_cases] + right + exact ⟨hc.left, hc.right, by rw [FPerm.swap_comm]⟩ + constructor + · exact Quotient.exact haeq + · constructor + · exact Ne.symm hc.left + · suffices a ∉ NominalSet.supp 𝔸 (⟨c, ⸨a, c⸩ • x⟩ : NameAbstraction' 𝔸 X) by + simp only [NameAbstraction'.supp, Set.union_singleton, Set.mem_insert_iff, not_or] at this + exact this.right + rw [hswap c (⸨a, c⸩ • x) haeq.symm] + simp [Ne.symm hc.left] + · intro h + specialize h ⟨a, x⟩ (by rfl) + simp only [NameAbstraction'.supp, Set.union_singleton, Set.mem_insert_iff, Ne.symm h_eq, false_or] at h + rw [Set.mem_diff_singleton] + exact ⟨h, Ne.symm h_eq⟩ · intro h x' hx' suffices NominalSet.supp 𝔸 x' = {x'.atom} ∪ NominalSet.supp 𝔸 x \ {a} by rw [this] @@ -320,20 +332,14 @@ lemma supp {a : 𝔸} {x : X} : NominalSet.supp 𝔸 (⟪a⟫ x) = NominalSet.su apply Quotient.sound exact (Setoid.symm hx') +@[simp] lemma fresh {a b : 𝔸} {x : X} : b # (⟪a⟫ x) ↔ b # x ∨ b = a := by + simp only [NominalSet.IsFresh, supp, Set.mem_diff, Set.mem_singleton_iff, not_and_or, Decidable.not_not] + end NameAbstraction end Quotient /-! -## Nominal Set Instance - -The equivalence classes of name abstractions form a nominal set where supp (⟪a⟫ x) = supp x \ {a}. --/ -section NominalSet - -end NominalSet - -/-! ## Abstraction Functor Name abstraction can also be considered as a functor `Nom → Nom`. |