implement lambda preterms

2 files changed, 132 insertions, 0 deletions

diff --git a/Nominal/Helpers/CountableString.lean b/Nominal/Helpers/CountableString.lean
new file mode 100644
index 0000000..7d2fcb7
--- /dev/null
+++ b/Nominal/Helpers/CountableString.lean
@@ -0,0 +1,12 @@
+import Mathlib
+
+instance : Countable Char where
+  exists_injective_nat' := by
+    exists Char.toNat
+    intro c₁ c₂ hc
+    rw [Char.toNat, Char.toNat, UInt32.toNat_inj] at hc
+    exact Char.eq_of_val_eq hc
+
+instance : Countable String := Countable.of_equiv (List Char)
+  { toFun := String.mk
+    invFun := String.data }
diff --git a/Nominal/LambdaCalculus/Preterms.lean b/Nominal/LambdaCalculus/Preterms.lean
new file mode 100644
index 0000000..c486a7e
--- /dev/null
+++ b/Nominal/LambdaCalculus/Preterms.lean
@@ -0,0 +1,120 @@
+import Mathlib
+import Nominal.Permutations
+import Nominal.Support
+import Nominal.Helpers.CountableString
+
+/-!
+# λ-Preterms
+
+As a practical example for nominal sets, this file defines λ-preterms (that is, λ-terms without α-equivalence).
+-/
+
+namespace Lambda
+
+/-!
+## Basic Syntax Definition
+
+Define the AST and a parser for it.
+-/
+section Syntax
+
+/-- We will use strings as the set of atoms, representing variable names. -/
+def Var := String
+  deriving DecidableEq, Countable, Infinite
+
+/-- Basic λ-preterm definition.
+
+We furthermore allow defining λ-terms as ⟫ t ⟪ with
+  t, u ::= x | λ x y ..., t | t u,
+where x, y, ... are variables. -/
+inductive Preterm
+  | var : Var → Preterm
+  | abs : Var → Preterm → Preterm
+  | app : Preterm → Preterm → Preterm
+  deriving DecidableEq
+
+open Lean Elab Meta
+
+declare_syntax_cat lam
+
+syntax ident : lam
+syntax "(" lam ")" : lam
+syntax:10 (name := stxabs) "λ " ident+ ", " lam : lam
+syntax:45 lam:45 lam:46 : lam
+
+partial def elabLam : Syntax → MetaM Expr
+  | `(lam | $x:ident) => mkAppM ``Preterm.var #[mkStrLit x.getId.toString]
+  | `(lam | ($t:lam)) => elabLam t
+  | `(lam | $t:lam $u:lam) => do mkAppM ``Preterm.app #[← elabLam t, ← elabLam u]
+  | `(lam | λ $xs:ident*, $t:lam) => do
+    xs.foldrM (fun x t' => mkAppM ``Preterm.abs #[mkStrLit x.getId.toString, t']) (← elabLam t)
+  | _ => throwUnsupportedSyntax
+
+elab "⟫ " t:lam " ⟪" : term => elabLam t
+
+example : ⟫ x y z ⟪ = ⟫ (x y) z ⟪ := by decide
+example : ⟫ λ x, λ y, x ⟪ = ⟫ λ x y, x ⟪ := by decide
+
+end Syntax
+
+/-!
+## Nominal Set Instance
+
+The set of preterms forms a nominal set, where the permutation action just renames all occurrences of a variable.
+-/
+section NominalSet
+
+namespace Preterm
+
+private def rename (π : FPerm Var) : Preterm → Preterm
+  | .var x => .var (π • x)
+  | .abs x t => .abs (π • x) (rename π t)
+  | .app t u => .app (rename π t) (rename π u)
+
+private lemma one_rename (t : Preterm) : rename 1 t = t := by
+  induction' t <;> all_goals simp [rename, *]
+
+private lemma mul_rename (π τ : FPerm Var) (t : Preterm) : rename (π * τ) t = rename π (rename τ t) := by
+  induction' t <;> all_goals simp [rename, mul_smul, *]
+
+instance : PermSet Var Preterm where
+  smul := rename
+  one_smul := one_rename
+  mul_smul := mul_rename
+
+@[simp] lemma smul_var {π : FPerm Var} {x : Var} : π • Preterm.var x = Preterm.var (π • x) := rfl
+@[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
+    induction' t <;> all_goals expose_names
+    · constructor
+      · simp [PermSet.HasSupport, PermSet.fix, aSupport, PermSet.fix']
+      · simp [aSupport]
+    · 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π
+        exact ⟨hπ.left, a_ih.left hπ.right⟩
+      · simp [aSupport, 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π
+        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]
+
+end Preterm
+
+end NominalSet
+
+end Lambda