diff options
Diffstat (limited to 'Nominal/Instances/Abstraction.lean')
| -rw-r--r-- | Nominal/Instances/Abstraction.lean | 29 |
1 files changed, 24 insertions, 5 deletions
diff --git a/Nominal/Instances/Abstraction.lean b/Nominal/Instances/Abstraction.lean index bb654ed..b4a6cee 100644 --- a/Nominal/Instances/Abstraction.lean +++ b/Nominal/Instances/Abstraction.lean @@ -207,8 +207,7 @@ private lemma alpha_eq_trans {x y z : NameAbstraction' 𝔸 X} : AlphaEq x y → · intro c ⟨hxy, hyz⟩ rw [hxy, hyz] -/-- Alpha-equivalence is an equivariant relation. -/ -lemma alpha_eq_equivariant : EquivariantRelation 𝔸 (AlphaEq : NameAbstraction' 𝔸 X → NameAbstraction' 𝔸 X → Prop) := by +private lemma alpha_eq_equivariant : EquivariantRelation 𝔸 (AlphaEq : NameAbstraction' 𝔸 X → NameAbstraction' 𝔸 X → Prop) := by intro x y π h rw [alpha_eq_iff_exists] at * obtain ⟨c, ⟨hcx, ⟨hcy, hc⟩⟩⟩ := h @@ -236,20 +235,40 @@ section Quotient variable (X : Type) [NominalSet 𝔸 X] /-- Associate the name abstraction structure with alpha-equivalence. -/ -instance NameAbstraction.setoid : Setoid (NameAbstraction' 𝔸 X) where +instance NameAbstraction.setoid : EquivariantSetoid 𝔸 (NameAbstraction' 𝔸 X) where r := AlphaEq iseqv := ⟨alpha_eq_refl, alpha_eq_symm, alpha_eq_trans⟩ + equivariant := alpha_eq_equivariant /-- Define name abstractions as the quotient set (𝔸 × X)/≈. -/ -def NameAbstraction := Quotient (NameAbstraction.setoid 𝔸 X) +def NameAbstraction := Quotient (NameAbstraction.setoid 𝔸 X).toSetoid /-- The equivalence class of a name abstraction (a, x), often written `⟪a⟫ x` -/ def NameAbstraction.mk {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] {X : Type} [NominalSet 𝔸 X] (a : 𝔸) (x : X) : NameAbstraction 𝔸 X := - Quotient.mk (setoid 𝔸 X) (.mk a 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. -/ notation "⟪" a "⟫ " t => NameAbstraction.mk a t +instance : NominalSet 𝔸 (NameAbstraction 𝔸 X) := Quotient.instNominalSet 𝔸 + +@[simp] +lemma NameAbstraction.smul {π : FPerm 𝔸} {a : 𝔸} {x : X } : π • (⟪a⟫ x) = ⟪π • a⟫ π • x := by congr + +@[simp] +lemma NameAbstraction.supp {a : 𝔸} {x : X} : NominalSet.supp 𝔸 (⟪a⟫ x) = NominalSet.supp 𝔸 x \ {a} := by + sorry + -- ext b; constructor + -- · apply NominalSet.support_subset_supp 𝔸 + -- · intro π hπ + -- simp [PermSet.fix'] + + -- sorry + -- · exact Set.Finite.diff (NominalSet.supp_finite 𝔸) + -- · rw [mk, Quotient.supp] + -- intro hb x' hx' + -- sorry + end Quotient /-! |