feat: MultiAppForStrongNorm

Cslib.lean

@@ -91,6 +91,7 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Basic
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaConfluence
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiApp
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
 public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
 public import Cslib.Logics.HML.Basic

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

@@ -0,0 +1,141 @@
+/-
+Copyright (c) 2025 David Wegmann. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Wegmann
+-/
+
+
+module
+
+
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
+
+set_option linter.unusedDecidableInType false
+
+@[expose] public section
+
+namespace Cslib
+
+universe u
+
+variable {Var : Type u}
+
+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 => Term.app (multiApp f as) a
+
+/-- A list of arguments performs a single reduction step
+
+    [x₁, ..., xᵢ ..., xₙ] ⭢βᶠ [x₁, ..., xᵢ', ..., xₙ]
+
+    if one of the arguments performs a single step xᵢ ⭢βᶠ xᵢ'
+    and the rest of the arguments are locally closed. -/
+@[scoped grind, reduction_sys "lβᶠ"]
+inductive ListFullBeta : List (Term Var) → List (Term Var) → Prop where
+/-- head of the list performs a single reduction step, the rest are locally closed -/
+| step : N ⭢βᶠ N' → (∀ N ∈ Ns, LC N) → ListFullBeta (N :: Ns) (N' :: Ns)
+/-- given a list that already contains a step, we can add locally closed terms to the front -/
+| cons : LC N → ListFullBeta Ns Ns' → ListFullBeta (N :: Ns) (N :: Ns')
+
+variable {M M' : Term Var} {Ns Ns' : List (Term Var)}
+
+/-- 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]
+
+/-- 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 [FullBeta.appR]
+
+/-- 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) :
+    M.multiApp Ns ↠βᶠ M'.multiApp Ns := by
+  induction steps <;> grind
+
+/-- 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 [FullBeta.appL, FullBeta.appR]
+
+/-- 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 [FullBeta.appL, FullBeta.appR]
+
+/-- 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:
+
+    Q = (λ M') N P₁ ... Pₙ where M ⭢βᶠ M' or
+    Q = (λ M) N' P₁ ... Pₙ where N ⭢βᶠ N' or
+    Q = (λ M) N P₁' ... Pₙ' where P_i ⭢βᶠ P_i' for some i or
+    Q = (M ^ N) P₁ ... Pₙ -/
+lemma invert_abs_multiApp_st {Ps} {M N Q : Term Var}
+  (h_red : multiApp (M.abs.app N) Ps ⭢βᶠ Q) :
+    (∃ M', M.abs ⭢βᶠ Term.abs M' ∧ Q = multiApp (M'.abs.app N) Ps) ∨
+    (∃ 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
+  | nil => grind [cases FullBeta]
+  | 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
+    cases h_red with
+    | beta => cases Ps <;> contradiction
+    | appR => grind [→ ListFullBeta.cons]
+    | appL => grind
+
+/-- If a term (λ M) N P₁ ... Pₙ reduces in multiple steps to Q, then either Q if of the form
+
+      Q = (λ M') N' P'₁ ... P'ₙ
+
+      or
+
+    we first reach an intermediate term of this shape,
+
+      (λ M) N P₁ ... Pₙ ↠βᶠ (λ M') N' P'₁ ... P'ₙ
+
+      then perform a beta reduction and reduce further to Q
+
+      (λ M') N' P'₁ ... P'ₙ ↠βᶠ M' ^ N' P'_₁ ... P'_ₙ ↠βᶠ Q
+
+   where M ↠βᶠ M' and N ↠βᶠ N' and P_i ↠βᶠ P_i' for all i -/
+lemma invert_abs_multiApp_mst {Ps} {M N Q : Term Var}
+  (h_red : multiApp (M.abs.app N) Ps ↠βᶠ Q) :
+    ∃ M' N' Ns', M.abs ↠βᶠ M'.abs ∧ N ↠βᶠ N' ∧ Ps ↠lβᶠ Ns' ∧
+                 (Q = multiApp (M'.abs.app N') Ns' ∨
+     (multiApp (M.abs.app N) Ps ↠βᶠ multiApp (M' ^ N') Ns' ∧
+                                     multiApp (M' ^ N') Ns' ↠βᶠ Q)) := by
+  induction h_red with
+  | refl => grind
+  | tail _ step ih =>
+    obtain ⟨_, _, _, _, _, _, h⟩ := ih
+    rcases h with heq | _
+    · subst heq
+      grind [invert_abs_multiApp_st step]
+    · grind [Relation.ReflTransGen.single]
+
+variable [DecidableEq Var] [HasFresh Var]
+
+/-- Just like ordinary beta reduction, the right-hand side
+    of a multi-application step is locally closed -/
+lemma multiApp_step_lc_r (step : Ns ⭢lβᶠ Ns') : ∀ N ∈ Ns', LC N := by
+  induction step <;> grind [FullBeta.step_lc_r]
+
+/-- Just like ordinary beta reduction, multiple steps of a argument list preserves local closure -/
+lemma multiApp_steps_lc (step : Ns ↠lβᶠ Ns') (H : ∀ N ∈ Ns, LC N) : ∀ N ∈ Ns', LC N := by
+  induction step <;> grind [FullBeta.step_lc_r, multiApp_step_lc_r]
+
+end LambdaCalculus.LocallyNameless.Untyped.Term
+
+end Cslib

CslibTests/GrindLint.lean

@@ -72,6 +72,8 @@ open_scoped_all Cslib
 #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullBeta.redex_app_l_cong
 #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullBeta.redex_app_r_cong
 #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.subst_intro
+#grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.ListFullBeta.cons
+#grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.ListFullBeta.step
 #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf.sub
 #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf.ty
 #grind_lint skip Cslib.Logic.HML.bisimulation_satisfies