From 308e33f705c0edbb302b87c869792a00f4575dfb Mon Sep 17 00:00:00 2001 From: lengyijun Date: Thu, 13 Aug 2026 13:19:10 +0800 Subject: [PATCH] refactor: .trans => .head/.tail --- Cslib/Computability/Automata/EpsilonNA/ToSingleAccept.lean | 4 ++-- Cslib/Computability/URM/StandardForm.lean | 4 ++-- Cslib/Foundations/Relation/Confluence.lean | 4 ++-- .../LambdaCalculus/LocallyNameless/Untyped/FullBetaEta.lean | 4 ++-- .../LocallyNameless/Untyped/StandardReduction.lean | 2 +- 5 files changed, 9 insertions(+), 9 deletions(-) diff --git a/Cslib/Computability/Automata/EpsilonNA/ToSingleAccept.lean b/Cslib/Computability/Automata/EpsilonNA/ToSingleAccept.lean index 6b85893fd..aad6f1371 100644 --- a/Cslib/Computability/Automata/EpsilonNA/ToSingleAccept.lean +++ b/Cslib/Computability/Automata/EpsilonNA/ToSingleAccept.lean @@ -118,11 +118,11 @@ theorem toSingleAccept_τSTr_τSTr {a : εNA.FinAcc State Symbol} | tail hτstr htr ih => subst hos' obtain ⟨_, rfl⟩ := Option.isSome_iff_exists.mp <| toSingleAccept_tr_antiDerivative_isSome htr - exact .trans (ih rfl) (.single htr) + exact .tail (ih rfl) htr · intro h cases h with | refl => exact LTS.τSTr.refl - | tail hτstr htr => exact .trans (.lift some (by rfl) _ _ hτstr) (.single htr) + | tail hτstr htr => exact .tail (.lift some (by rfl) _ _ hτstr) htr @[scoped grind →] theorem toSingleAccept_τSTr_none_accept {a : εNA.FinAcc State Symbol} diff --git a/Cslib/Computability/URM/StandardForm.lean b/Cslib/Computability/URM/StandardForm.lean index 51a288b6b..adcf37e01 100644 --- a/Cslib/Computability/URM/StandardForm.lean +++ b/Cslib/Computability/URM/StandardForm.lean @@ -138,7 +138,7 @@ theorem Steps.toStandardForm_halts {p : Program} {s s' : State} rcases Step.toStandardForm hstep with hsame | ⟨hhalted_mid, s_mid, hstep_mid, hhalted_mid', hregs_eq⟩ · obtain ⟨s₂, hsteps₂, hhalted₂, hregs_eq⟩ := ih - exact ⟨s₂, .trans (.single hsame) hsteps₂, hhalted₂, hregs_eq⟩ + exact ⟨s₂, .head hsame hsteps₂, hhalted₂, hregs_eq⟩ · grind [Steps.eq_of_halts .refl hhalted_mid hrest hhalted] /-- Forward halting theorem. -/ @@ -179,7 +179,7 @@ theorem Steps.from_toStandardForm_halts {p : Program} {s s' : State} rcases Step.from_toStandardForm hstep with hsame | ⟨hhalted_mid, s_mid, hstep_mid, hhalted_mid', hregs_eq⟩ · obtain ⟨s₂, hsteps₂, hhalted₂, hregs_eq⟩ := ih - exact ⟨s₂, .trans (.single hsame) hsteps₂, hhalted₂, hregs_eq⟩ + exact ⟨s₂, .head hsame hsteps₂, hhalted₂, hregs_eq⟩ · rename_i s_next have hrest_trivial : s_next = s' := Steps.eq_of_halts .refl hhalted_mid hrest hhalted subst hrest_trivial diff --git a/Cslib/Foundations/Relation/Confluence.lean b/Cslib/Foundations/Relation/Confluence.lean index 86ab56355..08d47fb00 100644 --- a/Cslib/Foundations/Relation/Confluence.lean +++ b/Cslib/Foundations/Relation/Confluence.lean @@ -192,7 +192,7 @@ theorem SN.normalizable (hx : SN r x) : Normalizable r x := by by_cases hy: (∃ y, r x y) · obtain ⟨y, hy⟩ := hy obtain ⟨z, hz, hnormal⟩ := ih y hy - exact ⟨z, .trans (.single hy) hz, hnormal⟩ + exact ⟨z, .head hy hz, hnormal⟩ · exists x lemma Terminating.apply (hr : Terminating r) (x : α) : SN r x := WellFounded.apply hr x @@ -304,7 +304,7 @@ theorem StronglyCommute.extend (h : StronglyCommute r₁ r₂) (xy : ReflTransGe | @tail b c _ bc ih => obtain ⟨w, bw, zw⟩ := ih cases bw with - | refl => exact ⟨c, .refl, zw.trans (.single bc)⟩ + | refl => exact ⟨c, .refl, zw.tail bc⟩ | single bw => cases h bc bw; grind [ReflTransGen.trans] theorem StronglyCommute.toCommute (h : StronglyCommute r₁ r₂) : Commute r₁ r₂ := by diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEta.lean index a78ade35f..e847f97de 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEta.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEta.lean @@ -41,7 +41,7 @@ theorem redex_app_l_cong (redex : M ↠βηᶠ M') (lc_N : LC N) : app M N ↠β induction redex with | refl => grind | tail _ h ih => - refine .trans ih (.single ?_) + refine .tail ih ?_ rcases h with h | h · exact join_inl (h.appR lc_N) · exact join_inr (h.appR lc_N) @@ -50,7 +50,7 @@ theorem redex_app_r_cong (redex : M ↠βηᶠ M') (lc_N : LC N) : app N M ↠β induction redex with | refl => grind | tail _ h ih => - refine .trans ih (.single ?_) + refine .tail ih ?_ rcases h with h | h · exact join_inl (h.appL lc_N) · exact join_inr (h.appL lc_N) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean index 96324ac57..628107821 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean @@ -322,7 +322,7 @@ lemma Standard.trans_step (h1 : M ⭢ₛ P) (h2 : P ⭢βᶠ N) : M ⭢ₛ N := have std_subst := std_abs.abs_subst std_M std_M.lc_l std_M.lc_r have s1 : L'.app M ↠ₙ L.abs.app M := CBN.steps_app_l_cong cbn_L1 std_M.lc_l have s2 : L.abs.app M ⭢ₙ L ^ M := .base (.beta (CBN.steps_lc_r std_L.lc_l cbn_L1) std_M.lc_l) - exact Standard.cbn_trans (.trans s1 (.single s2)) std_subst + exact Standard.cbn_trans (.tail s1 s2) std_subst /-- A standard reduction followed by a full β-reduction is a standard reduction. -/ lemma Standard.trans_redex (h1 : M ⭢ₛ P) (h2 : P ↠βᶠ N) : M ⭢ₛ N := by