diff options
Diffstat (limited to 'Nominal/Instances')
| -rw-r--r-- | Nominal/Instances/Abstraction.lean | 12 | ||||
| -rw-r--r-- | Nominal/Instances/Basic.lean | 10 |
2 files changed, 10 insertions, 12 deletions
diff --git a/Nominal/Instances/Abstraction.lean b/Nominal/Instances/Abstraction.lean index e03d67a..f1a711b 100644 --- a/Nominal/Instances/Abstraction.lean +++ b/Nominal/Instances/Abstraction.lean @@ -225,16 +225,12 @@ instance NameAbstraction.setoid_equivariant : Rel.Equivariant ๐ธ (setoid ๐ธ instAlphaEqEquivariant /-- Define name abstractions as the quotient set (๐ธ ร X)/โ. -/ -def NameAbstraction := Quotient (NameAbstraction.setoid ๐ธ X) +abbrev 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) (.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 +notation "โช" a "โซ " x:60 => (โฆโจa, xโฉโง : NameAbstraction _ _) instance : NominalSet ๐ธ (NameAbstraction ๐ธ X) := Quotient.instNominalSet ๐ธ @@ -390,13 +386,13 @@ private lemma map_id : map ๐ธ (EquivariantMap.id ๐ธ : X โโ[๐ธ] X) = Eq suffices โ (x : NameAbstraction ๐ธ X), map' ๐ธ (EquivariantMap.id ๐ธ) x = x by ext x; exact this x apply Quotient.ind intro x - simp [map', NameAbstraction.mk] + simp [map'] private lemma map_comp (f : Y โโ[๐ธ] Z) (g : X โโ[๐ธ] Y) : map ๐ธ (EquivariantMap.comp ๐ธ f g) = EquivariantMap.comp ๐ธ (map ๐ธ f) (map ๐ธ g) := by suffices โ (x : NameAbstraction ๐ธ X), map' ๐ธ (EquivariantMap.comp ๐ธ f g) x = (map' ๐ธ f) ((map' ๐ธ g) x) by ext x; exact this x apply Quotient.ind intro x - simp [map', NameAbstraction.mk] + simp [map'] /-- Name abstractions form a functor `Nom โฅค Nom`. -/ def Functor : Nom ๐ธ โฅค Nom ๐ธ := diff --git a/Nominal/Instances/Basic.lean b/Nominal/Instances/Basic.lean index b627c1b..7a88eeb 100644 --- a/Nominal/Instances/Basic.lean +++ b/Nominal/Instances/Basic.lean @@ -59,6 +59,7 @@ Every set can be made into a discrete nominal set, where supp x = โ
. -/ section Discrete +@[reducible] def NominalSet.mkDiscrete (X : Type) : NominalSet.Discrete ๐ธ X where smul ฯ x := x one_smul := by intro; rfl @@ -330,6 +331,7 @@ instance : PermSet ๐ธ (Quotient setoid) where instance instMkEquivariant : Function.Equivariant ๐ธ (Quotient.mk setoid) := by constructor; simp +@[reducible] def lift_equivariant {Y : Type} [PermSet ๐ธ Y] (f : X โ Y) [Function.Equivariant ๐ธ f] (h : โ (a b : X), a โ b โ f a = f b) : @@ -392,11 +394,11 @@ instance : PermSet ๐ธ S where rw [โ Set.equivariant ๐ธ S] exact x.propโฉ one_smul x := by - apply Subtype.eq + apply Subtype.ext exact MulAction.one_smul x.val mul_smul ฯ ฯ x := by - apply Subtype.eq - exact MulAction.mul_smul ฯ ฯ x.val + apply Subtype.ext + exact SemigroupAction.mul_smul ฯ ฯ x.val @[simp] lemma smul_val (ฯ : FPerm ๐ธ) (x : S) : (ฯ โข x).val = ฯ โข x.val := rfl @@ -410,7 +412,7 @@ instance : NominalSet ๐ธ S where use NominalSet.supp ๐ธ x.val constructor ยท intro ฯ hฯ - apply Subtype.eq + apply Subtype.ext exact NominalSet.supp_is_support ๐ธ hฯ ยท exact NominalSet.supp_finite ๐ธ |