diff options
Diffstat (limited to 'Nominal')
| -rw-r--r-- | Nominal/Equivariance.lean | 16 | ||||
| -rw-r--r-- | Nominal/Instances/Abstraction.lean | 98 |
2 files changed, 102 insertions, 12 deletions
diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean index 0fe9f91..3166e71 100644 --- a/Nominal/Equivariance.lean +++ b/Nominal/Equivariance.lean @@ -163,6 +163,16 @@ lemma supp_eq_if_inj {x : X} {f : X → Y} : Equivariant 𝔸 f → Function.Inj intro hequi hinj simp [NominalSet.supp, preserve_support_inj 𝔸 hequi 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) + +/-- 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] + end Equivariant /-- If there is an equivariant surjection from a nominal set into an (FPerm 𝔸)-Set, then that set is nominal. -/ @@ -306,6 +316,12 @@ def id : X →ₑ[𝔸] X := ⟨_root_.id, id_equivariant 𝔸⟩ def comp (f : Y →ₑ[𝔸] Z) (g : X →ₑ[𝔸] Y) : X →ₑ[𝔸] Z := ⟨f ∘ g, comp_equivariant 𝔸 f.equivariant g.equivariant⟩ @[simp] +lemma id_app (x : X) : id 𝔸 x = x := rfl + +@[simp] +lemma comp_app (f : Y →ₑ[𝔸] Z) (g : X →ₑ[𝔸] Y) (x : X) : comp 𝔸 f g x = f (g x) := rfl + +@[simp] lemma toFun_eq_coe {f : X →ₑ[𝔸] Y} : f.toFun = (f : X → Y) := rfl diff --git a/Nominal/Instances/Abstraction.lean b/Nominal/Instances/Abstraction.lean index 1fab31a..943bd43 100644 --- a/Nominal/Instances/Abstraction.lean +++ b/Nominal/Instances/Abstraction.lean @@ -113,23 +113,23 @@ private lemma alpha_eq_pred_equivariant : EquivariantRelation 𝔸 (AlphaEqPred simp only [smul_smul, FPerm.mul_swap_eq_swap_mul] at h' simpa [smul_smul] -private lemma alpha_eq_iff_exists {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ ∃ c, c # x ∧ c # y ∧ ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body := by +private lemma alpha_eq_iff_exists' {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 Equivariance.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 +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 Equivariance.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 +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 constructor - · rw [alpha_eq_iff_exists] + · rw [alpha_eq_iff_exists'] intro h obtain ⟨c, ⟨hcx, ⟨hcy, hc⟩⟩⟩ := h by_cases h_eq : x.atom = y.atom @@ -159,7 +159,7 @@ private lemma alpha_eq_iff_cases {x y : NameAbstraction' 𝔸 X} : AlphaEq x y _ = (⸨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] + · rw [alpha_eq_iff_all'] intro h c ⟨hcx, hcy⟩ cases h with | inl h => @@ -174,11 +174,11 @@ private lemma alpha_eq_iff_cases {x y : NameAbstraction' 𝔸 X} : AlphaEq x y rw [h.right.right, ← mul_smul, h_swap, mul_smul, NominalSet.fresh_swap_fix 𝔸 hcy.right h.right.left] private lemma alpha_eq_refl (x : NameAbstraction' 𝔸 X) : AlphaEq x x := by - rw [alpha_eq_iff_cases]; left + rw [alpha_eq_iff_cases']; left trivial 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] + rw [alpha_eq_iff_cases', alpha_eq_iff_cases'] intro h cases h with | inl h => @@ -204,7 +204,7 @@ private lemma alpha_eq_trans {x y z : NameAbstraction' 𝔸 X} : AlphaEq x y → private lemma alpha_eq_equivariant : EquivariantRelation 𝔸 (AlphaEq : NameAbstraction' 𝔸 X → NameAbstraction' 𝔸 X → Prop) := by intro x y π h - rw [alpha_eq_iff_exists] at * + rw [alpha_eq_iff_exists'] at * obtain ⟨c, ⟨hcx, ⟨hcy, hc⟩⟩⟩ := h use π • c constructor @@ -252,24 +252,37 @@ instance : NominalSet 𝔸 (NameAbstraction 𝔸 X) := Quotient.instNominalSet @[simp] lemma smul {π : FPerm 𝔸} {a : 𝔸} {x : X } : π • ⟪a⟫ x = ⟪π • a⟫ π • x := by congr +private lemma alpha_eq {x y : NameAbstraction' 𝔸 X} : x ≈ y ↔ AlphaEq x y := by rfl + /-- Two name abstractions are equal iff they are alpha-equivalent. -/ -lemma eq_iff_alpha_eq {a b : 𝔸} {x y : X} : ⟪a⟫ x = ⟪b⟫ y ↔ AlphaEq ⟨a, x⟩ ⟨b, y⟩ := by +lemma eq_iff_alpha_eq {a b : 𝔸} {x y : X} : ⟪a⟫ x = ⟪b⟫ y ↔ (⟨a, x⟩ : NameAbstraction' 𝔸 X) ≈ (⟨b, y⟩ : NameAbstraction' 𝔸 X) := by rw [mk, mk, Quotient.eq_iff_equiv] - rfl /-- The freshness quantifier in the AlphaEq definition is equivalent to "there exists some c # (x, y)". -/ +lemma alpha_eq_iff_exists {x y : NameAbstraction' 𝔸 X} : x ≈ y ↔ ∃ c, c # x ∧ c # y ∧ ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body := by + rw [alpha_eq, alpha_eq_iff_exists'] + +@[inherit_doc alpha_eq_iff_exists] lemma eq_iff_exists {a b : 𝔸} {x y : X} : ⟪a⟫ x = ⟪b⟫ y ↔ ∃ c, c ≠ a ∧ c ≠ b ∧ c # x ∧ c # y ∧ ⸨c, a⸩ • x = ⸨c, b⸩ • y := by simp only [eq_iff_alpha_eq, alpha_eq_iff_exists, NameAbstraction'.fresh, ne_eq] ac_nf /-- The freshness quantifier in the AlphaEq definition is equivalent to "for all c # (x, y)". -/ -lemma eq_iff_all {a b : 𝔸} {x y : X} : ⟪a⟫ x = ⟪b⟫ y ↔ ∀ c, c ≠ a ∧ c ≠ b ∧ c # x ∧ c # y → ⸨c, a⸩ • x = ⸨c, b⸩ • y := by +lemma alpha_eq_iff_all {x y : NameAbstraction' 𝔸 X} : x ≈ y ↔ ∀ c, c # x ∧ c # y → ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body := by + rw [alpha_eq, alpha_eq_iff_all'] + +@[inherit_doc alpha_eq_iff_all] +lemma eq_iff_all {a b : 𝔸} {x y : X} : ⟪a⟫ x = ⟪b⟫ y ↔ ∀ c, c ≠ a ∧ c ≠ b ∧ c # x ∧ c # y → ⸨c, a⸩ • x = ⸨c, b⸩ • y := by simp only [eq_iff_alpha_eq, alpha_eq_iff_all, NameAbstraction'.fresh, ne_eq] ac_nf /-- An alternative definition of α-equivalence: 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} : 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 + rw [alpha_eq, alpha_eq_iff_cases'] + +@[inherit_doc alpha_eq_iff_cases] lemma eq_iff_cases {a b : 𝔸} {x y : X} : ⟪a⟫ x = ⟪b⟫ y ↔ (a = b ∧ x = y) ∨ (a ≠ b ∧ a # y ∧ x = ⸨a, b⸩ • y) := by simp [eq_iff_alpha_eq, alpha_eq_iff_cases] @@ -338,10 +351,71 @@ end Quotient /-! ## Abstraction Functor -Name abstraction can also be considered as a functor `Nom → Nom`. +Name abstraction can also be considered as a functor `Nom ⥤ Nom`. -/ section Functor +open CategoryTheory +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 + intro x y hxy + rw [alpha_eq_iff_exists] at hxy + obtain ⟨c, ⟨hcx, hcy, hc⟩⟩ := hxy + rw [NameAbstraction'.fresh] at hcx + 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] + congr + exact + ⟨hcx.left, + hcy.left, + Equivariant.preserve_fresh 𝔸 f.equivariant hcx.right, + Equivariant.preserve_fresh 𝔸 f.equivariant hcy.right, + hc'⟩) + +private lemma map_equivariant (f : X →ₑ[𝔸] Y) : Equivariant 𝔸 (map' 𝔸 f) := by + apply Quotient.ind + intro x π + rw [← Quotient.mk_equivariant] + 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 + +/-- Lifts an equivariant function to name abstractions. -/ +def map (f : X →ₑ[𝔸] Y) : NameAbstraction 𝔸 X →ₑ[𝔸] NameAbstraction 𝔸 Y := + ⟨map' 𝔸 f, map_equivariant 𝔸 f⟩ + +/-- Application of equivariant functions lifted to name abstractions. -/ +@[simp] +lemma map_eq {f : X →ₑ[𝔸] Y} {a : 𝔸} {x : X} : map 𝔸 f (⟪a⟫ x) = ⟪a⟫ f x := rfl + +private lemma map_id : map 𝔸 (EquivariantMap.id 𝔸 : X →ₑ[𝔸] X) = EquivariantMap.id 𝔸 := by + suffices ∀ (x : NameAbstraction 𝔸 X), map' 𝔸 (EquivariantMap.id 𝔸) x = x by ext x; exact this x + apply Quotient.ind + intro x + simp [map', NameAbstraction.mk] + +private lemma map_comp (f : Y →ₑ[𝔸] Z) (g : X →ₑ[𝔸] Y) : map 𝔸 (EquivariantMap.comp 𝔸 f g) = EquivariantMap.comp 𝔸 (map 𝔸 f) (map 𝔸 g) := by + suffices ∀ (x : NameAbstraction 𝔸 X), map' 𝔸 (EquivariantMap.comp 𝔸 f g) x = (map' 𝔸 f) ((map' 𝔸 g) x) by ext x; exact this x + apply Quotient.ind + intro x + simp [map', NameAbstraction.mk] + +/-- 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_id := fun _ => map_id 𝔸 + map_comp f g := map_comp 𝔸 g f } + +end NameAbstraction end Functor |