feat(untyped): the Leftmost Reduction Theorem

Cslib.lean

@@ -138,6 +138,7 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Safety
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.StrongNorm
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Basic
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.BetaAt
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.CallByName
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Congruence
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
@@ -147,6 +148,7 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaEta
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEta
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEtaConfluence
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LeftmostReduction
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiApp
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiSubst
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties

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

@@ -0,0 +1,223 @@
+/-
+Copyright (c) 2026 Maximiliano Onofre Martínez. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Maximiliano Onofre Martínez
+-/
+
+module
+
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.CallByName
+
+/-! # Redex Positions
+
+This module defines β-reduction at a given redex position and proves its basic properties.
+
+## Reference
+
+* [M. Copes, *A machine-checked proof of the Standardization Theorem in λ-calculus*][Copes2018]
+
+-/
+
+@[expose] public section
+
+set_option linter.unusedDecidableInType false
+
+namespace Cslib
+
+universe u
+
+variable {Var : Type u}
+
+namespace LambdaCalculus.LocallyNameless.Untyped.Term
+
+/-- The number of β-redexes occurring in a term. -/
+@[grind]
+def countRedexes : Term Var → Nat
+| fvar _        => 0
+| bvar _        => 0
+| abs m         => countRedexes m
+| app (abs m) n => countRedexes m + countRedexes n + 1
+| app m n       => countRedexes m + countRedexes n
+
+/-- `BetaAt i M N` reduces the redex at position `i` of `M` to obtain `N`;
+    positions are counted from left to right. -/
+inductive BetaAt : Nat → Term Var → Term Var → Prop
+/-- The outermost redex sits at position `0`. -/
+| outer : LC (abs M) → LC N → BetaAt 0 (app (abs M) N) (M ^ N)
+/-- Reducing the operator advances the position by one when the operator is an abstraction. -/
+| appL : BetaAt i M M' → BetaAt (i + if IsAbs M then 1 else 0) (app M N) (app M' N)
+/-- Reducing the operand adds the operator's redex count, plus one when it is an abstraction. -/
+| appR : BetaAt i M M' →
+    BetaAt (i + countRedexes N + if IsAbs N then 1 else 0) (app N M) (app N M')
+/-- Reducing under a binder keeps the position. -/
+| abs (xs : Finset Var) :
+    (∀ x ∉ xs, BetaAt i (M ^ fvar x) (M' ^ fvar x)) → BetaAt i (abs M) (abs M')
+
+variable {L L' M M' N N' P : Term Var} {a b i m n : Nat}
+
+/-- Reducing a non-abstraction operator keeps the position. -/
+lemma BetaAt.appNoAbsL (h : BetaAt i M M') (hna : ¬IsAbs M) :
+    BetaAt i (app M N) (app M' N) := by
+  simpa [if_neg hna] using h.appL
+
+/-- Reducing an abstraction operator advances the position by one. -/
+lemma BetaAt.appAbsL (h : BetaAt i M M') (ha : IsAbs M) :
+    BetaAt (i + 1) (app M N) (app M' N) := by
+  simpa [if_pos ha] using h.appL
+
+/-- Reducing the operand adds the redex count of a non-abstraction operator. -/
+lemma BetaAt.appNoAbsR (h : BetaAt i M M') (hna : ¬IsAbs N) :
+    BetaAt (i + countRedexes N) (app N M) (app N M') := by
+  simpa [if_neg hna] using h.appR (N := N)
+
+/-- Reducing the operand adds the redex count of an abstraction operator, plus one. -/
+lemma BetaAt.appAbsR (h : BetaAt i M M') (ha : IsAbs N) :
+    BetaAt (i + countRedexes N + 1) (app N M) (app N M') := by
+  simpa [if_pos ha] using h.appR (N := N)
+
+/-- Opening with a free variable preserves the number of redexes. -/
+lemma countRedexes_openRec_fvar (M : Term Var) (k : Nat) (x : Var) :
+    countRedexes (M⟦k ↝ fvar x⟧) = countRedexes M := by
+  induction M generalizing k with
+  | bvar j => simp only [openRec_bvar]; split <;> rfl
+  | fvar => rfl
+  | abs M ih => grind [openRec_abs]
+  | app L R ihL ihR => cases L <;> grind [openRec_bvar, openRec_app, openRec_abs]
+
+/-- Opening the outermost binder with a free variable preserves the number of redexes. -/
+lemma countRedexes_open_fvar (M : Term Var) (x : Var) :
+    countRedexes (M ^ fvar x) = countRedexes M :=
+  countRedexes_openRec_fvar M 0 x
+
+/-- An application has at least as many redexes as its operator and operand combined. -/
+lemma countRedexes_app_le (M N : Term Var) :
+    countRedexes M + countRedexes N ≤ countRedexes (app M N) := by
+  cases M <;> grind
+
+/-- An application with an abstraction operator has one more redex than its parts. -/
+lemma countRedexes_app_abs {M : Term Var} (ha : IsAbs M) (N : Term Var) :
+    countRedexes (app M N) = countRedexes M + countRedexes N + 1 := by
+  cases ha
+  grind
+
+/-- Contracting a redex of an abstraction yields an abstraction. -/
+lemma BetaAt.isAbs_r (h : BetaAt i M N) (ha : IsAbs M) : IsAbs N := by
+  cases ha
+  cases h
+  exact .abs _
+
+/-- The source of a Call-by-Name step is never an abstraction. -/
+lemma cbn_not_isAbs (h : M ⭢ₙ N) : ¬IsAbs M := by
+  intro ha
+  cases ha
+  trivial
+
+/-- A single Call-by-Name step contracts the redex at position `0`. -/
+lemma BetaAt.of_cbn_step (h : M ⭢ₙ N) : BetaAt 0 M N := by
+  induction h with
+  | base h_beta =>
+    cases h_beta with
+    | beta lc_M lc_N => exact .outer lc_M lc_N
+  | app _ step_M ih => exact .appNoAbsL ih (cbn_not_isAbs step_M)
+
+/-- Renaming a free variable preserves the number of redexes. -/
+lemma countRedexes_subst_fvar [DecidableEq Var] (M : Term Var) (x y : Var) :
+    countRedexes (M[x := fvar y]) = countRedexes M := by
+  induction M with
+  | fvar z => simp only [subst_fvar]; split <;> rfl
+  | bvar => rfl
+  | abs M ih => grind
+  | app L R ihL ihR => cases L <;> grind
+
+/-- Renaming a free variable preserves being an abstraction. -/
+lemma isAbs_subst_fvar [DecidableEq Var] {x y : Var} : IsAbs (M[x := fvar y]) ↔ IsAbs M := by
+  cases M <;> grind
+
+/-- A `BetaAt` step is a full β-step. -/
+lemma BetaAt.to_step [DecidableEq Var] (h : BetaAt i M N) (lc : LC M) : M ⭢βᶠ N := by
+  induction h with
+  | outer lc_M lc_N => exact .base (.beta lc_M lc_N)
+  | appL _ ih =>
+    cases lc with
+    | app lc_L lc_R => exact .appR lc_R (ih lc_L)
+  | appR _ ih =>
+    cases lc with
+    | app lc_L lc_R => exact .appL lc_L (ih lc_R)
+  | abs xs _ ih =>
+    cases lc with
+    | abs ys _ h_body =>
+      apply Xi.abs (xs ∪ ys)
+      intro z hz
+      exact ih z (by grind) (h_body z (by grind))
+
+variable [HasFresh Var]
+
+/-- The position of a contracted redex is at most the redex count of the result. -/
+lemma BetaAt.le_countRedexes (h : BetaAt i M N) : i ≤ countRedexes N := by
+  induction h with
+  | outer => exact Nat.zero_le _
+  | appL step =>
+    split
+    · rw [countRedexes_app_abs (step.isAbs_r (by assumption))]
+      omega
+    · exact le_trans (by omega) (countRedexes_app_le _ _)
+  | appR =>
+    split
+    · rw [countRedexes_app_abs (by assumption)]
+      omega
+    · exact le_trans (by omega) (countRedexes_app_le _ _)
+  | abs xs =>
+    have := fresh_exists xs
+    grind [countRedexes_open_fvar]
+
+variable [DecidableEq Var]
+
+/-- Renaming a free variable preserves the position of the contracted redex. -/
+lemma BetaAt.rename (h : BetaAt i M M') (x y : Var) :
+    BetaAt i (M[x := fvar y]) (M'[x := fvar y]) := by
+  induction h with
+  | outer lc_M lc_N =>
+    rw [subst_open x (fvar y) _ _ (.fvar y)]
+    exact .outer (subst_lc lc_M (.fvar y)) (subst_lc lc_N (.fvar y))
+  | appL _ ih =>
+    split
+    · exact ih.appAbsL (isAbs_subst_fvar.mpr (by assumption))
+    · exact ih.appNoAbsL (mt isAbs_subst_fvar.mp (by assumption))
+  | appR _ ih =>
+    rw [← countRedexes_subst_fvar _ x y]
+    split
+    · exact ih.appAbsR (isAbs_subst_fvar.mpr (by assumption))
+    · exact ih.appNoAbsR (mt isAbs_subst_fvar.mp (by assumption))
+  | abs =>
+    apply BetaAt.abs <| free_union [fv] Var
+    grind
+
+/-- Contracting a redex preserves local closure. -/
+lemma BetaAt.lc_r (h : BetaAt i M M') (lc : LC M) : LC M' := by
+  induction h with
+  | outer lc_M lc_N => exact beta_lc lc_M lc_N
+  | appL _ ih =>
+    cases lc with
+    | app lc_L lc_R => exact .app (ih lc_L) lc_R
+  | appR _ ih =>
+    cases lc with
+    | app lc_L lc_R => exact .app lc_L (ih lc_R)
+  | abs xs _ ih =>
+    cases lc with
+    | abs ys _ h_body =>
+      apply LC.abs (xs ∪ ys)
+      intro z hz
+      exact ih z (by grind) (h_body z (by grind))
+
+/-- Closing a variable and abstracting preserves the position of the contracted redex. -/
+lemma BetaAt.abs_close {x : Var} (h : BetaAt i M M') (lc : LC M) :
+    BetaAt i (M⟦0 ↜ x⟧.abs) (M'⟦0 ↜ x⟧.abs) := by
+  apply BetaAt.abs ∅
+  intro z _
+  have lc' := h.lc_r lc
+  have hr : BetaAt i (M[x := fvar z]) (M'[x := fvar z]) := h.rename x z
+  grind
+
+end LambdaCalculus.LocallyNameless.Untyped.Term
+
+end Cslib

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

@@ -86,6 +86,16 @@ attribute [scoped grind .] LC.fvar LC.app
 inductive Value : Term Var → Prop
 | abs (e : Term Var) : e.abs.LC → e.abs.Value
 
+/-- `IsAbs m` holds when `m` is an abstraction. -/
+@[scoped grind]
+inductive IsAbs : Term Var → Prop
+| abs (m : Term Var) : IsAbs (abs m)
+
+instance (m : Term Var) : Decidable (IsAbs m) := by
+  cases m
+  case abs => exact isTrue (.abs _)
+  all_goals exact isFalse (by intro _; contradiction)
+
 set_option linter.tacticAnalysis.verifyGrindOnly false in
 /-- `M` is `LcAt 0` if and only if `M` is locally closed. -/
 theorem lcAt_iff_LC (M : Term Var) [HasFresh Var] : LcAt 0 M ↔ M.LC := by

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

@@ -0,0 +1,142 @@
+/-
+Copyright (c) 2026 Maximiliano Onofre Martínez. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Maximiliano Onofre Martínez
+-/
+
+module
+
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StandardReduction
+
+/-! # The Leftmost Reduction Theorem
+
+## Reference
+
+* [M. Copes, *A machine-checked proof of the Standardization Theorem in λ-calculus*][Copes2018]
+
+-/
+
+@[expose] public section
+
+set_option linter.unusedDecidableInType false
+
+namespace Cslib
+
+universe u
+
+variable {Var : Type u}
+
+namespace LambdaCalculus.LocallyNameless.Untyped.Term
+
+/-- A term is in normal form when it contains no β-redexes. -/
+@[grind]
+def BetaNormal (m : Term Var) : Prop := countRedexes m = 0
+
+/-- Leftmost reduction: a β-reduction contracting the redex at position 0. -/
+@[reduction_sys "ℓ"]
+abbrev Leftmost : Term Var → Term Var → Prop := BetaAt 0
+
+variable {L L' M M' N : Term Var} {i : Nat}
+
+/-- In a normal-form application, both sides are normal and the operator is not an
+    abstraction. -/
+lemma BetaNormal.app_inv (h : BetaNormal (app L M)) :
+    ¬IsAbs L ∧ BetaNormal L ∧ BetaNormal M := by
+  cases L <;> grind [countRedexes]
+
+/-- The body of a normal-form abstraction opens to a normal form. -/
+lemma BetaNormal.abs_open {x : Var} (h : BetaNormal (abs M)) : BetaNormal (M ^ fvar x) := by
+  rw [BetaNormal, countRedexes_open_fvar]
+  exact h
+
+/-- Leftmost reduction preserves being an abstraction. -/
+lemma Leftmost.steps_isAbs_r (h : M ↠ℓ N) (ha : IsAbs M) : IsAbs N := by
+  induction h with
+  | refl => exact ha
+  | tail _ step ih => exact step.isAbs_r ih
+
+/-- Left congruence for leftmost reduction, provided the target is not an abstraction. -/
+lemma Leftmost.steps_app_l_cong (h : L ↠ℓ L') (hna : ¬IsAbs L') :
+    app L M ↠ℓ app L' M := by
+  induction h
+  case refl => rfl
+  case tail P _ _ step ih =>
+    have hnb : ¬IsAbs P := mt step.isAbs_r hna
+    exact (ih hnb).tail (step.appNoAbsL hnb)
+
+/-- Reducing the operand across a non-abstraction normal form keeps the position. -/
+lemma BetaAt.app_r_cong (h : BetaAt i M M') (hL : BetaNormal L) (hna : ¬IsAbs L) :
+    BetaAt i (app L M) (app L M') := by
+  have := h.appNoAbsR hna
+  rwa [hL] at this
+
+/-- Right congruence for leftmost reduction, provided the operator is a non-abstraction
+    normal form. -/
+lemma Leftmost.steps_app_r_cong (h : M ↠ℓ M') (hL : BetaNormal L) (hna : ¬IsAbs L) :
+    app L M ↠ℓ app L M' := by
+  induction h with
+  | refl => rfl
+  | tail _ step ih => exact ih.tail (step.app_r_cong hL hna)
+
+/-- Congruence for leftmost reduction on applications whose reduced operator is a
+    non-abstraction normal form. -/
+lemma Leftmost.steps_app_cong (hL : L ↠ℓ L') (hM : M ↠ℓ M')
+    (hnf : BetaNormal L') (hna : ¬IsAbs L') : app L M ↠ℓ app L' M' :=
+  (steps_app_l_cong hL hna).trans (steps_app_r_cong hM hnf hna)
+
+/-- Call-by-Name reduction is contained in leftmost reduction. -/
+lemma Leftmost.of_cbn (h : M ↠ₙ N) : M ↠ℓ N := by
+  induction h with
+  | refl => rfl
+  | tail _ step ih => exact ih.tail (BetaAt.of_cbn_step step)
+
+variable [DecidableEq Var] [HasFresh Var]
+
+/-- Leftmost reduction preserves local closure. -/
+lemma Leftmost.steps_lc_r (h : M ↠ℓ M') (lc : LC M) : LC M' := by
+  induction h with
+  | refl => exact lc
+  | tail _ step ih => exact step.lc_r ih
+
+/-- Leftmost reduction is preserved by closing a variable and abstracting. -/
+lemma Leftmost.steps_abs_close {x : Var} (h : M ↠ℓ M') (lc : LC M) :
+    (M⟦0 ↜ x⟧.abs) ↠ℓ (M'⟦0 ↜ x⟧.abs) := by
+  induction h with
+  | refl => rfl
+  | tail hs step ih => exact ih.tail (step.abs_close (steps_lc_r hs lc))
+
+/-- Cofinite congruence rule for leftmost reduction under an abstraction. -/
+lemma Leftmost.steps_abs_cong (xs : Finset Var)
+    (cofin : ∀ x ∉ xs, (M ^ fvar x) ↠ℓ (M' ^ fvar x)) (lc : LC (abs M)) :
+    abs M ↠ℓ abs M' := by
+  have ⟨w, _⟩ := fresh_exists <| free_union [fv] Var
+  rw [open_close w M 0 (by grind), open_close w M' 0 (by grind)]
+  have hstep := cofin w (by grind)
+  have hlc := beta_lc lc (.fvar w)
+  exact steps_abs_close hstep hlc
+
+/-- A standard reduction to a normal form is a leftmost reduction. -/
+theorem Leftmost.of_standard (h : M ⭢ₛ N) (hn : BetaNormal N) : M ↠ℓ N := by
+  induction h
+  case fvar x => rfl
+  case app _ _ ihL ihM =>
+    have ⟨hna, hL', hM'⟩ := hn.app_inv
+    exact steps_app_cong (ihL hL') (ihM hM') hL' hna
+  case abs xs h_body ih =>
+    have lc := (Standard.abs xs h_body).lc_l
+    apply steps_abs_cong xs _ lc
+    intro x hx
+    exact ih x hx hn.abs_open
+  case rdx M N M' _ lc_M lc_N cbn std_P ih =>
+    have s1 : M.app N ↠ℓ M'.abs.app N := of_cbn (CBN.steps_app_l_cong cbn lc_N)
+    have s2 : M'.abs.app N ⭢ℓ M' ^ N := .outer (CBN.steps_lc_r lc_M cbn) lc_N
+    exact (s1.tail s2).trans (ih hn)
+
+/-- The leftmost reduction theorem: if a term β-reduces to a normal form, then leftmost
+    reduction reaches it. -/
+theorem Leftmost.normalization (lc : LC M) (h : M ↠βᶠ N) (hn : BetaNormal N) : M ↠ℓ N :=
+  of_standard (.standardization lc h) hn
+
+end LambdaCalculus.LocallyNameless.Untyped.Term
+
+end Cslib