1 files changed, 46 insertions, 3 deletions
diff --git a/Nominal/LambdaCalculus/Preterms.lean b/Nominal/LambdaCalculus/Preterms.lean
index eeb1d29..74f7397 100644
--- a/Nominal/LambdaCalculus/Preterms.lean
+++ b/Nominal/LambdaCalculus/Preterms.lean
@@ -9,6 +9,8 @@ import Nominal.Helpers.CountableString
 # λ-Preterms
 
 As a practical example for nominal sets, this file defines λ-preterms (that is, λ-terms without α-equivalence).
+
+For any preterm t, supp t is exactly the set of variables occurring in t (either bound or free).
 -/
 
 namespace Lambda
@@ -36,11 +38,17 @@ inductive Preterm
   deriving DecidableEq
 
 /-- The set of variables mentioned by a preterm. -/
-def vars : Preterm → Set Var
+def Preterm.vars : Preterm → Set Var
   | .var x => {x}
   | .abs x t => {x} ∪ vars t
   | .app t u => vars t ∪ vars u
 
+/-- The set of free variables in a preterm. -/
+def Preterm.fv : Preterm → Set Var
+  | .var x => {x}
+  | .abs x t => fv t \ {x}
+  | .app t u => fv t ∪ fv u
+
 open Lean Elab Meta
 
 declare_syntax_cat lam
@@ -142,8 +150,7 @@ private def equiv : EquivariantEquiv Var Preterm (Var ⊕ (Var × Preterm) ⊕ (
 @[simp] lemma equiv_app {t u : Preterm} : equiv.toFun (Preterm.app t u) = .inr (.inr (t, u)) := rfl
 
 /-- The support of a preterm consists exactly of the variables mentioned by it. -/
-lemma supp : NominalSet.supp Var = vars := by
-  funext x
+lemma supp {t : Preterm} : NominalSet.supp Var t = vars t := by
   fun_induction vars
   all_goals rw [EquivariantEquiv.supp_eq Var equiv]; simp [*]
 
@@ -151,4 +158,40 @@ end Preterm
 
 end NominalSet
 
+/-!
+## Variables
+
+Helpers for reasoning about variables in a preterm.
+-/
+section Variables
+
+namespace Preterm
+
+/-- The free variables are a subset of all variables in a preterm. -/
+lemma fv_subset_vars (t : Preterm) : t.fv ⊆ t.vars := by
+  induction' t <;> all_goals grind [Preterm.vars, Preterm.fv]
+
+/-- The set of variables in a preterm is finite. -/
+lemma vars_finite (t : Preterm) : t.vars.Finite := by
+  rw [← Preterm.supp]
+  exact NominalSet.supp_finite Var
+
+/-- The set of free variables in a preterm is finite. -/
+lemma fv_finite (t : Preterm) : t.fv.Finite := by
+  apply Set.Finite.subset (vars_finite t) (fv_subset_vars t)
+
+/-- The vars map is equivariant. -/
+lemma vars_equivariant : Function.Equivariant Var vars := by
+  intro t π
+  fun_induction vars <;> all_goals simp [vars, *, Set.smul_set_insert, Set.smul_set_union]
+
+/-- The fv map is equivariant. -/
+lemma fv_equivariant : Function.Equivariant Var fv := by
+  intro t π
+  fun_induction fv <;> all_goals simp [fv, *, Set.smul_set_sdiff, Set.smul_set_union]
+
+end Preterm
+
+end Variables
+
 end Lambda