From 8d9991a23e345c6bb5ed91f60292e4bb0a379c7e Mon Sep 17 00:00:00 2001
From: lengyijun <sjtu5140809011@gmail.com>
Date: Fri, 14 Aug 2026 19:04:02 +0800
Subject: [PATCH] feat: Add BetaAt uniqueness, FV preservation, and left
 redex-count bound
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Renaming BetaAt.le_countRedexes → BetaAt.le_countRedexes_r

new theorems : BetaAt.step_fv BetaAt.unique BetaAt.le_countRedexes_l Leftmost.steps_fv
---
 .../LocallyNameless/Untyped/BetaAt.lean       | 55 ++++++++++++++++++-
 .../Untyped/LeftmostReduction.lean            |  6 ++
 .../Untyped/StandardReduction.lean            |  2 +-
 3 files changed, 61 insertions(+), 2 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/BetaAt.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/BetaAt.lean
index 71b05e0de..0d8828a64 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/BetaAt.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/BetaAt.lean
@@ -151,8 +151,24 @@ lemma BetaAt.to_step [DecidableEq Var] (h : BetaAt i M N) (lc : LC M) : M ⭢β
 
 variable [HasFresh Var]
 
+lemma BetaAt.le_countRedexes_l (h : BetaAt i M N) : i < countRedexes M := by
+  induction h with
+  | outer => grind
+  | appL step =>
+    split
+    · grind
+    · exact le_trans (by omega) (countRedexes_app_le _ _)
+  | appR =>
+    split
+    · rw [countRedexes_app_abs (by assumption)]
+      omega
+    · exact le_trans (by omega) (countRedexes_app_le _ _)
+  | abs xs =>
+    have := fresh_exists xs
+    grind [countRedexes_open_fvar]
+
 /-- The position of a contracted redex is at most the redex count of the result. -/
-lemma BetaAt.le_countRedexes (h : BetaAt i M N) : i ≤ countRedexes N := by
+lemma BetaAt.le_countRedexes_r (h : BetaAt i M N) : i ≤ countRedexes N := by
   induction h with
   | outer => exact Nat.zero_le _
   | appL step =>
@@ -171,6 +187,16 @@ lemma BetaAt.le_countRedexes (h : BetaAt i M N) : i ≤ countRedexes N := by
 
 variable [DecidableEq Var]
 
+lemma BetaAt.step_fv (h : BetaAt i M M') : M'.fv ⊆ M.fv := by
+  induction h with
+  | outer _ _ => grind [open_preserve_not_fvar]
+  | appL _ _ => grind
+  | appR _ _ => grind
+  | abs xs _ _ =>
+    have ⟨x, _⟩ := fresh_exists <| free_union [fv] Var
+    have := open_close x
+    grind [open_preserve_not_fvar 0 M M']
+
 /-- Renaming a free variable preserves the position of the contracted redex. -/
 lemma BetaAt.rename (h : BetaAt i M M') (x y : Var) :
     BetaAt i (M[x := fvar y]) (M'[x := fvar y]) := by
@@ -217,6 +243,33 @@ lemma BetaAt.abs_close {x : Var} (h : BetaAt i M M') (lc : LC M) :
   have hr : BetaAt i (M[x := fvar z]) (M'[x := fvar z]) := h.rename x z
   grind
 
+lemma BetaAt.unique (hn : BetaAt i M N) (hp : BetaAt i M P) : N = P := by
+  induction hn generalizing P with
+  | outer _ _ =>
+      generalize hi : 0 = i at hp
+      cases hp <;> grind
+  | appL hn ih =>
+      generalize hi : ( _ +  if (IsAbs _) then 1 else 0) = i at hp
+      cases hp with
+      | outer => grind
+      | appL => grind
+      | appR hp =>
+          apply BetaAt.le_countRedexes_l at hn
+          omega
+  | appR hn ih =>
+      generalize hi : ( _ +  if (IsAbs _) then 1 else 0) = i at hp
+      cases hp with
+      | outer => grind
+      | appR => grind
+      | appL hp =>
+          apply BetaAt.le_countRedexes_l at hp
+          omega
+  | abs xs _ ih => cases hp with | abs xs hp =>
+      have ⟨x, _⟩ := fresh_exists <| free_union [fv] Var
+      specialize ih x (by grind) (hp x (by grind))
+      apply_fun (fun t => close t x) at ih
+      rw [<- open_close_var, <- open_close_var] at ih <;> grind
+
 end LambdaCalculus.LocallyNameless.Untyped.Term
 
 end Cslib
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
index e690a3375..e2f14e510 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
@@ -92,6 +92,12 @@ lemma Leftmost.of_cbn (h : M ↠ₙ N) : M ↠ℓ N := by
 
 variable [DecidableEq Var] [HasFresh Var]
 
+lemma Leftmost.steps_fv (steps : M ↠ℓ M') : M'.fv ⊆ M.fv := by
+  induction steps with
+  | refl => grind
+  | tail _ h _ => apply BetaAt.step_fv at h
+                  grind
+
 /-- Leftmost reduction preserves local closure. -/
 lemma Leftmost.steps_lc_r (h : M ↠ℓ M') (lc : LC M) : LC M' := by
   induction h with
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
index 628107821..312d13cf4 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
@@ -163,7 +163,7 @@ lemma StandardSeq.le_countRedexes_of_ne (h : StandardSeq n M N) (hne : M ≠ N)
     n ≤ countRedexes N := by
   cases h with
   | refl => contradiction
-  | tail _ step _ => exact step.le_countRedexes
+  | tail _ step _ => exact step.le_countRedexes_r
 
 omit [HasFresh Var] in
 /-- Reducing the operator of an application yields a standard sequence, with the final position