minor cleanup

4 files changed, 67 insertions, 15 deletions

diff --git a/Nominal/Helpers/CountableString.lean b/Nominal/Helpers/CountableString.lean
index 7d94516..b6f59f8 100644
--- a/Nominal/Helpers/CountableString.lean
+++ b/Nominal/Helpers/CountableString.lean
@@ -2,7 +2,7 @@ import Mathlib
 
 instance : Countable Char where
   exists_injective_nat' := by
-    exists Char.toNat
+    use Char.toNat
     intro c₁ c₂ hc
     rw [Char.toNat, Char.toNat, UInt32.toNat_inj] at hc
     exact Char.eq_of_val_eq hc
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) :=
diff --git a/Nominal/LambdaCalculus/Terms.lean b/Nominal/LambdaCalculus/Terms.lean
index 5362e04..be0d77d 100644
--- a/Nominal/LambdaCalculus/Terms.lean
+++ b/Nominal/LambdaCalculus/Terms.lean
@@ -43,8 +43,8 @@ instance Preterm.setoid : EquivariantSetoid Var Preterm where
     · exact AlphaEq.refl
     · exact AlphaEq.symm a_ih
     · exact AlphaEq.trans a_ih a_ih_1
-    · rw [Preterm.smul_abs]; exact AlphaEq.cong_abs a_ih
-    · rw [Preterm.smul_app]; exact AlphaEq.cong_app a_ih a_ih_1
+    · exact AlphaEq.cong_abs a_ih
+    · exact AlphaEq.cong_app a_ih a_ih_1
     · simp only [Preterm.smul_abs]
       rw [← mul_smul, FPerm.mul_swap_eq_swap_mul, mul_smul]
       apply AlphaEq.rename
@@ -57,7 +57,7 @@ def Term := Quotient Preterm.setoid.toSetoid
 namespace Term
 
 /-- The equivalence class of a λ-preterm. -/
-def mk : Preterm → Term := Quotient.mk Preterm.setoid.toSetoid
+abbrev mk : Preterm → Term := Quotient.mk Preterm.setoid.toSetoid
 
 instance : NominalSet Var Term := Quotient.instNominalSet Var
 
@@ -67,7 +67,7 @@ lemma smul {π : FPerm Var} {t : Preterm} : π • Term.mk t = Term.mk (π • t
 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
-  rw [mk, Quotient.eq_iff_equiv]
+  rw [Quotient.eq_iff_equiv]
 
 def var : Var → Term := fun x => mk (.var x)
 
@@ -226,7 +226,7 @@ lemma alpha_eq_var {x y : Var} : Preterm.var x ≈ Preterm.var y ↔ x = y := by
 
 @[inherit_doc alpha_eq_var]
 lemma eq_var {x y : Var} : Term.var x = Term.var y ↔ x = y := by
-  rw [var, var, mk, Quotient.eq_iff_equiv, alpha_eq_var]
+  rw [var, var, Quotient.eq_iff_equiv, alpha_eq_var]
 
 /-- Alternative characterization of α-equivalence for abstraction preterms. -/
 lemma alpha_eq_abs {x y : Var} {t u : Preterm} : Preterm.abs x t ≈ Preterm.abs y u ↔ ⟪x⟫ (⟦t⟧ : Term) = ⟪y⟫ (⟦u⟧ : Term) := by
@@ -239,7 +239,7 @@ lemma alpha_eq_abs {x y : Var} {t u : Preterm} : Preterm.abs x t ≈ Preterm.abs
 lemma eq_abs {x y : Var} {t u : Term} : Term.abs x t = Term.abs y u ↔ ⟪x⟫ t = ⟪y⟫ u := by
   obtain ⟨t', ht'⟩ := t.exists_rep
   obtain ⟨u', hu'⟩ := u.exists_rep
-  simp only [abs, mk, ← ht', Quotient.lift_mk, ← hu']
+  simp only [abs, ← ht', Quotient.lift_mk, ← hu']
   rw [Quotient.eq_iff_equiv, alpha_eq_abs]
 
 /-- Alternative characterization of α-equivalence for application preterms. -/
@@ -255,9 +255,35 @@ lemma eq_app {t₁ t₂ u₁ u₂ : Term} : Term.app t₁ t₂ = Term.app u₁ u
   obtain ⟨t₂', ht₂'⟩ := t₂.exists_rep
   obtain ⟨u₁', hu₁'⟩ := u₁.exists_rep
   obtain ⟨u₂', hu₂'⟩ := u₂.exists_rep
-  simp only [app, mk, ← ht₁', ← ht₂', Quotient.lift_mk, ← hu₁', ← hu₂']
+  simp only [app, ← ht₁', ← ht₂', Quotient.lift_mk, ← hu₁', ← hu₂']
   rw [Quotient.eq_iff_equiv, Quotient.eq_iff_equiv, Quotient.eq_iff_equiv, alpha_eq_app]
 
+end Term
+
+end AlphaEquivalence
+
+/-!
+## Nominal Set Instance
+
+Since they are a quotient type modulo an equivariant equivalence, the set of terms forms a nominal
+set. We show that renaming corresponds to renaming in the underlying preterms and that the support
+are exactly the free variables in a term (a notion thus well-defined for terms).
+-/
+section NominalSet
+
+namespace Term
+
+@[simp] lemma smul_var {π : FPerm Var} {x : Var} : π • var x = var (π • x) := rfl
+
+@[simp] lemma smul_abs {π : FPerm Var} {x : Var} {t : Term} : π • abs x t = abs (π • x) (π • t) := by
+  obtain ⟨t', ht'⟩ := t.exists_rep
+  simp [← ht']
+
+@[simp] lemma smul_app {π : FPerm Var} {t u : Term} : π • app t u = app (π • t) (π • u) := by
+  obtain ⟨t', ht'⟩ := t.exists_rep
+  obtain ⟨u', hu'⟩ := u.exists_rep
+  simp [← ht', ← hu']
+
 private def equiv : EquivariantEquiv Var Term (Var ⊕ (NameAbstraction Var Term) ⊕ (Term × Term)) :=
   { toFun t := Quotient.liftOn t
       (fun t => match t with
@@ -289,12 +315,12 @@ private def equiv : EquivariantEquiv Var Term (Var ⊕ (NameAbstraction Var Term
         | inl x =>
           obtain ⟨x', hx'⟩ := x.exists_rep
           obtain ⟨body, hbody⟩ := x'.body.exists_rep
-          simp only [← hx', abs, mk, Quotient.lift_mk, ← hbody, Sum.inr.injEq, Sum.inl.injEq]
-          rw [hbody]; rfl
+          simp only [← hx', abs, Quotient.lift_mk, ← hbody, Sum.inr.injEq, Sum.inl.injEq]
+          rw [hbody]
         | inr x =>
           obtain ⟨x', hx'⟩ := x.fst.exists_rep
           obtain ⟨y', hy'⟩ := x.snd.exists_rep
-          simp only [app, mk, ← hx', ← hy', Quotient.lift_mk, Sum.inr.injEq]
+          simp only [app, ← hx', ← hy', Quotient.lift_mk, Sum.inr.injEq]
           rw [hx', hy']
     toFun_equivariant := by
       intro t π
@@ -312,10 +338,29 @@ private lemma supp' (t : Preterm) : NominalSet.supp Var (⟦t⟧ : Term) = t.fv
     rw [EquivariantEquiv.supp_eq Var equiv]
     simp [Preterm.fv, *]
 
+/-- Free variables are preserved under α-equivalence. -/
 def fv : Term → Set Var := Quotient.lift Preterm.fv (by
   intro t u htu
   rw [← supp', ← supp', Quotient.sound htu])
 
+@[simp] lemma fv_preterm {t : Preterm} : fv ⟦t⟧ = t.fv := rfl
+
+@[simp] lemma fv_var {x : Var} : fv (var x) = {x} := rfl
+
+@[simp] lemma fv_abs {x : Var} {t : Term} : fv (abs x t) = fv t \ {x} := by
+  obtain ⟨t', ht'⟩ := t.exists_rep
+  simp [← ht', Preterm.fv]
+
+@[simp] lemma fv_app {t : Term} {u : Term} : fv (app t u) = fv t ∪ fv u := by
+  obtain ⟨t', ht'⟩ := t.exists_rep
+  obtain ⟨u', hu'⟩ := u.exists_rep
+  simp [← ht', ← hu', Preterm.fv]
+
+/-- The lifted fv function is also equivariant.-/
+lemma fv_equivariant : Function.Equivariant Var fv :=
+  Quotient.lift_equivariant Var _ _ Preterm.fv_equivariant
+
+/-- The support of a term consists exactly of the free variables in it. -/
 lemma supp : NominalSet.supp Var = fv := by
   apply funext
   apply Quotient.ind
@@ -324,6 +369,6 @@ lemma supp : NominalSet.supp Var = fv := by
 
 end Term
 
-end AlphaEquivalence
+end NominalSet
 
 end Lambda