Skip to content

Commit b39710e

Browse files
WegmannDavidchenson2018
WegmannDavid
and
chenson2018
authored
feat: StrongNormalizationUntypedAndStlc (#411)
This pull request adds general strong normalization lemmas and strong normalization via saturated sets for locally nameless stlc. --------- Co-authored-by: Chris Henson <chrishenson.net@gmail.com>
1 parent a915db9 commit b39710e

3 files changed

Lines changed: 279 additions & 0 deletions

File tree

‎Cslib.lean‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -89,6 +89,7 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Typing
8989
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.WellFormed
9090
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic
9191
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Safety
92+
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.StrongNorm
9293
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Basic
9394
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
9495
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaConfluence
@@ -98,6 +99,7 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
9899
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiApp
99100
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiSubst
100101
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
102+
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm
101103
public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
102104
public import Cslib.Logics.HML.Basic
103105
public import Cslib.Logics.HML.LogicalEquivalence

‎Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean‎

Lines changed: 124 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,124 @@
1+
/-
2+
Copyright (c) 2025 David Wegmann. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: David Wegmann
5+
-/
6+
7+
module
8+
9+
public import Cslib.Foundations.Data.HasFresh
10+
public import Cslib.Foundations.Data.Relation
11+
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic
12+
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
13+
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm
14+
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
15+
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiSubst
16+
17+
@[expose] public section
18+
19+
set_option linter.unusedDecidableInType false
20+
21+
namespace Cslib
22+
23+
universe u v
24+
25+
namespace LambdaCalculus.LocallyNameless.Stlc
26+
27+
open Untyped Typing LambdaCalculus.LocallyNameless.Untyped.Term
28+
29+
variable {Var : Type u} {Base : Type v} [DecidableEq Var] [HasFresh Var]
30+
31+
open LambdaCalculus.LocallyNameless.Stlc
32+
open scoped Term
33+
34+
/-- A set of terms is called saturated if it
35+
36+
1. only contains locally closed terms,
37+
2. only contains strongly normalizing terms,
38+
3. contains all neutral locally closed terms, and
39+
4. is closed under top-level β-reduction of the form (λ M) N P₁ … Pₙ → M ^ N P₁ … Pₙ.
40+
-/
41+
@[scoped grind]
42+
structure Saturated (S : Set (Term Var)) : Prop where
43+
lc : ∀ M ∈ S, LC M
44+
sn : ∀ M ∈ S, SN M
45+
neutal_lc : ∀ M, Neutral M → LC M → M ∈ S
46+
multiApp : ∀ M N P, LC N → SN N → multiApp (M ^ N) P ∈ S → multiApp (M.abs.app N) P ∈ S
47+
48+
/-- The semantic map maps each type to a corresponding saturated set of terms.
49+
For the strong normalization proof to work, we must ensure that
50+
Γ ⊢ t ∶ τ implies that t is in the set of terms corresponding to τ.
51+
52+
Strong normalization later follows from the fact that terms in saturated
53+
sets are strongly normalizing.
54+
-/
55+
@[simp, scoped grind =]
56+
def semanticMap : Ty Base → Set (Term Var)
57+
| .base _ => { t | SN t ∧ LC t }
58+
| .arrow τ₁ τ₂ => { t | ∀ s, s ∈ semanticMap τ₁ → app t s ∈ semanticMap τ₂ }
59+
60+
/-- The sets constructed by semanticMap are saturated -/
61+
lemma semanticMap_saturated (τ : Ty Base) : @Saturated Var (semanticMap τ) := by
62+
induction τ with
63+
| base => grind [sn_abs_app_multiApp, sn_neutral, open_abs_lc]
64+
| arrow τ₁ τ₂ ih₁ ih₂ =>
65+
constructor
66+
· grind [ih₁.neutal_lc (fvar <| fresh {}) (.fvar <| fresh {}) (.fvar <| fresh {}), cases LC]
67+
· grind [sn_app_left (Var := Var) (N := fvar <| fresh {})]
68+
· grind
69+
· intro M N P _ _ _ s _
70+
grind [ih₂.multiApp M N (s :: P)]
71+
72+
/-- The `entails_context` predicate ensures that each variable in the context
73+
is mapped to a term in the corresponding semantic map. -/
74+
abbrev entails_context (E : Term.Env Var) (Γ : Context Var (Ty Base)) :=
75+
∀ {x τ}, ⟨x, τ⟩ ∈ Γ → (multiSubst E (fvar x)) ∈ semanticMap τ
76+
77+
/-- The empty context is entailed by any environment. -/
78+
lemma entails_context_empty {Γ : Context Var (Ty Base)} : entails_context [] Γ := by
79+
have := semanticMap_saturated (Var := Var) (Base := Base)
80+
grind
81+
82+
open scoped Context in
83+
omit [HasFresh Var] in
84+
/-- The `entails_context` predicate is preserved when extending the context
85+
with a new variable, provided the new variable is fresh and its
86+
substitution is in the corresponding semantic map. -/
87+
lemma entails_context_cons (E : Term.Env Var) (Γ : Context Var (Ty Base))
88+
(x : Var) (τ : Ty Base) (sub : Term Var)
89+
(h_fresh : x ∉ E.dom ∪ E.fv ∪ Γ.dom)
90+
(h_mem : sub ∈ semanticMap τ) :
91+
entails_context E Γ → entails_context (⟨ x, sub ⟩ :: E) (⟨ x, τ ⟩ :: Γ) := by
92+
grind [multiSubst_fvar_fresh, subst_fresh, multiSubst_preserves_not_fvar]
93+
94+
/-- The `entails` predicate states that a term `t` is
95+
semantically valid with respect to a context `Γ` and a type `τ` -/
96+
abbrev entails (Γ : Context Var (Ty Base)) (t : Term Var) (τ : Ty Base) :=
97+
∀ E, env_LC E → (entails_context E Γ) → (multiSubst E t) ∈ semanticMap τ
98+
99+
/-- The `soundness` lemma states that if a term `t` has type `τ` in context `Γ`,
100+
then `t` is semantically valid with respect to `Γ` and `τ` -/
101+
lemma soundness {Γ : Context Var (Ty Base)} (derivation_t : Γ ⊢ t ∶ τ) : entails Γ t τ := by
102+
induction derivation_t with
103+
| var Γ xσ_mem_Γ => grind
104+
| @abs σ Γ t τ L HL IH =>
105+
intro E _ _ s
106+
have sat_semMap_σ := semanticMap_saturated (Var := Var) σ
107+
have sat_semMap_τ := semanticMap_saturated (Var := Var) τ
108+
have := sat_semMap_τ.multiApp (multiSubst E t) s []
109+
let := multiSubst E t
110+
have ⟨x, _⟩ := fresh_exists <| E.dom ∪ free_union [fv, Context.dom, Env.fv] Var
111+
have := IH (x := x) (E := ⟨x,s⟩ :: E)
112+
grind [multiSubst_abs, entails_context_cons, multiSubst_open_var]
113+
| app => grind [multiSubst_app]
114+
115+
/-- Using soundness and the fact that the empty context
116+
is entailed by any environment, we can conclude that
117+
a well-typed term is strongly normalizing. -/
118+
theorem strong_norm {t : Term Var} {τ : Ty Base} (der : Γ ⊢ t ∶ τ) : SN t := by
119+
apply (semanticMap_saturated τ).sn
120+
apply (soundness der [] (by grind) entails_context_empty)
121+
122+
end LambdaCalculus.LocallyNameless.Stlc
123+
124+
end Cslib

‎Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean‎

Lines changed: 153 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,153 @@
1+
/-
2+
Copyright (c) 2025 David Wegmann. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: David Wegmann
5+
-/
6+
7+
module
8+
9+
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
10+
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiApp
11+
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
12+
13+
@[expose] public section
14+
15+
set_option linter.unusedDecidableInType false
16+
17+
namespace Cslib
18+
19+
universe u
20+
21+
namespace LambdaCalculus.LocallyNameless.Untyped.Term
22+
23+
variable {Var : Type u} {t t' : Term Var}
24+
25+
open FullBeta
26+
27+
attribute [grind =] Finset.union_singleton
28+
29+
/-- A term is strongly normalizing if every reduction sequence terminates at some point.
30+
This is ensured by the following type as inductive data must always be finite. -/
31+
inductive SN {α} : Term α → Prop
32+
| sn t : (∀ t', t ⭢βᶠ t' → SN t') → SN t
33+
34+
attribute [scoped grind .] SN.sn
35+
36+
/-- A single β-reduction step preserves strong normalization. -/
37+
lemma sn_step (t_st_t' : t ⭢βᶠ t') (sn_t : SN t) : SN t' := by
38+
grind [cases SN]
39+
40+
/-- Multiple β-reduction steps also preserve strong normalization. -/
41+
lemma sn_steps (t_st_t' : t ↠βᶠ t') (sn_t : SN t) : SN t' := by
42+
induction t_st_t' with grind [sn_step]
43+
44+
/-- Free variables are strongly normalizing. -/
45+
lemma sn_fvar {x : Var} : SN (fvar x) := by
46+
grind [cases FullBeta]
47+
48+
/-- An application is strongly normalizing if the left and right terms are strongly normalizing,
49+
as well as all possible future top level abstraction application beta reductions -/
50+
lemma sn_app (t s : Term Var) (sn_t : SN t) (sn_s : SN s)
51+
(hβ : ∀ {t' s' : Term Var}, t ↠βᶠ t'.abs → s ↠βᶠ s' → SN (t' ^ s')) : SN (t.app s) := by
52+
induction sn_t generalizing s with
53+
| sn t ht ih_t =>
54+
induction sn_s with
55+
| sn s hs ih_s =>
56+
constructor
57+
intro u hstep
58+
cases hstep with
59+
| beta _ _ => grind
60+
| appL _ h_s_red => apply ih_s _ h_s_red
61+
grind [Relation.ReflTransGen.head]
62+
| appR _ h_t_red => apply ih_t _ h_t_red _ (SN.sn s hs)
63+
grind [Relation.ReflTransGen.head]
64+
65+
/-- The left side of a strongly normalizing application is strongly normalizing. -/
66+
lemma sn_app_left (M N : Term Var) (lc_N : Term.LC N) (sn_MN : SN (M.app N)) :
67+
SN M := by
68+
generalize Heq : M.app N = P
69+
rw [Heq] at sn_MN
70+
induction sn_MN generalizing M N with grind
71+
72+
/-- The right side of a strongly normalizing application is strongly normalizing. -/
73+
lemma sn_app_right (M N : Term Var) (lc_N : Term.LC M) (sn_MN : SN (M.app N)) :
74+
SN N := by
75+
generalize Heq : M.app N = P
76+
rw [Heq] at sn_MN
77+
induction sn_MN generalizing M N with grind
78+
79+
/-- A neutral term is a term of the form v t₁ … t_n where
80+
v is a variable and t₁ … t_n are strongly normalizing terms. -/
81+
@[scoped grind]
82+
inductive Neutral : Term Var → Prop
83+
/-- Just a bound variable is neutral. -/
84+
| bvar : ∀ n, Neutral (bvar n)
85+
/-- Just a free variable is neutral. -/
86+
| fvar : ∀ x, Neutral (fvar x)
87+
/-- Applying a strongly normalizing term to a neutral term yields a neutral term. -/
88+
| app : ∀ t1 t2, Neutral t1 → SN t2 → Neutral (app t1 t2)
89+
90+
--attribute [scoped grind .] Neutral.bvar Neutral.fvar Neutral.app
91+
92+
/-- Neutral terms only reduce to other neutral terms in a single step -/
93+
lemma neutral_step (Hneut : Neutral t) (Hstep : t ⭢βᶠ t') : Neutral t' := by
94+
induction Hneut generalizing t' with grind [cases FullBeta, sn_step]
95+
96+
/-- Neutral terms only reduce to other neutral terms in multiple steps -/
97+
lemma neutral_steps (Hneut : Neutral t) (Hsteps : t ↠βᶠ t') : Neutral t' := by
98+
induction Hsteps <;> grind [neutral_step]
99+
100+
/-- Neutral terms are strongly normalizing. -/
101+
lemma sn_neutral (Hneut : Neutral t) : SN t := by
102+
induction Hneut with
103+
| app => grind [→ neutral_steps, sn_app]
104+
| _ => grind [cases FullBeta]
105+
106+
/-- A lambda abstraction is strongly normalizing if its body is strongly normalizing. -/
107+
lemma sn_abs [DecidableEq Var] [HasFresh Var] {M N : Term Var} (sn_MN : SN (M ^ N)) (lc_N : LC N) :
108+
SN (abs M) := by
109+
generalize h : (M ^ N) = M_open at sn_MN
110+
induction sn_MN generalizing M N with
111+
| sn =>
112+
constructor
113+
intro _ h_step
114+
cases h_step with | abs _ H => grind [step_open_cong_l _ _ _ _ H]
115+
116+
/-- A term of the form λ M N P_1 … P_n is strongly normalizing if
117+
1. N is strongly normalizing,
118+
1. M ^ N P₁ … Pₙ is strongly normalizing,
119+
1. N is locally closed,
120+
1. M ^ N P₁ … Pₙ is locally closed -/
121+
lemma sn_abs_app_multiApp [DecidableEq Var] [HasFresh Var] {Ps} {M N : Term Var}
122+
(sn_N : SN N) (sn_MNPs : SN (multiApp (M ^ N) Ps))
123+
(lc_N : LC N) (lc_MNPs : LC (multiApp (M ^ N) Ps)) : SN (multiApp (M.abs.app N) Ps) := by
124+
induction Ps with
125+
| nil =>
126+
apply sn_app
127+
· grind [sn_abs]
128+
· exact sn_N
129+
· grind [→ steps_open_cong_abs, open_abs_lc, sn_steps]
130+
| cons P Ps ih =>
131+
apply sn_app
132+
· cases lc_MNPs with grind [sn_app_left]
133+
· grind [sn_app_right]
134+
· intro Q' P' hstep1 hstep2
135+
have ⟨M', N', Ps', h_M_red, h_N_red, h_Ps_red, h_cases⟩ := invert_abs_multiApp_mst hstep1
136+
rcases h_cases with h_P | ⟨h_st1, h_st2⟩
137+
· cases Ps' with grind
138+
· have innerSteps : (M ^ N).multiApp Ps ↠βᶠ (M' ^ N').multiApp Ps' := by
139+
trans
140+
· exact steps_multiApp_r h_Ps_red (by grind)
141+
· apply steps_multiApp_l
142+
· apply steps_open_cong_abs M M' N N' <;> grind [open_abs_lc]
143+
· grind [multiApp_steps_lc]
144+
apply sn_steps
145+
· calc ((M ^ N).multiApp Ps).app P
146+
_ ↠βᶠ ((M ^ N).multiApp Ps).app P' := by grind
147+
_ ↠βᶠ Q'.abs.app P' := redex_app_l_cong (.trans innerSteps h_st2) (by grind)
148+
_ ↠βᶠ Q' ^ P' := by grind [beta]
149+
· grind
150+
151+
end LambdaCalculus.LocallyNameless.Untyped.Term
152+
153+
end Cslib

0 commit comments

Comments
 (0)