feat: prove confluence for βη-reduction

Cslib.lean

@@ -94,6 +94,7 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Basic
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Congruence
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaConfluence
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaEtaConfluence
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEta
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEtaConfluence
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt

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

@@ -63,13 +63,22 @@ theorem redex_app_l_cong (redex : M ↠βᶠ M') (lc_N : LC N) : app M N ↠β
 theorem redex_app_r_cong (redex : M ↠βᶠ M') (lc_N : LC N) : app N M ↠βᶠ app N M' := by
   induction redex <;> grind
 
+/- Single reduction `app M (fvar x) ⭢βᶠ N` implies reduction on `M` or a root beta step. -/
+@[scoped grind →]
+lemma invert_step_app_fvar (step : app M (fvar x) ⭢βᶠ N) :
+    (∃ M', N = app M' (fvar x) ∧ M ⭢βᶠ M') ∨ (∃ M1, M = abs M1 ∧ N = M1 ^ fvar x) := by
+  cases step
+  case base h => cases h with | beta => exact .inr ⟨_, rfl, rfl⟩
+  case appR step_M _ => exact .inl ⟨_, rfl, step_M⟩
+  all_goals grind [cases Xi]
+
 variable [HasFresh Var] [DecidableEq Var]
 
 /-- The right side of a reduction is locally closed. -/
 @[scoped grind →]
 lemma step_lc_r (step : M ⭢βᶠ M') : LC M' := by
   induction step
-  case' abs => constructor; assumption
+  case abs => constructor; assumption
   all_goals grind
 
 lemma steps_lc_or_rfl {M M' : Term Var} (redex : M ↠βᶠ M') : (LC M ∧ LC M') ∨ M = M' := by
@@ -88,6 +97,16 @@ lemma redex_subst_cong (s s' : Term Var) (x y : Var) (step : s ⭢βᶠ s') :
     s [ x := fvar y ] ⭢βᶠ s' [ x := fvar y ] :=
   redex_subst_cong_lc _ _ _ _ step (.fvar y)
 
+/-- An β-reduction step does not introduce new free variables. -/
+lemma step_not_fv (step : M ⭢βᶠ N) (hw : w ∉ M.fv) : w ∉ N.fv := by
+  induction step with
+  | base h => cases h with | beta => grind [open_preserve_not_fvar]
+  | abs =>
+    have ⟨x, _⟩ := fresh_exists <| free_union [fv] Var
+    have := open_close x
+    grind [close_preserve_not_fvar, open_fresh_preserve_not_fvar]
+  | _ => grind
+
 /-- Abstracting then closing preserves a single reduction. -/
 lemma step_abs_close {x : Var} (step : M ⭢βᶠ M') : M⟦0 ↜ x⟧.abs ⭢βᶠ M'⟦0 ↜ x⟧.abs := by
   grind [Xi.abs ∅, redex_subst_cong]

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

@@ -0,0 +1,106 @@
+/-
+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.FullBetaConfluence
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEtaConfluence
+
+@[expose] public section
+
+set_option linter.unusedDecidableInType false
+
+/-! # βη-Confluence for the λ-calculus
+
+## Reference
+
+* [T. Nipkow, *More Church-Rosser Proofs (in Isabelle/HOL)*][Nipkow2001]
+
+-/
+
+namespace Cslib
+
+universe u
+
+variable {Var : Type u}
+variable [HasFresh Var] [DecidableEq Var]
+
+namespace LambdaCalculus.LocallyNameless.Untyped.Term
+
+open Relation
+
+/-- Full βη-reduction. -/
+@[reduction_sys "βηᶠ"]
+abbrev FullBetaEta : Term Var → Term Var → Prop := FullBeta ⊔ FullEta
+
+open FullEta FullBeta in
+/-- η-reduction and β-reduction strongly commute. -/
+lemma stronglyCommute_eta_beta : StronglyCommute (@FullEta Var) FullBeta := by
+  intro x y₁ y₂ h₁ st_beta
+  induction st_beta generalizing y₁
+  case base h1_b =>
+    cases h1_b
+    case beta M N _ _ =>
+      cases h₁
+      case base h => cases h
+      case appL v _ _ =>
+        use M ^ v
+        grind [step_open_cong_r]
+      case appR u st_eta_absM _ =>
+        have := step_lc_r st_eta_absM
+        cases st_eta_absM
+        case base h => use (disch := grind) app u N
+        case abs M_eta xs _ =>
+          have ⟨_, hz⟩ := fresh_exists (xs ∪ N.fv ∪ M.fv ∪ M_eta.fv)
+          use M_eta ^ N
+          grind [step_subst_cong_l]
+  case appL Z _ N _ _ ih =>
+    cases h₁
+    case base h => cases h
+    case appL _ _ st =>
+      use app Z (ih st).choose
+      grind [FullEta.redex_app_r_cong]
+    case appR z_red _ _ => use (disch := grind) app z_red N
+  case appR M _ Z _ _ ih =>
+    cases h₁
+    case base h => cases h
+    case appL z_red _ _ => use (disch := grind) app Z z_red
+    case appR _ st _ =>
+      use app (ih st).choose M
+      grind [FullEta.redex_app_l_cong]
+  case abs M N xs st_body_beta ih =>
+    cases h₁
+    case base h_eta =>
+      cases h_eta with | eta =>
+        have ⟨w, _⟩ := fresh_exists <| free_union [fv] Var
+        have st_beta_w : app y₁ (fvar w) ⭢βᶠ N ^ fvar w := by grind [st_body_beta w]
+        rcases invert_step_app_fvar st_beta_w with ⟨u', _, st_u⟩ | ⟨u1, _, _⟩
+        · use u'
+          grind [open_eq_app ?_ (step_not_fv st_u ?_)]
+        · use abs u1
+          grind [open_injective w N u1]
+    case abs S ys st_body_eta =>
+      have ⟨w, _⟩ := fresh_exists <| free_union [fv] Var
+      obtain ⟨K, h_beta, h_eta⟩ := ih w (by grind) (st_body_eta w (by grind))
+      use abs (K ^* w)
+      constructor
+      · cases h_beta with
+        | refl => grind [open_close]
+        | single => exact .single (Xi.abs {w} (by grind [FullBeta.redex_subst_cong]))
+      · rw [open_close w N 0 (by grind)]
+        exact FullEta.redex_abs_close h_eta (FullBeta.step_lc_r (st_body_beta w (by grind)))
+
+open Commute in
+/-- βη-reduction is confluent. -/
+theorem confluent_beta_eta : Confluent (@FullBetaEta Var) := by
+  apply join_confluent
+  · exact confluence_beta
+  · exact stronglyConfluent_eta.toConfluent
+  exact symmetric stronglyCommute_eta_beta.toCommute
+
+end LambdaCalculus.LocallyNameless.Untyped.Term
+
+end Cslib

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

@@ -12,6 +12,8 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Congruence
 
 public section
 
+set_option linter.unusedDecidableInType false
+
 /-! # η-reduction for the λ-calculus -/
 
 namespace Cslib
@@ -24,13 +26,13 @@ namespace LambdaCalculus.LocallyNameless.Untyped.Term
 
 /-- A single η-reduction step. -/
 @[scoped grind]
-inductive BaseEta : Term Var → Term Var → Prop
+inductive Eta : Term Var → Term Var → Prop
 /-- The eta rule: λx. M x ⟶ M, provided x is not free in M. -/
-| eta : LC M → BaseEta (abs (app M (bvar 0))) M
+| eta : LC M → Eta (abs (app M (bvar 0))) M
 
 /-- Full η-reduction, defined as the congruence closure of the base η-rule. -/
 @[reduction_sys "ηᶠ"]
-abbrev FullEta : Term Var → Term Var → Prop := Xi BaseEta
+abbrev FullEta : Term Var → Term Var → Prop := Xi Eta
 
 namespace FullEta
 
@@ -42,6 +44,14 @@ lemma step_lc_r (step : M ⭢ηᶠ M') : LC M' := by
   refine Xi.step_lc_r ?_ step
   grind
 
+/-- Left congruence rule for application in multiple reduction. -/
+theorem redex_app_l_cong (redex : M ↠ηᶠ M') (lc_N : LC N) : app M N ↠ηᶠ app M' N := by
+  induction redex <;> grind
+
+/-- Right congruence rule for application in multiple reduction. -/
+theorem redex_app_r_cong (redex : M ↠ηᶠ M') (lc_N : LC N) : app N M ↠ηᶠ app N M' := by
+  induction redex <;> grind
+
 /- Single reduction `app M (fvar x) ⭢ηᶠ N` implies `N = app M' (fvar x)` for some M' -/
 @[scoped grind →]
 lemma invert_step_app_fvar (step : (app M (fvar x)) ⭢ηᶠ N) :
@@ -69,6 +79,65 @@ lemma eta_subst_fvar {x y : Var} (step : M ⭢ηᶠ M') : M [ x := fvar y ] ⭢
   | abs => grind [Xi.abs <| free_union Var]
   | _ => grind
 
+/-- Abstracting then closing preserves a single η-reduction step. -/
+lemma step_abs_close {x} (step : M ⭢ηᶠ M') (lc_M : LC M) : (M ^* x).abs ⭢ηᶠ (M' ^* x).abs := by
+  grind [Xi.abs ∅]
+
+/-- Abstracting then closing preserves multiple reductions. -/
+lemma redex_abs_close {x} (steps : M ↠ηᶠ M') (lc_M : LC M) : (M ^* x).abs ↠ηᶠ (M' ^* x).abs := by
+  induction steps using Relation.ReflTransGen.head_induction_on
+  case refl => exact .refl
+  case head b c st_bc _ ih => exact .head (step_abs_close st_bc lc_M) (ih (step_lc_r st_bc))
+
+/-- Multiple reduction of opening implies multiple reduction of abstraction. -/
+theorem redex_abs_cong {M M' : Term Var} (xs : Finset Var)
+    (cofin : ∀ x ∉ xs, (M ^ fvar x) ↠ηᶠ M' ^ fvar x) (lc_M : LC M.abs) :
+    M.abs ↠ηᶠ M'.abs := by
+  cases lc_M
+  case abs L hL =>
+    have ⟨x, _⟩ := fresh_exists <| free_union [fv] Var
+    rw [open_close x M 0, open_close x M' 0]
+    all_goals grind [redex_abs_close (x := x) (cofin x ?_) (hL x ?_)]
+
+/- `t ⭢ηᶠ t'` implies `s [ x := t ] ↠ηᶠ s [ x := t' ]`. -/
+lemma step_subst_cong_r {x : Var} (s t t' : Term Var) (st : t ⭢ηᶠ t') (lc_s : LC s) (lc_t : LC t) :
+    s [ x := t ] ↠ηᶠ s [ x := t' ] := by
+  induction lc_s generalizing t t' with
+  | fvar => grind
+  | app hl hr ih_l ih_r =>
+    trans
+    · exact redex_app_l_cong (ih_l t t' st lc_t) (subst_lc hr lc_t)
+    · exact redex_app_r_cong (ih_r t t' st lc_t) (subst_lc hl (step_lc_r st))
+  | abs L body h_lc_body ih =>
+    apply redex_abs_cong (L ∪ {x})
+    · intro z
+      grind =>
+        have : (body ^ fvar z)[x := t] ↠ηᶠ (body ^ fvar z)[x := t']
+        finish
+    · exact subst_lc (LC.abs L body h_lc_body) lc_t
+
+/- `steps_subst_cong_r` can be generalized to multiple reductions `t ↠ηᶠ t'`. -/
+lemma steps_subst_cong_r {x : Var} (s t t' : Term Var) (st : t ↠ηᶠ t') (lc_s : LC s) (lc_t : LC t) :
+    s [ x := t ] ↠ηᶠ s [ x := t' ] := by
+  induction st using Relation.ReflTransGen.head_induction_on
+  case refl => rfl
+  case head _ _ st _ ih => exact .trans (step_subst_cong_r s _ _ st lc_s lc_t) (ih (step_lc_r st))
+
+/- `t ⭢ηᶠ t'` implies `s ^ t ↠ηᶠ s ^ t'`. -/
+lemma step_open_cong_r {s t t' : Term Var} (lc_s : LC s.abs) (lc_t : LC t) (step : t ⭢ηᶠ t') :
+    (s ^ t) ↠ηᶠ s ^ t' := by
+  cases lc_s
+  case abs L hL =>
+    have ⟨x, _⟩ := fresh_exists <| free_union [fv] Var
+    grind [step_subst_cong_r (x := x) (s ^ fvar x) t t' step (hL x ?_) lc_t]
+
+/- `steps_open_cong_r` can be generalized to multiple reductions `t ↠ηᶠ t'`. -/
+lemma steps_open_cong_r {s t t' : Term Var} (lc_s : LC s.abs) (lc_t : LC t) (steps : t ↠ηᶠ t') :
+    (s ^ t) ↠ηᶠ s ^ t' := by
+  induction steps using Relation.ReflTransGen.head_induction_on
+  case refl => rfl
+  case head _ _ st _ ih => exact .trans (step_open_cong_r lc_s lc_t st) (ih (step_lc_r st))
+
 /- Closing a sequence of η-reduction steps over a fresh variable preserves the steps. -/
 open Relation in
 lemma close_eta_steps (hx_M : x ∉ M.fv) (st_M : ReflGen FullEta (M ^ fvar x) N) :
@@ -78,6 +147,21 @@ lemma close_eta_steps (hx_M : x ∉ M.fv) (st_M : ReflGen FullEta (M ^ fvar x) N
   | single st =>
     exact .single (Xi.abs {x} (by grind))
 
+/- `s ⭢ηᶠ s'` implies `s [ x := N ] ⭢ηᶠ s' [ x := N ]`. -/
+lemma step_subst_cong_l {x : Var} (s s' N : Term Var) (step : s ⭢ηᶠ s') (lc_N : LC N) :
+    s [ x := N ] ⭢ηᶠ s' [ x := N ] := by
+  induction step
+  case base h => cases h with | eta lc => exact Xi.base (.eta (subst_lc lc lc_N))
+  case abs => grind [Xi.abs <| free_union Var, subst_open_var]
+  all_goals grind
+
+/- `steps_subst_cong_l` can be generalized to multiple reductions `s ↠ηᶠ s'`. -/
+lemma steps_subst_cong_l {x : Var} (s s' N : Term Var) (steps : s ↠ηᶠ s') (lc_N : LC N) :
+    s [ x := N ] ↠ηᶠ s' [ x := N ] := by
+  induction steps with
+  | refl => rfl
+  | tail _ step ih => grind [step_subst_cong_l]
+
 end LambdaCalculus.LocallyNameless.Untyped.Term.FullEta
 
 end Cslib

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

@@ -46,7 +46,7 @@ lemma stronglyConfluent_eta : StronglyConfluent (@FullEta Var) := by
         have ⟨w, _⟩ := fresh_exists <| free_union [fv] Var
         have ⟨M', _, _⟩ := invert_step_app_fvar <| st_body w <| by grind
         use M'
-        grind [→ BaseEta.eta, step_not_fv, open_eq_app]
+        grind [→ Eta.eta, step_not_fv, open_eq_app]
   case appL Z _ N _ _ ih =>
     cases h₂
     case base h => cases h
@@ -64,7 +64,7 @@ lemma stronglyConfluent_eta : StronglyConfluent (@FullEta Var) := by
       have ⟨w, _⟩ := fresh_exists <| free_union [fv] Var
       have ⟨M', _, _⟩ := invert_step_app_fvar <| st_M_N w (by grind)
       use M'
-      grind [→ BaseEta.eta, step_not_fv, open_eq_app]
+      grind [→ Eta.eta, step_not_fv, open_eq_app]
     case abs N _ st_M_N =>
       have ⟨x, _⟩ := fresh_exists <| free_union [fv] Var
       have ⟨w, _⟩ := ih x (by grind) (z := N ^ fvar x) (st_M_N x (by grind))

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

@@ -63,6 +63,11 @@ lemma open_fresh_preserve_not_fvar {k x y} (m : Term Var) (nmem : x ∉ m.fv) (n
     x ∉ (m⟦k ↝ fvar y⟧).fv := by
   induction m generalizing k <;> grind
 
+/-- Opening preserves free variables. -/
+lemma open_preserve_not_fvar {k x} (m n : Term Var) (nmem_m : x ∉ m.fv) (nmem_n : x ∉ n.fv) :
+    x ∉ (m⟦k ↝ n⟧).fv := by
+  induction m generalizing k <;> grind
+
 /-- Substitution preserves free variables. -/
 lemma subst_preserve_not_fvar {x y : Var} (m n : Term Var) (nmem : x ∉ m.fv ∪ n.fv) :
     x ∉ (m [y := n]).fv := by