feat: Terminating FullEta

Cslib.lean

@@ -179,6 +179,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

@@ -7,8 +7,10 @@ Authors: Maximiliano Onofre Martínez
 module
 
 public import Cslib.Foundations.Relation.Attr
+public import Cslib.Foundations.Relation.Defs
 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 -/
 
@@ -149,6 +151,11 @@ 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 _ => grind [fresh_exists <| free_union [fv] Var]
+  | _ => 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) :
@@ -158,6 +165,11 @@ lemma close_eta_steps (hx_M : x ∉ M.fv) (st_M : ReflGen FullEta (M ^ fvar x) N
   | single st =>
     exact .single (Xi.abs {x} (by grind [step_subst_cong_l]))
 
+open Relation in
+lemma terminating : Terminating (@FullEta Var) :=
+  Subrelation.wf (fun {a b} (h : flip FullEta a b) => step_size h)
+      (InvImage.wf size Nat.lt_wfRel.wf)
+
 end LambdaCalculus.LocallyNameless.Untyped.Term.FullEta
 
 end Cslib

Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Size.lean

@@ -0,0 +1,40 @@
+/-
+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, 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_fvar (i) (x : Var) (M) : M⟦i ↝ fvar x⟧.size = M.size := by
+  induction M generalizing i <;> grind
+
+theorem size_open_fvar (x : Var) (t : Term Var) : size (t ^ fvar x) = size t :=
+  size_openRec_fvar 0 x t
+
+end LambdaCalculus.LocallyNameless.Untyped.Term
+
+end Cslib