minor cleanup

1 files changed, 56 insertions, 11 deletions

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