diff options
Diffstat (limited to 'Nominal/Instances/Abstraction.lean')
| -rw-r--r-- | Nominal/Instances/Abstraction.lean | 6 |
1 files changed, 3 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 |