From 4fc2e653162df149b6fd642f5bd1a4ddaf97ccaf Mon Sep 17 00:00:00 2001 From: lengyijun Date: Fri, 26 Jun 2026 14:04:39 +0800 Subject: [PATCH] feat(LocallyNameless/Untyped): add `FullEta.steps_lc_l` MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Introduce `FullEta.steps_lc_l` lemma: if `M ↠ηᶠ M'` and `LC M'`, then `LC M` - Add `@[scoped grind →]` attribute to `step_lc_l` --- .../LambdaCalculus/LocallyNameless/Untyped/FullEta.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean index 2231d2b08..eee34a2a9 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 @@ -52,6 +53,9 @@ lemma step_lc_l [HasFresh Var] (step : M ⭢ηᶠ M') : LC M := by | appR lc_Z _ ih => exact LC.app ih lc_Z | @abs M' _ xs _ ih => exact LC.abs xs M' ih +lemma steps_lc_l [HasFresh Var] (step : M ↠ηᶠ M') (h : LC M') : LC M := by + induction step with grind + /-- Left congruence rule for application in multiple reduction. -/ theorem redex_app_l_cong (redex : M ↠ηᶠ M') (lc_N : LC N) : app M N ↠ηᶠ app M' N := by induction redex <;> grind