diff options
| -rw-r--r-- | Nominal/Equivariance.lean | 49 | ||||
| -rw-r--r-- | Nominal/Instances/Basic.lean | 6 | ||||
| -rw-r--r-- | Nominal/Permutations.lean | 11 | ||||
| -rw-r--r-- | Nominal/Support.lean | 30 |
4 files changed, 89 insertions, 7 deletions
diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean index 8475a21..368d266 100644 --- a/Nominal/Equivariance.lean +++ b/Nominal/Equivariance.lean @@ -195,11 +195,56 @@ namespace Equivariance variable {X : Type} [NominalSet 𝔸 X] {R: Rel 𝔸 X} {x : X} +-- We continue with a circular implication chain argument to show these equivalences. + +private lemma for_fresh_iff₁ : EquivariantRelation 𝔸 R → (И a, R a x) → (∃ a, a # x ∧ R a x) := by + intro hequi h + have hinf : ({a | R a x} \ NominalSet.supp 𝔸 x).Infinite := Set.Infinite.diff h (NominalSet.supp_finite 𝔸) + obtain ⟨a, ha⟩ := hinf.nonempty + simp at ha + use a; exact ha.symm + +private lemma for_fresh_iff₂ : EquivariantRelation 𝔸 R → (∃ a, a # x ∧ R a x) → (∀ a, a # x → R a x) := by + intro hequi h + obtain ⟨a, ⟨hfresha, ha⟩⟩ := h + intro b hfreshb + have hmem := hequi a x ⸨a, b⸩ ha + rw [PermSet.atom_swap, Equiv.swap_apply_left] at hmem + rw [NominalSet.fresh_swap_fix 𝔸 hfresha hfreshb] at hmem + exact hmem + +private lemma for_fresh_iff₃ : EquivariantRelation 𝔸 R → (∀ a, a # x → R a x) → (И a, R a x) := by + intro hequi h + have hsub : {a : 𝔸 | R a x}ᶜ ⊆ NominalSet.supp 𝔸 x := by + rw [Set.compl_subset_comm] + intro a ha + rw [Set.mem_compl_iff] at ha + exact h a ha + simp [NominalSet.ForFresh] + apply Set.infinite_of_finite_compl + apply Set.Finite.subset (NominalSet.supp_finite 𝔸) hsub + /-- The quantifier in `И a, a R x` is equivalent to "for any fresh `a`". -/ -lemma for_fresh_iff_exists : EquivariantRelation 𝔸 R → ((И a, R a x) ↔ (∃ a, a # x ∧ R a x)) := by sorry +lemma for_fresh_iff_exists : EquivariantRelation 𝔸 R → ((И a, R a x) ↔ (∃ a, a # x ∧ R a x)) := by + intro hequi; constructor + · intro h + apply for_fresh_iff₁ 𝔸 hequi + exact h + · intro h + apply for_fresh_iff₃ 𝔸 hequi + apply for_fresh_iff₂ 𝔸 hequi + exact h /-- The quantifier in `И a, a R x` is equivalent to "for all fresh `a`". -/ -lemma for_fresh_iff_all : EquivariantRelation 𝔸 R → ((И a, R a x) ↔ (∀ a, a # x → R a x)) := by sorry +lemma for_fresh_iff_all : EquivariantRelation 𝔸 R → ((И a, R a x) ↔ (∀ a, a # x → R a x)) := by + intro hequi; constructor + · intro h + apply for_fresh_iff₂ 𝔸 hequi + apply for_fresh_iff₁ 𝔸 hequi + exact h + · intro h + apply for_fresh_iff₃ 𝔸 hequi + exact h end Equivariance diff --git a/Nominal/Instances/Basic.lean b/Nominal/Instances/Basic.lean index 82fd683..577cff8 100644 --- a/Nominal/Instances/Basic.lean +++ b/Nominal/Instances/Basic.lean @@ -38,10 +38,8 @@ instance : NominalSet 𝔸 𝔸 where simp at hc have hfix : ⸨a, c⸩ ∈ PermSet.fix 𝔸 S := by intro d hd - apply Equiv.Perm.supp_notin - simp [FPerm.swap, Equiv.Perm.supp_swap, Ne.symm hc.left] - exact ⟨ne_of_mem_of_not_mem hd ha, ne_of_mem_of_not_mem hd hc.right⟩ - have h₁ : ⸨a, c⸩ • a = c := by simp [show ⸨a,c⸩ • a = (Equiv.swap a c) a from rfl] + apply FPerm.swap_neq (ne_of_mem_of_not_mem hd ha) (ne_of_mem_of_not_mem hd hc.right) + have h₁ : ⸨a, c⸩ • a = c := by rw [PermSet.atom_swap, Equiv.swap_apply_left] have h₂ : ⸨a, c⸩ • a = a := by apply hsuppS; assumption rw [h₁] at h₂ exact hc.left h₂ diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean index 1bcb00f..a583b4c 100644 --- a/Nominal/Permutations.lean +++ b/Nominal/Permutations.lean @@ -133,6 +133,14 @@ lemma mul_swap_eq_swap_mul {π : FPerm X} {a b : X} : π * ⸨a, b⸩ = ⸨π a, apply ext apply Equiv.mul_swap_eq_swap_mul +/-- If c is not equal to a or b, then (a b) leaves c unchanged. -/ +lemma swap_neq {a b c : X} : c ≠ a → c ≠ b → ⸨a, b⸩ c = c := by + intro ha hb + apply Equiv.Perm.supp_notin + simp only [swap, Equiv.Perm.supp_swap, ne_eq, ite_not, Set.mem_ite_empty_left, Set.mem_insert_iff, Set.mem_singleton_iff, not_and, not_or] + intro _ + exact ⟨ha, hb⟩ + end FPerm example : FPerm ℕ := ⸨1, 2⸩ * ⸨3, 4⸩ * ⸨2, 3⸩ @@ -168,4 +176,7 @@ open Pointwise /-- The powerset of an (FPerm 𝔸)-Set forms an (FPerm 𝔸)-Set using pointwise permutation. -/ 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 + end PermSet diff --git a/Nominal/Support.lean b/Nominal/Support.lean index 64cc371..89021a0 100644 --- a/Nominal/Support.lean +++ b/Nominal/Support.lean @@ -170,6 +170,24 @@ lemma support_sInter {x : X} {C : Set (Set 𝔸)}: C.Finite → C.Nonempty → ( · exact support_inter 𝔸 hsing.left hsing.right hC'.left hC'.right · apply Set.Finite.inter_of_left hsing.right +/-- If two permutations π and σ are equal for all atoms in a support of x, then πx = σx. -/ +lemma support_permutations_eq {π σ : FPerm 𝔸} {x : X} {S : Set 𝔸} : PermSet.HasSupport 𝔸 x S → (∀ a ∈ S, π a = σ a) → π • x = σ • x := by + intro hsupp heq + have hfix : σ⁻¹ * π ∈ PermSet.fix 𝔸 S := by + intro a ha + calc + (σ⁻¹ * π) • a = σ⁻¹ (π a) := rfl + _ = σ⁻¹ (σ a) := by rw [heq a ha] + _ = (σ⁻¹ * σ) a := rfl + _ = (1 : FPerm 𝔸) a := by rw [inv_mul_cancel] + _ = a := rfl + calc + π • x = (1 * π) • x := rfl + _ = (σ * σ⁻¹ * π) • x := by rw [mul_inv_cancel] + _ = (σ * (σ⁻¹ * π)) • x := rfl + _ = σ • ((σ⁻¹ * π) • x) := by rw [smul_smul] + _ = σ • x := by rw [hsupp hfix] + end PermSet end Support @@ -286,10 +304,20 @@ lemma fresh_exists {x : X} : ∃ (a : 𝔸), a # x := by obtain ⟨a, ⟨_, ha⟩⟩ := Set.Infinite.exists_notMem_finite h_inf h_fin use a +/-- If a and b are fresh for x, then (a b) fixes x. -/ +lemma fresh_swap_fix {a b : 𝔸} {x : X} : a # x → b # x → ⸨a, b⸩ ∈ PermSet.fix' 𝔸 x := by + intro ha hb + suffices ⸨a, b⸩ • x = (1 : FPerm 𝔸) • x by + simp only [one_smul, PermSet.fix', Set.mem_setOf_eq] at *; assumption + apply PermSet.support_permutations_eq + · exact supp_is_support 𝔸 + · intro c hc + apply FPerm.swap_neq (ne_of_mem_of_not_mem hc ha) (ne_of_mem_of_not_mem hc hb) + /-- If a proposition holds for suitably fresh a, then one can always pick such an a. -/ lemma for_fresh_exists {P : 𝔸 → Prop} : (И a, P a) → (∃ a, P a) := by simp [NominalSet.ForFresh]; intro h - exact Set.Infinite.nonempty h + exact h.nonempty /-- Extensionality lemma for the freshness quantifier. -/ lemma for_fresh_ext {P Q : 𝔸 → Prop} : (∀ a, P a ↔ Q a) → (И a, P a) = (И a, Q a) := by |