From 091fd832586627fbf31375fb5487d5e6fa6f7053 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Sun, 26 Oct 2025 13:26:57 +0100 Subject: finish name abstraction proofs --- Nominal/Equivariance.lean | 3 +- Nominal/Instances/Abstraction.lean | 83 +++++++++++++++++++++++++++++--------- Nominal/Permutations.lean | 5 +++ Nominal/Support.lean | 18 ++++++++- 4 files changed, 86 insertions(+), 23 deletions(-) diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean index 57c6d11..189ca66 100644 --- a/Nominal/Equivariance.lean +++ b/Nominal/Equivariance.lean @@ -215,6 +215,8 @@ variable {X : Type} [NominalSet 𝔸 X] {R: Rel 𝔸 X} {x : X} private lemma for_fresh_iff₁ : EquivariantRelation 𝔸 R → (И a, R a x) → (∃ a, a # x ∧ R a x) := by intro hequi h + apply Set.Finite.infinite_compl at h + simp at h have hinf : ({a | R a x} \ NominalSet.supp 𝔸 x).Infinite := Set.Infinite.diff h (NominalSet.supp_finite 𝔸) obtain ⟨a, ha⟩ := hinf.nonempty simp only [Set.mem_diff, Set.mem_setOf_eq] at ha @@ -237,7 +239,6 @@ private lemma for_fresh_iff₃ : EquivariantRelation 𝔸 R → (∀ a, a # x rw [Set.mem_compl_iff] at ha exact h a ha simp only [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`". -/ diff --git a/Nominal/Instances/Abstraction.lean b/Nominal/Instances/Abstraction.lean index 660c2ab..bb654ed 100644 --- a/Nominal/Instances/Abstraction.lean +++ b/Nominal/Instances/Abstraction.lean @@ -133,15 +133,19 @@ lemma alpha_eq_iff_all {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ ∀ c, For ⟪a⟫ x = ⟪b⟫ y, we either have (a, x) = (b, y) or x is just (a b) y, requiring that a is not in the support of y. -/ lemma alpha_eq_iff_cases {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ (x.atom = y.atom ∧ x.body = y.body) ∨ (x.atom ≠ y.atom ∧ x.atom # y.body ∧ x.body = ⸨x.atom, y.atom⸩ • y.body) := by - by_cases h_eq : x.atom = y.atom - · constructor - · sorry - · sorry - · constructor - · rw [alpha_eq_iff_exists] - intro h; right - obtain ⟨c, ⟨hcx, ⟨hcy, hc⟩⟩⟩ := h - constructor + constructor + · rw [alpha_eq_iff_exists] + intro h + obtain ⟨c, ⟨hcx, ⟨hcy, hc⟩⟩⟩ := h + by_cases h_eq : x.atom = y.atom + · left; constructor + · exact h_eq + · calc + x.body = ⸨c, x.atom⸩ • ⸨c, x.atom⸩ • x.body := by rw [← mul_smul, FPerm.swap_mul_self, one_smul] + _ = ⸨c, x.atom⸩ • ⸨c, y.atom⸩ • y.body := by rw [hc] + _ = ⸨c, y.atom⸩ • ⸨c, y.atom⸩ • y.body := by rw [h_eq] + _ = y.body := by rw [← mul_smul, FPerm.swap_mul_self, one_smul] + · right; constructor · exact h_eq · simp at hcx simp at hcy @@ -160,24 +164,63 @@ lemma alpha_eq_iff_cases {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ (x.at _ = (⸨c, x.atom⸩ * ⸨c, y.atom⸩) • y.body := by rw [mul_smul, hc] _ = ⸨x.atom, y.atom⸩ • ⸨c, x.atom⸩ • y.body := by rw [← mul_smul, h_swap] _ = ⸨x.atom, y.atom⸩ • y.body := by rw [NominalSet.fresh_swap_fix 𝔸 hcy.right h_atom] - · rw [alpha_eq_iff_all] - intro h c ⟨hcx, hcy⟩ + · rw [alpha_eq_iff_all] + intro h c ⟨hcx, hcy⟩ + cases h with + | inl h => + rw [h.left, h.right] + | inr h => simp at hcx simp at hcy - simp only [h_eq, false_and, ne_eq, not_false_eq_true, true_and, false_or] at h have h_swap : ⸨c, x.atom⸩ * ⸨x.atom, y.atom⸩ = ⸨c, y.atom⸩ * ⸨c, x.atom⸩ := by ext a by_cases a = c <;> by_cases a = x.atom <;> by_cases a = y.atom - all_goals simp_all [FPerm.swap_apply_of_ne_of_ne, hcy.left, hcx.left, Ne.symm hcy.left, Ne.symm hcx.left, Ne.symm h_eq] - rw [h.right, ← mul_smul, h_swap, mul_smul, NominalSet.fresh_swap_fix 𝔸 hcy.right h.left] - -private lemma alpha_eq_refl (x : NameAbstraction' 𝔸 X) : AlphaEq x x := by sorry + all_goals simp_all [FPerm.swap_apply_of_ne_of_ne, hcy.left, hcx.left, Ne.symm hcy.left, Ne.symm hcx.left, Ne.symm h.left] + rw [h.right.right, ← mul_smul, h_swap, mul_smul, NominalSet.fresh_swap_fix 𝔸 hcy.right h.right.left] -private lemma alpha_eq_symm {x y : NameAbstraction' 𝔸 X} : AlphaEq x y → AlphaEq y x := by sorry +private lemma alpha_eq_refl (x : NameAbstraction' 𝔸 X) : AlphaEq x x := by + rw [alpha_eq_iff_cases]; left + trivial -private lemma alpha_eq_trans {x y z : NameAbstraction' 𝔸 X} : AlphaEq x y → AlphaEq y z → AlphaEq x z := by sorry - -lemma alpha_eq_equivariant : EquivariantRelation 𝔸 (AlphaEq : NameAbstraction' 𝔸 X → NameAbstraction' 𝔸 X → Prop) := by sorry +private lemma alpha_eq_symm {x y : NameAbstraction' 𝔸 X} : AlphaEq x y → AlphaEq y x := by + rw [alpha_eq_iff_cases, alpha_eq_iff_cases] + intro h + cases h with + | inl h => + left; exact ⟨h.left.symm, h.right.symm⟩ + | inr h => + right; constructor + · exact h.left.symm + · constructor + · have h : ⸨x.atom, y.atom⸩ • x.atom # x.body := by + rw [h.right.right] + exact NominalSet.fresh_equivariant 𝔸 _ _ _ h.right.left + simp at h; exact h + · rw [h.right.right, ← mul_smul, FPerm.swap_comm, FPerm.swap_mul_self, one_smul] + +private lemma alpha_eq_trans {x y z : NameAbstraction' 𝔸 X} : AlphaEq x y → AlphaEq y z → AlphaEq x z := by + intro hxy hyz + have h : AlphaEq x y ∧ AlphaEq y z := ⟨hxy, hyz⟩ + simp only [AlphaEq, AlphaEq, NominalSet.for_fresh_and] at h + apply NominalSet.for_fresh_imp + · exact h + · intro c ⟨hxy, hyz⟩ + rw [hxy, hyz] + +/-- Alpha-equivalence is an equivariant relation. -/ +lemma alpha_eq_equivariant : EquivariantRelation 𝔸 (AlphaEq : NameAbstraction' 𝔸 X → NameAbstraction' 𝔸 X → Prop) := by + intro x y π h + rw [alpha_eq_iff_exists] at * + obtain ⟨c, ⟨hcx, ⟨hcy, hc⟩⟩⟩ := h + use π • c + constructor + · apply NominalSet.fresh_equivariant; exact hcx + · constructor + · apply NominalSet.fresh_equivariant; exact hcy + · -- XXX: This is largely similar to alpha_eq_pred... + have h' : π • ⸨c, x.atom⸩ • x.body = π • ⸨c, y.atom⸩ • y.body := by congr + simp only [smul_smul, FPerm.mul_swap_eq_swap_mul] at h' + simpa [smul_smul] end NameAbstraction diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean index 1726ed7..a2f8d56 100644 --- a/Nominal/Permutations.lean +++ b/Nominal/Permutations.lean @@ -138,6 +138,11 @@ lemma swap_mul_self {a b : X} : ⸨a, b⸩ * ⸨a, b⸩ = 1 := by apply ext simp [swap] +/-- Lifting of Equiv.swap_comm to finite permutations. -/ +lemma swap_comm {a b : X} : ⸨a, b⸩ = ⸨b, a⸩ := by + apply ext + simp [swap, Equiv.swap_comm] + /-- Lifting of Equiv.swap_apply_of_ne_of_ne to finite permutations. -/ lemma swap_apply_of_ne_of_ne {a b c : X} : c ≠ a → c ≠ b → ⸨a, b⸩ c = c := by intro ha hb diff --git a/Nominal/Support.lean b/Nominal/Support.lean index d80503f..b8e6809 100644 --- a/Nominal/Support.lean +++ b/Nominal/Support.lean @@ -271,9 +271,9 @@ section Freshness We also write И a, P for for_fresh (fun a => P), using the cyrillic letter И. -A proposition holds for "suitably fresh" atoms iff there are infinitely many such "suitably fresh" atoms to choose from. -/ +A proposition holds for "suitably fresh" atoms iff the set of atoms that are not "suitably fresh" is finite. -/ def NominalSet.ForFresh {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] (P : 𝔸 → Prop) : Prop := - {a : 𝔸 | P a}.Infinite + {a : 𝔸 | P a}ᶜ.Finite macro "И" x:ident "," t:term : term => `(NominalSet.ForFresh (fun $x => $t)) @@ -318,6 +318,8 @@ lemma fresh_swap_fix {a b : 𝔸} {x : X} : a # x → b # x → ⸨a, b⸩ ∈ P /-- 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 only [ForFresh]; intro h + apply Set.Finite.infinite_compl at h + rw [compl_compl] at h exact h.nonempty /-- Extensionality lemma for the freshness quantifier. -/ @@ -327,6 +329,18 @@ lemma for_fresh_ext {P Q : 𝔸 → Prop} : (∀ a, P a ↔ Q a) → (И a, P a) suffices {a | P a} = {a | Q a} by rw [this] exact Set.ext h +/-- The freshness quantifier preserves implications. -/ +lemma for_fresh_imp {P Q : 𝔸 → Prop} : (И a, P a) → (∀ a, P a → Q a) → (И a, Q a) := by + intro hfin himp + apply Set.Finite.subset + · exact hfin + · simp only [Set.compl_subset_compl, Set.setOf_subset_setOf] + exact himp + +/-- The freshness quantifier commutes with conjunctions. -/ +lemma for_fresh_and {P Q : 𝔸 → Prop} : (И a, P a) ∧ (И a, Q a) ↔ (И a, P a ∧ Q a) := by + simp [ForFresh, Set.setOf_and, Set.compl_inter] + end NominalSet end Freshness -- cgit v1.3.1