diff options
Diffstat (limited to 'Nominal/Instances/Abstraction.lean')
| -rw-r--r-- | Nominal/Instances/Abstraction.lean | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/Nominal/Instances/Abstraction.lean b/Nominal/Instances/Abstraction.lean index 943bd43..ba2fbf9 100644 --- a/Nominal/Instances/Abstraction.lean +++ b/Nominal/Instances/Abstraction.lean @@ -60,7 +60,7 @@ private lemma ofPair_surjective : Function.Surjective (ofPair 𝔸 X) := by use ⟨x.atom, x.body⟩ simp [ofPair] -private lemma ofPair_equivariant : Equivariant 𝔸 (ofPair 𝔸 X) := by +private lemma ofPair_equivariant : Function.Equivariant 𝔸 (ofPair 𝔸 X) := by intro x π ext <;> simp [ofPair] @@ -69,7 +69,7 @@ instance : NominalSet 𝔸 (NameAbstraction' 𝔸 X) := @[simp] lemma supp {x : NameAbstraction' 𝔸 X} : NominalSet.supp 𝔸 x = NominalSet.supp 𝔸 x.body ∪ {x.atom} := by have h : NominalSet.supp 𝔸 (ofPair 𝔸 X (x.atom, x.body)) = NominalSet.supp 𝔸 (x.atom, x.body) := - Equivariant.supp_eq_if_inj 𝔸 (ofPair_equivariant 𝔸 X) (ofPair_injective 𝔸 X) + Function.Equivariant.supp_eq_if_inj 𝔸 (ofPair_equivariant 𝔸 X) (ofPair_injective 𝔸 X) simp only [Prod.supp, NominalSet.supp_atom, ofPair] at h rwa [Set.union_comm] at h @@ -105,7 +105,7 @@ 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 : EquivariantRelation 𝔸 (AlphaEqPred : 𝔸 → NameAbstraction' 𝔸 X × NameAbstraction' 𝔸 X → Prop) := by +private lemma alpha_eq_pred_equivariant : Rel.Equivariant 𝔸 (AlphaEqPred : 𝔸 → NameAbstraction' 𝔸 X × NameAbstraction' 𝔸 X → Prop) := by intro a x π rw [AlphaEqPred, AlphaEqPred] intro h @@ -116,14 +116,14 @@ private lemma alpha_eq_pred_equivariant : EquivariantRelation 𝔸 (AlphaEqPred 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 + 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 Equivariance.for_fresh_iff_all + apply Rel.Equivariant.for_fresh_iff_all exact alpha_eq_pred_equivariant simp [Prod.fresh, AlphaEqPred] @@ -202,7 +202,7 @@ 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 : EquivariantRelation 𝔸 (AlphaEq : NameAbstraction' 𝔸 X → NameAbstraction' 𝔸 X → Prop) := by +private lemma alpha_eq_equivariant : Rel.Equivariant 𝔸 (AlphaEq : NameAbstraction' 𝔸 X → NameAbstraction' 𝔸 X → Prop) := by intro x y π h rw [alpha_eq_iff_exists'] at * obtain ⟨c, ⟨hcx, ⟨hcy, hc⟩⟩⟩ := h @@ -377,11 +377,11 @@ private def map' (f : X →ₑ[𝔸] Y) : NameAbstraction 𝔸 X → NameAbstrac exact ⟨hcx.left, hcy.left, - Equivariant.preserve_fresh 𝔸 f.equivariant hcx.right, - Equivariant.preserve_fresh 𝔸 f.equivariant hcy.right, + Function.Equivariant.preserve_fresh 𝔸 f.equivariant hcx.right, + Function.Equivariant.preserve_fresh 𝔸 f.equivariant hcy.right, hc'⟩) -private lemma map_equivariant (f : X →ₑ[𝔸] Y) : Equivariant 𝔸 (map' 𝔸 f) := by +private lemma map_equivariant (f : X →ₑ[𝔸] Y) : Function.Equivariant 𝔸 (map' 𝔸 f) := by apply Quotient.ind intro x π rw [← Quotient.mk_equivariant] |