diff options
| -rw-r--r-- | Nominal/Instances/Abstraction.lean | 81 | ||||
| -rw-r--r-- | Nominal/Permutations.lean | 35 |
2 files changed, 102 insertions, 14 deletions
diff --git a/Nominal/Instances/Abstraction.lean b/Nominal/Instances/Abstraction.lean index b4a6cee..76cb360 100644 --- a/Nominal/Instances/Abstraction.lean +++ b/Nominal/Instances/Abstraction.lean @@ -243,31 +243,84 @@ instance NameAbstraction.setoid : EquivariantSetoid 𝔸 (NameAbstraction' 𝔸 /-- Define name abstractions as the quotient set (𝔸 × X)/≈. -/ def NameAbstraction := Quotient (NameAbstraction.setoid 𝔸 X).toSetoid +namespace NameAbstraction + /-- The equivalence class of a name abstraction (a, x), often written `⟪a⟫ x` -/ -def NameAbstraction.mk {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] {X : Type} [NominalSet 𝔸 X] (a : 𝔸) (x : X) : NameAbstraction 𝔸 X := +def mk {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] {X : Type} [NominalSet 𝔸 X] (a : 𝔸) (x : X) : NameAbstraction 𝔸 X := Quotient.mk (setoid 𝔸 X).toSetoid (.mk a x) /-- We write `⟪a⟫ x` instead of the usual `⟨a⟩ x` because `⟨⟩` is already heavily used in Lean for constructors. -/ -notation "⟪" a "⟫ " t => NameAbstraction.mk a t +notation "⟪" a "⟫ " t => mk a t instance : NominalSet 𝔸 (NameAbstraction 𝔸 X) := Quotient.instNominalSet 𝔸 @[simp] -lemma NameAbstraction.smul {π : FPerm 𝔸} {a : 𝔸} {x : X } : π • (⟪a⟫ x) = ⟪π • a⟫ π • x := by congr +lemma smul {π : FPerm 𝔸} {a : 𝔸} {x : X } : π • (⟪a⟫ x) = ⟪π • a⟫ π • x := by congr + +/-- Two name abstractions are equal iff they are alpha-equivalent. -/ +lemma eq_iff_alpha_eq {a b : 𝔸} {x y : X} : (⟪a⟫ x) = (⟪b⟫ y) ↔ AlphaEq ⟨a, x⟩ ⟨b, y⟩ := by + rw [mk, mk, Quotient.eq_iff_equiv] + rfl + +/-- Lifting of alpha_eq_iff_exists to name abstractions. -/ +lemma eq_iff_exists {a b : 𝔸} {x y : X} : (⟪a⟫ x) = (⟪b⟫ y) ↔ ∃ c, c ≠ a ∧ c ≠ b ∧ c # x ∧ c # y ∧ ⸨c, a⸩ • x = ⸨c, b⸩ • y := by + simp only [eq_iff_alpha_eq, alpha_eq_iff_exists, NameAbstraction'.fresh, ne_eq] + ac_nf + +/-- Lifting of alpha_eq_iff_exists to name abstractions. -/ +lemma eq_iff_all {a b : 𝔸} {x y : X} : (⟪a⟫ x) = (⟪b⟫ y) ↔ ∀ c, c ≠ a ∧ c ≠ b ∧ c # x ∧ c # y → ⸨c, a⸩ • x = ⸨c, b⸩ • y := by + simp only [eq_iff_alpha_eq, alpha_eq_iff_all, NameAbstraction'.fresh, ne_eq] + ac_nf + +/-- Lifting of alpha_eq_iff_cases to name abstractions. -/ +lemma eq_iff_cases {a b : 𝔸} {x y : X} : (⟪a⟫ x) = (⟪b⟫ y) ↔ (a = b ∧ x = y) ∨ (a ≠ b ∧ a # y ∧ x = ⸨a, b⸩ • y) := by + simp [eq_iff_alpha_eq, alpha_eq_iff_cases] @[simp] -lemma NameAbstraction.supp {a : 𝔸} {x : X} : NominalSet.supp 𝔸 (⟪a⟫ x) = NominalSet.supp 𝔸 x \ {a} := by - sorry - -- ext b; constructor - -- · apply NominalSet.support_subset_supp 𝔸 - -- · intro π hπ - -- simp [PermSet.fix'] +lemma supp {a : 𝔸} {x : X} : NominalSet.supp 𝔸 (⟪a⟫ x) = NominalSet.supp 𝔸 x \ {a} := by + 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 + cases heq with + | inl h => + rw [h.left, h.right] + simp only [NameAbstraction'.supp, Set.union_singleton, Set.union_diff_self, Set.singleton_union] + | inr h => + simp only [NameAbstraction'.supp, Set.union_comm] + rw [h.right.right, NominalSet.supp_equivariant 𝔸 y ⸨a, b⸩] + ext c + by_cases h₁ : c = b + · simp [h₁] + · by_cases h₂ : c = a + · simp [h₂, show a ∉ NominalSet.supp 𝔸 y by exact h.right.left] + · simp [h₁, h₂, ← PermSet.atom_set_swap_ne_ne] + 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 + · intro h x' hx' + suffices NominalSet.supp 𝔸 x' = {x'.atom} ∪ NominalSet.supp 𝔸 x \ {a} by + rw [this] + exact Set.mem_union_right {x'.atom} h + apply hswap + apply Quotient.sound + exact (Setoid.symm hx') - -- sorry - -- · exact Set.Finite.diff (NominalSet.supp_finite 𝔸) - -- · rw [mk, Quotient.supp] - -- intro hb x' hx' - -- sorry +end NameAbstraction end Quotient diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean index 0d6b81c..bc775b9 100644 --- a/Nominal/Permutations.lean +++ b/Nominal/Permutations.lean @@ -202,4 +202,39 @@ instance {X : Type} [PermSet 𝔸 X] : PermSet 𝔸 (Set X) where /-- Simplification for swaps applied to an atom. -/ @[simp] lemma PermSet.atom_swap {a b c : 𝔸} : ⸨a, b⸩ • c = (Equiv.swap a b) c := by rfl +/-- Given x = (a b) y, we also know y = (a b) x. -/ +lemma PermSet.swap_switch {X : Type} [PermSet 𝔸 X] {a b : 𝔸} {x y : X} : x = ⸨a, b⸩ • y → y = ⸨a, b⸩ • x := by + intro h + have h' : ⸨a, b⸩ • x = ⸨a, b⸩ • ⸨a, b⸩ • y := by congr + rw [← mul_smul, FPerm.swap_mul_self, one_smul] at h' + exact h'.symm + +/-- If the element is not affected by the swap, membership of it is the same as before the swap. -/ +lemma PermSet.atom_set_swap_ne_ne {a b c : 𝔸} {S : Set 𝔸} : c ≠ a → c ≠ b → (c ∈ S ↔ c ∈ ⸨a, b⸩ • S) := by + intro ha hb + constructor + · intro h + rw [← FPerm.swap_apply_of_ne_of_ne ha hb] + exact Set.smul_mem_smul_set h + · intro h + have h' : ⸨a, b⸩ c ∈ ⸨a, b⸩ • ⸨a, b⸩ • S := Set.smul_mem_smul_set h + rw [FPerm.swap_apply_of_ne_of_ne ha hb, ← mul_smul, FPerm.swap_mul_self, one_smul] at h' + exact h' + +/-- If an element is swapped, its membership is exactly that of the other element in the swapped set. -/ +lemma PermSet.atom_set_swap_left {a b : 𝔸} {S : Set 𝔸} : a ∈ S ↔ b ∈ ⸨a, b⸩ • S := by + constructor + · intro h + have h' : ⸨a, b⸩ a ∈ ⸨a, b⸩ • S := Set.smul_mem_smul_set h + rw [FPerm.swap_apply_left] at h' + exact h' + · intro h + have h' : ⸨a, b⸩ b ∈ ⸨a, b⸩ • ⸨a, b⸩ • S := Set.smul_mem_smul_set h + rw [FPerm.swap_apply_right, ← mul_smul, FPerm.swap_mul_self, one_smul] at h' + exact h' + +/-- If an element is swapped, its membership is exactly that of the other element in the swapped set. -/ +lemma PermSet.atom_set_swap_right {a b : 𝔸} {S : Set 𝔸} : b ∈ S ↔ a ∈ ⸨a, b⸩ • S := by + rw [FPerm.swap_comm, atom_set_swap_left] + end PermSet |