From 324ef34e4a6605af42b1355b8f85e0838f87e1cc Mon Sep 17 00:00:00 2001 From: lengyijun Date: Sun, 26 Jul 2026 05:50:04 +0800 Subject: [PATCH] refactor(LocallyNameless): remove unnecessary LC assumptions from eta reduction lemmas MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Drop `M.LC` param from `step_abs_close`, `redex_abs_close`, `redex_abs_cong`, `step_open_cong_r`, `step_subst_cong_r`, `steps_open_cong_r`, `steps_subst_cong_r`, `FullBeta.steps_open_cong_l_abs` - Add `@[scoped grind →]` to `FullEta.step_lc_l` --- .../LocallyNameless/Untyped/FullBeta.lean | 2 +- .../Untyped/FullBetaEtaConfluence.lean | 2 +- .../LocallyNameless/Untyped/FullEta.lean | 32 +++++++++---------- 3 files changed, 17 insertions(+), 19 deletions(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean index a896d8825..399eeee23 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean @@ -146,7 +146,7 @@ lemma invert_steps_abs {s t : Term Var} (step : s.abs ↠βᶠ t) : /- `λ s ↠βᶠ λ s'` implies `s ^ t ↠βᶠ s' ^ t'` -/ lemma steps_open_cong_l_abs - (s s' t : Term Var) (steps : s.abs ↠βᶠ s'.abs) (lc_s : LC s.abs) (lc_t : LC t) : + (s s' t : Term Var) (steps : s.abs ↠βᶠ s'.abs) (lc_t : LC t) : (s ^ t) ↠βᶠ (s' ^ t) := by generalize eq : s.abs = s_abs at steps generalize eq' : s'.abs = s'_abs at steps diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEtaConfluence.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEtaConfluence.lean index 074d34a3f..c3452374a 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEtaConfluence.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEtaConfluence.lean @@ -88,7 +88,7 @@ lemma stronglyCommute_eta_beta : StronglyCommute (@FullEta Var) FullBeta := by | 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))) + exact FullEta.redex_abs_close h_eta open Commute in /-- βη-reduction is confluent. -/ diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean index 2231d2b08..a830d898f 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean @@ -45,6 +45,7 @@ lemma step_lc_r (step : M ⭢ηᶠ M') : LC M' := by grind /-- The left side of an η-reduction is locally closed. -/ +@[scoped grind →] lemma step_lc_l [HasFresh Var] (step : M ⭢ηᶠ M') : LC M := by induction step with | base h_e => cases h_e with | eta => apply LC.abs ∅; grind @@ -97,64 +98,61 @@ lemma steps_subst_cong_l {x : Var} (s s' N : Term Var) (steps : s ↠ηᶠ s') ( | tail _ step ih => grind [step_subst_cong_l] /-- 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 +lemma step_abs_close {x} (step : M ⭢ηᶠ M') : (M ^* x).abs ⭢ηᶠ (M' ^* x).abs := by apply Xi.abs ∅ grind [step_subst_cong_l] /-- 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 +lemma redex_abs_close {x} (steps : M ↠ηᶠ 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)) + case head b c st_bc _ ih => exact .head (step_abs_close st_bc) ih /-- 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) : + (cofin : ∀ x ∉ xs, (M ^ fvar x) ↠ηᶠ M' ^ fvar x) : 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 ?_)] + all_goals grind [redex_abs_close (x := x) (cofin 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) : +lemma step_subst_cong_r {x : Var} (s t t' : Term Var) (st : t ⭢ηᶠ t') (lc_s : LC s) : 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)) + · exact redex_app_l_cong (ih_l t t' st) (subst_lc hr (by grind)) + · exact redex_app_r_cong (ih_r t t' st) (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) : +lemma steps_subst_cong_r {x : Var} (s t t' : Term Var) (st : t ↠ηᶠ t') (lc_s : LC s) : 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)) + case head _ _ st _ ih => exact .trans (step_subst_cong_r s _ _ st lc_s) ih /- `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') : +lemma step_open_cong_r {s t t' : Term Var} (lc_s : LC s.abs) (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] + grind [step_subst_cong_r (x := x) (s ^ fvar x) t t' step (hL x ?_)] /- `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') : +lemma steps_open_cong_r {s t t' : Term Var} (lc_s : LC s.abs) (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)) + case head _ _ st _ ih => exact .trans (step_open_cong_r lc_s st) ih /- Closing a sequence of η-reduction steps over a fresh variable preserves the steps. -/ open Relation in