diff options
Diffstat (limited to 'Nominal/Instances/Abstraction.lean')
| -rw-r--r-- | Nominal/Instances/Abstraction.lean | 63 |
1 files changed, 32 insertions, 31 deletions
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 } |