From ea38ef0cb2c57e10696c7fb6108732a6f454818c Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Thu, 20 Nov 2025 11:56:18 +0100 Subject: wip terms --- Nominal/Instances/Basic.lean | 5 + Nominal/LambdaCalculus/Preterms.lean | 49 ++++++- Nominal/LambdaCalculus/Terms.lean | 264 +++++++++++++++++++++++++++++++++++ Nominal/Permutations.lean | 5 + 4 files changed, 320 insertions(+), 3 deletions(-) create mode 100644 Nominal/LambdaCalculus/Terms.lean diff --git a/Nominal/Instances/Basic.lean b/Nominal/Instances/Basic.lean index d41e87f..dea5bcf 100644 --- a/Nominal/Instances/Basic.lean +++ b/Nominal/Instances/Basic.lean @@ -282,6 +282,11 @@ lemma supp {x : X} : NominalSet.supp 𝔸 (Quotient.mk setoid.toSetoid x) = {a | simp only [FPerm.swap_inv, PermSet.atom_swap, Equiv.swap_apply_left] exact hc.right +/-- If an atom is not in the support of the equivalence class, one can always pick a representative where it is not in the least support. -/ +lemma supp_pick_fresh {a : 𝔸} {x : X} : a ∉ NominalSet.supp 𝔸 (Quotient.mk setoid.toSetoid x) → ∃ (y : X), y ≈ x ∧ a ∉ NominalSet.supp 𝔸 y := by + contrapose + simp [not_exists, not_and, not_not, supp] + end Quotient end Quotient 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 diff --git a/Nominal/LambdaCalculus/Terms.lean b/Nominal/LambdaCalculus/Terms.lean new file mode 100644 index 0000000..2118156 --- /dev/null +++ b/Nominal/LambdaCalculus/Terms.lean @@ -0,0 +1,264 @@ +import Mathlib +import Nominal.LambdaCalculus.Preterms +import Nominal.Instances.Basic +import Nominal.Instances.Abstraction +import Nominal.Permutations + +/-! +# λ-Terms + +The set of λ-terms is the quotient of λ-preterms modulo α-equivalence. + +We will show that this set also forms a nominal set and that, for any term t, supp t is exactly the set of free variables in t. +-/ + +namespace Lambda + +/-! +## α-Equivalence + +We will define the notion of α-equivalence between λ-preterms in the usual way. +-/ +section AlphaEquivalence + +/-- +α-equivalence is the congruence generated by + λ x, t ≈ λ y, (x y) t if y ∉ fv(t) +-/ +inductive AlphaEq : Preterm → Preterm → Prop where + | refl {t : Preterm} : AlphaEq t t + | symm {t u : Preterm} : AlphaEq t u → AlphaEq u t + | trans {t u s : Preterm} : AlphaEq t u → AlphaEq u s → AlphaEq t s + | cong_abs {x : Var} {t u : Preterm} : AlphaEq t u → AlphaEq (.abs x t) (.abs x u) + | cong_app {t₁ t₂ u₁ u₂ : Preterm} : AlphaEq t₁ u₁ → AlphaEq t₂ u₂ → AlphaEq (.app t₁ t₂) (.app u₁ u₂) + | rename {x y : Var} {t : Preterm} : y ∉ t.fv → AlphaEq (.abs x t) (.abs y (⸨x, y⸩ • t)) + +/-- By definition, AlphaEq is an equivariant equivalence relation. -/ +instance Preterm.setoid : EquivariantSetoid Var Preterm where + r := AlphaEq + iseqv := ⟨fun x => AlphaEq.refl, AlphaEq.symm, AlphaEq.trans⟩ + equivariant := by + intro t u π htu + induction' htu <;> all_goals expose_names + · 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 + · simp only [Preterm.smul_abs] + rw [← mul_smul, FPerm.mul_swap_eq_swap_mul, mul_smul] + apply AlphaEq.rename + rw [Preterm.fv_equivariant, Set.smul_mem_smul_set_iff] + exact h + +/-- Define λ-terms as the quotient Preterm/≈. -/ +def Term := Quotient Preterm.setoid.toSetoid + +namespace Term + +/-- The equivalence class of a λ-preterm. -/ +def mk : Preterm → Term := Quotient.mk Preterm.setoid.toSetoid + +instance : NominalSet Var Term := Quotient.instNominalSet Var + +@[simp] +lemma smul {π : FPerm Var} {t : Preterm} : π • Term.mk t = Term.mk (π • t) := by congr + +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] + +def var : Var → Term := fun x => mk (.var x) + +def abs : Var → Term → Term := fun x => + Quotient.lift + (fun t => mk (.abs x t)) + (by intro t t'; rw [eq_iff_alpha_eq]; exact AlphaEq.cong_abs) + +def app : Term → Term → Term := + Quotient.lift₂ + (fun t u => mk (.app t u)) + (by intro t₁ t₂ u₁ u₂; rw [eq_iff_alpha_eq]; exact AlphaEq.cong_app) + +@[simp] +lemma abs_preterm {x : Var} {t : Preterm} : abs x (mk t) = mk (.abs x t) := rfl + +@[simp] +lemma app_preterm {t u : Preterm} : app (mk t) (mk u) = mk (.app t u) := rfl + +/-- Alternative characterization of α-equivalence for each preterm constructor. -/ +inductive AlphaEq' : Preterm → Preterm → Prop where + | var {x : Var} : AlphaEq' (.var x) (.var x) + | abs {x y : Var} {t u : Preterm} : ⟪x⟫ (⟦t⟧ : Term) = ⟪y⟫ (⟦u⟧ : Term) → AlphaEq' (.abs x t) (.abs y u) + | app {t₁ t₂ u₁ u₂ : Preterm} : (⟦t₁⟧ : Term) = (⟦u₁⟧ : Term) → (⟦t₂⟧ : Term) = (⟦u₂⟧ : Term) → AlphaEq' (.app t₁ t₂) (.app u₁ u₂) + +namespace AlphaEq' + +lemma refl {t : Preterm} : AlphaEq' t t := by + cases t + · exact var + · exact abs rfl + · exact app rfl rfl + +lemma symm {t u : Preterm} : AlphaEq' t u → AlphaEq' u t := by + intro h + cases h <;> all_goals expose_names + · exact var + · exact abs h.symm + · exact app h.symm h_1.symm + +lemma trans {t u s : Preterm} : AlphaEq' t u → AlphaEq' u s → AlphaEq' t s := by + intro h₁ h₂ + cases h₁ <;> all_goals expose_names + · cases h₂; exact var + · cases h₂; expose_names; exact abs (h.trans h_1) + · cases h₂; expose_names; exact app (h.trans h_2) (h_1.trans h_3) + +end AlphaEq' + +private lemma pick_fresh {t : Preterm} : ∀ x ∉ t.fv, ∃ u, t ≈ u ∧ x ∉ u.vars := by + induction' t <;> all_goals expose_names + · intro x h + use .var a + exact ⟨by rfl, h⟩ + · rw [Preterm.fv] + intro x h + have hinf : ({x} ∪ a_1.vars)ᶜ.Infinite := by + apply Set.Finite.infinite_compl + exact Set.Finite.union (Set.finite_singleton x) (Preterm.vars_finite a_1) + obtain ⟨c, hc⟩ := hinf.nonempty + simp only [Set.singleton_union, Set.mem_compl_iff, Set.mem_insert_iff, not_or] at hc + obtain ⟨u, hu⟩ := a_ih c (fun h => hc.right (Preterm.fv_subset_vars a_1 h)) + use Preterm.abs c (⸨a, c⸩ • u) + simp [Preterm.vars] + constructor + · trans + · exact AlphaEq.cong_abs hu.left + · exact AlphaEq.rename (fun h => hu.right (Preterm.fv_subset_vars u h)) + · sorry + · sorry + +lemma alpha_eq_iff : AlphaEq = AlphaEq' := by + ext t u + constructor + · intro h; induction' h <;> all_goals expose_names + · exact AlphaEq'.refl + · exact AlphaEq'.symm a_ih + · exact AlphaEq'.trans a_ih a_ih_1 + · apply AlphaEq'.abs + rw [← alpha_eq, ← Quotient.eq_iff_equiv] at h + rw [h] + · apply AlphaEq'.app + · rw [← alpha_eq, ← Quotient.eq_iff_equiv] at h + rw [h] + · rw [← alpha_eq, ← Quotient.eq_iff_equiv] at h_1 + rw [h_1] + · obtain ⟨z, ⟨hz₁, hz₂⟩⟩ := pick_fresh y h + apply AlphaEq'.abs + rw [Quotient.mk_equivariant, Quotient.sound hz₁, NameAbstraction.eq_iff_cases] + by_cases hxy : x = y + · left + simp [hxy, FPerm.swap_self, one_smul] + · right + constructor + · exact hxy + · constructor + · rw [← Preterm.supp] at hz₂ + nth_rw 1 [show x = ⸨x, y⸩ • y by simp] + apply NominalSet.fresh_equivariant + exact Function.Equivariant.preserve_fresh Var (Quotient.mk_equivariant Var) hz₂ + · rw [← mul_smul, FPerm.swap_mul_self, one_smul] + · intro h; cases h <;> all_goals expose_names + · exact AlphaEq.refl + · rw [NameAbstraction.eq_iff_cases] at h + cases h with + | inl h => + rw [h.left] + apply AlphaEq.cong_abs + rw [← alpha_eq, ← Quotient.eq_iff_equiv] + exact h.right + | inr h => + obtain ⟨s, ⟨hs₁, hs₂⟩⟩ := Quotient.supp_pick_fresh Var h.right.left + rw [← Quotient.sound hs₁, ← Quotient.mk_equivariant] at h + have hrename : Preterm.abs y s ≈ Preterm.abs x (⸨y, x⸩ • s) := by + apply AlphaEq.rename + rw [Preterm.supp] at hs₂ + exact fun h => hs₂ (Preterm.fv_subset_vars s h) + calc + Preterm.abs x t ≈ Preterm.abs x (⸨x, y⸩ • s) := AlphaEq.cong_abs (eq_iff_alpha_eq.mp h.right.right) + _ ≈ Preterm.abs y s := by rw [FPerm.swap_comm]; symm; exact hrename + _ ≈ Preterm.abs y u := AlphaEq.cong_abs hs₁ + · apply AlphaEq.cong_app + · rw [Quotient.eq_iff_equiv] at h + exact h + · rw [Quotient.eq_iff_equiv] at h_1 + exact h_1 + + +/-- Alternative characterization of α-equivalence for variable preterms. -/ +lemma alpha_eq_var {x y : Var} : Preterm.var x ≈ Preterm.var y ↔ x = y := by + sorry + +@[inherit_doc alpha_eq_var] +lemma eq_var {x y : Var} : Term.var x = Term.var y ↔ x = y := by + sorry + +/-- 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⟫ Term.mk t = ⟪y⟫ Term.mk u := by + sorry + +@[inherit_doc alpha_eq_abs] +lemma eq_abs {x y : Var} {t u : Term} : Term.abs x t = Term.abs y u ↔ ⟪x⟫ t = ⟪y⟫ u := by + sorry + +/-- Alternative characterization of α-equivalence for application preterms. -/ +lemma alpha_eq_app {t₁ t₂ u₁ u₂ : Preterm} : Preterm.app t₁ t₂ ≈ Preterm.app u₁ u₂ ↔ t₁ ≈ u₁ ∧ t₂ ≈ u₂ := by + sorry + +@[inherit_doc alpha_eq_app] +lemma eq_app {t₁ t₂ u₁ u₂ : Term} : Term.app t₁ t₂ = Term.app u₁ u₂ ↔ t₁ = u₁ ∧ t₂ = u₂ := by + sorry + +private def equiv : EquivariantEquiv Var Term (Var ⊕ (NameAbstraction Var Term) ⊕ (Term × Term)) := + { toFun t := Quotient.liftOn t + (fun t => match t with + | .var x => .inl x + | .abs x t' => .inr (.inl (⟪x⟫ Term.mk t')) + | .app t' u' => .inr (.inr ⟨(Term.mk t'), (Term.mk u')⟩)) + (by + intro t u htu + cases htu + sorry) + invFun + | .inl x => .var x + | .inr (.inl x) => Quotient.liftOn x + (fun x => .abs x.atom x.body) + (by sorry) + | .inr (.inr x) => .app x.fst x.snd + left_inv := by sorry + right_inv := by sorry + toFun_equivariant := by sorry + } + +@[simp] private lemma equiv_var {x : Var} : equiv.toFun ⟦.var x⟧ = .inl x := rfl +@[simp] private lemma equiv_abs {x : Var} {t : Preterm} : equiv.toFun ⟦.abs x t⟧ = .inr (.inl (⟪x⟫ ⟦t⟧)) := rfl +@[simp] private lemma equiv_app {t u : Preterm} : equiv.toFun ⟦.app t u⟧ = .inr (.inr (⟦t⟧, ⟦u⟧)) := rfl + +def fv : Term → Set Var := Quotient.lift Preterm.fv + (by sorry) + +lemma supp : NominalSet.supp Var = fv := by + apply funext + apply Quotient.ind + intro t + induction' t; all_goals + expose_names + rw [EquivariantEquiv.supp_eq Var equiv] + simp [fv, Preterm.fv, *] + +end Term + +end AlphaEquivalence + +end Lambda diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean index bc775b9..79a5042 100644 --- a/Nominal/Permutations.lean +++ b/Nominal/Permutations.lean @@ -138,6 +138,11 @@ lemma swap_mul_self {a b : X} : ⸨a, b⸩ * ⸨a, b⸩ = 1 := by apply ext simp [swap] +/-- Lifting of Equiv.swap_self to finite permutations.-/ +lemma swap_self {a : X} : ⸨a, a⸩ = 1 := by + ext + simp [swap] + /-- Lifting of Equiv.swap_comm to finite permutations. -/ lemma swap_comm {a b : X} : ⸨a, b⸩ = ⸨b, a⸩ := by apply ext -- cgit v1.3.1