diff options
Diffstat (limited to 'Nominal/Instances')
| -rw-r--r-- | Nominal/Instances/Abstraction.lean | 6 | ||||
| -rw-r--r-- | Nominal/Instances/Basic.lean | 7 |
2 files changed, 10 insertions, 3 deletions
diff --git a/Nominal/Instances/Abstraction.lean b/Nominal/Instances/Abstraction.lean index 052f604..69e29f2 100644 --- a/Nominal/Instances/Abstraction.lean +++ b/Nominal/Instances/Abstraction.lean @@ -229,7 +229,7 @@ def NameAbstraction := Quotient (NameAbstraction.setoid 𝔸 X).toSetoid namespace NameAbstraction /-- The equivalence class of a name abstraction (a, x), often written `⟪a⟫ x` -/ -def mk {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] {X : Type} [NominalSet 𝔸 X] (a : 𝔸) (x : X) : NameAbstraction 𝔸 X := +abbrev mk {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] {X : Type} [NominalSet 𝔸 X] (a : 𝔸) (x : X) : NameAbstraction 𝔸 X := Quotient.mk (setoid 𝔸 X).toSetoid (.mk a x) /-- We write `⟪a⟫ x` instead of the usual `⟨a⟩ x` because `⟨⟩` is already heavily used in Lean for constructors. -/ @@ -244,7 +244,7 @@ private lemma alpha_eq {x y : NameAbstraction' 𝔸 X} : x ≈ y ↔ AlphaEq x y /-- Two name abstractions are equal iff they are alpha-equivalent. -/ 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] + rw [Quotient.eq_iff_equiv] /-- 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 @@ -293,7 +293,7 @@ private lemma raw_supp_swap {a b : 𝔸} {x y : X} : ⟪a⟫ x = ⟪b⟫ y → N @[simp] lemma supp {a : 𝔸} {x : X} : NominalSet.supp 𝔸 (⟪a⟫ x) = NominalSet.supp 𝔸 x \ {a} := by - rw [mk, Quotient.supp] + rw [Quotient.supp] ext b constructor · by_cases h_eq : a = b diff --git a/Nominal/Instances/Basic.lean b/Nominal/Instances/Basic.lean index dea5bcf..7f461ac 100644 --- a/Nominal/Instances/Basic.lean +++ b/Nominal/Instances/Basic.lean @@ -254,6 +254,13 @@ instance : PermSet 𝔸 (Quotient setoid.toSetoid) where lemma mk_equivariant : Function.Equivariant 𝔸 (Quotient.mk setoid.toSetoid) := by simp [Function.Equivariant] +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 π + obtain ⟨x', hx'⟩ := x.exists_rep + simp [← hx', hequi x' π] + variable {X : Type} [NominalSet 𝔸 X] {setoid : EquivariantSetoid 𝔸 X} instance : NominalSet 𝔸 (Quotient setoid.toSetoid) := |