From 75d1f4a9c41e0d8200c2417c1fb7dfa5b456ae1b Mon Sep 17 00:00:00 2001
From: lengyijun <sjtu5140809011@gmail.com>
Date: Fri, 4 Sep 2026 13:30:07 +0800
Subject: [PATCH] feat(LocallyNameless): new theorems in FullBetaEta

1. The old multi-step lemmas

redex_app_l_cong and redex_app_r_cong

become

single-step: step_app_l_cong / step_app_r_cong
multi-step: steps_app_l_cong / steps_app_r_cong

2. new theorems:

  Normal.sup_iff
  step_fv
  steps_fv
  step_subst_cong_l
  steps_subst_cong_l
---
 Cslib/Foundations/Relation/Confluence.lean    |  7 +++
 .../LocallyNameless/Untyped/FullBetaEta.lean  | 56 ++++++++++++++-----
 2 files changed, 48 insertions(+), 15 deletions(-)

diff --git a/Cslib/Foundations/Relation/Confluence.lean b/Cslib/Foundations/Relation/Confluence.lean
index c6e71e623..ddee7a636 100644
--- a/Cslib/Foundations/Relation/Confluence.lean
+++ b/Cslib/Foundations/Relation/Confluence.lean
@@ -131,6 +131,13 @@ theorem Normal_iff (r : α → α → Prop) (x : α) : Normal r x ↔ ∀ y, ¬
 theorem Normal.reflTransGen_eq (h : Normal r x) (xy : ReflTransGen r x y) : x = y := by
   induction xy <;> grind
 
+theorem Normal.sup_iff (x : α) : Normal (r₁ ⊔ r₂) x ↔ Normal r₁ x /\ Normal r₂ x := by
+  constructor
+  · intros g
+    constructor <;> intros h <;> apply g <;> obtain ⟨t, _⟩ := h <;> exists t <;> tauto
+  · rintro _ ⟨t, h⟩
+    cases h <;> grind
+
 /-- For a Church-Rosser relation, elements in an equivalence class must be multi-step related. -/
 theorem ChurchRosser.normal_eqvGen_reflTransGen (cr : ChurchRosser r) (norm : Normal r x)
     (xy : EqvGen r y x) : ReflTransGen r y x := by
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEta.lean
index e847f97de..b701b971c 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEta.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEta.lean
@@ -37,23 +37,49 @@ abbrev FullBetaEta : Term Var → Term Var → Prop := FullBeta ⊔ FullEta
 
 namespace FullBetaEta
 
-theorem redex_app_l_cong (redex : M ↠βηᶠ M') (lc_N : LC N) : app M N ↠βηᶠ app M' N := by
-  induction redex with
+variable {M M' N N' : Term Var}
+
+theorem step_app_l_cong (step : M ⭢βηᶠ M') (h_lc : LC N) : app M N ⭢βηᶠ app M' N := by
+    rcases step with h | h
+    · exact join_inl (h.appR h_lc)
+    · exact join_inr (h.appR h_lc)
+
+theorem step_app_r_cong (step : M ⭢βηᶠ M') (h_lc : LC N) : app N M ⭢βηᶠ app N M' := by
+    rcases step with h | h
+    · exact join_inl (h.appL h_lc)
+    · exact join_inr (h.appL h_lc)
+
+theorem steps_app_l_cong (steps : M ↠βηᶠ M') (h_lc : LC N) : app M N ↠βηᶠ app M' N := by
+  induction steps with
+  | refl => grind
+  | tail _ h ih => exact ih.tail (step_app_l_cong h h_lc)
+
+theorem steps_app_r_cong (steps : M ↠βηᶠ M') (h_lc : LC N) : app N M ↠βηᶠ app N M' := by
+  induction steps with
   | refl => grind
-  | tail _ h ih =>
-    refine .tail ih ?_
-    rcases h with h | h
-    · exact join_inl (h.appR lc_N)
-    · exact join_inr (h.appR lc_N)
-
-theorem redex_app_r_cong (redex : M ↠βηᶠ M') (lc_N : LC N) : app N M ↠βηᶠ app N M' := by
-  induction redex with
+  | tail _ h ih => exact ih.tail (step_app_r_cong h h_lc)
+
+variable [HasFresh Var] [DecidableEq Var]
+
+lemma step_fv (step : M ⭢βηᶠ M') : M'.fv ⊆ M.fv := by
+    cases step with
+    | inl h => grind [FullBeta.step_not_fv h]
+    | inr h => grind [FullEta.step_not_fv h]
+
+lemma steps_fv (steps : M ↠βηᶠ M') : M'.fv ⊆ M.fv := by
+  induction steps with
   | refl => grind
-  | tail _ h ih =>
-    refine .tail ih ?_
-    rcases h with h | h
-    · exact join_inl (h.appL lc_N)
-    · exact join_inr (h.appL lc_N)
+  | tail _ step _ => grind [step_fv step]
+
+lemma step_subst_cong_l (x : Var) (step : M ⭢βηᶠ M') (h_lc : LC N) :
+    M[x := N] ⭢βηᶠ M'[x := N] := by
+  cases step with
+  | inl h => exact Or.inl (FullBeta.redex_subst_cong_lc _ _ _ _ h h_lc)
+  | inr h => exact Or.inr (FullEta.step_subst_cong_l _ _ _  h h_lc)
+
+lemma steps_subst_cong_l (x : Var) (steps : M ↠βηᶠ M') (h_lc : LC N) :
+    M[x := N] ↠βηᶠ M'[x := N] := by
+  induction steps with grind [step_subst_cong_l]
 
 end FullBetaEta