prove supp of preterms

1 files changed, 46 insertions, 12 deletions

diff --git a/Nominal/LambdaCalculus/Preterms.lean b/Nominal/LambdaCalculus/Preterms.lean
index c486a7e..eeb1d29 100644
--- a/Nominal/LambdaCalculus/Preterms.lean
+++ b/Nominal/LambdaCalculus/Preterms.lean
@@ -1,6 +1,8 @@
 import Mathlib
 import Nominal.Permutations
 import Nominal.Support
+import Nominal.Equivariance
+import Nominal.Instances.Basic
 import Nominal.Helpers.CountableString
 
 /-!
@@ -33,6 +35,12 @@ inductive Preterm
   | app : Preterm → Preterm → Preterm
   deriving DecidableEq
 
+/-- The set of variables mentioned by a preterm. -/
+def vars : Preterm → Set Var
+  | .var x => {x}
+  | .abs x t => {x} ∪ vars t
+  | .app t u => vars t ∪ vars u
+
 open Lean Elab Meta
 
 declare_syntax_cat lam
@@ -86,32 +94,58 @@ instance : PermSet Var Preterm where
 @[simp] lemma smul_abs {π : FPerm Var} {x : Var} {t : Preterm} : π • Preterm.abs x t = Preterm.abs (π • x) (π • t) := rfl
 @[simp] lemma smul_app {π : FPerm Var} {t u : Preterm} : π • Preterm.app t u = Preterm.app (π • t) (π • u) := rfl
 
-private def aSupport : Preterm → Set Var
-  | .var x => {x}
-  | .abs x t => {x} ∪ aSupport t
-  | .app t u => aSupport t ∪ aSupport u
-
 instance : NominalSet Var Preterm where
   fin_supp t := by
-    use aSupport t
+    use vars t
     induction' t <;> all_goals expose_names
     · constructor
-      · simp [PermSet.HasSupport, PermSet.fix, aSupport, PermSet.fix']
-      · simp [aSupport]
+      · simp [PermSet.HasSupport, PermSet.fix, vars, PermSet.fix']
+      · simp [vars]
     · constructor
       · intro π hπ
         simp only [PermSet.fix', smul_abs, Preterm.abs.injEq, Set.mem_setOf_eq]
-        simp only [PermSet.fix, aSupport, Set.singleton_union, Set.mem_insert_iff, forall_eq_or_imp, Set.mem_setOf_eq] at hπ
+        simp only [PermSet.fix, vars, Set.singleton_union, Set.mem_insert_iff, forall_eq_or_imp, Set.mem_setOf_eq] at hπ
         exact ⟨hπ.left, a_ih.left hπ.right⟩
-      · simp [aSupport, Set.Finite.insert, a_ih]
+      · simp [vars, Set.Finite.insert, a_ih]
     · constructor
       · intro π hπ
         simp only [PermSet.fix', smul_app, Preterm.app.injEq, Set.mem_setOf_eq]
-        simp only [PermSet.fix, aSupport, Set.mem_union, Set.mem_setOf_eq] at hπ
+        simp only [PermSet.fix, vars, Set.mem_union, Set.mem_setOf_eq] at hπ
         constructor
         · exact a_ih.left (fun x hx => hπ x (Or.inl hx))
         · exact a_ih_1.left (fun x hx => hπ x (Or.inr hx))
-      · simp [aSupport, a_ih, a_ih_1]
+      · simp [vars, a_ih, a_ih_1]
+
+/-- It's easiest to prove the least support via an equivalence between preterms and a well-known nominal type. -/
+private def equiv : EquivariantEquiv Var Preterm (Var ⊕ (Var × Preterm) ⊕ (Preterm × Preterm)) :=
+  { toFun
+      | .var x => .inl x
+      | .abs x t => .inr (.inl ⟨x, t⟩)
+      | .app t u => .inr (.inr ⟨t, u⟩)
+    invFun
+      | .inl x => .var x
+      | .inr (.inl x) => .abs x.fst x.snd
+      | .inr (.inr x) => .app x.fst x.snd
+    left_inv := by intro x; cases x <;> all_goals simp
+    right_inv := by
+      intro x
+      cases x with
+      | inl _ => simp
+      | inr x' => cases x' <;> all_goals simp
+    toFun_equivariant := by
+      intro t π
+      cases t <;> all_goals simp
+  }
+
+@[simp] lemma equiv_var {x : Var} : equiv.toFun (Preterm.var x) = .inl x := rfl
+@[simp] lemma equiv_abs {x : Var} {t : Preterm} : equiv.toFun (Preterm.abs x t) = .inr (.inl (x, t)) := rfl
+@[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
+  fun_induction vars
+  all_goals rw [EquivariantEquiv.supp_eq Var equiv]; simp [*]
 
 end Preterm