update lean

7 files changed, 32 insertions, 35 deletions

diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean
index 2682a55..e9bd850 100644
--- a/Nominal/Equivariance.lean
+++ b/Nominal/Equivariance.lean
@@ -25,7 +25,7 @@ class inductive Function.Equivariant (f : X → Y) : Prop
 
 lemma Function.equivariant (f : X → Y) [Equivariant 𝔸 f] :
     ∀ (x : X) (π : FPerm 𝔸), f (π • x) = π • f x := by
-  cases (inferInstanceAs (Equivariant 𝔸 f)); assumption
+  cases (inferInstance : Equivariant 𝔸 f); assumption
 
 /-- A set is equivariant if it is closed under permutations. -/
 class inductive Set.Equivariant (S : Set X) : Prop
@@ -34,7 +34,7 @@ class inductive Set.Equivariant (S : Set X) : Prop
 /-- For equivariant sets, we even have "if and only if". -/
 lemma Set.equivariant (S : Set X) [Equivariant 𝔸 S] :
     ∀ (x : X) (π : FPerm 𝔸), x ∈ S ↔ π • x ∈ S := by
-  cases (inferInstanceAs (Equivariant 𝔸 S)); rename_i h
+  cases (inferInstance : Equivariant 𝔸 S); rename_i h
   intro x π; constructor
   · intro hx; exact h x π hx
   · intro hx
@@ -49,7 +49,7 @@ class inductive Rel.Equivariant (R : Rel X Y) : Prop
 /-- For equivariant relations, we even have "if and only if". -/
 lemma Rel.equivariant (R : Rel X Y) [Rel.Equivariant 𝔸 R] :
     ∀ (x : X) (y : Y) (π : FPerm 𝔸), R x y ↔ R (π • x) (π • y) := by
-  cases (inferInstanceAs (Equivariant 𝔸 R)); rename_i h
+  cases (inferInstance : Equivariant 𝔸 R); rename_i h
   intro x y π; constructor
   · intro hxy; exact h x y π hxy
   · intro hxy
@@ -83,6 +83,7 @@ instance Function.Equivariant.comp
     _             = π • (f (g x)) := by rw [← Function.equivariant 𝔸 f]
 
 /-- If a function is equivariant, its inverse is also equivariant. -/
+@[reducible]
 def Function.Equivariant.inv
     {f : X → Y} [Function.Equivariant 𝔸 f] {inv : Y → X}
     (hleft : Function.LeftInverse inv f)
@@ -191,6 +192,7 @@ lemma preserve_fresh_inj {a : 𝔸} {x : X} {f : X → Y} [Equivariant 𝔸 f] :
 end Function.Equivariant
 
 /-- If there is an equivariant surjection from a nominal set into an (FPerm 𝔸)-Set, then that set is nominal. -/
+@[reducible]
 def NominalSet.ofEquivariantSurjective
     {X Y : Type} [NominalSet 𝔸 X] [PermSet 𝔸 Y]
     (f : X → Y) [Function.Equivariant 𝔸 f] (hsurj : Function.Surjective f) :
@@ -385,6 +387,7 @@ instance EquivariantEquiv.invFunEquivariant
   equiv.invFun_equivariant
 
 /-- If an (FPerm 𝔸)-Set is equivalent to a nominal set, it is also a nominal set. -/
+@[reducible]
 def NominalSet.ofEquivariantEquiv {X Y : Type} [PermSet 𝔸 X] [NominalSet 𝔸 Y] (equiv : EquivariantEquiv 𝔸 X Y) : NominalSet 𝔸 X :=
   NominalSet.ofEquivariantSurjective 𝔸 equiv.invFun equiv.symm.surjective
 
diff --git a/Nominal/Helpers/CountableString.lean b/Nominal/Helpers/CountableString.lean
index b6f59f8..c887f96 100644
--- a/Nominal/Helpers/CountableString.lean
+++ b/Nominal/Helpers/CountableString.lean
@@ -5,10 +5,10 @@ instance : Countable Char where
     use Char.toNat
     intro c₁ c₂ hc
     rw [Char.toNat, Char.toNat, UInt32.toNat_inj] at hc
-    exact Char.eq_of_val_eq hc
+    exact Char.ext hc
 
 instance : Countable String := Countable.of_equiv (List Char)
-  { toFun := String.mk
-    invFun := String.data
+  { toFun := String.ofList
+    invFun := String.toList
     left_inv x := by simp
     right_inv x := by simp }
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 𝔸
 
diff --git a/Nominal/LambdaCalculus/Terms.lean b/Nominal/LambdaCalculus/Terms.lean
index 91f4fb8..7af82cd 100644
--- a/Nominal/LambdaCalculus/Terms.lean
+++ b/Nominal/LambdaCalculus/Terms.lean
@@ -53,40 +53,37 @@ instance Preterm.instSetoidEquivariant : Rel.Equivariant Var setoid.r := by
     exact h
 
 /-- Define λ-terms as the quotient Preterm/≈. -/
-def Term := Quotient Preterm.setoid
+abbrev Term := Quotient Preterm.setoid
 
 namespace Term
 
-/-- The equivalence class of a λ-preterm. -/
-abbrev mk : Preterm → Term := Quotient.mk Preterm.setoid
-
 instance : NominalSet Var Term := Quotient.instNominalSet Var
 
 @[simp]
-lemma smul {π : FPerm Var} {t : Preterm} : π • Term.mk t = Term.mk (π • t) := by congr
+lemma smul {π : FPerm Var} {t : Preterm} : π • (⟦t⟧ : Term) = ⟦π • t⟧ := by congr
 
 private lemma alpha_eq {t u : Preterm} : t ≈ u ↔ AlphaEq t u := by rfl
 
-lemma eq_iff_alpha_eq {t u : Preterm} : mk t = mk u ↔ t ≈ u := by
+lemma eq_iff_alpha_eq {t u : Preterm} : (⟦t⟧ : Term) = (⟦u⟧ : Term) ↔ t ≈ u := by
   rw [Quotient.eq_iff_equiv]
 
-def var : Var → Term := fun x => mk (.var x)
+def var : Var → Term := fun x => ⟦.var x⟧
 
 def abs : Var → Term → Term := fun x =>
   Quotient.lift
-    (fun t => mk (.abs x t))
+    (fun t => ⟦.abs x t⟧)
     (by intro t t'; rw [eq_iff_alpha_eq]; exact AlphaEq.cong_abs)
 
 def app : Term → Term → Term :=
   Quotient.lift₂
-    (fun t u => mk (.app t u))
+    (fun t u => ⟦.app t u⟧)
     (by intro t₁ t₂ u₁ u₂; rw [eq_iff_alpha_eq]; exact AlphaEq.cong_app)
 
 @[simp]
-lemma abs_preterm {x : Var} {t : Preterm} : abs x (mk t) = mk (.abs x t) := rfl
+lemma abs_preterm {x : Var} {t : Preterm} : abs x ⟦t⟧ = ⟦.abs x t⟧ := rfl
 
 @[simp]
-lemma app_preterm {t u : Preterm} : app (mk t) (mk u) = mk (.app t u) := rfl
+lemma app_preterm {t u : Preterm} : app ⟦t⟧ ⟦u⟧ = ⟦.app t u⟧ := rfl
 
 /-- Alternative characterization of α-equivalence for each preterm constructor. -/
 inductive AlphaEq' : Preterm → Preterm → Prop where
@@ -242,7 +239,6 @@ lemma eq_abs {x y : Var} {t u : Term} : Term.abs x t = Term.abs y u ↔ ⟪x⟫
   obtain ⟨u', hu'⟩ := u.exists_rep
   simp only [abs, ← ht', Quotient.lift_mk, ← hu']
   rw [Quotient.eq_iff_equiv, alpha_eq_abs]
-  rfl
 
 /-- Alternative characterization of α-equivalence for application preterms. -/
 lemma alpha_eq_app {t₁ t₂ u₁ u₂ : Preterm} : Preterm.app t₁ t₂ ≈ Preterm.app u₁ u₂ ↔ t₁ ≈ u₁ ∧ t₂ ≈ u₂ := by
@@ -295,7 +291,7 @@ private def equiv : EquivariantEquiv Var Term (Var ⊕ (NameAbstraction Var Term
       (by
         intro t u htu
         rw [alpha_eq, alpha_eq_iff] at htu
-        cases htu <;> simp only [Sum.inr.injEq, Sum.inl.injEq, *]; assumption)
+        cases htu <;> simp [*])
     invFun
       | .inl x => .var x
       | .inr (.inl x) => Quotient.liftOn x
diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean
index 0a4974a..f1115d3 100644
--- a/Nominal/Permutations.lean
+++ b/Nominal/Permutations.lean
@@ -42,7 +42,7 @@ lemma supp_one : (1 : Equiv.Perm X).supp = ∅ := by
 
 /-- The support of the inverse function is the same as the function's support. -/
 lemma supp_inv (π : Equiv.Perm X) : π⁻¹.supp = π.supp := by
-  simp [supp, set_support_inv_eq]
+  simp [supp, set_support_symm_eq]
 
 /-- The support of two concatenated permutations is a subset of the individual supports as a union. -/
 lemma supp_mul_subset (π τ : Equiv.Perm X) : (π * τ).supp ⊆ π.supp ∪ τ.supp := by
@@ -199,10 +199,10 @@ instance : PermSet 𝔸 𝔸 where
 
 instance : OrbitFinite 𝔸 𝔸 where
   fin_orbits := Finite.of_equiv Unit
-    { toFun _ := Quotient.mk _ (inferInstanceAs (Nonempty 𝔸)).some
+    { toFun _ := Quotient.mk _ (inferInstance : Nonempty 𝔸).some
       invFun _ := ()
       right_inv := by
-        let chosen := (inferInstanceAs (Nonempty 𝔸)).some
+        let chosen := (inferInstance : Nonempty 𝔸).some
         apply Quotient.ind; intro a
         rw [Quotient.eq]
         show chosen ∈ MulAction.orbit (FPerm 𝔸) a
diff --git a/Nominal/Support.lean b/Nominal/Support.lean
index 7888a68..fde20c7 100644
--- a/Nominal/Support.lean
+++ b/Nominal/Support.lean
@@ -79,7 +79,7 @@ lemma support_inter {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S.Finite
       simp)
   let m' := (S \ T).restrict m
   rw [Set.injOn_iff_injective, show (S \ T).restrict m = m' by rfl] at h_m_injective
-  obtain h_m_inv := Function.partialInv_of_injective h_m_injective
+  obtain h_m_inv := h_m_injective.isPartialInv
   have h_m_image : m '' (S \ T) ⊆ (π'.supp ∪ S ∪ T)ᶜ :=
     Set.image_subset_iff.mpr h_m_preimage