diff options
| -rw-r--r-- | Nominal/Equivariance.lean | 39 | ||||
| -rw-r--r-- | Nominal/Instances/Abstraction.lean | 30 | ||||
| -rw-r--r-- | Nominal/LambdaCalculus/Preterms.lean | 58 |
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 |