feat: SN FullEta

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

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) :

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

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