From c5a5623c3ee6635432fb203ea3bb2cad94832f14 Mon Sep 17 00:00:00 2001
From: lengyijun <sjtu5140809011@gmail.com>
Date: Wed, 2 Sep 2026 13:19:55 +0800
Subject: [PATCH 1/4] refactor(Locallynameless): abbrev multiApp = `List.foldl
 app`

Replace the recursive multiApp definition with List.foldl app
Remove the now-unnecessary multiApp_tail lemma and adapt proofs to List.foldl_concat
Make semanticMap_saturated use explicit grind only lemmas for the new multiApp representation
New theorems : multiapp_openRec and multiapp_fv
---
 .../LocallyNameless/Stlc/StrongNorm.lean      |  3 +-
 .../LocallyNameless/Untyped/MultiApp.lean     | 31 +++++++++++--------
 .../LocallyNameless/Untyped/StrongNorm.lean   | 13 +++++---
 3 files changed, 28 insertions(+), 19 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean
index b55058f31..092a38af8 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean
@@ -70,7 +70,8 @@ lemma semanticMap_saturated (τ : Ty Base) : @Saturated Var (semanticMap τ) :=
     · grind [sn_app_left (Var := Var) (N := fvar <| fresh {})]
     · grind
     · intro M N P _ _ _ s _
-      grind [ih₂.multiApp M N (P ++ [s]), multiApp_tail]
+      grind only [semanticMap, = List.foldl_append, = List.foldl_cons, usr Set.mem_ofPred_eq,
+                  = List.foldl_nil, ih₂.multiApp M N (P ++ [s])]
 
 /-- The `entailsContext` predicate ensures that each variable in the context
     is mapped to a term in the corresponding semantic map. -/
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
index 877390646..7cd25589f 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
@@ -26,9 +26,7 @@ namespace LambdaCalculus.LocallyNameless.Untyped.Term
 /-- multiApp f [x₁, x₂, ..., xₙ] applies the arguments x₁, x₂, ..., xₙ
     to f in left-associative order, i.e. as (((f x₁) x₂) ... xₙ). -/
 @[simp, scoped grind =]
-def multiApp (f : Term Var) : List (Term Var) → Term Var
-| []      => f
-| a :: as => multiApp (app f a) as
+abbrev multiApp (f : Term Var) (Ns : List (Term Var)) := Ns.foldl app f
 
 /-- A list of arguments performs a single reduction step
 
@@ -45,11 +43,6 @@ inductive ListFullBeta : List (Term Var) → List (Term Var) → Prop where
 
 variable {M M' : Term Var} {Ns Ns' : List (Term Var)}
 
-lemma multiApp_tail {N} : (M.multiApp (Ns ++ [N])) = (M.multiApp Ns).app  N:= by
-  induction Ns generalizing M with
-  | nil => grind
-  | cons head tail ih => rw [List.cons_append]; apply ih
-
 /-- A term resulting from a multi-application is locally closed if
     and only if the leftmost term and all arguments applied to it are locally closed -/
 @[scoped grind ←]
@@ -77,6 +70,17 @@ lemma step_multiApp_r (steps : Ns ⭢lβᶠ Ns') (lc_M : LC M) : M.multiApp Ns 
 lemma steps_multiApp_r (steps : Ns ↠lβᶠ Ns') (lc_M : LC M) : M.multiApp Ns ↠βᶠ M.multiApp Ns' := by
   induction steps <;> grind
 
+lemma multiapp_openRec {i} :
+   (multiApp M Ns)⟦i ↝ M'⟧ = multiApp (M⟦i ↝ M'⟧) (Ns.map (openRec i M')) := by
+  induction Ns generalizing M with
+  | nil => grind
+  | cons head tail ih => grind [@ih (M.app head)]
+
+lemma multiapp_fv [DecidableEq Var] : (multiApp M Ns).fv = (Ns.map fv).foldl Union.union M.fv := by
+  induction Ns generalizing M with
+  | nil => grind
+  | cons head tail ih => grind [@ih (M.app head)]
+
 lemma listFullBeta_cons_r (h : Ns ⭢lβᶠ Ns') (h_lc : ∀ M ∈ l, LC M) : (l ++ Ns) ⭢lβᶠ (l ++ Ns') := by
   induction l using List.reverseRecOn generalizing Ns Ns' with grind
 
@@ -98,17 +102,18 @@ lemma invert_abs_multiApp_st {Ps} {M N Q : Term Var}
     (∃ Ps', Ps ⭢lβᶠ Ps' ∧ Q = multiApp (M.abs.app N) Ps') ∨
     (Q = multiApp (M ^ N) Ps) := by
   induction Ps using List.reverseRecOn generalizing M N Q with
-  | nil => grind only [cases Xi, multiApp]
+  | nil => grind [cases Xi]
   | append_singleton Ps P ih =>
-    rw [multiApp_tail] at h_red
+    unfold multiApp at h_red
+    rw [List.foldl_concat] at h_red
     cases h_red with
     | @appL _ _ P' _ P_P' =>
       have : (Ps ++ [P]) ⭢lβᶠ Ps ++ [P'] := by apply listFullBeta_cons_r (.step P_P' ?_) <;> grind
-      grind [multiApp_tail]
+      grind
     | appR _ h =>
       have {Ps'} (h : Ps ⭢lβᶠ Ps') : (Ps ++ [P]) ⭢lβᶠ Ps' ++ [P] := listFullBeta_cons_l h (by grind)
-      grind [multiApp_tail]
-    | base => induction Ps using List.reverseRecOn with grind [multiApp_tail]
+      grind
+    | base => induction Ps using List.reverseRecOn with grind
 
 
 /-- If a term (λ M) N P₁ ... Pₙ reduces in multiple steps to Q, then either Q if of the form
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean
index 550f63e1e..5d892ee5e 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean
@@ -131,16 +131,18 @@ lemma sn_abs_app_multiApp [DecidableEq Var] [HasFresh Var] {Ps} {M N : Term Var}
     · exact sn_N
     · grind [→ steps_open_cong_abs, open_abs_lc, sn_steps]
   | append_singleton Ps P ih =>
-    rw [multiApp_tail]
+    unfold multiApp
+    rw [List.foldl_concat]
     apply sn_app
-    · rw [multiApp_tail] at sn_MNPs lc_MNPs
+    · unfold multiApp at sn_MNPs lc_MNPs
+      rw [List.foldl_concat] at sn_MNPs lc_MNPs
       cases lc_MNPs
       grind [sn_app_left]
-    · grind [multiApp_tail, sn_app_right]
+    · grind [sn_app_right]
     · intro Q' P' hstep1 hstep2
       have ⟨M', N', Ps', h_M_red, h_N_red, h_Ps_red, h_cases⟩ := invert_abs_multiApp_mst hstep1
       rcases h_cases with h_P | ⟨h_st1, h_st2⟩
-      · induction Ps' using List.reverseRecOn with grind [multiApp_tail]
+      · induction Ps' using List.reverseRecOn with grind
       · have innerSteps : (M ^ N).multiApp Ps ↠βᶠ (M' ^ N').multiApp Ps' := by
           trans
           · exact steps_multiApp_r h_Ps_red (by grind)
@@ -148,7 +150,8 @@ lemma sn_abs_app_multiApp [DecidableEq Var] [HasFresh Var] {Ps} {M N : Term Var}
             · apply steps_open_cong_abs M M' N N' <;> grind [open_abs_lc]
             · grind [multiApp_steps_lc]
         refine sn_steps ?_ sn_MNPs
-        rw [multiApp_tail]
+        unfold multiApp
+        rw [List.foldl_concat]
         · calc ((M ^ N).multiApp Ps).app P
             _ ↠βᶠ ((M ^ N).multiApp Ps).app P' := by grind
             _ ↠βᶠ Q'.abs.app P' := redex_app_l_cong (.trans innerSteps h_st2) (by grind)

From 6ebcb4703e0f6f56be3599d93a82c609f1863d71 Mon Sep 17 00:00:00 2001
From: lengyijun <sjtu5140809011@gmail.com>
Date: Wed, 2 Sep 2026 14:05:59 +0800
Subject: [PATCH 2/4] feat: `ListFullBeta` context lemmas

Rename `listFullBeta_cons_r/l` to `listFullBeta_concat_r/l` to reflect their general concatenation behavior.
Add specialized `cons` lemmas for reducing the head term or the tail list.
---
 .../LocallyNameless/Untyped/MultiApp.lean        | 16 ++++++++++++----
 1 file changed, 12 insertions(+), 4 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
index 7cd25589f..7d708ea0e 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
@@ -81,12 +81,20 @@ lemma multiapp_fv [DecidableEq Var] : (multiApp M Ns).fv = (Ns.map fv).foldl Uni
   | nil => grind
   | cons head tail ih => grind [@ih (M.app head)]
 
-lemma listFullBeta_cons_r (h : Ns ⭢lβᶠ Ns') (h_lc : ∀ M ∈ l, LC M) : (l ++ Ns) ⭢lβᶠ (l ++ Ns') := by
+lemma listFullBeta_concat_r (h : Ns ⭢lβᶠ Ns') (h_lc : ∀ M ∈ l, LC M) : (l ++ Ns) ⭢lβᶠ (l ++ Ns') := by
   induction l using List.reverseRecOn generalizing Ns Ns' with grind
 
-lemma listFullBeta_cons_l (h : Ns ⭢lβᶠ Ns') (h_lc : ∀ M ∈ l, LC M) : (Ns ++ l) ⭢lβᶠ (Ns' ++ l) := by
+lemma listFullBeta_concat_l (h : Ns ⭢lβᶠ Ns') (h_lc : ∀ M ∈ l, LC M) : (Ns ++ l) ⭢lβᶠ (Ns' ++ l) := by
   induction h with grind
 
+lemma listFullBeta_cons_r (h : Ns ↠lβᶠ Ns') (h_lc : LC M) : (M :: Ns) ↠lβᶠ (M :: Ns') := by
+  induction h with grind
+
+lemma listFullBeta_cons_l (h : M ↠βᶠ M') (h_lc : ∀ M ∈ Ns, LC M) : (M :: Ns) ↠lβᶠ (M' :: Ns) := by
+  induction h with
+  | refl => grind
+  | tail _ h ih => exact .tail ih (.step h h_lc)
+
 set_option linter.tacticAnalysis.verifyGrindOnly false in
 /-- If a term (λ M) N P_1 ... P_n reduces in a single step to Q, then
     Q must be one of the following forms:
@@ -108,10 +116,10 @@ lemma invert_abs_multiApp_st {Ps} {M N Q : Term Var}
     rw [List.foldl_concat] at h_red
     cases h_red with
     | @appL _ _ P' _ P_P' =>
-      have : (Ps ++ [P]) ⭢lβᶠ Ps ++ [P'] := by apply listFullBeta_cons_r (.step P_P' ?_) <;> grind
+      have : (Ps ++ [P]) ⭢lβᶠ Ps ++ [P'] := by apply listFullBeta_concat_r (.step P_P' ?_) <;> grind
       grind
     | appR _ h =>
-      have {Ps'} (h : Ps ⭢lβᶠ Ps') : (Ps ++ [P]) ⭢lβᶠ Ps' ++ [P] := listFullBeta_cons_l h (by grind)
+      have {Ps'} (h : Ps ⭢lβᶠ Ps') : (Ps ++ [P]) ⭢lβᶠ Ps' ++ [P] := listFullBeta_concat_l h (by grind)
       grind
     | base => induction Ps using List.reverseRecOn with grind
 

From 10506860bfc291bfa49571d76ceff358db6bf38d Mon Sep 17 00:00:00 2001
From: lengyijun <sjtu5140809011@gmail.com>
Date: Wed, 2 Sep 2026 14:12:12 +0800
Subject: [PATCH 3/4] Add `multiApp` congruence lemmas for union reductions
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Add `step_multiApp_l_union` to lift a single `(Xi R1 ⊔ Xi R2)` reduction through a multi-application.
Add `steps_multiApp_l_union` for the corresponding reflexive-transitive closure.
Use the new single-step lemma to simplify the proof of the multi-step result.
---
 .../LocallyNameless/Untyped/MultiApp.lean        | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
index 7d708ea0e..92b65da0f 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
@@ -61,6 +61,22 @@ lemma steps_multiApp_l (steps : M ↠βᶠ M') (lc_Ns : ∀ N ∈ Ns, LC N) :
     M.multiApp Ns ↠βᶠ M'.multiApp Ns := by
   induction steps <;> grind
 
+lemma step_multiApp_l_union {R1 R2} (step : (Xi R1 ⊔ Xi R2) M M') (lc_Ns : ∀ N ∈ Ns, LC N) :
+   (Xi R1 ⊔ Xi R2) (multiApp M Ns) (multiApp M' Ns) := by
+  induction Ns generalizing M M' with
+  | nil => grind
+  | cons head tail ih =>
+      apply ih ?_ (by grind)
+      cases step with
+        | inl h =>  left; grind
+        | inr h =>  right; grind
+
+lemma steps_multiApp_l_union {R1 R2}
+  (steps : Relation.ReflTransGen (Xi R1 ⊔ Xi R2) M M')
+  (lc_Ns : ∀ N ∈ Ns, LC N) :
+   Relation.ReflTransGen (Xi R1 ⊔ Xi R2) (multiApp M Ns) (multiApp M' Ns) := by
+  induction steps <;> grind [step_multiApp_l_union]
+
 /-- Congruence lemma for single reduction of one of the arguments of a multi-application -/
 @[scoped grind ←]
 lemma step_multiApp_r (steps : Ns ⭢lβᶠ Ns') (lc_M : LC M) : M.multiApp Ns ⭢βᶠ M.multiApp Ns' := by

From bf0dd161616fb8fec8a48e07687c54efebffc3c7 Mon Sep 17 00:00:00 2001
From: lengyijun <sjtu5140809011@gmail.com>
Date: Wed, 2 Sep 2026 14:23:24 +0800
Subject: [PATCH 4/4] format

---
 .../LocallyNameless/Untyped/MultiApp.lean              | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
index 92b65da0f..dfcaddb12 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
@@ -97,10 +97,12 @@ lemma multiapp_fv [DecidableEq Var] : (multiApp M Ns).fv = (Ns.map fv).foldl Uni
   | nil => grind
   | cons head tail ih => grind [@ih (M.app head)]
 
-lemma listFullBeta_concat_r (h : Ns ⭢lβᶠ Ns') (h_lc : ∀ M ∈ l, LC M) : (l ++ Ns) ⭢lβᶠ (l ++ Ns') := by
+lemma listFullBeta_concat_r (h : Ns ⭢lβᶠ Ns') (h_lc : ∀ M ∈ l, LC M) :
+  (l ++ Ns) ⭢lβᶠ (l ++ Ns') := by
   induction l using List.reverseRecOn generalizing Ns Ns' with grind
 
-lemma listFullBeta_concat_l (h : Ns ⭢lβᶠ Ns') (h_lc : ∀ M ∈ l, LC M) : (Ns ++ l) ⭢lβᶠ (Ns' ++ l) := by
+lemma listFullBeta_concat_l (h : Ns ⭢lβᶠ Ns') (h_lc : ∀ M ∈ l, LC M) :
+  (Ns ++ l) ⭢lβᶠ (Ns' ++ l) := by
   induction h with grind
 
 lemma listFullBeta_cons_r (h : Ns ↠lβᶠ Ns') (h_lc : LC M) : (M :: Ns) ↠lβᶠ (M :: Ns') := by
@@ -135,8 +137,8 @@ lemma invert_abs_multiApp_st {Ps} {M N Q : Term Var}
       have : (Ps ++ [P]) ⭢lβᶠ Ps ++ [P'] := by apply listFullBeta_concat_r (.step P_P' ?_) <;> grind
       grind
     | appR _ h =>
-      have {Ps'} (h : Ps ⭢lβᶠ Ps') : (Ps ++ [P]) ⭢lβᶠ Ps' ++ [P] := listFullBeta_concat_l h (by grind)
-      grind
+    have {Ps'} (h : Ps ⭢lβᶠ Ps') : (Ps ++ [P]) ⭢lβᶠ Ps' ++ [P] := listFullBeta_concat_l h (by grind)
+    grind
     | base => induction Ps using List.reverseRecOn with grind