Skip to content

refactor: .trans => .head/.tail #797

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
lengyijun wants to merge 1 commit into
base: main
Choose a base branch
from
+9 −9
Open

refactor: .trans => .head/.tail #797

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions Cslib/Computability/Automata/EpsilonNA/ToSingleAccept.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand Down
4 changes: 2 additions & 2 deletions Cslib/Computability/URM/StandardForm.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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. -/
Expand Down Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions Cslib/Foundations/Relation/Confluence.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEta.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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)
Expand Down
2 changes: 1 addition & 1 deletion Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading