feat(locallynameless): eta-postpone

Cslib.lean

@@ -227,8 +227,10 @@ 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.BetaNfLc
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.CallByName
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Congruence
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.EtaPostpone
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaConfluence
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaEta
@@ -239,9 +241,12 @@ 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.ParEta
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Size
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StandardReduction
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.WeakNorm
 public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
 public import Cslib.Languages.LambdaCalculus.Named.Untyped.Properties
 public import Cslib.Languages.Mech.Choreography.Basic

Cslib/Foundations/Relation/Confluence.lean

@@ -92,6 +92,47 @@ theorem Commute.isTrans_join₂_reflTransGen (h : Commute r₁ r₂) :
 theorem Confluent.isTrans_join_reflTransGen (h : Confluent r) : IsTrans α (Join (ReflTransGen r)) :=
   Commute.isTrans_join₂_reflTransGen h
 
+-- mirror of `SemiCommute.to_commute`
+theorem SemiDiamondCommute.to_diamond_commute (h : SemiDiamondCommute r₁ r₂) :
+  DiamondCommute (ReflTransGen r₁) (TransGen r₂) := by
+  intro a b₁ b₂ hab₁ hab₂
+  induction hab₁ with
+  | refl => use b₂
+  | tail hab hbb' ih =>
+    obtain ⟨d, hd, hd'⟩ := ih
+    obtain ⟨e, he, he'⟩ := h hbb' hd
+    use e, he, hd'.trans he'
+
+theorem semiDiamondCommute_iff_diamondCommute :
+    SemiDiamondCommute r₁ r₂ ↔ DiamondCommute (ReflTransGen r₁) (TransGen r₂) :=
+  ⟨fun h => h.to_diamond_commute, fun h => fun _ _ _ hxy₁ hxy₂ => h (.single hxy₁) hxy₂⟩
+
+theorem Commute.to_semiDiamondCommute (hc : Commute r₁ r₂) (h : TransGenCommute r₁ r₂) :
+  SemiDiamondCommute r₁ r₂ := by
+  intros x y z hxy hyz
+  induction hyz with
+  | single hyz => exact h hxy hyz
+  | tail h₁ h₂ h₃ =>
+    obtain ⟨w, hw₁, hw₂⟩ := h₃
+    obtain ⟨s, hs₁, hs₂⟩ := hc hw₂ (.single h₂)
+    exact ⟨s, hw₁.trans_left hs₁, hs₂⟩
+
+theorem SemiDiamondCommute.to_commute (h : SemiDiamondCommute r₁ r₂) : Commute r₁ r₂ := by
+  intro x y₁ y₂ hxy₁ hxy₂
+  rcases hxy₂.cases_head with rfl | ⟨c, hxc, hcy₂⟩
+  · exact ⟨y₁, .refl, hxy₁⟩
+  · obtain ⟨z, hz₁, hz₂⟩ := h.to_diamond_commute hxy₁ (TransGen.head' hxc hcy₂)
+    exact ⟨z, hz₁.to_reflTransGen, hz₂⟩
+
+theorem SemiDiamondCommute.to_transGenCommute (h : SemiDiamondCommute r₁ r₂) :
+    TransGenCommute r₁ r₂ :=
+  fun _ _ _ hxy₁ hxy₂ => h hxy₁ (.single hxy₂)
+
+theorem commute_and_transGenCommute_iff_semiDiamondCommute :
+    Commute r₁ r₂ ∧ TransGenCommute r₁ r₂ ↔ SemiDiamondCommute r₁ r₂ :=
+    ⟨fun ⟨hc, h⟩ => hc.to_semiDiamondCommute h,
+     fun h => ⟨h.to_commute, h.to_transGenCommute⟩⟩
+
 theorem SemiCommute.to_commute (h : SemiCommute r₁ r₂) : Commute r₁ r₂ := by
   intro a b₁ b₂ hab₁ hab₂
   induction hab₁ with

Cslib/Foundations/Relation/Defs.lean

@@ -92,6 +92,22 @@ abbrev StronglyConfluent (r : α → α → Prop) :=
 def StronglyCommute (r₁ r₂ : α → α → Prop) :=
   ∀ {x y₁ y₂}, r₁ x y₁ → r₂ x y₂ → ∃ z, ReflGen r₂ y₁ z ∧ ReflTransGen r₁ y₂ z
 
+/--
+`TransGenCommute r₁ r₂` states that a single step of `r₁` and a single step of `r₂`
+with the same source can be joined by a path along `r₂` from the first result and a
+reflexive-transitive path along `r₁` from the second result.
+-/
+abbrev TransGenCommute (r₁ r₂ : α → α → Prop) :=
+  ∀ ⦃x y₁ y₂⦄, r₁ x y₁ → r₂ x y₂ → ∃ z, TransGen r₂ y₁ z ∧ ReflTransGen r₁ y₂ z
+
+/--
+`SemiDiamondCommute r₁ r₂` is the asymmetric version of the commutation square where one
+branch takes a single `r₁`-step and the other takes a non-empty `r₂`-path. The two
+outcomes are then joinable by a further `r₂`-path and an `r₁`-reflexive-transitive path.
+-/
+abbrev SemiDiamondCommute (r₁ r₂ : α → α → Prop) :=
+  ∀ ⦃x y₁ y₂⦄, r₁ x y₁ → TransGen r₂ x y₂ → ∃ z, TransGen r₂ y₁ z ∧ ReflTransGen r₁ y₂ z
+
 /-! ### Normalization properties -/
 
 /-- An element is reducible with respect to a relation if there is a value it is related to. -/

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

@@ -0,0 +1,116 @@
+/-
+Copyright (c) 2025 Chris Henson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yijun Leng
+-/
+
+
+module
+
+public import Cslib.Foundations.Relation.Attr
+public import Cslib.Foundations.Relation.Defs
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.BetaAt
+
+/-! # Beta-normal forms in the locally nameless λ-calculus
+
+This file defines `BetaNfLc`, the inductive predicate of locally-closed β-normal forms.
+
+-/
+
+
+@[expose] public section
+
+set_option linter.unusedDecidableInType false
+
+namespace Cslib
+
+universe u
+
+namespace LambdaCalculus.LocallyNameless.Untyped.Term
+
+variable {Var : Type u}
+
+
+/-- BetaNfLc terms (locally closed β-normal forms) -/
+inductive BetaNfLc : Term Var → Prop where
+  | fvar (x : Var) : BetaNfLc (fvar x)
+  | app {M N : Term Var} : BetaNfLc M → ¬ M.IsAbs → BetaNfLc N → BetaNfLc (app M N)
+  | abs (xs : Finset Var) {M : Term Var} : (∀ x ∉ xs, BetaNfLc (M ^ fvar x)) → BetaNfLc M.abs
+
+/--
+`BetaNfLcNotAbs M` means that `M` is a locally closed β-normal form and is not an
+abstraction. -/
+abbrev BetaNfLcNotAbs (M : Term Var) : Prop := BetaNfLc M ∧ ¬ M.IsAbs
+
+theorem BetaNfLcNotAbs.fvar (x : Var) : BetaNfLcNotAbs (Term.fvar x) := ⟨BetaNfLc.fvar x, by grind⟩
+
+variable {M N : Term Var}
+
+theorem BetaNfLcNotAbs.app (hM : BetaNfLcNotAbs M) (hN : BetaNfLc N) : BetaNfLcNotAbs (app M N) :=
+  ⟨BetaNfLc.app hM.1 (by grind) hN, by grind⟩
+
+theorem BetaNfLcNotAbs.normal (h : BetaNfLcNotAbs M) : BetaNfLc M := h.1
+
+@[grind ->]
+theorem BetaNfLc.lc (h : BetaNfLc M) : LC M := by
+  induction h with
+  | fvar x => exact LC.fvar x
+  | app _ _ _ ihM ihN => exact LC.app ihM ihN
+  | abs xs _ ih => exact LC.abs xs _ ih
+
+theorem BetaNfLcNotAbs.lc (h : BetaNfLcNotAbs M) : LC M := h.1.lc
+
+variable [DecidableEq Var] [HasFresh Var]
+
+theorem BetaNfLc.betaNF (h : BetaNfLc M) : Relation.Normal FullBeta M := by
+  induction h with
+  | fvar x =>
+    rintro ⟨N, hN⟩
+    cases hN with | base hN => cases hN
+  | app _ _ _ _ _ =>
+    rintro ⟨z, hz⟩
+    cases hz <;> grind
+  | abs xs hM ih =>
+    rintro ⟨ys, hys⟩
+    cases hys with
+    | base hys => cases hys
+    | abs xs h =>
+        have ⟨x, _⟩ := fresh_exists <| free_union [fv] Var
+        exact ih x (by grind) ⟨_, h x (by grind)⟩
+
+theorem BetaNfLc.subst_fvar (h : BetaNfLc M) (x y : Var) : BetaNfLc (M[x:=Term.fvar y]) := by
+  induction h with
+  | fvar z =>
+      rw [Term.subst_fvar]
+      split <;> exact .fvar _
+  | abs xs hM ih =>
+    apply BetaNfLc.abs (xs ∪ { x }) (fun z hz => ?_)
+    convert ih z (by grind)
+    rw [Term.subst_open_var] <;> grind
+  | app _ h₁ h₂ h₃ h₄ =>
+    apply BetaNfLc.app h₃ (fun hC => ?_) h₄
+    rw [isAbs_subst_fvar] at hC
+    grind
+
+theorem betaNF_normal (hlc : LC M) (h : Relation.Normal FullBeta M) : BetaNfLc M := by
+  induction hlc with
+  | fvar x => exact BetaNfLc.fvar x
+  | abs hN e _ ih =>
+    apply BetaNfLc.abs (hN ∪ e.fv)
+      (fun x hx => ih x (by grind) (fun ⟨t, g⟩ => h ⟨(t^*x).abs, Xi.abs e.fv (fun y hy => ?_)⟩))
+    rw [close_open_to_subst _ _ _ (FullBeta.step_lc_r g) (by grind)]
+    have g := FullBeta.redex_subst_cong_lc _ _ (fvar y) x g (by grind)
+    rwa [<- subst_intro _ _ _ (by grind)] at g
+  | app m_lc n_lc hm hn =>
+    refine .app (hm (fun ⟨ _, hu⟩ => h ⟨ _, .appR n_lc hu⟩)) (fun hC => h ?_)
+                (hn (fun ⟨ _, hu⟩ => h ⟨ _, .appL m_lc hu⟩))
+    cases hC
+    exact ⟨_, Xi.base (Beta.beta m_lc n_lc)⟩
+
+theorem betaNF_iff : LC M /\ Relation.Normal FullBeta M ↔ BetaNfLc M :=
+  ⟨by grind [betaNF_normal], fun h => ⟨BetaNfLc.lc h, BetaNfLc.betaNF h⟩⟩
+
+end LambdaCalculus.LocallyNameless.Untyped.Term
+
+end Cslib

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

@@ -0,0 +1,147 @@
+/-
+Copyright (c) 2025 Chris Henson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yijun Leng
+-/
+
+
+module
+
+public import Cslib.Foundations.Relation.Confluence
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaEtaConfluence
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.ParEta
+
+/-!  # η-postpone theorems
+
+This file presents 5 postponement theorems for moving η-reduction behind
+β-reduction.
+
+## Main results
+
+* `transgen_postpone_eta_beta`: if `P →ηᶠ Q` and `Q →βᶠ R`, then there is a term
+  `S` with `P ↠β+ S` and `S ↠ηᶠ R`.
+* `commute_etastar_beta`: if `P ↠ηᶠ Q` and `Q ↠βᶠ R`, then there is a term
+  `S` with `P ↠βᶠ S` and `S ↠ηᶠ R`.
+* `semiDiamondCommute_eta_beta`: if `P →ηᶠ Q` and `Q ↠β+ R`, then there is a term
+  `S` with `P ↠β+ S` and `S ↠ηᶠ R`.
+* `diamondcommute_etaplus_betastar`: if `P ↠ηᶠ Q` and `Q ↠β+ R`, then there is
+  a term `S` with `P ↠β+ S` and `S ↠ηᶠ R`.
+* `eta_postpone`: if `P ↠βηᶠ Q`, then there is a term `S` such that
+  `P ↠βᶠ S` and `S ↠ηᶠ Q`.
+
+## Reference
+
+* [Y. Takahashi, *Parallel Reductions in λ-Calculus*][Takahashi1995]
+
+-/
+
+@[expose] public section
+
+set_option linter.unusedDecidableInType false
+
+namespace Cslib
+
+universe u
+
+namespace LambdaCalculus.LocallyNameless.Untyped.Term
+
+open Relation Function
+
+variable {Var : Type u} [DecidableEq Var] [HasFresh Var]
+
+/-- An η-step followed by a β-step can be postponed: if `P →ηᶠ Q` and `Q →βᶠ R`,
+then there exists `S` such that `TransGen FullBeta P S` and `S ↠ηᶠ R`. -/
+theorem transgen_postpone_eta_beta : TransGenCommute (swap (FullEta (Var := Var))) FullBeta := by
+  intros y x z hη hβ
+  induction hη generalizing z with
+  | base hη => cases hη with | eta h_lc =>
+  exact ⟨Term.abs (z.app (bvar 0)),
+        FullBeta.transgen_abs_cong ∅ (fun x hx => FullBeta.transgen_app_l (.fvar _)
+                  (.single (by rwa [open_lc _ _ _ h_lc, open_lc _ _ _ (FullBeta.step_lc_r hβ)]))),
+        .single (.base (.eta (FullBeta.step_lc_r hβ))) ⟩
+  | appL _ h ih =>
+    cases hβ with
+    | base hβ => cases hβ with | beta hm hn =>
+        refine ⟨_, .single (.base (.beta hm (FullEta.step_lc_l h))), ?_⟩
+        rw [reflTransGen_swap] at *
+        exact FullEta.step_open_cong_r hm h
+    | appL h1 h2 =>
+        obtain ⟨w, hw1, hw2⟩ := ih h2
+        refine ⟨_, FullBeta.transgen_app_r h1 hw1, ?_⟩
+        rw [reflTransGen_swap] at *
+        exact FullEta.redex_app_r_cong hw2 h1
+    | appR _ h2 =>  exact ⟨_, .single (.appR (FullEta.step_lc_l h) h2),
+                              .single (.appL (FullBeta.step_lc_r h2) h)⟩
+  | appR _ h ih =>
+    cases hβ with
+    | appL _ h2 => exact ⟨_, .single (.appL (FullEta.step_lc_l h) h2),
+                             .single (.appR (FullBeta.step_lc_r h2) h)⟩
+    | appR h1 h2 =>
+        obtain ⟨w, hw1, hw2⟩ := ih h2
+        refine ⟨_, FullBeta.transgen_app_l h1 hw1, ?_⟩
+        rw [reflTransGen_swap] at *
+        exact FullEta.redex_app_l_cong hw2 h1
+    | base hβ =>
+      cases hβ with | beta hm hz => cases h with
+        | abs xs h =>
+            refine ⟨_, .single (.base (.beta (FullEta.step_lc_l (Xi.abs xs h)) hz)), ?_⟩
+            rw [reflTransGen_swap] at *
+            exact FullEta.steps_open_cong_l xs (by grind) hz
+        | base h =>
+            cases h with | eta h =>
+              refine ⟨_, .head (.base (.beta ?_ hz)) (.single (.base (.beta ?_ (by grind)))), ?_⟩
+              · rw [<- lcAt_iff_LC] at *
+                simp_all only [LcAt, zero_add, Order.lt_one_iff, decide_true, Bool.and_true]
+                apply lcAt_le _ _ _ (by omega) hm
+              · rw [<- lcAt_iff_LC] at *
+                simp_all only [LcAt, zero_add]
+                rw [lcAt_openRec_iff_lcAt _ _ _ (lcAt_le _ _ _ (by omega) hz)]
+                exact lcAt_le _ _ _ (by omega) hm
+              · rw [<- lcAt_iff_LC] at *
+                rw [lcAt_openRec_above_lcAt _ _ 1 _ (by omega) (by grind)]
+                grind
+  | abs xs hx ih =>
+      cases hβ with | base hβ => cases hβ | abs ys hy =>
+        rename_i _ _ N
+        have ⟨x, _⟩ := fresh_exists <| free_union [fv] Var
+        obtain ⟨w, hw1, hw2⟩ := ih x (by grind) (hy x (by grind))
+        refine ⟨(w ^* x).abs, FullBeta.transgen_abs_cong (free_union [fv] Var) fun c hc => ?_, ?_⟩
+        · rw [close_open_to_subst _ _ _ ?_ (by grind)]
+          · have g := FullBeta.transgen_subst_cong _ _ (fvar c) x hw1 (by grind)
+            rw [subst_open, subst_fvar] at g <;> grind
+          · cases hw1 <;> apply FullBeta.step_lc_r <;> assumption
+        · rw [open_close_var x N (by grind)]
+          rw [reflTransGen_swap] at *
+          exact FullEta.redex_abs_close hw2
+
+/-- If `P ↠ηᶠ Q` and `Q ↠βᶠ R`, then there exists `S` such that `P ↠βᶠ S` and `S ↠ηᶠ R`. -/
+theorem commute_etastar_beta : Commute (swap FullEta) (FullBeta (Var := Var)) := by
+  intros _ _ _ hη hβ
+  simp only [<- reflTransGen_parallel_fullBeta] at hβ
+  rw [reflTransGen_swap] at hη
+  simp only [<- reflTransGen_parallel_fullEta] at hη
+  rw [<- reflTransGen_swap] at hη
+  obtain ⟨s, _, g⟩ := commute_parEta_parBeta hη hβ
+  refine ⟨s, by simp_all [← reflTransGen_parallel_fullBeta], ?_⟩
+  rw [reflTransGen_swap] at *
+  exact reflTransGen_le_of_le ParEta.le_reflTransGen_fullEta _ _ g
+
+/-- If `P →ηᶠ Q` and `Q ↠β+ R`, then there exists `P'` with `P ↠β+  P'` and `P' ↠ηᶠ R`. -/
+theorem semiDiamondCommute_eta_beta : SemiDiamondCommute (swap FullEta) (FullBeta (Var := Var)) :=
+  Commute.to_semiDiamondCommute commute_etastar_beta transgen_postpone_eta_beta
+
+/-- If `P ↠ηᶠ Q` and `Q ↠β+ R`, then there exists `P'` with `P ↠β+  P'` and `P' ↠ηᶠ R`. -/
+theorem diamondcommute_etaplus_betastar :
+    DiamondCommute (ReflTransGen (swap FullEta)) (TransGen (FullBeta (Var := Var))) :=
+  SemiDiamondCommute.to_diamond_commute semiDiamondCommute_eta_beta
+
+theorem eta_postpone {M N : Term Var} (h : M ↠βηᶠ N) : ∃ L, M ↠βᶠ L ∧ L ↠ηᶠ N := by
+  have g := (commute_equivalents.out 2 4 rfl rfl).mp (commute_etastar_beta (Var := Var)) N M
+  rw [sup_comm, reflTransGen_swap] at g
+  obtain ⟨L, g, _⟩ := g h
+  rw [reflTransGen_swap] at g
+  grind
+
+end LambdaCalculus.LocallyNameless.Untyped.Term
+
+end Cslib