fix(LocallyNameless): change multiApp to right-recursive

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

@@ -71,7 +71,7 @@ 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 (s :: P)]
+      grind [ih₂.multiApp M N (P ++ [s]), multiApp_tail]
 
 /-- 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

@@ -28,7 +28,7 @@ namespace LambdaCalculus.LocallyNameless.Untyped.Term
 @[simp, scoped grind =]
 def multiApp (f : Term Var) : List (Term Var) → Term Var
 | []      => f
-| a :: as => Term.app (multiApp f as) a
+| a :: as => multiApp (app f a) as
 
 /-- A list of arguments performs a single reduction step
 
@@ -45,18 +45,23 @@ 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 with grind [cases LC]
+  induction Ns generalizing M with grind [cases LC]
 
 /-- Just like ordinary beta reduction, the left-hand side
     of a multi-application step is locally closed -/
 @[scoped grind ←]
 lemma step_multiApp_l (steps : M ⭢βᶠ M') (lc_Ns : ∀ N ∈ Ns, LC N) :
     M.multiApp Ns ⭢βᶠ M'.multiApp Ns := by
-  induction Ns <;> grind
+  induction Ns generalizing M M' with grind
 
 /-- Congruence lemma for multi reduction of the left most term of a multi-application -/
 lemma steps_multiApp_l (steps : M ↠βᶠ M') (lc_Ns : ∀ N ∈ Ns, LC N) :
@@ -66,12 +71,18 @@ lemma steps_multiApp_l (steps : M ↠βᶠ M') (lc_Ns : ∀ N ∈ Ns, LC N) :
 /-- 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
-  induction steps <;> grind
+  induction steps generalizing M <;> grind
 
 /-- Congruence lemma for multiple reduction of one of the arguments of a multi-application -/
 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
+  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
+  induction h with grind
+
 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:
@@ -86,16 +97,19 @@ lemma invert_abs_multiApp_st {Ps} {M N Q : Term Var}
     (∃ N', N ⭢βᶠ N' ∧ Q = multiApp (M.abs.app N') Ps) ∨
     (∃ Ps', Ps ⭢lβᶠ Ps' ∧ Q = multiApp (M.abs.app N) Ps') ∨
     (Q = multiApp (M ^ N) Ps) := by
-  induction Ps generalizing M N Q with
+  induction Ps using List.reverseRecOn generalizing M N Q with
   | nil => grind only [cases Xi, multiApp]
-  | cons P Ps ih =>
-    generalize Heq : (M.abs.app N).multiApp Ps = Q'
-    have : ∀ P', Q'.app P' = (M.abs.app N).multiApp (P' :: Ps) := by grind
-    rw [multiApp, Heq] at h_red
+  | append_singleton Ps P ih =>
+    rw [multiApp_tail] at h_red
     cases h_red with
-    | base => cases Ps <;> grind
-    | appR => grind [→ ListFullBeta.cons]
-    | appL => grind
+    | @appL _ _ P' _ P_P' =>
+      have : (Ps ++ [P]) ⭢lβᶠ Ps ++ [P'] := by apply listFullBeta_cons_r (.step P_P' ?_) <;> grind
+      grind [multiApp_tail]
+    | 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]
+
 
 /-- 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

@@ -124,36 +124,37 @@ lemma sn_abs_app_multiApp [DecidableEq Var] [HasFresh Var] {Ps} {M N : Term Var}
     (sn_N : SN FullBeta N) (sn_MNPs : SN FullBeta (multiApp (M ^ N) Ps))
     (lc_N : LC N) (lc_MNPs : LC (multiApp (M ^ N) Ps)) :
     SN FullBeta (multiApp (M.abs.app N) Ps) := by
-  induction Ps with
+  induction Ps using List.reverseRecOn with
   | nil =>
     apply sn_app
     · grind [sn_abs]
     · exact sn_N
     · grind [→ steps_open_cong_abs, open_abs_lc, sn_steps]
-  | cons P Ps ih =>
+  | append_singleton Ps P ih =>
+    rw [multiApp_tail]
     apply sn_app
-    · cases lc_MNPs with grind [sn_app_left]
-    · grind [sn_app_right]
+    · grind [cases LC, multiApp_tail, sn_app_left]
+    · grind [multiApp_tail, 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⟩
-      · cases Ps' with grind
+      · induction Ps' using List.reverseRecOn with grind [multiApp_tail]
       · 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]
         · 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)
             _ ↠βᶠ Q' ^ P' := by
               rw [Relation.reflTransGen_iff_eq_or_transGen] at ⊢ innerSteps h_st2
               right
-              cases lc_MNPs
               refine Relation.TransGen.single (Xi.base (Beta.beta ?_ ?_))
-              all_goals grind only [→ step_lc_r]
+              all_goals grind
 
 end LambdaCalculus.LocallyNameless.Untyped.Term