prove supp of preterms

3 files changed, 94 insertions, 33 deletions

diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean
index 7087076..4ba580d 100644
--- a/Nominal/Equivariance.lean
+++ b/Nominal/Equivariance.lean
@@ -77,6 +77,12 @@ lemma comp_equivariant {f : Y → Z} {g : X → Y} : Function.Equivariant 𝔸 f
     f (g (π • x)) = f (π • g x)   := by rw [hg]
     _             = π • (f (g x)) := by rw [hf]
 
+/-- If a function is equivariant, its inverse is also equivariant. -/
+lemma Function.inv_equivariant {f : X → Y} {inv : Y → X} : Function.LeftInverse inv f → Function.RightInverse inv f → Function.Equivariant 𝔸 f → Function.Equivariant 𝔸 inv := by
+  intro hleft hright hequi y π
+  apply hleft.injective
+  rw [hequi, hright, hright]
+
 /-- The subset relation is equivariant. -/
 lemma Set.subset_equivariant : Rel.Equivariant 𝔸 (Set.Subset : Set X → Set X → Prop) := by
   intro S T π hST x hx
@@ -332,3 +338,36 @@ class EquivariantSetoid (X : Type) [PermSet 𝔸 X] extends Setoid X where
   equivariant : Rel.Equivariant 𝔸 r
 
 end BundledFunction
+
+/-!
+## Equivalences
+
+If two types are equivalent and the conversion function is also equivariant, we know some additional information about nominal set structures.
+-/
+section Equivalence
+
+/-- An equivalence where the function is equivariant. -/
+structure EquivariantEquiv (X Y : Type) [PermSet 𝔸 X] [PermSet 𝔸 Y] extends Equiv X Y where
+  toFun_equivariant : Function.Equivariant 𝔸 toFun
+  invFun_equivariant : Function.Equivariant 𝔸 invFun := Function.inv_equivariant 𝔸 left_inv right_inv toFun_equivariant
+
+def Equivariant.Equiv.symm {𝔸 X Y : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] [PermSet 𝔸 X] [PermSet 𝔸 Y] (equiv : EquivariantEquiv 𝔸 X Y) : EquivariantEquiv 𝔸 Y X :=
+  { toFun := equiv.invFun
+    invFun := equiv.toFun
+    toFun_equivariant := equiv.invFun_equivariant
+    left_inv := equiv.right_inv
+    right_inv := equiv.left_inv
+  }
+
+/-- If an (FPerm 𝔸)-Set is equivalent to a nominal set, it is also a nominal set. -/
+def NominalSet.fromEquivariantEquiv {X Y : Type} [PermSet 𝔸 X] [NominalSet 𝔸 Y] (equiv : EquivariantEquiv 𝔸 X Y) : NominalSet 𝔸 X :=
+  NominalSet.fromEquivariantSurjective 𝔸 equiv.invFun equiv.invFun_equivariant equiv.symm.surjective
+
+/-- If two nominal sets are equivalent, the corresponding least supports are equal. -/
+lemma EquivariantEquiv.supp_eq {X Y : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y] (equiv : EquivariantEquiv 𝔸 X Y) (x : X) : NominalSet.supp 𝔸 x = NominalSet.supp 𝔸 (equiv.toFun x) := by
+  symm
+  apply Function.Equivariant.supp_eq_if_inj
+  · exact equiv.toFun_equivariant
+  · exact equiv.injective
+
+end Equivalence
diff --git a/Nominal/Instances/Abstraction.lean b/Nominal/Instances/Abstraction.lean
index ba2fbf9..052f604 100644
--- a/Nominal/Instances/Abstraction.lean
+++ b/Nominal/Instances/Abstraction.lean
@@ -46,31 +46,19 @@ instance : PermSet 𝔸 (NameAbstraction' 𝔸 X) where
   one_smul := by intro _; ext <;> simp [one_smul]
   mul_smul := by intro _ _ _; ext <;> simp [mul_smul]
 
-private def ofPair (x : (𝔸 × X)) : NameAbstraction' 𝔸 X := ⟨x.fst, x.snd⟩
-
-private lemma ofPair_injective : Function.Injective (ofPair 𝔸 X) := by
-  intro x y hxy
-  simp only [ofPair, mk.injEq] at hxy
-  ext
-  · exact hxy.left
-  · exact hxy.right
-
-private lemma ofPair_surjective : Function.Surjective (ofPair 𝔸 X) := by
-  intro x
-  use ⟨x.atom, x.body⟩
-  simp [ofPair]
-
-private lemma ofPair_equivariant : Function.Equivariant 𝔸 (ofPair 𝔸 X) := by
-  intro x π
-  ext <;> simp [ofPair]
+private def equiv : EquivariantEquiv 𝔸 (NameAbstraction' 𝔸 X) (𝔸 × X) :=
+  { toFun x := ⟨x.atom, x.body⟩
+    invFun x := ⟨x.fst, x.snd⟩
+    toFun_equivariant := by intro x π; ext <;> simp
+  }
 
 instance : NominalSet 𝔸 (NameAbstraction' 𝔸 X) :=
-  NominalSet.fromEquivariantSurjective 𝔸 (ofPair 𝔸 X) (ofPair_equivariant 𝔸 X) (ofPair_surjective 𝔸 X)
+  NominalSet.fromEquivariantEquiv 𝔸 (equiv 𝔸 X)
 
 @[simp] lemma supp {x : NameAbstraction' 𝔸 X} : NominalSet.supp 𝔸 x = NominalSet.supp 𝔸 x.body ∪ {x.atom} := by
-  have h : NominalSet.supp 𝔸 (ofPair 𝔸 X (x.atom, x.body)) = NominalSet.supp 𝔸 (x.atom, x.body) :=
-    Function.Equivariant.supp_eq_if_inj 𝔸 (ofPair_equivariant 𝔸 X) (ofPair_injective 𝔸 X)
-  simp only [Prod.supp, NominalSet.supp_atom, ofPair] at h
+  have h : NominalSet.supp 𝔸 x = NominalSet.supp 𝔸 (x.atom, x.body) :=
+    EquivariantEquiv.supp_eq 𝔸 (equiv 𝔸 X) x
+  simp only [Prod.supp, NominalSet.supp_atom] at h
   rwa [Set.union_comm] at h
 
 @[simp] lemma fresh {a : 𝔸} {x : NameAbstraction' 𝔸 X} : a # x ↔ a ≠ x.atom ∧ a # x.body := by
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