@@ -12,6 +12,8 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Congruence
1212
1313public section
1414
15+ set_option linter.unusedDecidableInType false
16+
1517/-! # η-reduction for the λ-calculus -/
1618
1719namespace Cslib
@@ -24,13 +26,13 @@ namespace LambdaCalculus.LocallyNameless.Untyped.Term
2426
2527/-- A single η-reduction step. -/
2628@ [scoped grind]
27- inductive BaseEta : Term Var → Term Var → Prop
29+ inductive Eta : Term Var → Term Var → Prop
2830/-- The eta rule: λx. M x ⟶ M, provided x is not free in M. -/
29- | eta : LC M → BaseEta (abs (app M (bvar 0 ))) M
31+ | eta : LC M → Eta (abs (app M (bvar 0 ))) M
3032
3133/-- Full η-reduction, defined as the congruence closure of the base η-rule. -/
3234@ [reduction_sys "ηᶠ" ]
33- abbrev FullEta : Term Var → Term Var → Prop := Xi BaseEta
35+ abbrev FullEta : Term Var → Term Var → Prop := Xi Eta
3436
3537namespace FullEta
3638
@@ -42,6 +44,14 @@ lemma step_lc_r (step : M ⭢ηᶠ M') : LC M' := by
4244 refine Xi.step_lc_r ?_ step
4345 grind
4446
47+ /-- Left congruence rule for application in multiple reduction. -/
48+ theorem redex_app_l_cong (redex : M ↠ηᶠ M') (lc_N : LC N) : app M N ↠ηᶠ app M' N := by
49+ induction redex <;> grind
50+
51+ /-- Right congruence rule for application in multiple reduction. -/
52+ theorem redex_app_r_cong (redex : M ↠ηᶠ M') (lc_N : LC N) : app N M ↠ηᶠ app N M' := by
53+ induction redex <;> grind
54+
4555/- Single reduction `app M (fvar x) ⭢ηᶠ N` implies `N = app M' (fvar x)` for some M' -/
4656@ [scoped grind →]
4757lemma invert_step_app_fvar (step : (app M (fvar x)) ⭢ηᶠ N) :
@@ -69,6 +79,65 @@ lemma eta_subst_fvar {x y : Var} (step : M ⭢ηᶠ M') : M [ x := fvar y ] ⭢
6979 | abs => grind [Xi.abs <| free_union Var]
7080 | _ => grind
7181
82+ /-- Abstracting then closing preserves a single η-reduction step. -/
83+ lemma step_abs_close {x} (step : M ⭢ηᶠ M') (lc_M : LC M) : (M ^* x).abs ⭢ηᶠ (M' ^* x).abs := by
84+ grind [Xi.abs ∅]
85+
86+ /-- Abstracting then closing preserves multiple reductions. -/
87+ lemma redex_abs_close {x} (steps : M ↠ηᶠ M') (lc_M : LC M) : (M ^* x).abs ↠ηᶠ (M' ^* x).abs := by
88+ induction steps using Relation.ReflTransGen.head_induction_on
89+ case refl => exact .refl
90+ case head b c st_bc _ ih => exact .head (step_abs_close st_bc lc_M) (ih (step_lc_r st_bc))
91+
92+ /-- Multiple reduction of opening implies multiple reduction of abstraction. -/
93+ theorem redex_abs_cong {M M' : Term Var} (xs : Finset Var)
94+ (cofin : ∀ x ∉ xs, (M ^ fvar x) ↠ηᶠ M' ^ fvar x) (lc_M : LC M.abs) :
95+ M.abs ↠ηᶠ M'.abs := by
96+ cases lc_M
97+ case abs L hL =>
98+ have ⟨x, _⟩ := fresh_exists <| free_union [fv] Var
99+ rw [open_close x M 0 , open_close x M' 0 ]
100+ all_goals grind [redex_abs_close (x := x) (cofin x ?_) (hL x ?_)]
101+
102+ /- `t ⭢ηᶠ t'` implies `s [ x := t ] ↠ηᶠ s [ x := t' ]`. -/
103+ lemma step_subst_cong_r {x : Var} (s t t' : Term Var) (st : t ⭢ηᶠ t') (lc_s : LC s) (lc_t : LC t) :
104+ s [ x := t ] ↠ηᶠ s [ x := t' ] := by
105+ induction lc_s generalizing t t' with
106+ | fvar => grind
107+ | app hl hr ih_l ih_r =>
108+ trans
109+ · exact redex_app_l_cong (ih_l t t' st lc_t) (subst_lc hr lc_t)
110+ · exact redex_app_r_cong (ih_r t t' st lc_t) (subst_lc hl (step_lc_r st))
111+ | abs L body h_lc_body ih =>
112+ apply redex_abs_cong (L ∪ {x})
113+ · intro z
114+ grind =>
115+ have : (body ^ fvar z)[x := t] ↠ηᶠ (body ^ fvar z)[x := t']
116+ finish
117+ · exact subst_lc (LC.abs L body h_lc_body) lc_t
118+
119+ /- `steps_subst_cong_r` can be generalized to multiple reductions `t ↠ηᶠ t'`. -/
120+ lemma steps_subst_cong_r {x : Var} (s t t' : Term Var) (st : t ↠ηᶠ t') (lc_s : LC s) (lc_t : LC t) :
121+ s [ x := t ] ↠ηᶠ s [ x := t' ] := by
122+ induction st using Relation.ReflTransGen.head_induction_on
123+ case refl => rfl
124+ case head _ _ st _ ih => exact .trans (step_subst_cong_r s _ _ st lc_s lc_t) (ih (step_lc_r st))
125+
126+ /- `t ⭢ηᶠ t'` implies `s ^ t ↠ηᶠ s ^ t'`. -/
127+ lemma step_open_cong_r {s t t' : Term Var} (lc_s : LC s.abs) (lc_t : LC t) (step : t ⭢ηᶠ t') :
128+ (s ^ t) ↠ηᶠ s ^ t' := by
129+ cases lc_s
130+ case abs L hL =>
131+ have ⟨x, _⟩ := fresh_exists <| free_union [fv] Var
132+ grind [step_subst_cong_r (x := x) (s ^ fvar x) t t' step (hL x ?_) lc_t]
133+
134+ /- `steps_open_cong_r` can be generalized to multiple reductions `t ↠ηᶠ t'`. -/
135+ lemma steps_open_cong_r {s t t' : Term Var} (lc_s : LC s.abs) (lc_t : LC t) (steps : t ↠ηᶠ t') :
136+ (s ^ t) ↠ηᶠ s ^ t' := by
137+ induction steps using Relation.ReflTransGen.head_induction_on
138+ case refl => rfl
139+ case head _ _ st _ ih => exact .trans (step_open_cong_r lc_s lc_t st) (ih (step_lc_r st))
140+
72141/- Closing a sequence of η-reduction steps over a fresh variable preserves the steps. -/
73142open Relation in
74143lemma close_eta_steps (hx_M : x ∉ M.fv) (st_M : ReflGen FullEta (M ^ fvar x) N) :
@@ -78,6 +147,21 @@ lemma close_eta_steps (hx_M : x ∉ M.fv) (st_M : ReflGen FullEta (M ^ fvar x) N
78147 | single st =>
79148 exact .single (Xi.abs {x} (by grind))
80149
150+ /- `s ⭢ηᶠ s'` implies `s [ x := N ] ⭢ηᶠ s' [ x := N ]`. -/
151+ lemma step_subst_cong_l {x : Var} (s s' N : Term Var) (step : s ⭢ηᶠ s') (lc_N : LC N) :
152+ s [ x := N ] ⭢ηᶠ s' [ x := N ] := by
153+ induction step
154+ case base h => cases h with | eta lc => exact Xi.base (.eta (subst_lc lc lc_N))
155+ case abs => grind [Xi.abs <| free_union Var, subst_open_var]
156+ all_goals grind
157+
158+ /- `steps_subst_cong_l` can be generalized to multiple reductions `s ↠ηᶠ s'`. -/
159+ lemma steps_subst_cong_l {x : Var} (s s' N : Term Var) (steps : s ↠ηᶠ s') (lc_N : LC N) :
160+ s [ x := N ] ↠ηᶠ s' [ x := N ] := by
161+ induction steps with
162+ | refl => rfl
163+ | tail _ step ih => grind [step_subst_cong_l]
164+
81165end LambdaCalculus.LocallyNameless.Untyped.Term.FullEta
82166
83167end Cslib
0 commit comments