From 71a6a3d5b6f4b428b463bc4a0766c91d8c1d5768 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Wed, 3 Dec 2025 20:34:41 +0100 Subject: refactor equivariant props to use type classes --- Algebra/Term.lean | 106 ++++++++++++++++- Nominal/Category.lean | 4 +- Nominal/Equivariance.lean | 224 +++++++++++++++++++---------------- Nominal/Instances/Abstraction.lean | 63 +++++----- Nominal/Instances/Basic.lean | 111 ++++++++++++----- Nominal/LambdaCalculus/Preterms.lean | 10 +- Nominal/LambdaCalculus/Terms.lean | 53 +++++---- Nominal/Support.lean | 6 + 8 files changed, 379 insertions(+), 198 deletions(-) diff --git a/Algebra/Term.lean b/Algebra/Term.lean index 20fd009..665999f 100644 --- a/Algebra/Term.lean +++ b/Algebra/Term.lean @@ -80,7 +80,7 @@ def Substitution.apply {n l : ℕ} (σ : Substitution 𝔸 sig X Y l) (t : TermA apply ih1; exact h arg⟩ private def rename' (π : FPerm 𝔸) : Term 𝔸 sig X → Term 𝔸 sig X - | .var x => .var x + | .var x => .var (π • x) | .pure f args => .pure f (fun x => rename' π (args x)) | .free a f args => .free (π • a) f (fun x => rename' π (args x)) | .bound a f args => .bound (π • a) f (fun x => rename' π (args x)) @@ -97,6 +97,100 @@ instance : PermSet 𝔸 (Term 𝔸 sig X) where one_smul := one_rename 𝔸 mul_smul := mul_rename 𝔸 +@[simp] lemma smul_var {π : FPerm 𝔸} {x : X} : + π • (Term.var x : Term 𝔸 sig X) = Term.var (π • x) := rfl + +@[simp] lemma smul_pure {π : FPerm 𝔸} {f : sig.pure} {args : sig.pureArgs f → Term 𝔸 sig X} : + π • Term.pure f args = Term.pure f ((π • ·) ∘ args) := rfl + +@[simp] lemma smul_free {π : FPerm 𝔸} {a : 𝔸} {f : sig.free} {args : sig.freeArgs f → Term 𝔸 sig X} : + π • Term.free a f args = Term.free (π • a) f ((π • ·) ∘ args) := rfl + +@[simp] lemma smul_bound {π : FPerm 𝔸} {a : 𝔸} {f : sig.bound} {args : sig.boundArgs f → Term 𝔸 sig X} : + π • Term.bound a f args = Term.bound (π • a) f ((π • ·) ∘ args) := rfl + +private def atoms : Term 𝔸 sig X → Set 𝔸 + | .var x => NominalSet.supp 𝔸 x + | .pure f args => ⋃₀ {atoms (args x) | x : sig.pureArgs f} + | .free a f args => {a} ∪ ⋃₀ {atoms (args x) | x : sig.freeArgs f} + | .bound a f args => {a} ∪ ⋃₀ {atoms (args x) | x : sig.boundArgs f} + +private lemma atoms_finite (t : Term 𝔸 sig X) : (atoms 𝔸 t).Finite := by + fun_induction atoms <;> all_goals expose_names + · exact NominalSet.supp_finite 𝔸 + · have hfin := (sig.pureArgs_fintype f).finite + apply Set.Finite.sUnion + · simp only [Set.setOf_exists, Set.setOf_eq_eq_singleton', Set.iUnion_singleton_eq_range] + apply Set.finite_range + · intro S ⟨x, hS⟩ + rw [← hS] + exact ih1 x + · have hfin := (sig.freeArgs_fintype f).finite + apply Set.Finite.union + · exact Set.finite_singleton a + · apply Set.Finite.sUnion + · simp only [Set.setOf_exists, Set.setOf_eq_eq_singleton', Set.iUnion_singleton_eq_range] + apply Set.finite_range + · intro S ⟨x, hS⟩ + rw [← hS] + exact ih1 x + · have hfin := (sig.boundArgs_fintype f).finite + apply Set.Finite.union + · exact Set.finite_singleton a + · apply Set.Finite.sUnion + · simp only [Set.setOf_exists, Set.setOf_eq_eq_singleton', Set.iUnion_singleton_eq_range] + apply Set.finite_range + · intro S ⟨x, hS⟩ + rw [← hS] + exact ih1 x + +private lemma atoms_support (t : Term 𝔸 sig X) : PermSet.HasSupport 𝔸 t (atoms 𝔸 t) := by + intro π + fun_induction atoms <;> all_goals expose_names + · have hsupp : PermSet.HasSupport 𝔸 x (NominalSet.supp 𝔸 x) := NominalSet.supp_is_support 𝔸 + intro hπ + simp only [PermSet.fix', smul_var, Term.var.injEq, Set.mem_setOf_eq] + exact hsupp hπ + · intro hπ + simp only [PermSet.fix', smul_pure, Term.pure.injEq, heq_eq_eq, true_and, Set.mem_setOf_eq] + ext x + rw [Function.comp_apply] + apply ih1 + apply PermSet.fix_antitone_mem 𝔸 hπ + apply Set.subset_sUnion_of_mem + use x + · intro hπ + simp only [PermSet.fix', smul_free, Term.free.injEq, heq_eq_eq, true_and, Set.mem_setOf_eq] + constructor + · apply PermSet.fix_antitone_mem 𝔸 hπ + apply Set.subset_union_left + rfl + · ext x + rw [Function.comp_apply] + apply ih1 + apply PermSet.fix_antitone_mem 𝔸 hπ + apply Set.subset_union_of_subset_right + apply Set.subset_sUnion_of_mem + use x + · intro hπ + simp only [PermSet.fix', smul_bound, Term.bound.injEq, heq_eq_eq, true_and, Set.mem_setOf_eq] + constructor + · apply PermSet.fix_antitone_mem 𝔸 hπ + apply Set.subset_union_left + rfl + · ext x + rw [Function.comp_apply] + apply ih1 + apply PermSet.fix_antitone_mem 𝔸 hπ + apply Set.subset_union_of_subset_right + apply Set.subset_sUnion_of_mem + use x + +instance : NominalSet 𝔸 (Term 𝔸 sig X) where + fin_supp t := by + use atoms 𝔸 t + exact ⟨atoms_support 𝔸 t, atoms_finite 𝔸 t⟩ + private def rename {n : ℕ} (π : FPerm 𝔸) (t : TermAtDepth 𝔸 sig X n) : TermAtDepth 𝔸 sig X n := ⟨π • t.val, by suffices ∀ t n, t.HasDepth 𝔸 n → (rename' 𝔸 π t).HasDepth 𝔸 n by @@ -109,9 +203,11 @@ private def rename {n : ℕ} (π : FPerm 𝔸) (t : TermAtDepth 𝔸 sig X n) : constructor; intro arg apply ih1; exact h arg⟩ -instance {n : ℕ} : PermSet 𝔸 (TermAtDepth 𝔸 sig X n) where - smul := rename 𝔸 - one_smul t := by apply Subtype.eq; exact one_rename 𝔸 t.val - mul_smul π τ t := by apply Subtype.eq; exact mul_rename 𝔸 π τ t.val +instance Term.instHasDepthEquivariant {n : ℕ} : Set.Equivariant 𝔸 {t : Term 𝔸 sig X | HasDepth 𝔸 t n} := by + constructor; intro t π ht + exact (rename 𝔸 π ⟨t, ht⟩).prop + +instance {n : ℕ} : NominalSet 𝔸 (TermAtDepth 𝔸 sig X n) := + (Subtype.instNominalSetElem 𝔸 : NominalSet 𝔸 {t : Term 𝔸 sig X | Term.HasDepth 𝔸 t n}) end Algebra diff --git a/Nominal/Category.lean b/Nominal/Category.lean index 721dfb0..343c40c 100644 --- a/Nominal/Category.lean +++ b/Nominal/Category.lean @@ -69,7 +69,7 @@ instance : HasForget₂ (Nom 𝔸) (Action Type (FPerm 𝔸)) where map f := ⟨f.toFun, by intro π ext x - simp only [EquivariantMap.toFun_eq_coe, types_comp_apply, Action.ofMulAction_apply] - apply f.equivariant⟩ } + simp only [types_comp_apply, Action.ofMulAction_apply] + rw [Function.equivariant 𝔸 f.toFun]⟩ } end Forget diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean index 4ba580d..2682a55 100644 --- a/Nominal/Equivariance.lean +++ b/Nominal/Equivariance.lean @@ -20,40 +20,42 @@ section Definition variable {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] /-- A function is equivariant if it is invariant to applying a permutation before or after the function. -/ -def Function.Equivariant (f : X → Y) : Prop := - ∀ (x : X) (π : FPerm 𝔸), f (π • x) = π • f x +class inductive Function.Equivariant (f : X → Y) : Prop + | intro : (∀ (x : X) (π : FPerm 𝔸), f (π • x) = π • f x) → Equivariant f -/-- A set is equivariant if it is closed under permutations. -/ -def Set.Equivariant (S : Set X) : Prop := - ∀ (x : X) (π : FPerm 𝔸), x ∈ S → π • x ∈ S +lemma Function.equivariant (f : X → Y) [Equivariant 𝔸 f] : + ∀ (x : X) (π : FPerm 𝔸), f (π • x) = π • f x := by + cases (inferInstanceAs (Equivariant 𝔸 f)); assumption -/-- A binary relation is equivariant if it is closed under permutations. -/ -def Rel.Equivariant (R : Rel X Y) : Prop := - ∀ (x : X) (y : Y) (π : FPerm 𝔸), R x y → R (π • x) (π • y) +/-- A set is equivariant if it is closed under permutations. -/ +class inductive Set.Equivariant (S : Set X) : Prop + | intro : (∀ (x : X) (π : FPerm 𝔸), x ∈ S → π • x ∈ S) → Equivariant S /-- For equivariant sets, we even have "if and only if". -/ -lemma Set.Equivariant.iff {S : Set X} : Set.Equivariant 𝔸 S ↔ ∀ (x : X) (π : FPerm 𝔸), x ∈ S ↔ π • x ∈ S := by - constructor - · intro h x π; constructor - · intro hx; exact h x π hx - · intro hx - apply (h (π • x) π⁻¹) at hx - simp only [inv_smul_smul] at hx - exact hx - · intro h x π hx - exact (h x π).mp hx +lemma Set.equivariant (S : Set X) [Equivariant 𝔸 S] : + ∀ (x : X) (π : FPerm 𝔸), x ∈ S ↔ π • x ∈ S := by + cases (inferInstanceAs (Equivariant 𝔸 S)); rename_i h + intro x π; constructor + · intro hx; exact h x π hx + · intro hx + apply (h (π • x) π⁻¹) at hx + simp only [inv_smul_smul] at hx + exact hx + +/-- A binary relation is equivariant if it is closed under permutations. -/ +class inductive Rel.Equivariant (R : Rel X Y) : Prop + | intro : (∀ (x : X) (y : Y) (π : FPerm 𝔸), R x y → R (π • x) (π • y)) → Equivariant R /-- For equivariant relations, we even have "if and only if". -/ -lemma Rel.Equivariant.iff {R : Rel X Y} : Rel.Equivariant 𝔸 R ↔ ∀ (x : X) (y : Y) (π : FPerm 𝔸), R x y ↔ R (π • x) (π • y) := by - constructor - · intro h x y π; constructor - · intro hxy; exact h x y π hxy - · intro hxy - apply (h (π • x) (π • y) π⁻¹) at hxy - simp only [inv_smul_smul] at hxy - exact hxy - · intro h x y π hxy - exact (h x y π).mp hxy +lemma Rel.equivariant (R : Rel X Y) [Rel.Equivariant 𝔸 R] : + ∀ (x : X) (y : Y) (π : FPerm 𝔸), R x y ↔ R (π • x) (π • y) := by + cases (inferInstanceAs (Equivariant 𝔸 R)); rename_i h + intro x y π; constructor + · intro hxy; exact h x y π hxy + · intro hxy + apply (h (π • x) (π • y) π⁻¹) at hxy + simp only [inv_smul_smul] at hxy + exact hxy end Definition @@ -67,25 +69,32 @@ section Trivial variable {X Y Z : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] [PermSet 𝔸 Z] /-- The identity function is equivariant. -/ -lemma id_equivariant : Function.Equivariant 𝔸 (id : X → X) := by - simp [Function.Equivariant] +instance Function.Equivariant.id : Function.Equivariant 𝔸 (id : X → X) := by + constructor + simp /-- The composition of two equivariant functions is equivariant. -/ -lemma comp_equivariant {f : Y → Z} {g : X → Y} : Function.Equivariant 𝔸 f → Function.Equivariant 𝔸 g → Function.Equivariant 𝔸 (f ∘ g) := by - intro hf hg x π +instance Function.Equivariant.comp + {f : Y → Z} [Function.Equivariant 𝔸 f] {g : X → Y} [Function.Equivariant 𝔸 g] : + Function.Equivariant 𝔸 (f ∘ g) := by + constructor; intro x π calc - f (g (π • x)) = f (π • g x) := by rw [hg] - _ = π • (f (g x)) := by rw [hf] + f (g (π • x)) = f (π • g x) := by rw [← Function.equivariant 𝔸 g] + _ = π • (f (g x)) := by rw [← Function.equivariant 𝔸 f] /-- If a function is equivariant, its inverse is also equivariant. -/ -lemma Function.inv_equivariant {f : X → Y} {inv : Y → X} : Function.LeftInverse inv f → Function.RightInverse inv f → Function.Equivariant 𝔸 f → Function.Equivariant 𝔸 inv := by - intro hleft hright hequi y π +def Function.Equivariant.inv + {f : X → Y} [Function.Equivariant 𝔸 f] {inv : Y → X} + (hleft : Function.LeftInverse inv f) + (hright : Function.RightInverse inv f) : + Function.Equivariant 𝔸 inv := by + constructor; intro y π apply hleft.injective - rw [hequi, hright, hright] + rw [Function.equivariant 𝔸 f, hright, hright] /-- The subset relation is equivariant. -/ -lemma Set.subset_equivariant : Rel.Equivariant 𝔸 (Set.Subset : Set X → Set X → Prop) := by - intro S T π hST x hx +instance Set.Equivariant.subset : Rel.Equivariant 𝔸 (Set.Subset : Set X → Set X → Prop) := by + constructor; intro S T π hST x hx rw [Set.mem_smul_set_iff_inv_smul_mem] at hx rw [Set.mem_smul_set_iff_inv_smul_mem] exact hST hx @@ -104,27 +113,29 @@ variable {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] namespace Function.Equivariant /-- Equivariant functions preserve supports. -/ -lemma preserve_support {x : X} {f : X → Y} {S : Set 𝔸} : Equivariant 𝔸 f → PermSet.HasSupport 𝔸 x S → PermSet.HasSupport 𝔸 (f x) S := by - intro hequi hsupp π hπ +lemma preserve_support {x : X} {f : X → Y} [Equivariant 𝔸 f] {S : Set 𝔸} : + PermSet.HasSupport 𝔸 x S → PermSet.HasSupport 𝔸 (f x) S := by + intro hsupp π hπ calc - π • f x = f (π • x) := by rw [← hequi] + π • f x = f (π • x) := by rw [← equivariant 𝔸 f] _ = f x := by rw [hsupp hπ] /-- Equivariant injective functions exactly preserve supports. -/ -lemma preserve_support_inj {x : X} {f : X → Y} {S : Set 𝔸} : Equivariant 𝔸 f → f.Injective → (PermSet.HasSupport 𝔸 x S ↔ PermSet.HasSupport 𝔸 (f x) S) := by - intro hequi hinj; constructor - · exact preserve_support 𝔸 hequi +lemma preserve_support_inj {x : X} {f : X → Y} [Equivariant 𝔸 f] {S : Set 𝔸} : + f.Injective → (PermSet.HasSupport 𝔸 x S ↔ PermSet.HasSupport 𝔸 (f x) S) := by + intro hinj; constructor + · exact preserve_support 𝔸 · intro hsupp π hπ by_contra h - have : π • f x ≠ f x := by rw [← hequi]; exact fun a => h (hinj a) + have : π • f x ≠ f x := by rw [← equivariant 𝔸 f]; intro hcontra; exact h (hinj hcontra) have : π • f x = f x := hsupp hπ contradiction end Function.Equivariant /-- HasSupport is an equivariant relation. -/ -lemma PermSet.support_equivariant : Rel.Equivariant 𝔸 (HasSupport 𝔸 : X → Set 𝔸 → Prop) := by - intro x S π hS σ hσ +instance PermSet.instHasSupportEquivariant : Rel.Equivariant 𝔸 (HasSupport 𝔸 : X → Set 𝔸 → Prop) := by + constructor; intro x S π hS σ hσ have hfix : (π⁻¹ * σ * π) ∈ fix 𝔸 S := by intro a ha calc @@ -154,52 +165,58 @@ variable {X Y : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y] namespace Function.Equivariant /-- If f is equivariant, then supp (f x) ⊆ supp x. -/ -lemma supp_subset {x : X} {f : X → Y} : Equivariant 𝔸 f → NominalSet.supp 𝔸 (f x) ⊆ NominalSet.supp 𝔸 x := by - intro hequi +lemma supp_subset {x : X} {f : X → Y} [Equivariant 𝔸 f] : + NominalSet.supp 𝔸 (f x) ⊆ NominalSet.supp 𝔸 x := by apply NominalSet.support_subset_supp - · exact preserve_support 𝔸 hequi (NominalSet.supp_is_support 𝔸) + · exact preserve_support 𝔸 (NominalSet.supp_is_support 𝔸) · exact NominalSet.supp_finite 𝔸 /-- If f is equivariant and injective, then supp (f x) = supp x. -/ -lemma supp_eq_if_inj {x : X} {f : X → Y} : Equivariant 𝔸 f → Function.Injective f → NominalSet.supp 𝔸 (f x) = NominalSet.supp 𝔸 x := by - intro hequi hinj - simp [NominalSet.supp, preserve_support_inj 𝔸 hequi hinj] +lemma supp_eq_if_inj {x : X} {f : X → Y} [Equivariant 𝔸 f] : + Function.Injective f → NominalSet.supp 𝔸 (f x) = NominalSet.supp 𝔸 x := by + intro hinj + simp [NominalSet.supp, preserve_support_inj 𝔸 hinj] /-- If f is equivariant and a # x, then a # f x. -/ -lemma preserve_fresh {a : 𝔸} {x : X} {f : X → Y} : Equivariant 𝔸 f → a # x → a # f x := by - intro hequi hx ha - exact hx ((supp_subset 𝔸 hequi) ha) +lemma preserve_fresh {a : 𝔸} {x : X} {f : X → Y} [Equivariant 𝔸 f] : a # x → a # f x := by + intro hx ha + exact hx (supp_subset 𝔸 ha) /-- If f is equivariant and injective, then a # x iff a # f x. -/ -lemma preserve_fresh_inj {a : 𝔸} {x : X} {f : X → Y} : Equivariant 𝔸 f → Function.Injective f → (a # x ↔ a # f x) := by - intro hequi hinj - rw [NominalSet.IsFresh, NominalSet.IsFresh, supp_eq_if_inj 𝔸 hequi hinj] +lemma preserve_fresh_inj {a : 𝔸} {x : X} {f : X → Y} [Equivariant 𝔸 f] : + Function.Injective f → (a # x ↔ a # f x) := by + intro hinj + rw [NominalSet.IsFresh, NominalSet.IsFresh, supp_eq_if_inj 𝔸 hinj] end Function.Equivariant /-- If there is an equivariant surjection from a nominal set into an (FPerm 𝔸)-Set, then that set is nominal. -/ -def NominalSet.fromEquivariantSurjective {X Y : Type} [NominalSet 𝔸 X] [PermSet 𝔸 Y] (f : X → Y) (hequi : Function.Equivariant 𝔸 f) (hsurj : Function.Surjective f) : NominalSet 𝔸 Y where +def NominalSet.ofEquivariantSurjective + {X Y : Type} [NominalSet 𝔸 X] [PermSet 𝔸 Y] + (f : X → Y) [Function.Equivariant 𝔸 f] (hsurj : Function.Surjective f) : + NominalSet 𝔸 Y where fin_supp := by intro y obtain ⟨x, hx⟩ := hsurj y use (NominalSet.supp 𝔸 x) constructor · rw [← hx] - exact Function.Equivariant.preserve_support 𝔸 hequi (supp_is_support 𝔸) + exact Function.Equivariant.preserve_support 𝔸 (supp_is_support 𝔸) · exact supp_finite 𝔸 /-- supp is an equivariant function. -/ -lemma NominalSet.supp_equivariant : Function.Equivariant 𝔸 (supp 𝔸 : X → Set 𝔸) := by - intro x π; ext a; constructor +instance NominalSet.instSuppEquivariant : Function.Equivariant 𝔸 (supp 𝔸 : X → Set 𝔸) := by + constructor; intro x π + ext a; constructor · apply support_subset_supp 𝔸 - · apply PermSet.support_equivariant + · rw [← Rel.equivariant 𝔸 (PermSet.HasSupport 𝔸)] exact supp_is_support 𝔸 · apply Set.Finite.smul_set exact supp_finite 𝔸 · intro ha S hS have hsupp : PermSet.HasSupport 𝔸 x (π⁻¹ • S) := by rw [show x = π⁻¹ • π • x by exact eq_inv_smul_iff.mpr rfl] - apply PermSet.support_equivariant + rw [← Rel.equivariant 𝔸 (PermSet.HasSupport 𝔸)] exact hS.out.left rw [Set.mem_smul_set_iff_inv_smul_mem] at ha suffices π⁻¹ • a ∈ π⁻¹ • S by rw [Set.smul_mem_smul_set_iff] at this; assumption @@ -210,9 +227,9 @@ lemma NominalSet.supp_equivariant : Function.Equivariant 𝔸 (supp 𝔸 : X → exact hS.out.right /-- Freshness is an equivariant relation. -/ -lemma NominalSet.fresh_equivariant : Rel.Equivariant 𝔸 (NominalSet.IsFresh : 𝔸 → X → Prop) := by - intro x y π h - rwa [IsFresh, supp_equivariant, Set.smul_mem_smul_set_iff] +instance NominalSet.instFreshEquivariant : Rel.Equivariant 𝔸 (NominalSet.IsFresh : 𝔸 → X → Prop) := by + constructor; intro x y π h + rwa [IsFresh, Function.equivariant 𝔸 (supp 𝔸), Set.smul_mem_smul_set_iff] end Nominal @@ -229,8 +246,8 @@ 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₁ : Equivariant 𝔸 R → (И a, R a x) → (∃ a, a # x ∧ R a x) := by - intro hequi h +private lemma for_fresh_iff₁ : (И a, R a x) → (∃ a, a # x ∧ R a x) := by + intro 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 𝔸) @@ -238,17 +255,16 @@ private lemma for_fresh_iff₁ : Equivariant 𝔸 R → (И a, R a x) → (∃ a simp only [Set.mem_diff, Set.mem_setOf_eq] at ha use a; exact ha.symm -private lemma for_fresh_iff₂ : Equivariant 𝔸 R → (∃ a, a # x ∧ R a x) → (∀ a, a # x → R a x) := by - intro hequi h +private lemma for_fresh_iff₂ [Rel.Equivariant 𝔸 R] : (∃ a, a # x ∧ R a x) → (∀ a, a # x → R a x) := by + intro 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 + rw [Rel.equivariant 𝔸 R b x ⸨a, b⸩] + rw [PermSet.atom_swap, Equiv.swap_apply_right, NominalSet.fresh_swap_fix 𝔸 hfresha hfreshb] + exact ha -private lemma for_fresh_iff₃ : Equivariant 𝔸 R → (∀ a, a # x → R a x) → (И a, R a x) := by - intro hequi h +private lemma for_fresh_iff₃ : (∀ a, a # x → R a x) → (И a, R a x) := by + intro h have hsub : {a : 𝔸 | R a x}ᶜ ⊆ NominalSet.supp 𝔸 x := by rw [Set.compl_subset_comm] intro a ha @@ -258,25 +274,25 @@ private lemma for_fresh_iff₃ : Equivariant 𝔸 R → (∀ a, a # x → R a x) 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 : Equivariant 𝔸 R → ((И a, R a x) ↔ (∃ a, a # x ∧ R a x)) := by - intro hequi; constructor +lemma for_fresh_iff_exists [Rel.Equivariant 𝔸 R] : ((И a, R a x) ↔ (∃ a, a # x ∧ R a x)) := by + constructor · intro h - apply for_fresh_iff₁ 𝔸 hequi + apply for_fresh_iff₁ exact h · intro h - apply for_fresh_iff₃ 𝔸 hequi - apply for_fresh_iff₂ 𝔸 hequi + apply for_fresh_iff₃ + apply for_fresh_iff₂ exact h /-- The quantifier in `И a, a R x` is equivalent to "for all fresh `a`". -/ -lemma for_fresh_iff_all : Equivariant 𝔸 R → ((И a, R a x) ↔ (∀ a, a # x → R a x)) := by - intro hequi; constructor +lemma for_fresh_iff_all [Rel.Equivariant 𝔸 R] : ((И a, R a x) ↔ (∀ a, a # x → R a x)) := by + constructor · intro h - apply for_fresh_iff₂ 𝔸 hequi - apply for_fresh_iff₁ 𝔸 hequi + apply for_fresh_iff₂ + apply for_fresh_iff₁ exact h · intro h - apply for_fresh_iff₃ 𝔸 hequi + apply for_fresh_iff₃ exact h end Rel.Equivariant @@ -305,6 +321,9 @@ notation:25 X " →ₑ[" A "] " Y => EquivariantMap A X Y variable {X Y Z : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] [PermSet 𝔸 Z] +instance EquivariantMap.toFunEquivariant (f : X →ₑ[𝔸] Y) : Function.Equivariant 𝔸 f.toFun := + f.equivariant + instance : FunLike (X →ₑ[𝔸] Y) X Y where coe := EquivariantMap.toFun coe_injective' f g h := by cases f; cases g; congr @@ -312,10 +331,10 @@ instance : FunLike (X →ₑ[𝔸] Y) X Y where namespace EquivariantMap /-- The identity function. -/ -def id : X →ₑ[𝔸] X := ⟨_root_.id, id_equivariant 𝔸⟩ +def id : X →ₑ[𝔸] X := ⟨_root_.id, inferInstance⟩ /-- Function composition. -/ -def comp (f : Y →ₑ[𝔸] Z) (g : X →ₑ[𝔸] Y) : X →ₑ[𝔸] Z := ⟨f ∘ g, comp_equivariant 𝔸 f.equivariant g.equivariant⟩ +def comp (f : Y →ₑ[𝔸] Z) (g : X →ₑ[𝔸] Y) : X →ₑ[𝔸] Z := ⟨f.toFun ∘ g.toFun, inferInstance⟩ @[simp] lemma id_app (x : X) : id 𝔸 x = x := rfl @@ -333,10 +352,6 @@ lemma ext {f g : X →ₑ[𝔸] Y} (h : ∀ a, f a = g a) : f = g := end EquivariantMap -/-- Extended setoid definition that also requires the relation to be equivariant. -/ -class EquivariantSetoid (X : Type) [PermSet 𝔸 X] extends Setoid X where - equivariant : Rel.Equivariant 𝔸 r - end BundledFunction /-! @@ -349,7 +364,7 @@ section Equivalence /-- An equivalence where the function is equivariant. -/ structure EquivariantEquiv (X Y : Type) [PermSet 𝔸 X] [PermSet 𝔸 Y] extends Equiv X Y where toFun_equivariant : Function.Equivariant 𝔸 toFun - invFun_equivariant : Function.Equivariant 𝔸 invFun := Function.inv_equivariant 𝔸 left_inv right_inv toFun_equivariant + invFun_equivariant : Function.Equivariant 𝔸 invFun := Function.Equivariant.inv 𝔸 left_inv right_inv def Equivariant.Equiv.symm {𝔸 X Y : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] [PermSet 𝔸 X] [PermSet 𝔸 Y] (equiv : EquivariantEquiv 𝔸 X Y) : EquivariantEquiv 𝔸 Y X := { toFun := equiv.invFun @@ -359,15 +374,24 @@ def Equivariant.Equiv.symm {𝔸 X Y : Type} [Infinite 𝔸] [Countable 𝔸] [D right_inv := equiv.left_inv } +instance EquivariantEquiv.toFunEquivariant + {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] + (equiv : EquivariantEquiv 𝔸 X Y) : Function.Equivariant 𝔸 equiv.toFun := + equiv.toFun_equivariant + +instance EquivariantEquiv.invFunEquivariant + {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] + (equiv : EquivariantEquiv 𝔸 X Y) : Function.Equivariant 𝔸 equiv.invFun := + equiv.invFun_equivariant + /-- If an (FPerm 𝔸)-Set is equivalent to a nominal set, it is also a nominal set. -/ -def NominalSet.fromEquivariantEquiv {X Y : Type} [PermSet 𝔸 X] [NominalSet 𝔸 Y] (equiv : EquivariantEquiv 𝔸 X Y) : NominalSet 𝔸 X := - NominalSet.fromEquivariantSurjective 𝔸 equiv.invFun equiv.invFun_equivariant equiv.symm.surjective +def NominalSet.ofEquivariantEquiv {X Y : Type} [PermSet 𝔸 X] [NominalSet 𝔸 Y] (equiv : EquivariantEquiv 𝔸 X Y) : NominalSet 𝔸 X := + NominalSet.ofEquivariantSurjective 𝔸 equiv.invFun equiv.symm.surjective /-- If two nominal sets are equivalent, the corresponding least supports are equal. -/ lemma EquivariantEquiv.supp_eq {X Y : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y] (equiv : EquivariantEquiv 𝔸 X Y) (x : X) : NominalSet.supp 𝔸 x = NominalSet.supp 𝔸 (equiv.toFun x) := by symm apply Function.Equivariant.supp_eq_if_inj - · exact equiv.toFun_equivariant - · exact equiv.injective + exact equiv.injective end Equivalence diff --git a/Nominal/Instances/Abstraction.lean b/Nominal/Instances/Abstraction.lean index 69e29f2..e03d67a 100644 --- a/Nominal/Instances/Abstraction.lean +++ b/Nominal/Instances/Abstraction.lean @@ -49,11 +49,11 @@ instance : PermSet 𝔸 (NameAbstraction' 𝔸 X) where private def equiv : EquivariantEquiv 𝔸 (NameAbstraction' 𝔸 X) (𝔸 × X) := { toFun x := ⟨x.atom, x.body⟩ invFun x := ⟨x.fst, x.snd⟩ - toFun_equivariant := by intro x π; ext <;> simp + toFun_equivariant := by constructor; intro x π; ext <;> simp } instance : NominalSet 𝔸 (NameAbstraction' 𝔸 X) := - NominalSet.fromEquivariantEquiv 𝔸 (equiv 𝔸 X) + NominalSet.ofEquivariantEquiv 𝔸 (equiv 𝔸 X) @[simp] lemma supp {x : NameAbstraction' 𝔸 X} : NominalSet.supp 𝔸 x = NominalSet.supp 𝔸 x.body ∪ {x.atom} := by have h : NominalSet.supp 𝔸 x = NominalSet.supp 𝔸 (x.atom, x.body) := @@ -93,8 +93,8 @@ private lemma alpha_eq_iff_pred {x y : NameAbstraction' 𝔸 X} : AlphaEq x y = apply NominalSet.for_fresh_ext simp [AlphaEqPred] -private lemma alpha_eq_pred_equivariant : Rel.Equivariant 𝔸 (AlphaEqPred : 𝔸 → NameAbstraction' 𝔸 X × NameAbstraction' 𝔸 X → Prop) := by - intro a x π +private instance instAlphaEqPredEquivariant : Rel.Equivariant 𝔸 (AlphaEqPred : 𝔸 → NameAbstraction' 𝔸 X × NameAbstraction' 𝔸 X → Prop) := by + constructor; intro a x π rw [AlphaEqPred, AlphaEqPred] intro h have h' : π • ⸨a, x.fst.atom⸩ • x.fst.body = π • ⸨a, x.snd.atom⸩ • x.snd.body := by congr @@ -105,14 +105,12 @@ private lemma alpha_eq_iff_exists' {x y : NameAbstraction' 𝔸 X} : AlphaEq x y suffices (∃ c, c # x ∧ c # y ∧ ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body) = (∃ c, c # (x, y) ∧ AlphaEqPred c (x, y)) by rw [alpha_eq_iff_pred, this] apply Rel.Equivariant.for_fresh_iff_exists - exact alpha_eq_pred_equivariant simp [Prod.fresh, AlphaEqPred, @and_assoc] private lemma alpha_eq_iff_all' {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ ∀ c, c # x ∧ c # y → ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body := by suffices (∀ c, c # x ∧ c # y → ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body) = (∀ c, c # (x, y) → AlphaEqPred c (x, y)) by rw [alpha_eq_iff_pred, this] apply Rel.Equivariant.for_fresh_iff_all - exact alpha_eq_pred_equivariant simp [Prod.fresh, AlphaEqPred] private 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 @@ -132,8 +130,9 @@ private lemma alpha_eq_iff_cases' {x y : NameAbstraction' 𝔸 X} : AlphaEq x y · exact h_eq · simp at hcx simp at hcy - have h_atom : (⸨c, y.atom⸩ * ⸨c, x.atom⸩) • c # (⸨c, y.atom⸩ * ⸨c, x.atom⸩) • x.body := - NominalSet.fresh_equivariant 𝔸 _ _ _ hcx.right + have h_atom : (⸨c, y.atom⸩ * ⸨c, x.atom⸩) • c # (⸨c, y.atom⸩ * ⸨c, x.atom⸩) • x.body := by + rw [← Rel.equivariant 𝔸 NominalSet.IsFresh] + exact hcx.right have h_swap : ⸨c, x.atom⸩ * ⸨c, y.atom⸩ = ⸨x.atom, y.atom⸩ * ⸨c, x.atom⸩ := by ext a by_cases a = c <;> by_cases a = x.atom <;> by_cases a = y.atom @@ -176,8 +175,8 @@ private lemma alpha_eq_symm {x y : NameAbstraction' 𝔸 X} : AlphaEq x y → Al · 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 + rw [h.right.right, ← Rel.equivariant 𝔸 NominalSet.IsFresh] + exact h.right.left simp at h; exact h · rw [h.right.right, ← mul_smul, FPerm.swap_comm, FPerm.swap_mul_self, one_smul] @@ -190,15 +189,15 @@ private lemma alpha_eq_trans {x y z : NameAbstraction' 𝔸 X} : AlphaEq x y → · intro c ⟨hxy, hyz⟩ rw [hxy, hyz] -private lemma alpha_eq_equivariant : Rel.Equivariant 𝔸 (AlphaEq : NameAbstraction' 𝔸 X → NameAbstraction' 𝔸 X → Prop) := by - intro x y π h +private instance instAlphaEqEquivariant : Rel.Equivariant 𝔸 (AlphaEq : NameAbstraction' 𝔸 X → NameAbstraction' 𝔸 X → Prop) := by + constructor; 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 + · rw [← Rel.equivariant 𝔸 NominalSet.IsFresh]; exact hcx · constructor - · apply NominalSet.fresh_equivariant; exact hcy + · rw [← Rel.equivariant 𝔸 NominalSet.IsFresh]; 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' @@ -218,19 +217,21 @@ section Quotient variable (X : Type) [NominalSet 𝔸 X] /-- Associate the name abstraction structure with alpha-equivalence. -/ -instance NameAbstraction.setoid : EquivariantSetoid 𝔸 (NameAbstraction' 𝔸 X) where +instance NameAbstraction.setoid : Setoid (NameAbstraction' 𝔸 X) where r := AlphaEq iseqv := ⟨alpha_eq_refl, alpha_eq_symm, alpha_eq_trans⟩ - equivariant := alpha_eq_equivariant + +instance NameAbstraction.setoid_equivariant : Rel.Equivariant 𝔸 (setoid 𝔸 X) := + instAlphaEqEquivariant /-- Define name abstractions as the quotient set (𝔸 × X)/≈. -/ -def NameAbstraction := Quotient (NameAbstraction.setoid 𝔸 X).toSetoid +def NameAbstraction := Quotient (NameAbstraction.setoid 𝔸 X) namespace NameAbstraction /-- The equivalence class of a name abstraction (a, x), often written `⟪a⟫ x` -/ abbrev mk {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] {X : Type} [NominalSet 𝔸 X] (a : 𝔸) (x : X) : NameAbstraction 𝔸 X := - Quotient.mk (setoid 𝔸 X).toSetoid (.mk a x) + Quotient.mk (setoid 𝔸 X) (.mk a x) /-- We write `⟪a⟫ x` instead of the usual `⟨a⟩ x` because `⟨⟩` is already heavily used in Lean for constructors. -/ notation "⟪" a "⟫ " x:60 => mk a x @@ -283,7 +284,7 @@ private lemma raw_supp_swap {a b : 𝔸} {x y : X} : ⟪a⟫ x = ⟪b⟫ y → N 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⸩] + rw [h.right.right, Function.equivariant 𝔸 (NominalSet.supp 𝔸)] ext c by_cases h₁ : c = b · simp [h₁] @@ -350,7 +351,7 @@ namespace NameAbstraction variable {X Y Z : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y] [NominalSet 𝔸 Z] private def map' (f : X →ₑ[𝔸] Y) : NameAbstraction 𝔸 X → NameAbstraction 𝔸 Y := - Quotient.lift (fun x => ⟪x.atom⟫ f x.body) (by + Quotient.lift (fun x => ⟪x.atom⟫ f.toFun x.body) (by intro x y hxy rw [alpha_eq_iff_exists] at hxy obtain ⟨c, ⟨hcx, hcy, hc⟩⟩ := hxy @@ -358,28 +359,28 @@ private def map' (f : X →ₑ[𝔸] Y) : NameAbstraction 𝔸 X → NameAbstrac rw [NameAbstraction'.fresh] at hcy rw [eq_iff_exists] use c - have hc' : ⸨c,x.atom⸩ • f x.body = ⸨c,y.atom⸩ • f y.body := by - rw [show f x.body = f.toFun x.body from rfl, ← f.equivariant] - rw [show f y.body = f.toFun y.body from rfl, ← f.equivariant] + have hc' : ⸨c,x.atom⸩ • f.toFun x.body = ⸨c,y.atom⸩ • f.toFun y.body := by + rw [← Function.equivariant 𝔸 f.toFun] + rw [← Function.equivariant 𝔸 f.toFun] congr exact ⟨hcx.left, hcy.left, - Function.Equivariant.preserve_fresh 𝔸 f.equivariant hcx.right, - Function.Equivariant.preserve_fresh 𝔸 f.equivariant hcy.right, + Function.Equivariant.preserve_fresh 𝔸 hcx.right, + Function.Equivariant.preserve_fresh 𝔸 hcy.right, hc'⟩) -private lemma map_equivariant (f : X →ₑ[𝔸] Y) : Function.Equivariant 𝔸 (map' 𝔸 f) := by +private instance instMapEquivariant (f : X →ₑ[𝔸] Y) : Function.Equivariant 𝔸 (map' 𝔸 f) := by + constructor apply Quotient.ind intro x π - rw [← Quotient.mk_equivariant] + rw [← Function.equivariant 𝔸 (Quotient.mk _)] simp only [map', Quotient.lift_mk, NameAbstraction'.smul_atom, NameAbstraction'.smul_body, smul] - rw [show f (π • x.body) = f.toFun (π • x.body) from rfl, f.equivariant] - rfl + rw [← Function.equivariant 𝔸 f.toFun] /-- Lifts an equivariant function to name abstractions. -/ def map (f : X →ₑ[𝔸] Y) : NameAbstraction 𝔸 X →ₑ[𝔸] NameAbstraction 𝔸 Y := - ⟨map' 𝔸 f, map_equivariant 𝔸 f⟩ + ⟨map' 𝔸 f, instMapEquivariant 𝔸 f⟩ /-- Application of equivariant functions lifted to name abstractions. -/ @[simp] @@ -400,7 +401,7 @@ private lemma map_comp (f : Y →ₑ[𝔸] Z) (g : X →ₑ[𝔸] Y) : map 𝔸 /-- Name abstractions form a functor `Nom ⥤ Nom`. -/ def Functor : Nom 𝔸 ⥤ Nom 𝔸 := { obj X := ⟨NameAbstraction 𝔸 X⟩ - map f := ⟨NameAbstraction.map 𝔸 f, NameAbstraction.map_equivariant 𝔸 f⟩ + map f := ⟨NameAbstraction.map 𝔸 f, NameAbstraction.instMapEquivariant 𝔸 f⟩ map_id := fun _ => map_id 𝔸 map_comp f g := map_comp 𝔸 g f } diff --git a/Nominal/Instances/Basic.lean b/Nominal/Instances/Basic.lean index 7f461ac..dcca75b 100644 --- a/Nominal/Instances/Basic.lean +++ b/Nominal/Instances/Basic.lean @@ -140,11 +140,11 @@ instance : NominalSet 𝔸 (X × Y) where lemma supp_comm {x : X} {y : Y} : NominalSet.supp 𝔸 (x, y) = NominalSet.supp 𝔸 (y, x) := by simp; apply Set.union_comm -lemma fst_equivariant : Function.Equivariant 𝔸 (Prod.fst : X × Y → X) := by - simp [Function.Equivariant] +instance instFstEquivariant : Function.Equivariant 𝔸 (Prod.fst : X × Y → X) := by + constructor; simp -lemma snd_equivariant : Function.Equivariant 𝔸 (Prod.snd : X × Y → Y) := by - simp [Function.Equivariant] +instance instSndEquivariant : Function.Equivariant 𝔸 (Prod.snd : X × Y → Y) := by + constructor; simp end Prod @@ -212,11 +212,11 @@ instance : NominalSet 𝔸 (X ⊕ Y) where @[simp] lemma fresh_inr {a : 𝔸} {y : Y} : a # (.inr y : X ⊕ Y) ↔ a # y := by simp [NominalSet.IsFresh] -lemma inl_equivariant : Function.Equivariant 𝔸 (Sum.inl : X → X ⊕ Y) := by - simp [Function.Equivariant] +instance instInlEquivariant : Function.Equivariant 𝔸 (Sum.inl : X → X ⊕ Y) := by + constructor; simp -lemma inr_equivariant : Function.Equivariant 𝔸 (Sum.inr : Y → X ⊕ Y) := by - simp [Function.Equivariant] +instance instInrEquivariant : Function.Equivariant 𝔸 (Sum.inr : Y → X ⊕ Y) := by + constructor; simp end Sum @@ -231,17 +231,18 @@ section Quotient namespace Quotient -variable {X : Type} [PermSet 𝔸 X] {setoid : EquivariantSetoid 𝔸 X} +variable {X : Type} [PermSet 𝔸 X] {setoid : Setoid X} [Rel.Equivariant 𝔸 setoid.r] -instance : SMul (FPerm 𝔸) (Quotient setoid.toSetoid) where +instance : SMul (FPerm 𝔸) (Quotient setoid) where smul π := Quotient.lift (fun x => ⟦π • x⟧) (by intro x y hxy simp only [Quotient.eq] - apply setoid.equivariant x y π hxy) + rw [← Rel.equivariant 𝔸 setoid.r] + exact hxy) -@[simp] lemma smul_quotient (π : FPerm 𝔸) (x : X) : (π • Quotient.mk setoid.toSetoid x) = ⟦π • x⟧ := rfl +@[simp] lemma smul_quotient (π : FPerm 𝔸) (x : X) : (π • Quotient.mk setoid x) = ⟦π • x⟧ := rfl -instance : PermSet 𝔸 (Quotient setoid.toSetoid) where +instance : PermSet 𝔸 (Quotient setoid) where one_smul := by apply Quotient.ind intro x @@ -251,32 +252,33 @@ instance : PermSet 𝔸 (Quotient setoid.toSetoid) where apply Quotient.ind simp [mul_smul] -lemma mk_equivariant : Function.Equivariant 𝔸 (Quotient.mk setoid.toSetoid) := by - simp [Function.Equivariant] +instance instMkEquivariant : Function.Equivariant 𝔸 (Quotient.mk setoid) := by + constructor; simp -lemma lift_equivariant - {Y : Type} [PermSet 𝔸 Y] (f : X → Y) (h : ∀ (a b : X), a ≈ b → f a = f b) : - Function.Equivariant 𝔸 f → Function.Equivariant 𝔸 (Quotient.lift f h) := by - intro hequi x π +def lift_equivariant + {Y : Type} [PermSet 𝔸 Y] (f : X → Y) [Function.Equivariant 𝔸 f] + (h : ∀ (a b : X), a ≈ b → f a = f b) : + Function.Equivariant 𝔸 (Quotient.lift f h) := by + constructor; intro x π obtain ⟨x', hx'⟩ := x.exists_rep - simp [← hx', hequi x' π] + simp [← hx', Function.equivariant 𝔸 f] -variable {X : Type} [NominalSet 𝔸 X] {setoid : EquivariantSetoid 𝔸 X} +variable {X : Type} [NominalSet 𝔸 X] {setoid : Setoid X} [Rel.Equivariant 𝔸 setoid.r] -instance : NominalSet 𝔸 (Quotient setoid.toSetoid) := - NominalSet.fromEquivariantSurjective 𝔸 (Quotient.mk setoid.toSetoid) (mk_equivariant 𝔸) mk_surjective +instance : NominalSet 𝔸 (Quotient setoid) := + NominalSet.ofEquivariantSurjective 𝔸 (Quotient.mk setoid) mk_surjective -lemma supp {x : X} : NominalSet.supp 𝔸 (Quotient.mk setoid.toSetoid x) = {a | ∀ (x' : X), x' ≈ x → a ∈ NominalSet.supp 𝔸 x'} := by +lemma supp {x : X} : NominalSet.supp 𝔸 (Quotient.mk setoid x) = {a | ∀ (x' : X), x' ≈ x → a ∈ NominalSet.supp 𝔸 x'} := by ext a constructor · intro ha x' hx' rw [← Quotient.sound hx'] at ha - have hsub : NominalSet.supp 𝔸 (Quotient.mk setoid.toSetoid x') ⊆ NominalSet.supp 𝔸 x' := - Function.Equivariant.supp_subset 𝔸 (mk_equivariant 𝔸) + have hsub : NominalSet.supp 𝔸 (Quotient.mk setoid x') ⊆ NominalSet.supp 𝔸 x' := + Function.Equivariant.supp_subset 𝔸 exact hsub ha · contrapose; intro ha simp only [Set.mem_setOf_eq, Classical.not_imp, not_forall] - have hfin₁ : (NominalSet.supp 𝔸 (Quotient.mk setoid.toSetoid x)).Finite := NominalSet.supp_finite 𝔸 + have hfin₁ : (NominalSet.supp 𝔸 (Quotient.mk setoid x)).Finite := NominalSet.supp_finite 𝔸 have hfin₂ : (NominalSet.supp 𝔸 x).Finite := NominalSet.supp_finite 𝔸 -- Show that we can find a fresh c for which (a c) • ⟦x⟧ = ⟦x⟧ obtain ⟨c, hc⟩ := Infinite.exists_notMem_finset (hfin₁.toFinset ∪ hfin₂.toFinset) @@ -285,15 +287,66 @@ lemma supp {x : X} : NominalSet.supp 𝔸 (Quotient.mk setoid.toSetoid x) = {a | · apply Quotient.exact rw [← smul_quotient] exact NominalSet.fresh_swap_fix 𝔸 ha hc.left - · rw [NominalSet.supp_equivariant, Set.mem_smul_set_iff_inv_smul_mem] + · rw [Function.equivariant 𝔸 (NominalSet.supp 𝔸), Set.mem_smul_set_iff_inv_smul_mem] simp only [FPerm.swap_inv, PermSet.atom_swap, Equiv.swap_apply_left] exact hc.right /-- If an atom is not in the support of the equivalence class, one can always pick a representative where it is not in the least support. -/ -lemma supp_pick_fresh {a : 𝔸} {x : X} : a ∉ NominalSet.supp 𝔸 (Quotient.mk setoid.toSetoid x) → ∃ (y : X), y ≈ x ∧ a ∉ NominalSet.supp 𝔸 y := by +lemma supp_pick_fresh {a : 𝔸} {x : X} : a ∉ NominalSet.supp 𝔸 (Quotient.mk setoid x) → ∃ (y : X), y ≈ x ∧ a ∉ NominalSet.supp 𝔸 y := by contrapose simp [not_exists, not_and, not_not, supp] end Quotient end Quotient + +/-! +## Subtypes + +If X is a nominal set, Y is a subtype of X, and π • x ∈ Y for all π ∈ FPerm 𝔸 and x ∈ X, then Y is +also a nominal set. +-/ +section Subtype + +namespace Subtype + +variable {X : Type} [PermSet 𝔸 X] {S : Set X} [Set.Equivariant 𝔸 S] + +instance : PermSet 𝔸 S where + smul π x := ⟨π • x.val, by + rw [← Set.equivariant 𝔸 S] + exact x.prop⟩ + one_smul x := by + apply Subtype.eq + exact MulAction.one_smul x.val + mul_smul π τ x := by + apply Subtype.eq + exact MulAction.mul_smul π τ x.val + +@[simp] lemma smul_val (π : FPerm 𝔸) (x : S) : (π • x).val = π • x.val := rfl + +instance instValEquivariant : Function.Equivariant 𝔸 (Subtype.val : S → X) := by + constructor; simp + +variable {X : Type} [NominalSet 𝔸 X] {S : Set X} [Set.Equivariant 𝔸 S] + +instance : NominalSet 𝔸 S where + fin_supp x := by + use NominalSet.supp 𝔸 x.val + constructor + · intro π hπ + apply Subtype.eq + exact NominalSet.supp_is_support 𝔸 hπ + · exact NominalSet.supp_finite 𝔸 + +@[simp] lemma supp {x : S} : NominalSet.supp 𝔸 x = NominalSet.supp 𝔸 x.val := by + symm + apply Function.Equivariant.supp_eq_if_inj + exact val_injective + +@[simp] lemma fresh {a : 𝔸} {x : S} : a # x ↔ a # x.val := by + simp [NominalSet.IsFresh] + +end Subtype + +end Subtype diff --git a/Nominal/LambdaCalculus/Preterms.lean b/Nominal/LambdaCalculus/Preterms.lean index c133343..81622af 100644 --- a/Nominal/LambdaCalculus/Preterms.lean +++ b/Nominal/LambdaCalculus/Preterms.lean @@ -141,7 +141,7 @@ private def equiv : EquivariantEquiv Var Preterm (Var ⊕ (Var × Preterm) ⊕ ( | inl _ => simp | inr x' => cases x' <;> all_goals simp toFun_equivariant := by - intro t π + constructor; intro t π cases t <;> all_goals simp } @@ -181,13 +181,13 @@ lemma fv_finite (t : Preterm) : t.fv.Finite := by apply Set.Finite.subset (vars_finite t) (fv_subset_vars t) /-- The vars map is equivariant. -/ -lemma vars_equivariant : Function.Equivariant Var vars := by - intro t π +instance instVarsEquivariant : Function.Equivariant Var vars := by + constructor; intro t π fun_induction vars <;> all_goals simp [vars, *, Set.smul_set_insert, Set.smul_set_union] /-- The fv map is equivariant. -/ -lemma fv_equivariant : Function.Equivariant Var fv := by - intro t π +instance instFvEquivariant : Function.Equivariant Var fv := by + constructor; intro t π fun_induction fv <;> all_goals simp [fv, *, Set.smul_set_sdiff, Set.smul_set_union] end Preterm diff --git a/Nominal/LambdaCalculus/Terms.lean b/Nominal/LambdaCalculus/Terms.lean index be0d77d..91f4fb8 100644 --- a/Nominal/LambdaCalculus/Terms.lean +++ b/Nominal/LambdaCalculus/Terms.lean @@ -34,30 +34,31 @@ inductive AlphaEq : Preterm → Preterm → Prop where | rename {x y : Var} {t : Preterm} : y ∉ t.fv → AlphaEq (.abs x t) (.abs y (⸨x, y⸩ • t)) /-- By definition, AlphaEq is an equivariant equivalence relation. -/ -instance Preterm.setoid : EquivariantSetoid Var Preterm where +instance Preterm.setoid : Setoid Preterm where r := AlphaEq - iseqv := ⟨fun x => AlphaEq.refl, AlphaEq.symm, AlphaEq.trans⟩ - equivariant := by - intro t u π htu - induction' htu <;> all_goals expose_names - · exact AlphaEq.refl - · exact AlphaEq.symm a_ih - · exact AlphaEq.trans a_ih a_ih_1 - · exact AlphaEq.cong_abs a_ih - · exact AlphaEq.cong_app a_ih a_ih_1 - · simp only [Preterm.smul_abs] - rw [← mul_smul, FPerm.mul_swap_eq_swap_mul, mul_smul] - apply AlphaEq.rename - rw [Preterm.fv_equivariant, Set.smul_mem_smul_set_iff] - exact h + iseqv := ⟨fun _ => AlphaEq.refl, AlphaEq.symm, AlphaEq.trans⟩ + +instance Preterm.instSetoidEquivariant : Rel.Equivariant Var setoid.r := by + constructor; intro t u π htu + induction' htu <;> all_goals expose_names + · exact AlphaEq.refl + · exact AlphaEq.symm a_ih + · exact AlphaEq.trans a_ih a_ih_1 + · exact AlphaEq.cong_abs a_ih + · exact AlphaEq.cong_app a_ih a_ih_1 + · simp only [Preterm.smul_abs] + rw [← mul_smul, FPerm.mul_swap_eq_swap_mul, mul_smul] + apply AlphaEq.rename + rw [Function.equivariant Var Preterm.fv, Set.smul_mem_smul_set_iff] + exact h /-- Define λ-terms as the quotient Preterm/≈. -/ -def Term := Quotient Preterm.setoid.toSetoid +def Term := Quotient Preterm.setoid namespace Term /-- The equivalence class of a λ-preterm. -/ -abbrev mk : Preterm → Term := Quotient.mk Preterm.setoid.toSetoid +abbrev mk : Preterm → Term := Quotient.mk Preterm.setoid instance : NominalSet Var Term := Quotient.instNominalSet Var @@ -135,7 +136,7 @@ private lemma pick_fresh {t : Preterm} : ∀ x ∉ t.fv, ∃ u, t ≈ u ∧ x rw [Set.singleton_union, Set.mem_compl_iff, Set.mem_insert_iff, not_or] at hc have hc' : c ∉ (π • a_1).fv := fun h => hc.right (Preterm.fv_subset_vars _ h) obtain ⟨u, hu⟩ := a_ih (⸨π • a, c⸩ * π) x (by - rw [mul_smul, Preterm.fv_equivariant] + rw [mul_smul, Function.equivariant Var Preterm.fv] intro hcontra by_cases hxa : x = π • a · rw [hxa, ← PermSet.atom_set_swap_right] at hcontra @@ -177,7 +178,7 @@ lemma alpha_eq_iff : AlphaEq = AlphaEq' := by rw [h_1] · obtain ⟨z, ⟨hz₁, hz₂⟩⟩ := pick_fresh y h apply AlphaEq'.abs - rw [Quotient.mk_equivariant, Quotient.sound hz₁, NameAbstraction.eq_iff_cases] + rw [Function.equivariant Var (Quotient.mk _), Quotient.sound hz₁, NameAbstraction.eq_iff_cases] by_cases hxy : x = y · left simp [hxy, FPerm.swap_self, one_smul] @@ -187,8 +188,8 @@ lemma alpha_eq_iff : AlphaEq = AlphaEq' := by · constructor · rw [← Preterm.supp] at hz₂ nth_rw 1 [show x = ⸨x, y⸩ • y by simp] - apply NominalSet.fresh_equivariant - exact Function.Equivariant.preserve_fresh Var (Quotient.mk_equivariant Var) hz₂ + rw [← Rel.equivariant Var NominalSet.IsFresh] + exact Function.Equivariant.preserve_fresh Var hz₂ · rw [← mul_smul, FPerm.swap_mul_self, one_smul] · intro h; cases h <;> all_goals expose_names · exact AlphaEq.refl @@ -201,7 +202,7 @@ lemma alpha_eq_iff : AlphaEq = AlphaEq' := by exact h.right | inr h => obtain ⟨s, ⟨hs₁, hs₂⟩⟩ := Quotient.supp_pick_fresh Var h.right.left - rw [← Quotient.sound hs₁, ← Quotient.mk_equivariant] at h + rw [← Quotient.sound hs₁, ← Function.equivariant Var (Quotient.mk _)] at h have hrename : Preterm.abs y s ≈ Preterm.abs x (⸨y, x⸩ • s) := by apply AlphaEq.rename rw [Preterm.supp] at hs₂ @@ -241,6 +242,7 @@ lemma eq_abs {x y : Var} {t u : Term} : Term.abs x t = Term.abs y u ↔ ⟪x⟫ obtain ⟨u', hu'⟩ := u.exists_rep simp only [abs, ← ht', Quotient.lift_mk, ← hu'] rw [Quotient.eq_iff_equiv, alpha_eq_abs] + rfl /-- Alternative characterization of α-equivalence for application preterms. -/ lemma alpha_eq_app {t₁ t₂ u₁ u₂ : Preterm} : Preterm.app t₁ t₂ ≈ Preterm.app u₁ u₂ ↔ t₁ ≈ u₁ ∧ t₂ ≈ u₂ := by @@ -293,7 +295,7 @@ private def equiv : EquivariantEquiv Var Term (Var ⊕ (NameAbstraction Var Term (by intro t u htu rw [alpha_eq, alpha_eq_iff] at htu - cases htu <;> simp [*]) + cases htu <;> simp only [Sum.inr.injEq, Sum.inl.injEq, *]; assumption) invFun | .inl x => .var x | .inr (.inl x) => Quotient.liftOn x @@ -323,7 +325,7 @@ private def equiv : EquivariantEquiv Var Term (Var ⊕ (NameAbstraction Var Term simp only [app, ← hx', ← hy', Quotient.lift_mk, Sum.inr.injEq] rw [hx', hy'] toFun_equivariant := by - intro t π + constructor; intro t π obtain ⟨t', ht'⟩ := t.exists_rep rw [← ht'] cases t' <;> all_goals rfl @@ -357,8 +359,7 @@ def fv : Term → Set Var := Quotient.lift Preterm.fv (by simp [← ht', ← hu', Preterm.fv] /-- The lifted fv function is also equivariant.-/ -lemma fv_equivariant : Function.Equivariant Var fv := - Quotient.lift_equivariant Var _ _ Preterm.fv_equivariant +instance instFvEquivariant : Function.Equivariant Var fv := Quotient.lift_equivariant Var _ _ /-- The support of a term consists exactly of the free variables in it. -/ lemma supp : NominalSet.supp Var = fv := by diff --git a/Nominal/Support.lean b/Nominal/Support.lean index 93e7aaa..7888a68 100644 --- a/Nominal/Support.lean +++ b/Nominal/Support.lean @@ -38,6 +38,12 @@ lemma fix_antitone {X : Type} [PermSet 𝔸 X] {S T : Set X} : S ⊆ T → PermS intro hsub π hπ x hx exact hπ x (hsub hx) +/-- Restatement of `fix_antitone` that is sometimes more convenient for use with apply. -/ +lemma fix_antitone_mem {X : Type} [PermSet 𝔸 X] {S T : Set X} {π : FPerm 𝔸} : + π ∈ PermSet.fix 𝔸 T → S ⊆ T → π ∈ PermSet.fix 𝔸 S := by + intro hπ hsub + exact fix_antitone 𝔸 hsub hπ + /-- If π fixes S ∪ T, it fixes both S and T. -/ lemma fix_union {X : Type} [PermSet 𝔸 X] {S T : Set X} : PermSet.fix 𝔸 (S ∪ T) ⊆ PermSet.fix 𝔸 S ∩ PermSet.fix 𝔸 T := by apply Set.subset_inter <;> all_goals simp [fix_antitone] -- cgit v1.3.1