From 072b238e0745ac72b3c41702a0c2a111fc3b5529 Mon Sep 17 00:00:00 2001 From: lengyijun Date: Mon, 5 Oct 2026 08:32:00 +0800 Subject: [PATCH 1/2] feat(Relation): add TransGenCommute, SemiDiamondCommute and related equivalences MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Introduce intermediate commutation notions between single-step and multi-step properties: - TransGenCommute: single r₁ + single r₂ join via TransGen r₂ and ReflTransGen r₁ - SemiDiamondCommute: single r₁ + TransGen r₂ join via TransGen r₂ and ReflTransGen r₁ Prove the corresponding implications and equivalences mirroring the existing SemiCommute ↔ Commute development, including: - SemiDiamondCommute ↔ DiamondCommute (ReflTransGen r₁) (TransGen r₂) - Commute ∧ TransGenCommute ↔ SemiDiamondCommute --- Cslib/Foundations/Relation/Confluence.lean | 41 ++++++++++++++++++++++ Cslib/Foundations/Relation/Defs.lean | 16 +++++++++ 2 files changed, 57 insertions(+) diff --git a/Cslib/Foundations/Relation/Confluence.lean b/Cslib/Foundations/Relation/Confluence.lean index 09681fa6f6..e16f0c39a4 100644 --- a/Cslib/Foundations/Relation/Confluence.lean +++ b/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 diff --git a/Cslib/Foundations/Relation/Defs.lean b/Cslib/Foundations/Relation/Defs.lean index 07a6980e14..a986c8a88c 100644 --- a/Cslib/Foundations/Relation/Defs.lean +++ b/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. -/ From a6c508792add6f4e70a55f2bb731d402e519618d Mon Sep 17 00:00:00 2001 From: lengyijun Date: Tue, 13 Oct 2026 07:20:13 +0800 Subject: [PATCH 2/2] feat: eta-postpone MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 5 version of eta-postpone theorems: * `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`. Ai usage: `ParEta.lean` and `BetaNfLc.lean` are generated by @Aristotle-Harmonic --- Cslib.lean | 5 + .../LocallyNameless/Untyped/BetaNfLc.lean | 116 ++++++ .../LocallyNameless/Untyped/EtaPostpone.lean | 147 +++++++ .../LocallyNameless/Untyped/FullBeta.lean | 31 ++ .../LocallyNameless/Untyped/FullEta.lean | 20 + .../LocallyNameless/Untyped/ParEta.lean | 393 ++++++++++++++++++ .../LocallyNameless/Untyped/Size.lean | 40 ++ .../LocallyNameless/Untyped/StrongNorm.lean | 40 +- .../LocallyNameless/Untyped/WeakNorm.lean | 72 ++++ CslibTests/GrindLint.lean | 5 + references.bib | 11 + 11 files changed, 879 insertions(+), 1 deletion(-) create mode 100644 Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/BetaNfLc.lean create mode 100644 Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/EtaPostpone.lean create mode 100644 Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/ParEta.lean create mode 100644 Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Size.lean create mode 100644 Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/WeakNorm.lean diff --git a/Cslib.lean b/Cslib.lean index 1c70985ff2..7f69709b30 100644 --- a/Cslib.lean +++ b/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 diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/BetaNfLc.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/BetaNfLc.lean new file mode 100644 index 0000000000..825bf05f4c --- /dev/null +++ b/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 diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/EtaPostpone.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/EtaPostpone.lean new file mode 100644 index 0000000000..f33abf6b86 --- /dev/null +++ b/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 diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean index 9e11add0fe..858572fe2e 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean @@ -60,6 +60,15 @@ 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 +lemma transgen_app_l (lc_N : LC N) (steps : Relation.TransGen FullBeta M M') : + Relation.TransGen FullBeta (app M N) (app M' N) := by + induction steps <;> grind + +lemma transgen_app_r (lc_N : LC N) (steps : Relation.TransGen FullBeta M M') : + Relation.TransGen FullBeta (app N M) (app N M') := by + induction steps <;> grind + + set_option linter.tacticAnalysis.verifyGrindOnly false in /- Single reduction `app M (fvar x) ⭢βᶠ N` implies reduction on `M` or a root beta step. -/ @[scoped grind →] @@ -91,6 +100,14 @@ lemma redex_subst_cong_lc (s s' t : Term Var) (x : Var) (step : s ⭢βᶠ s') ( grind (ematch := 7) [Xi.abs <| free_union Var] | _ => grind +lemma steps_subst_cong (s s' t : Term Var) (x : Var) (steps : s ↠βᶠ s') (h_lc : LC t) : + s[ x := t ] ↠βᶠ s'[ x := t ] := by + induction steps with grind [redex_subst_cong_lc] + +lemma transgen_subst_cong (s s' t : Term Var) (x : Var) (steps : Relation.TransGen FullBeta s s') + (h_lc : LC t) :Relation.TransGen FullBeta (s[ x := t ]) (s'[ x := t ]) := by + induction steps with grind [redex_subst_cong_lc] + /-- Substitution respects a single reduction step of a free variable. -/ lemma redex_subst_cong (s s' : Term Var) (x y : Var) (step : s ⭢βᶠ s') : s[x := fvar y] ⭢βᶠ s'[x := fvar y] := @@ -117,6 +134,12 @@ lemma redex_abs_close {x : Var} (step : M ↠βᶠ M') : (M⟦0 ↜ x⟧.abs ↠ case single ih => exact Relation.ReflTransGen.single (step_abs_close ih) case trans l r => exact Relation.ReflTransGen.trans l r +lemma transgen_abs_close (x : Var) (steps : Relation.TransGen FullBeta M M') : + Relation.TransGen FullBeta (abs (M ^* x)) (abs (M' ^* x)) := by + induction steps with + | single step => exact .single (step_abs_close step) + | tail _ step ih => apply ih.tail (step_abs_close step) + /-- Multiple reduction of opening implies multiple reduction of abstraction. -/ theorem step_abs_cong (xs : Finset Var) (cofin : ∀ x ∉ xs, (M ^ fvar x) ⭢βᶠ (M' ^ fvar x)) : M.abs ⭢βᶠ M'.abs := by @@ -124,6 +147,14 @@ theorem step_abs_cong (xs : Finset Var) (cofin : ∀ x ∉ xs, (M ^ fvar x) ⭢ rw [open_close fresh M 0 ?_, open_close fresh M' 0 ?_] all_goals grind [step_abs_close] +/-- Multiple reduction of opening implies multiple reduction of abstraction. -/ +theorem transgen_abs_cong (xs : Finset Var) + (cofin : ∀ x ∉ xs, Relation.TransGen FullBeta (M ^ fvar x) (M' ^ fvar x)) : + Relation.TransGen FullBeta M.abs M'.abs := by + have ⟨fresh, _⟩ := fresh_exists <| free_union [fv] Var + rw [open_close_var fresh M (by grind), open_close_var fresh M' (by grind)] + grind [transgen_abs_close] + /-- Multiple reduction of opening implies multiple reduction of abstraction. -/ theorem redex_abs_cong (xs : Finset Var) (cofin : ∀ x ∉ xs, (M ^ fvar x) ↠βᶠ (M' ^ fvar x)) : M.abs ↠βᶠ M'.abs := by diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean index 7f73ff772a..d2c1ccb3a6 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean @@ -7,8 +7,10 @@ Authors: Maximiliano Onofre Martínez module public import Cslib.Foundations.Relation.Attr +public import Cslib.Foundations.Relation.Defs public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Congruence +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Size /-! # η-reduction for the λ-calculus -/ @@ -149,6 +151,18 @@ lemma steps_open_cong_r {s t t' : Term Var} (lc_s : LC s.abs) (steps : t ↠η case refl => rfl case head _ _ st _ ih => exact .trans (step_open_cong_r lc_s st) ih +theorem steps_open_cong_l (xs : Finset Var) + (h : ∀ x ∉ xs, (M ^ fvar x) ↠ηᶠ (M' ^ fvar x)) (hn : LC N) : + (M ^ N) ↠ηᶠ (M' ^ N) := by + have ⟨z, hz⟩ := fresh_exists <| free_union [fv] Var + rw [Term.subst_intro z N _ (by grind), Term.subst_intro z N _ (by grind)] + exact steps_subst_cong_l _ _ _ (h z (by grind)) hn + +lemma step_size (step : M ⭢ηᶠ M') : M'.size + 2 = M.size := by + induction step with + | abs xs _ => grind [fresh_exists <| free_union [fv] Var] + | _ => grind + /- 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) : @@ -158,6 +172,12 @@ 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 [step_subst_cong_l])) +open Relation in +lemma terminating : Terminating (@FullEta Var) := + Subrelation.wf (r := InvImage (· < ·) size) + (fun {a b} (h : FullEta b a) => by have := step_size h; simp only [InvImage]; omega) + (InvImage.wf size Nat.lt_wfRel.wf) + end LambdaCalculus.LocallyNameless.Untyped.Term.FullEta end Cslib diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/ParEta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/ParEta.lean new file mode 100644 index 0000000000..8706f6987c --- /dev/null +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/ParEta.lean @@ -0,0 +1,393 @@ +/- +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.BetaNfLc +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaConfluence +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEta + +/-! # Parallel η-reduction + +This file formalises [Takahashi1995] Section 3. + +## Design + +This file only contain theorems related to `ParEta` and `etaExp`. +η-postpone theorems are placed in `EtaPostpone.lean`. + +## 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} + +/-- A parallel η-reduction step. -/ +inductive ParEta : Term Var → Term Var → Prop +/-- Free variables parallel step to themselves. -/ + | fvar (x : Var) : ParEta (fvar x) (fvar x) +/-- A parallel left and right congruence rule for application. -/ + | app : ParEta M M' → ParEta N N' → ParEta (app M N) (app M' N') +/-- Congruence rule for lambda terms. -/ + | abs (xs : Finset Var) : + (∀ x ∉ xs, ParEta (M ^ fvar x) (M' ^ fvar x)) → ParEta (abs M) (abs M') +/-- A parallel η-reduction. -/ + | eta : ParEta M M' → ParEta (abs (app M (bvar 0))) M' + +variable {L M M' N N' : Term Var} {xs : Finset Var} + +/-- Parallel η-reduction is reflexive on locally closed terms. -/ +@[scoped grind ->] +theorem ParEta.lc_refl (h : LC M) : ParEta M M := by + induction h with + | fvar x => exact ParEta.fvar x + | abs xs t _ ih => exact ParEta.abs xs ih + | app _ _ ihM ihN => exact ParEta.app ihM ihN + +theorem FullEta.le_parallel : (· ⭢ηᶠ ·) ≤ (ParEta : Term Var → Term Var → Prop) := by + intro M N step + induction step with + | base h => cases h with | eta h => exact ParEta.eta (ParEta.lc_refl h) + | appL h_lc _ ih => exact ParEta.app (ParEta.lc_refl h_lc) ih + | appR h_lc _ ih => exact ParEta.app ih (ParEta.lc_refl h_lc) + | abs xs _ ih => exact ParEta.abs xs ih + +@[scoped grind ->] +theorem ParEta.step_lc_r (h : ParEta M N) : LC N := 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 _ fun x hx => ih x hx + | @eta M M' _ ih => exact ih + +@[scoped grind ->] +theorem ParEta.step_lc_l [HasFresh Var] (h : ParEta M N) : 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 _ fun x hx => (ih x hx) + | @eta M M' _ ih => exact LC.abs ∅ _ fun x _ => LC.app (by grind) (by grind) + +theorem ParEta.le_reflTransGen_fullEta [DecidableEq Var] [HasFresh Var] : + (ParEta : Term Var → Term Var → Prop) ≤ (· ↠ηᶠ ·) := by + intro M N para + induction para with + | fvar x => exact ReflTransGen.refl + | eta hMM' ih => exact .head (Xi.base (.eta (ParEta.step_lc_l hMM'))) ih + | app hM hN ihM ihN => exact .trans (FullEta.redex_app_l_cong ihM ((ParEta.step_lc_l hN))) + (FullEta.redex_app_r_cong ihN ((ParEta.step_lc_r hM))) + | abs xs h ih => exact FullEta.redex_abs_cong xs ih + +theorem reflTransGen_parallel_fullEta [DecidableEq Var] [HasFresh Var] : + (ReflTransGen ParEta : Term Var → Term Var → Prop) = (· ↠ηᶠ ·) := by + apply le_antisymm + · exact reflTransGen_le_of_le ParEta.le_reflTransGen_fullEta + · exact ReflTransGen.mono FullEta.le_parallel + +/-- Parallel reduction respects substitution. -/ +theorem ParEta.para_subst [DecidableEq Var] [HasFresh Var] (x : Var) + (pm : ParEta M M') (pn : ParEta N N') : ParEta (M[x:=N]) (M'[x:= N']) := by + induction pm generalizing N N' with + | fvar _ => grind + | app _ _ _ _ => exact ParEta.app (by grind) (by grind) + | abs xs h ih => exact ParEta.abs (xs ∪ { x }) fun x hx => by grind + | eta hMM' ih => exact ParEta.eta (ih pn) + +/-- Parallel substitution respects fresh opening. -/ +theorem ParEta.para_open_out [DecidableEq Var] [HasFresh Var] + (hbody : ∀ x ∉ xs, ParEta (M ^ Term.fvar x) (M' ^ Term.fvar x)) + (hN : ParEta N N') : ParEta (M ^ N) (M' ^ N') := by + have ⟨z, hz⟩ := fresh_exists <| free_union [fv] Var + convert ParEta.para_subst z (hbody z (by grind)) hN + · rw [Term.subst_intro z _ _ (by grind)] + · rw [Term.subst_intro z _ _ (by grind)] + +/-- `etaExp M` is the standard η-expansion of a term `M`, represented as `λ. M (bvar 0)`. -/ +abbrev etaExp (M : Term Var) : Term Var := abs (app M (bvar 0)) + +/- [Takahashi1995] Lemma 3.2 (variable case). -/ +theorem parEta_inv_fvar {x : Var} (h : ParEta M (fvar x)) : ∃ k, M = etaExp^[k] (fvar x) := by + generalize hm : fvar x = M at h + induction h with + | fvar x => exists 0 + | app _ _ _ _ => grind + | abs xs _ _ => grind + | eta _ ih => + obtain ⟨k, rfl⟩ := ih hm + exists k + 1 + rw [add_comm, Function.iterate_add] + simp + +/- [Takahashi1995] Lemma 3.2 (application case).-/ +theorem parEta_inv_app : ParEta L (app M' N') -> + ∃ k M N, L = etaExp^[k] (app M N) ∧ ParEta M M' ∧ ParEta N N' := by + induction n : Term.size L using Nat.strong_induction_on generalizing L M' N' with + | h n ih => + rintro (h | h | h | h) + · exact ⟨0, _, _, rfl, h, by assumption⟩ + · obtain ⟨k, A', B', rfl, hA', hB'⟩ := ih _ (by grind) rfl h + refine ⟨k + 1, A', B', ?_, hA', hB'⟩ + rw [add_comm, Function.iterate_add] + simp + +/- [Takahashi1995] Lemma 3.2 (abstraction case). -/ +theorem parEta_inv_abs : ParEta M (Term.abs N) -> + ∃ (k : ℕ) (A' : Term Var) (xs : Finset Var), M = etaExp^[k] (Term.abs A') ∧ + ∀ x ∉ xs, ParEta (A' ^ fvar x) (N ^ fvar x) := by + induction n : Term.size M using Nat.strong_induction_on generalizing M N with + | h n ih => + rintro (h | h | h | h) + · exact ⟨0, _, h, rfl, by assumption⟩ + · obtain ⟨k, A', xs, rfl, hA'⟩ := ih _ (by grind) rfl h + refine ⟨k + 1, A', xs, ?_, hA'⟩ + rw [add_comm, Function.iterate_add] + simp + +theorem parEta_etaExp (h : ParEta M N) (k : ℕ) : ParEta (etaExp^[k] M) N := by + induction k with + | zero => exact h + | succ k ih => + rw [add_comm, Function.iterate_add] + exact ParEta.eta ih + +variable [HasFresh Var] + +@[simp, scoped grind <-] +theorem etaExp_lc (hM : LC M) (k : ℕ) : LC (etaExp^[k] M) := by + induction k with + | zero => exact hM + | succ k ih => + rw [add_comm, Function.iterate_add] + exact LC.abs ∅ _ (by grind) + +theorem etaExp_fullEtaStar (hM : LC M) (k : ℕ) : (etaExp^[k] M) ↠ηᶠ M := by + induction k with + | zero => exact .refl + | succ n ih => + refine .trans ?_ ih + rw [add_comm, Function.iterate_add, iterate_one, comp_apply, etaExp] + grind + +theorem etaExp_app_collapse (hm : LC M) (hn : LC N) (k : ℕ) : + (app (etaExp^[k] M) N) ↠βᶠ (app M N) := by + induction k with + | zero => exact .refl + | succ k ih => + rw [add_comm, Function.iterate_add, Function.iterate_one, Function.comp_apply] + exact .trans (.head (.base (.beta (LC.abs ∅ _ (by grind)) hn)) (by grind)) ih + +theorem Normal.etaExp_one (h : BetaNfLcNotAbs M) : BetaNfLc (etaExp M) := + .abs ∅ fun x hx => .app (by grind) (by grind) (.fvar _) + +theorem parallel_etaExp_abs_app (h : ∀ x ∉ xs, (M ^ fvar x) ⭢ₚ (M' ^ fvar x)) + (step : N ⭢ₚ N') (j : ℕ) : (Term.app (etaExp^[j] M.abs) N) ⭢ₚ (M' ^ N') := by + induction j generalizing M M' N N' xs with + | zero => exact Parallel.beta xs h step + | succ j ih => + have hCabs : M.abs.LC := LC.abs xs _ (by grind) + rw [add_comm, Function.iterate_add] + exact .beta xs (fun x hx => by grind [ih h (.fvar x), etaExp_lc hCabs j]) step + + +variable [DecidableEq Var] + +theorem etaExp_betaStar_congr (h : M ↠βᶠ M') (k : ℕ) : (etaExp^[k] M) ↠βᶠ (etaExp^[k] M') := by + cases FullBeta.steps_lc_or_rfl h with + | inr => grind + | inl hM => + induction k with + | zero => exact h + | succ k ih => + rw [add_comm, Function.iterate_add] + exact FullBeta.redex_abs_cong ∅ + (fun _ _ => FullBeta.redex_app_l_cong (by grind [etaExp_lc hM.1 k]) (.fvar _)) + +theorem etaExp_abs_collapse (hm : M.abs.LC) (k : ℕ) : (etaExp^[k] M.abs) ↠βᶠ M.abs := by + have h_beta : FullBeta (M.abs.app (bvar 0)).abs M.abs := by + obtain ⟨x, hx⟩ := fresh_exists <| free_union [fv] Var + exact .abs { x } fun y _ => + by grind [Xi.base (Beta.beta (show LC M.abs from hm) (show LC (fvar y) from LC.fvar y))] + induction k with + | zero => exact .refl + | succ k ih => + rw [add_comm, Function.iterate_add] + exact .tail + (FullBeta.redex_abs_cong ∅ + (fun x _ => .trans (.trans (by grind) (FullBeta.redex_app_l_cong ih (.fvar x))) (by grind))) + h_beta + +theorem etaExp_NormalNotAbs_normalForm (hne : BetaNfLcNotAbs M) (k : ℕ) : + ∃ M', (etaExp^[k] M) ↠βᶠ M' ∧ BetaNfLc M' := by + by_cases hk : k = 0 + · exact ⟨M, by subst hk; exact ReflTransGen.refl, hne.1⟩ + · obtain ⟨k, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hk + exists (M.app (bvar 0)).abs + induction k with + | zero => exact ⟨ReflTransGen.refl, Normal.etaExp_one hne⟩ + | succ n h => + refine ⟨?_, by grind⟩ + have heq : (n + 1).succ = 1 + (n + 1) := by omega + rw [heq, Function.iterate_add] + apply FullBeta.redex_abs_cong ∅ fun x hx => ?_ + apply BetaNfLcNotAbs.lc at hne + unfold open' openRec + rw [open_lc _ _ M hne, open_lc] + apply etaExp_app_collapse <;> grind + apply etaExp_lc hne + +theorem parBeta_etaExp_congr (h : M ⭢ₚ M') (k : ℕ) : (etaExp^[k] M) ⭢ₚ (etaExp^[k] M') := by + induction k with + | zero => exact h + | succ k ih => + rw [add_comm, Function.iterate_add] + exact Parallel.abs ∅ (by grind) + +theorem core_par (hm : BetaNfLc M) : ∀ L, ParEta L M → + (∃ N, L ↠βᶠ N ∧ BetaNfLc N) ∧ + (BetaNfLcNotAbs M → ∃ k B, L ↠βᶠ (etaExp^[k] B) ∧ BetaNfLcNotAbs B) := by + induction hm with + | fvar x => + intro L hL + obtain ⟨k, rfl⟩ := parEta_inv_fvar hL + exact ⟨etaExp_NormalNotAbs_normalForm (BetaNfLcNotAbs.fvar x) k, + fun _ => ⟨k, Term.fvar x, ReflTransGen.refl, BetaNfLcNotAbs.fvar x⟩⟩ + | @app M N hM hMne hN ihM ihN => + intro L hL + obtain ⟨j, M', N', rfl, hM', hN'⟩ := parEta_inv_app hL + have lcN' : LC N' := (ParEta.step_lc_l hN') + obtain ⟨k1, B1, hB1red, hB1neu⟩ := (ihM M' hM').2 ⟨hM, (by grind)⟩ + obtain ⟨Nhat, hNred, hNnorm⟩ := (ihN N' hN').1 + have hcollapse : (app M' N') ↠βᶠ (app B1 Nhat) := + (FullBeta.redex_app_l_cong hB1red lcN').trans + ((FullBeta.redex_app_r_cong hNred (etaExp_lc (BetaNfLcNotAbs.lc hB1neu) k1)).trans + (etaExp_app_collapse (BetaNfLcNotAbs.lc hB1neu) (BetaNfLc.lc hNnorm) k1)) + have hBneu : BetaNfLcNotAbs (app B1 Nhat) := BetaNfLcNotAbs.app hB1neu hNnorm + have hcongr : (etaExp^[j] (app M' N')) ↠βᶠ (etaExp^[j] (app B1 Nhat)) := + etaExp_betaStar_congr hcollapse j + obtain ⟨M2, h2red, h2norm⟩ := etaExp_NormalNotAbs_normalForm hBneu j + exact ⟨⟨M2, hcongr.trans h2red, h2norm⟩, fun _ => ⟨j, app B1 Nhat, hcongr, hBneu⟩⟩ + | @abs xs body hbody ihbody => + intro L hL + obtain ⟨j, body', xs2, rfl, hred⟩ := parEta_inv_abs hL + obtain ⟨x0, hx0⟩ := fresh_exists <| free_union [fv] Var + obtain ⟨C0, hC0red, hC0norm⟩ := + (ihbody x0 (by grind) (body' ^ fvar x0) (hred x0 (by grind))).1 + set D := C0 ^* x0 with hDdef + have hDred : ∀ x : Var, (body' ^ fvar x) ↠βᶠ (D ^ fvar x) := by + intro x + have e1 : body' ^ fvar x = (body' ^ fvar x0)[x0 := fvar x] := + by rw [Term.subst_intro x0]; grind + have e2 : D ^ fvar x = C0[x0 := fvar x] := by rw [hDdef, close_open_to_subst] <;> grind + rw [e1, e2] + exact FullBeta.steps_subst_cong _ _ _ _ hC0red (LC.fvar x) + have hDnormal : BetaNfLc D.abs := by + refine .abs ∅ (fun x _ => ?_) + rw [hDdef, close_open_to_subst _ _ _ (by grind) (by grind)] + exact .subst_fvar hC0norm x0 x + exact ⟨⟨D.abs, + (etaExp_betaStar_congr (FullBeta.redex_abs_cong ∅ (fun x _ => hDred x)) j).trans + (etaExp_abs_collapse (BetaNfLc.lc hDnormal) j), hDnormal⟩, by grind⟩ + +/- +[Takahashi1995] Lemma 3.4: Parallel η/β postponement: + a parallel η-step postpones over a parallel β-step: + `M ⟹η P ⟹β N` implies `M ⟹β P' ⟹η N` for some `P'`. +-/ +theorem diamondCommute_parEta_parBeta : DiamondCommute (swap (ParEta (Var := Var))) Parallel := by + intros P M N hη hβ + induction hβ generalizing M with + | fvar x => exact ⟨M, Parallel.lc_refl M (ParEta.step_lc_l hη), by grind⟩ + | app _ _ ih1 ih2 => + obtain ⟨k, M1, M2, rfl, hM1, hM2⟩ := parEta_inv_app hη + obtain ⟨P1, hP1, hP1'⟩ := ih1 hM1 + obtain ⟨P2, hP2, hP2'⟩ := ih2 hM2 + exact ⟨etaExp^[k] (app P1 P2), + parBeta_etaExp_congr (Parallel.app hP1 hP2) k, + parEta_etaExp (ParEta.app hP1' hP2') k⟩ + | abs xs hβ ih => + rename_i xs M M' + obtain ⟨k, M0, xs2, rfl, hM0⟩ := parEta_inv_abs hη + obtain ⟨x0, hx0⟩ := fresh_exists <| free_union [fv] Var + obtain ⟨Q0, hQ0⟩ := ih x0 (by grind) (hM0 x0 (by grind)) + set M0' : Term Var := Q0 ^* x0 + have hM0_cofinite : ∀ x ∉ xs ∪ xs2, (M0 ^ fvar x) ⭢ₚ (M0' ^ fvar x) := by + intro x hx + have h_subst : M0 ^ fvar x = (M0 ^ fvar x0)[x0 := fvar x] := Term.subst_intro _ _ _ (by grind) + have h_subst' : M0' ^ fvar x = Q0[x0 := fvar x] := by rw [close_open_to_subst] <;> grind + rw [h_subst, h_subst'] + apply para_subst <;> grind + have hM0'_cofinite : ∀ x ∉ xs ∪ xs2, ParEta (M0' ^ fvar x) (M' ^ fvar x) := by + intro x hx + have h_subst' : M0' ^ fvar x = Q0[x0 := fvar x] := by rw [close_open_to_subst] <;> grind + have h_subst'' : M' ^ fvar x = (M' ^ fvar x0)[x0:= fvar x] := subst_intro _ _ _ (by grind) + rw [h_subst', h_subst''] + exact ParEta.para_subst x0 hQ0.2 (ParEta.fvar x) + exact ⟨etaExp^[k] M0'.abs, + parBeta_etaExp_congr (Parallel.abs (xs ∪ xs2) hM0_cofinite) _, + parEta_etaExp (ParEta.abs (xs ∪ xs2) hM0'_cofinite) _⟩ + | beta xs h₁ h₂ h₃ h₄ => + rename_i xs M' N' M'' N'' + obtain ⟨k, M₁, M₂, rfl, hM₁, hM₂⟩ := parEta_inv_app hη + obtain ⟨j, M₁b, xs', rfl, hM₁b⟩ := parEta_inv_abs hM₁ + obtain ⟨x0, hx0'⟩ := fresh_exists <| free_union [fv] Var + obtain ⟨Q₁, hQ₁, hQ₂⟩ := h₃ x0 (by grind) (hM₁b x0 (by grind)) + set M₁b' : Term Var := Q₁ ^* x0 + have hM₁b'_family : ∀ x ∉ xs ∪ xs', (M₁b ^ fvar x) ⭢ₚ (M₁b' ^ fvar x) := by + intro x hx + have hsub : M₁b ^ fvar x = (M₁b ^ fvar x0)[x0 := fvar x] := by + rw [Term.subst_intro] + grind + have hsub' : M₁b' ^ fvar x = Q₁[x0 := fvar x] := by rw [close_open_to_subst] <;> grind + rw [hsub, hsub'] + exact para_subst x0 hQ₁ (Parallel.fvar x) + have hM₁b'_family' : ∀ x ∉ xs ∪ xs', ParEta (M₁b' ^ fvar x) (N' ^ fvar x) := by + intro x hx + have hsub : M₁b' ^ fvar x = Q₁[x0 := fvar x] := by rw [close_open_to_subst] <;> grind + have hsub' : N' ^ fvar x = (N' ^ fvar x0)[x0 := fvar x] := by + rw [subst_intro x0 _ _ (by grind)] + rw [hsub, hsub'] + exact ParEta.para_subst x0 hQ₂ (ParEta.fvar x) + obtain ⟨P', hP', hP''⟩ := h₄ hM₂ + exact ⟨etaExp^[k] (M₁b' ^ P'), + parBeta_etaExp_congr (parallel_etaExp_abs_app hM₁b'_family hP' j) k, + parEta_etaExp (ParEta.para_open_out hM₁b'_family' hP'') k⟩ + +theorem commute_parEta_parBeta : Commute (swap (ParEta (Var := Var))) Parallel := + DiamondCommute.to_commute diamondCommute_parEta_parBeta + +/-- [Takahashi1995] Lemma 3.6: If `M ⟹_η N` (parallel η-reduction) and `N` has a +β-normal form, then `M` has a β-normal form. -/ +theorem parEta_hasBetaNF (h : ParEta M N) (hn : Normalizable FullBeta N) : + Normalizable FullBeta M := by + obtain ⟨N, hQN, hN⟩ := hn + have hNlc : LC N := by cases (FullBeta.steps_lc_or_rfl hQN) with grind [ParEta.step_lc_r h] + simp only [<- reflTransGen_parallel_fullBeta] at hQN + obtain ⟨P', hPP', hP'N⟩ := DiamondCommute.diamond_commute_reflTransGen_right + (r₁ := (swap (ParEta (Var := Var)))) (r₂ := Parallel) diamondCommute_parEta_parBeta h hQN + obtain ⟨M, hP'M, hMnorm⟩ := (core_par (betaNF_normal hNlc hN) P' hP'N).1 + simp only [reflTransGen_parallel_fullBeta] at hPP' + exact ⟨M, .trans hPP' hP'M, BetaNfLc.betaNF hMnorm⟩ + +end LambdaCalculus.LocallyNameless.Untyped.Term + +end Cslib diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Size.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Size.lean new file mode 100644 index 0000000000..fdf93b833d --- /dev/null +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Size.lean @@ -0,0 +1,40 @@ +/- +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.Languages.LambdaCalculus.LocallyNameless.Untyped.Basic + +/-! Size of untyped lambda calculus term. -/ + +@[expose] public section + +namespace Cslib + +namespace LambdaCalculus.LocallyNameless.Untyped.Term + +universe u + +variable {Var : Type u} + +/-- Computes the size of a lambda calculus term. -/ +@[simp, scoped grind =] +def size : Term Var -> Nat +| bvar _ => 0 +| fvar _ => 0 +| abs t => 1 + size t +| app t1 t2 => 1 + size t1 + size t2 + +@[scoped grind =] +theorem size_openRec_fvar (i) (x : Var) (M) : M⟦i ↝ fvar x⟧.size = M.size := by + induction M generalizing i <;> grind + +theorem size_open_fvar (x : Var) (M : Term Var) : size (M ^ fvar x) = size M := + size_openRec_fvar 0 x M + +end LambdaCalculus.LocallyNameless.Untyped.Term + +end Cslib diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean index b54be7de11..4229ad0b68 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean @@ -6,8 +6,8 @@ Authors: David Wegmann module -public import Cslib.Foundations.Relation.Termination public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiApp +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.EtaPostpone /-! Strong normalization (termination) for full beta-reduction of untyped lambda calculus. -/ @@ -156,6 +156,44 @@ lemma sn_abs_app_multiApp [DecidableEq Var] [HasFresh Var] {Ps} {M N : Term Var} refine Relation.TransGen.single (Xi.base (Beta.beta ?_ ?_)) all_goals grind +lemma eta_preserves_sn_transgen_beta [DecidableEq Var] [HasFresh Var] : + Preserves (ReflTransGen (FullEta (Var := Var))) (SN (TransGen FullBeta)) := by + intros t t' steps sn_t + induction sn_t generalizing t' with | intro t h ih => + apply Acc.intro _ fun t'' ht'' => ?_ + rw [reflTransGen_swap] at steps + obtain ⟨_, h1, h2⟩ := diamondcommute_etaplus_betastar steps ht'' + rw [reflTransGen_swap] at h2 + exact ih _ h1 h2 + +lemma eta_preserves_sn_beta [DecidableEq Var] [HasFresh Var] : + Preserves (ReflTransGen (FullEta (Var := Var))) (SN FullBeta) := + fun _ _ steps sn_t => + (SN.iff_transGen _).mp (eta_preserves_sn_transgen_beta steps (SN.transGen sn_t)) + +theorem sn_betaEta_of_sn_fullBeta [DecidableEq Var] [HasFresh Var] + (hB : SN ((TransGen FullBeta) : Term Var → Term Var → Prop) t) : + SN (FullBetaEta : Term Var → Term Var → Prop) t := by + replace hB : ∃ s : Term Var, + SN ((TransGen FullBeta) : Term Var → Term Var → Prop) s ∧ s ↠ηᶠ t := ⟨t, hB, .refl⟩ + obtain ⟨s, hs, steps⟩ := hB + induction hs generalizing t with | intro s hBacc IHB => + induction hn : t.size using Nat.strong_induction_on generalizing t with | h n IHE => + refine Acc.intro _ fun b hb => ?_ + rcases hb with hbeta | heta + · rw [reflTransGen_swap] at steps + obtain ⟨d, hd1, hd2⟩ := diamondcommute_etaplus_betastar steps (.single hbeta) + rw [reflTransGen_swap] at hd2 + exact SN.of_rel_reflTransGen (IHB d hd1 .refl) (by grind) + · have hsz : b.size < t.size := by have := FullEta.step_size heta; omega + exact IHE _ (hn ▸ hsz) (steps.tail heta) rfl + +/-- A term is βη-strongly-normalising iff it is β-strongly-normalising. -/ +theorem beta_sn_iff_betaEta_sn [DecidableEq Var] [HasFresh Var] : + SN FullBeta t ↔ SN FullBetaEta t := + ⟨fun h => sn_betaEta_of_sn_fullBeta (by rwa [SN.iff_transGen]), + fun h => Subrelation.accessible (fun hab => Or.inl hab) h⟩ + end LambdaCalculus.LocallyNameless.Untyped.Term end Cslib diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/WeakNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/WeakNorm.lean new file mode 100644 index 0000000000..0c4736b1b2 --- /dev/null +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/WeakNorm.lean @@ -0,0 +1,72 @@ +/- +Copyright (c) 2025 David Wegmann. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yijun Leng +-/ + +module + +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.EtaPostpone + +/-! Weak normalization for full beta-reduction of untyped lambda calculus. -/ + +@[expose] public section + +set_option linter.unusedDecidableInType false + +namespace Cslib + +universe u + +namespace LambdaCalculus.LocallyNameless.Untyped.Term + +variable {Var : Type u} [DecidableEq Var] [HasFresh Var] {t t' : Term Var} + +open FullBeta Relation + +/-- [Takahashi1995] 3.7: If `P ↠ηᶠ Q` and `P` is a β-normal form, + then `Q` is a β-normal form. -/ +theorem etastar_preserves_normal_beta : + Preserves ((· ↠ηᶠ ·) : Term Var → Term Var → Prop) (Normal FullBeta) := by + rintro _ _ steps hP ⟨_, hR⟩ + rw [reflTransGen_swap] at steps + obtain ⟨y, hy, _⟩ := diamondcommute_etaplus_betastar steps (.single hR) + rw [TransGen.head'_iff] at hy + exact hP (by grind) + +theorem etastar_hasBetaNF (steps : t ↠ηᶠ t') (hQ : Normalizable FullBeta t') : + Normalizable FullBeta t := by + induction steps with + | refl => grind + | tail _ step ih => exact ih (parEta_hasBetaNF (FullEta.le_parallel _ _ step) hQ) + +/-- A term has a βη-normal form ⇔ it has a β-normal form. -/ +theorem hasBetaNF_iff_hasBetaEtaNF : Normalizable FullBeta t ↔ Normalizable FullBetaEta t := by + refine ⟨fun ⟨y, hy, hβ⟩ => ?_, fun ⟨y, hy, hβηnormal⟩ => ?_⟩ + · obtain ⟨z, hz, hnormal⟩ := SN.normalizable (FullEta.terminating.apply y) + refine ⟨z, .trans (.mono le_sup_left _ _ hy) (.mono le_sup_right _ _ hz), fun ⟨_, h⟩ => ?_⟩ + have := etastar_preserves_normal_beta hz hβ + cases h <;> grind + · obtain ⟨L, hβ, hη⟩ := eta_postpone hy + rw [Normal.sup_iff] at hβηnormal + obtain ⟨_, _⟩ := hβηnormal + have h : Normalizable FullBeta y := by exists y + obtain ⟨W, hw, hnormal⟩ := etastar_hasBetaNF hη h + exact ⟨W, .trans hβ hw, hnormal⟩ + +theorem etastar_iff_hasBetaNF (steps : t ↠ηᶠ t') : + Normalizable FullBeta t ↔ Normalizable FullBeta t' := by + refine ⟨fun hP => ?_, fun hQ => etastar_hasBetaNF steps hQ⟩ + rw [hasBetaNF_iff_hasBetaEtaNF] at * + obtain ⟨Z, βηsteps, hZ⟩ := hP + obtain ⟨_, refl_steps, _⟩ := confluent_beta_eta βηsteps (.mono le_sup_right _ _ steps) + grind [Normal.reflTransGen_eq hZ refl_steps] + +theorem etastar_iff_hasBetaEtaNF (steps : t ↠ηᶠ t') : + Normalizable FullBetaEta t ↔ Normalizable FullBetaEta t' := by + repeat rw [← hasBetaNF_iff_hasBetaEtaNF] + exact etastar_iff_hasBetaNF steps + +end LambdaCalculus.LocallyNameless.Untyped.Term + +end Cslib diff --git a/CslibTests/GrindLint.lean b/CslibTests/GrindLint.lean index 10011fda5e..b85c2d1a36 100644 --- a/CslibTests/GrindLint.lean +++ b/CslibTests/GrindLint.lean @@ -64,9 +64,14 @@ open_scoped_all Cslib #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.para_subst #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.FullBeta.invert_step_app_fvar #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.subst_intro +#grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.subst_openRec #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.Untyped.Term.beta_lc +#grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.close_open_to_subst +#grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.step_multiApp_r #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.Modal.Satisfies.iff_iff_iff diff --git a/references.bib b/references.bib index 2191bd6fc6..3c59244825 100644 --- a/references.bib +++ b/references.bib @@ -597,6 +597,17 @@ @mastersthesis{Copes2018 year = {2018} } +@article{Takahashi1995, + author = {Takahashi, Yoshihiko}, + title = {Parallel Reductions in {$\lambda$}-Calculus}, + journal = {Information and Computation}, + volume = {118}, + number = {1}, + pages = {120--127}, + year = {1995}, + doi = {10.1006/inco.1995.1057} +} + @book{AroraBarak09, author = {Sanjeev Arora and Boaz Barak},