From 71a6a3d5b6f4b428b463bc4a0766c91d8c1d5768 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Wed, 3 Dec 2025 20:34:41 +0100 Subject: refactor equivariant props to use type classes --- Nominal/LambdaCalculus/Preterms.lean | 10 +++---- Nominal/LambdaCalculus/Terms.lean | 53 ++++++++++++++++++------------------ 2 files changed, 32 insertions(+), 31 deletions(-) (limited to 'Nominal/LambdaCalculus') diff --git a/Nominal/LambdaCalculus/Preterms.lean b/Nominal/LambdaCalculus/Preterms.lean index c133343..81622af 100644 --- a/Nominal/LambdaCalculus/Preterms.lean +++ b/Nominal/LambdaCalculus/Preterms.lean @@ -141,7 +141,7 @@ private def equiv : EquivariantEquiv Var Preterm (Var ⊕ (Var × Preterm) ⊕ ( | inl _ => simp | inr x' => cases x' <;> all_goals simp toFun_equivariant := by - intro t π + constructor; intro t π cases t <;> all_goals simp } @@ -181,13 +181,13 @@ 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 π +instance instVarsEquivariant : Function.Equivariant Var vars := by + constructor; 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 π +instance instFvEquivariant : Function.Equivariant Var fv := by + constructor; intro t π fun_induction fv <;> all_goals simp [fv, *, Set.smul_set_sdiff, Set.smul_set_union] end Preterm diff --git a/Nominal/LambdaCalculus/Terms.lean b/Nominal/LambdaCalculus/Terms.lean index be0d77d..91f4fb8 100644 --- a/Nominal/LambdaCalculus/Terms.lean +++ b/Nominal/LambdaCalculus/Terms.lean @@ -34,30 +34,31 @@ inductive AlphaEq : Preterm → Preterm → Prop where | 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 +instance Preterm.setoid : Setoid 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 - · exact AlphaEq.cong_abs a_ih - · 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 + iseqv := ⟨fun _ => AlphaEq.refl, AlphaEq.symm, AlphaEq.trans⟩ + +instance Preterm.instSetoidEquivariant : Rel.Equivariant Var setoid.r := by + constructor; 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 + · exact AlphaEq.cong_abs a_ih + · 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 [Function.equivariant Var Preterm.fv, Set.smul_mem_smul_set_iff] + exact h /-- Define λ-terms as the quotient Preterm/≈. -/ -def Term := Quotient Preterm.setoid.toSetoid +def Term := Quotient Preterm.setoid namespace Term /-- The equivalence class of a λ-preterm. -/ -abbrev mk : Preterm → Term := Quotient.mk Preterm.setoid.toSetoid +abbrev mk : Preterm → Term := Quotient.mk Preterm.setoid instance : NominalSet Var Term := Quotient.instNominalSet Var @@ -135,7 +136,7 @@ private lemma pick_fresh {t : Preterm} : ∀ x ∉ t.fv, ∃ u, t ≈ u ∧ x rw [Set.singleton_union, Set.mem_compl_iff, Set.mem_insert_iff, not_or] at hc have hc' : c ∉ (π • a_1).fv := fun h => hc.right (Preterm.fv_subset_vars _ h) obtain ⟨u, hu⟩ := a_ih (⸨π • a, c⸩ * π) x (by - rw [mul_smul, Preterm.fv_equivariant] + rw [mul_smul, Function.equivariant Var Preterm.fv] intro hcontra by_cases hxa : x = π • a · rw [hxa, ← PermSet.atom_set_swap_right] at hcontra @@ -177,7 +178,7 @@ lemma alpha_eq_iff : AlphaEq = AlphaEq' := by 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] + rw [Function.equivariant Var (Quotient.mk _), Quotient.sound hz₁, NameAbstraction.eq_iff_cases] by_cases hxy : x = y · left simp [hxy, FPerm.swap_self, one_smul] @@ -187,8 +188,8 @@ lemma alpha_eq_iff : AlphaEq = AlphaEq' := by · 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 [← Rel.equivariant Var NominalSet.IsFresh] + exact Function.Equivariant.preserve_fresh Var hz₂ · rw [← mul_smul, FPerm.swap_mul_self, one_smul] · intro h; cases h <;> all_goals expose_names · exact AlphaEq.refl @@ -201,7 +202,7 @@ lemma alpha_eq_iff : AlphaEq = AlphaEq' := by 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 + rw [← Quotient.sound hs₁, ← Function.equivariant Var (Quotient.mk _)] at h have hrename : Preterm.abs y s ≈ Preterm.abs x (⸨y, x⸩ • s) := by apply AlphaEq.rename rw [Preterm.supp] at hs₂ @@ -241,6 +242,7 @@ lemma eq_abs {x y : Var} {t u : Term} : Term.abs x t = Term.abs y u ↔ ⟪x⟫ obtain ⟨u', hu'⟩ := u.exists_rep simp only [abs, ← ht', Quotient.lift_mk, ← hu'] rw [Quotient.eq_iff_equiv, alpha_eq_abs] + rfl /-- 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 @@ -293,7 +295,7 @@ private def equiv : EquivariantEquiv Var Term (Var ⊕ (NameAbstraction Var Term (by intro t u htu rw [alpha_eq, alpha_eq_iff] at htu - cases htu <;> simp [*]) + cases htu <;> simp only [Sum.inr.injEq, Sum.inl.injEq, *]; assumption) invFun | .inl x => .var x | .inr (.inl x) => Quotient.liftOn x @@ -323,7 +325,7 @@ private def equiv : EquivariantEquiv Var Term (Var ⊕ (NameAbstraction Var Term simp only [app, ← hx', ← hy', Quotient.lift_mk, Sum.inr.injEq] rw [hx', hy'] toFun_equivariant := by - intro t π + constructor; intro t π obtain ⟨t', ht'⟩ := t.exists_rep rw [← ht'] cases t' <;> all_goals rfl @@ -357,8 +359,7 @@ def fv : Term → Set Var := Quotient.lift Preterm.fv (by simp [← ht', ← hu', Preterm.fv] /-- The lifted fv function is also equivariant.-/ -lemma fv_equivariant : Function.Equivariant Var fv := - Quotient.lift_equivariant Var _ _ Preterm.fv_equivariant +instance instFvEquivariant : Function.Equivariant Var fv := Quotient.lift_equivariant Var _ _ /-- The support of a term consists exactly of the free variables in it. -/ lemma supp : NominalSet.supp Var = fv := by -- cgit v1.3.1