refactor(Locallynameless): abbrev multiApp = List.foldl app

Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean

@@ -66,7 +66,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. -/

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,16 +43,11 @@ 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 ←]
 lemma multiApp_lc : LC (M.multiApp Ns) ↔ LC M ∧ (∀ N ∈ Ns, LC N) := by
-  induction Ns generalizing M with grind [cases LC]
+  induction Ns using List.reverseRecOn with grind [cases LC]
 
 /-- Just like ordinary beta reduction, the left-hand side
     of a multi-application step is locally closed -/
@@ -71,6 +64,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
@@ -80,12 +89,33 @@ 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 listFullBeta_cons_r (h : Ns ⭢lβᶠ Ns') (h_lc : ∀ M ∈ l, LC M) : (l ++ Ns) ⭢lβᶠ (l ++ Ns') := by
+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_append_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_append_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:
@@ -101,17 +131,17 @@ 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
+    simp only [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]
+      have : (Ps ++ [P]) ⭢lβᶠ Ps ++ [P'] := by apply listFullBeta_append_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)
-      grind [multiApp_tail]
-    | base => induction Ps using List.reverseRecOn with grind [multiApp_tail]
+    have {Ps'} (h : Ps ⭢lβᶠ Ps') : (Ps ++ [P]) ⭢lβᶠ Ps' ++ [P] := listFullBeta_append_l h (by grind)
+    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

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

@@ -129,24 +129,24 @@ 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]
+    simp only [List.foldl_concat]
     apply sn_app
-    · rw [multiApp_tail] at sn_MNPs lc_MNPs
+    · simp only [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)
           · apply steps_multiApp_l
             · 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]
+        simp only [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)