diff options
Diffstat (limited to 'Nominal')
| -rw-r--r-- | Nominal/Category.lean | 4 | ||||
| -rw-r--r-- | Nominal/Equivariance.lean | 224 | ||||
| -rw-r--r-- | Nominal/Instances/Abstraction.lean | 63 | ||||
| -rw-r--r-- | Nominal/Instances/Basic.lean | 111 | ||||
| -rw-r--r-- | Nominal/LambdaCalculus/Preterms.lean | 10 | ||||
| -rw-r--r-- | Nominal/LambdaCalculus/Terms.lean | 53 | ||||
| -rw-r--r-- | Nominal/Support.lean | 6 |
7 files changed, 278 insertions, 193 deletions
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] |