From 62f95ea12bb2d945573868190e90c579b47eab3c Mon Sep 17 00:00:00 2001
From: lengyijun <sjtu5140809011@gmail.com>
Date: Thu, 20 Aug 2026 08:23:50 +0800
Subject: [PATCH] feat: SN FullEta
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Adds a size measure on untyped λ-terms and uses it to prove that full η-reduction is strongly normalizing.
---
 Cslib.lean                                    |  1 +
 .../LocallyNameless/Untyped/FullEta.lean      |  8 ++++
 .../LocallyNameless/Untyped/Size.lean         | 37 +++++++++++++++++++
 .../LocallyNameless/Untyped/StrongNorm.lean   |  8 ++++
 4 files changed, 54 insertions(+)
 create mode 100644 Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Size.lean

diff --git a/Cslib.lean b/Cslib.lean
index 982b94f5d..526d5e48b 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -157,6 +157,7 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LeftmostRed
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiApp
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiSubst
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Size
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StandardReduction
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm
 public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean
index a830d898f..8c133be3d 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean
@@ -9,6 +9,7 @@ module
 public import Cslib.Foundations.Relation.Attr
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Congruence
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Size
 
 /-! # η-reduction for the λ-calculus -/
 
@@ -154,6 +155,13 @@ lemma steps_open_cong_r {s t t' : Term Var} (lc_s : LC s.abs) (steps : t ↠η
   case refl => rfl
   case head _ _ st _ ih => exact .trans (step_open_cong_r lc_s st) ih
 
+lemma step_size (step : M ⭢ηᶠ M') : M'.size < M.size := by
+  induction step with
+  | abs xs _ =>
+    have ⟨x, _⟩ := fresh_exists <| free_union [fv] Var
+    grind
+  | _ => grind
+
 /- Closing a sequence of η-reduction steps over a fresh variable preserves the steps. -/
 open Relation in
 lemma close_eta_steps (hx_M : x ∉ M.fv) (st_M : ReflGen FullEta (M ^ fvar x) N) :
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Size.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Size.lean
new file mode 100644
index 000000000..5a308e4cf
--- /dev/null
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Size.lean
@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2025 Chris Henson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yijun Leng
+-/
+
+module
+
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Basic
+
+/-! Size of untyped lambda calculus term. -/
+
+@[expose] public section
+
+namespace Cslib
+
+namespace LambdaCalculus.LocallyNameless.Untyped.Term
+
+universe u
+
+variable {Var : Type u}
+
+/-- Computes the size of a lambda calculus term. -/
+@[simp, scoped grind =]
+def size : Term Var -> Nat
+| bvar _ => 0
+| fvar _ => 0
+| abs t => 1 + size t
+| app t1 t2 => 1 + size t1 + size t2
+
+@[scoped grind =]
+theorem size_openRec {x : Var} {M i} : M⟦i ↝ fvar x⟧.size = M.size := by
+  induction M generalizing i <;> grind
+
+end LambdaCalculus.LocallyNameless.Untyped.Term
+
+end Cslib
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean
index ea45ee0e8..c72f3bfa9 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean
@@ -7,6 +7,7 @@ Authors: David Wegmann
 module
 
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEta
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiApp
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
 public import Cslib.Foundations.Relation.Confluence
@@ -156,6 +157,13 @@ lemma sn_abs_app_multiApp [DecidableEq Var] [HasFresh Var] {Ps} {M N : Term Var}
               refine Relation.TransGen.single (Xi.base (Beta.beta ?_ ?_))
               all_goals grind
 
+lemma sn_eta [HasFresh Var] [DecidableEq Var] : SN FullEta t := by
+  induction h : t.size using Nat.strong_induction_on generalizing t with | h n ih =>
+  apply SN.intro
+  intros y hy
+  apply FullEta.step_size at hy
+  exact ih y.size (by omega) rfl
+
 end LambdaCalculus.LocallyNameless.Untyped.Term
 
 end Cslib