From 896d757841634f6d05cff4d1b15e5812c10f9782 Mon Sep 17 00:00:00 2001 From: David Wegmann Date: Sun, 8 Feb 2026 19:16:45 +0100 Subject: [PATCH 1/5] added general lemmas for strong normalization of untyped lambda terms and a partially complete proof for strong norm of stlc --- .../LocallyNameless/Stlc/StrongNorm.lean | 251 ++++++++++++++++++ .../LocallyNameless/Untyped/StrongNorm.lean | 127 +++++++++ 2 files changed, 378 insertions(+) create mode 100644 Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean create mode 100644 Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean new file mode 100644 index 00000000..f3bf9f46 --- /dev/null +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean @@ -0,0 +1,251 @@ +import Cslib.Foundations.Data.Relation +import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic +import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta +import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm + +namespace Cslib + +universe u v + +namespace LambdaCalculus.LocallyNameless.Stlc + +open Untyped Typing LambdaCalculus.LocallyNameless.Untyped.Term + +variable {Var : Type u} {Base : Type v} [DecidableEq Var] [HasFresh Var] + +open LambdaCalculus.LocallyNameless.Stlc +open scoped Term + + + + + +def fv (Ns : Context Var (Term Var)) : Finset Var := + match Ns with + | [] => {} + | ⟨ _, sub ⟩ :: Ns' => sub.fv ∪ fv Ns' + +def multi_subst (σ : Context Var (Term Var)) (M : Term Var) : Term Var := + match σ with + | [] => M + | ⟨ i, sub ⟩ :: σ' => (multi_subst σ' M) [ i := sub ] + +def multi_subst_fvar_fresh (Ns : Context Var (Term Var)) : + ∀ x ∉ Ns.dom, multi_subst Ns (Term.fvar x) = Term.fvar x := by + induction Ns <;> intro x h_fresh + · case nil => + simp [multi_subst] + · case cons N Ns ih => + simp only [multi_subst] + simp only [Context.dom] at h_fresh + rw[ih] + · rw[subst_fvar] + by_cases h : N.1 = x <;> simp_all + · simp_all + +lemma multi_subst_preserves_not_fvar {x : Var} + (M : Term Var) + (Ns : Context Var (Term Var)) + (nmem : x ∉ M.fv ∪ fv Ns) : + x ∉ (multi_subst Ns M).fv := by + induction Ns + · case nil => + rw[multi_subst] + simp_all + · case cons N Ns ih => + rw[multi_subst] + apply subst_preserve_not_fvar + rw[fv] at nmem + simp_all + + + +def multi_subst_app (M N : Term Var) (Ps : Context Var (Term Var)) : + multi_subst Ps (Term.app M N) = Term.app (multi_subst Ps M) (multi_subst Ps N) := by + induction Ps + · rfl + · case cons N Ns ih => rw[multi_subst,multi_subst,ih]; rfl + +def multi_subst_abs (M : Term Var) (Ns : Context Var (Term Var)) : + multi_subst Ns (Term.abs M) = + Term.abs (multi_subst Ns M) := by + induction Ns + · rfl + · case cons N Ns ih => rw[multi_subst, ih]; rfl + +lemma open'_fvar_subst (M N : Term Var) (x : Var) (H : x ∉ Term.fv M) : + (i : Nat) → (M ⟦ i ↝ Term.fvar x ⟧) [x := N] = M ⟦ i ↝ N ⟧ := by + induction M <;> intro i + · case bvar j => + rw[Term.openRec_bvar, Term.openRec_bvar] + by_cases h : i = j <;> simp[h, Term.subst_fvar, Term.subst_bvar] + · case fvar y => + rw[Term.openRec_fvar, Term.openRec_fvar] + simp only [Term.fv, Finset.mem_singleton] at H + simp only [subst_fvar, ite_eq_right_iff] + intro H + contradiction + · case abs M ih => + rw[Term.openRec_abs, Term.openRec_abs] + rw[Term.subst_abs] + rw[ih H] + · case app l r ih_l ih_r => + rw[Term.openRec_app, Term.openRec_app] + rw[Term.subst_app] + simp only [Term.fv, Finset.mem_union, not_or] at H + rw[ih_l H.1] + rw[ih_r H.2] + +lemma swap_subst_fresh (M N P : Term Var) (x y : Var) : + (M [x := N]) [y := P] = (M [y := P]) [x := N] := by + sorry + + +lemma multi_subst_open (M P : Term Var) (Ns : Context Var (Term Var)) (x : Var) : + x ∉ M.fv ∪ fv Ns → + (multi_subst Ns (M ^ (Term.fvar x))) [x := P] = + (multi_subst Ns M) ^ P := by + intro h_fresh + induction Ns + · unfold Term.open' + rw[multi_subst, multi_subst, open'_fvar_subst] + simp_all + · case cons N Ns ih => + rw[multi_subst, multi_subst] + rw[←swap_subst_fresh] + rw[ih] + rw[subst_open] + sorry + + +def is_saturated (S : Set (Term Var)) : Prop := + (∀ M ∈ S, SN M) ∧ + (∀ M, neutral M → M ∈ S) ∧ + (∀ M N P, SN N → multi_app (M ^ N) P ∈ S → multi_app ((Term.abs M).app N) P ∈ S) + +def semanticMap (τ : Ty Base) : Set (Term Var) := + match τ with + | Ty.base _ => { t : Term Var | SN t } + | Ty.arrow τ₁ τ₂ => + { t : Term Var | ∀ s : Term Var, s ∈ semanticMap τ₁ → (Term.app t s) ∈ semanticMap τ₂ } + +def semanticMap_saturated (τ : Ty Base) : + @is_saturated Var (semanticMap τ) := by + induction τ + · case base b => + constructor + · intro M hM + exact hM + · constructor + · intro M hneut + apply neutral_sn + assumption + · intro M N P sn_N h_app + apply multi_app_sn <;> assumption + · case arrow τ₁ τ₂ ih₁ ih₂ => + constructor + · intro M hM + apply sn_app_left M (Term.fvar (fresh {})) + · constructor + · apply ih₂.1 + apply hM + apply ih₁.2.1 + constructor + · constructor + · intro M hneut s hs + apply ih₂.2.1 + apply neutral.app + · assumption + · apply ih₁.1 + exact hs + · intro M N P sn_N h_app s hs + apply ih₂.2.2 M N (s::P) + · apply sn_N + · apply h_app + assumption + + + + + +def entails_context (Ns : Context Var (Term Var)) (Γ : Context Var (Ty Base)) := + ∀ {x τ}, ⟨ x, τ ⟩ ∈ Γ → (multi_subst Ns (Term.fvar x)) ∈ semanticMap τ + +lemma entails_context_empty {Γ : Context Var (Ty Base)} : + entails_context [] Γ := by + intro x τ h_mem + rw[multi_subst] + apply (semanticMap_saturated τ).2.1 + constructor + + +lemma entails_context_cons (Ns : Context Var (Term Var)) (Γ : Context Var (Ty Base)) + (x : Var) (τ : Ty Base) (sub : Term Var) : + x ∉ Ns.dom ∪ fv Ns ∪ Γ.dom → + sub ∈ semanticMap τ → + entails_context Ns Γ → entails_context (⟨ x, sub ⟩ :: Ns) (⟨ x, τ ⟩ :: Γ) := by + intro h_fresh h_mem h_entails y σ h_mem + rw[multi_subst] + rw[entails_context] at h_entails + cases h_mem + · case head => + rw[multi_subst_fvar_fresh] + · rw[subst_fvar] + simp_all + · simp_all + · case tail h_mem => + specialize (h_entails h_mem) + rw [subst_fresh] + · assumption + · apply multi_subst_preserves_not_fvar + apply List.mem_keys_of_mem at h_mem + aesop + + + + +def entails (Γ : Context Var (Ty Base)) (t : Term Var) (τ : Ty Base) := + ∀ Ns, (entails_context Ns Γ) → (multi_subst Ns t) ∈ semanticMap τ + + + + +theorem soundness {Γ : Context Var (Ty Base)} {t : Term Var} {τ : Ty Base} : + Γ ⊢ t ∶ τ → entails Γ t τ := by + intro derivation_t + induction derivation_t + · case var Γ xσ_mem_Γ => + intro Ns hsat + apply hsat xσ_mem_Γ + · case' abs σ Γ t τ L IH derivation_t => + intro Ns hsat s hsat_s + rw[multi_subst_abs] + apply (semanticMap_saturated _).2.2 _ _ [] + · apply (semanticMap_saturated _).1 + assumption + · rw[multi_app] + set x := fresh (t.fv ∪ L ∪ Ns.dom ∪ fv Ns ∪ Context.dom Γ) + have hfresh : x ∉ t.fv ∪ L ∪ Ns.dom ∪ fv Ns ∪ Context.dom Γ := by apply fresh_notMem + have hfreshL : x ∉ L := by simp_all + have H1 := derivation_t x hfreshL + rw[entails] at H1 + specialize H1 (⟨x,s⟩ :: Ns) + rw [multi_subst, multi_subst_open] at H1 + · apply H1 + apply entails_context_cons <;> simp_all + · simp_all + · case app derivation_t derivation_t' IH IH' => + intro Ns hsat + rw[multi_subst_app] + apply IH Ns hsat + apply IH' Ns hsat + +theorem strong_norm {Γ} {t : Term Var} {τ : Ty Base} (der : Γ ⊢ t ∶ τ) : SN t := by + have H := soundness der + specialize H [] entails_context_empty + apply (semanticMap_saturated τ).1 + assumption + +end LambdaCalculus.LocallyNameless.Stlc + +end Cslib diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean new file mode 100644 index 00000000..6eba6b7c --- /dev/null +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean @@ -0,0 +1,127 @@ +module + +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta + +public section + +namespace Cslib + +universe u + +variable {Var : Type u} + + +namespace LambdaCalculus.LocallyNameless.Untyped.Term + +attribute [grind =] Finset.union_singleton + +inductive SN {α} : Term α → Prop +| sn t : (∀ t', (t ⭢βᶠ t') → SN t') → SN t + +@[aesop safe] +lemma sn_step {t t' : Term Var} (t_st_t' : t ⭢βᶠ t') (sn_t : SN t) : SN t' := by + cases sn_t; grind + +lemma sn_fvar {x : Var} : SN (Term.fvar x) := by + constructor + intro t' hstep + cases hstep + +lemma sn_app (t s : Term Var) : + SN t → + SN s → + (∀ {t' s' : Term Var}, t ↠βᶠ t'.abs → s ↠βᶠ s' → SN (t' ^ s')) → + SN (t.app s) := by + sorry + + + +lemma sn_app_left (M N : Term Var) : Term.LC N → SN (M.app N) → SN M := by + intro lc_N h_sn + generalize Heq : M.app N = P + rw[Heq] at h_sn + revert M N + induction h_sn + · case sn P h_sn ih => + intro M N lc_N Heq + rw[←Heq] at ih + constructor + intro M' h_step + apply ih (M'.app N) + apply Term.FullBeta.appR <;> assumption + · apply lc_N + · rfl + +@[aesop safe constructors] +inductive neutral : Term Var → Prop +| bvar : ∀ n, neutral (Term.bvar n) +| fvar : ∀ x, neutral (Term.fvar x) +| app : ∀ t1 t2, neutral t1 → SN t2 → neutral (Term.app t1 t2) + +@[aesop safe] +lemma neutral_step {t : Term Var} : + neutral t → ∀ t', t ⭢βᶠ t' → neutral t' := by + intro Hneut + induction Hneut <;> intro t' step + · case bvar n => + cases step + · case fvar x => + cases step + · case app IH Hneut => + cases step <;> try aesop + · contradiction + +@[aesop safe] +lemma neutral_mst {t t' : Term Var} : + neutral t → t ↠βᶠ t' → neutral t' := by + intro Hneut h_red + induction h_red <;> aesop + +lemma neutral_sn {t : Term Var} (Hneut : neutral t) : SN t := by + induction Hneut + · case bvar n => constructor; intro t' hstep; cases hstep + · case fvar x => constructor; intro t' hstep; cases hstep + · case app t1 t'_neut t1_sn t1'_sn => + apply sn_app <;> try assumption + intro t1' t2' hstep1 hstep2 + have H_neut := neutral_mst t'_neut hstep1 + contradiction + +def multi_app (f : Term Var) (args : List (Term Var)) := + match args with + | [] => f + | a :: as => Term.app (multi_app f as) a + +--lemma open_sn : ∀ {i} {M : Term Var} {N : Term Var}, +-- SN N → +-- SN (M ⟦ i ↝ N ⟧) := by sorry + +lemma abs_sn : ∀ {M : Term Var}, + SN M → SN (Term.abs M) := by + intro M sn_M + induction sn_M + · constructor + intro M' h_step + +lemma app_sn : ∀ {t u : Term Var}, + SN t → + SN u → + (∀ t' s', t ↠βᶠ (Term.abs t') → s ↠βᶠ s' → SN (t' ^ s')) → + SN (Term.app t u) := by sorry + +lemma multi_app_sn : ∀ {l} {t u : Term Var}, + SN u → + SN (multi_app (t ^ u) l) → + --------------------------- + SN (multi_app ((Term.abs t).app u) l) := by + intro l + induction l <;> intros t u sn_u sn_app + · case nil => + rw[multi_app] + rw[multi_app] at sn_app + apply app_sn <;> try assumption + · sorry + · intro t' u' hstep1 hstep2 + sorry + · case cons a l ih => + sorry From 0d664ca05fe2eb2e172c183289fda113033de103 Mon Sep 17 00:00:00 2001 From: David Wegmann Date: Sun, 15 Feb 2026 06:45:15 +0100 Subject: [PATCH 2/5] almost finished strong norm proof for stlc --- .../LocallyNameless/Stlc/StrongNorm.lean | 187 +++++++++++------- .../LocallyNameless/Untyped/Properties.lean | 4 + .../LocallyNameless/Untyped/StrongNorm.lean | 112 ++++++++--- 3 files changed, 203 insertions(+), 100 deletions(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean index f3bf9f46..8757fe22 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean @@ -18,19 +18,33 @@ open scoped Term +abbrev Environment (Var : Type u) := Context Var (Term Var) +def multi_subst (σ : Environment Var) (M : Term Var) : Term Var := + match σ with + | [] => M + | ⟨ i, sub ⟩ :: σ' => (multi_subst σ' M) [ i := sub ] -def fv (Ns : Context Var (Term Var)) : Finset Var := +def fv (Ns : Environment Var) : Finset Var := match Ns with | [] => {} | ⟨ _, sub ⟩ :: Ns' => sub.fv ∪ fv Ns' -def multi_subst (σ : Context Var (Term Var)) (M : Term Var) : Term Var := - match σ with - | [] => M - | ⟨ i, sub ⟩ :: σ' => (multi_subst σ' M) [ i := sub ] +@[simp] +def context_LC (Γ : Environment Var) : Prop := + ∀ {x M}, ⟨ x, M ⟩ ∈ Γ → LC M + +lemma context_LC_cons {Γ : Environment Var} {x : Var} {sub : Term Var} : + LC sub → context_LC Γ → context_LC (⟨ x, sub ⟩ :: Γ) := by + intro lc_sub lc_Γ y σ h_mem + cases h_mem + · assumption + · apply lc_Γ + assumption -def multi_subst_fvar_fresh (Ns : Context Var (Term Var)) : + + +def multi_subst_fvar_fresh (Ns : Environment Var) : ∀ x ∉ Ns.dom, multi_subst Ns (Term.fvar x) = Term.fvar x := by induction Ns <;> intro x h_fresh · case nil => @@ -45,7 +59,7 @@ def multi_subst_fvar_fresh (Ns : Context Var (Term Var)) : lemma multi_subst_preserves_not_fvar {x : Var} (M : Term Var) - (Ns : Context Var (Term Var)) + (Ns : Environment Var) (nmem : x ∉ M.fv ∪ fv Ns) : x ∉ (multi_subst Ns M).fv := by induction Ns @@ -60,13 +74,13 @@ lemma multi_subst_preserves_not_fvar {x : Var} -def multi_subst_app (M N : Term Var) (Ps : Context Var (Term Var)) : +def multi_subst_app (M N : Term Var) (Ps : Environment Var) : multi_subst Ps (Term.app M N) = Term.app (multi_subst Ps M) (multi_subst Ps N) := by induction Ps · rfl · case cons N Ns ih => rw[multi_subst,multi_subst,ih]; rfl -def multi_subst_abs (M : Term Var) (Ns : Context Var (Term Var)) : +def multi_subst_abs (M : Term Var) (Ns : Environment Var) : multi_subst Ns (Term.abs M) = Term.abs (multi_subst Ns M) := by induction Ns @@ -96,73 +110,96 @@ lemma open'_fvar_subst (M N : Term Var) (x : Var) (H : x ∉ Term.fv M) : rw[ih_l H.1] rw[ih_r H.2] -lemma swap_subst_fresh (M N P : Term Var) (x y : Var) : - (M [x := N]) [y := P] = (M [y := P]) [x := N] := by - sorry +lemma multi_subst_open_var (M : Term Var) (Ns : Environment Var) (x : Var) : + x ∉ Ns.dom → + context_LC Ns → + (multi_subst Ns (M ^ (Term.fvar x))) = + (multi_subst Ns M) ^ (Term.fvar x) := by + intro h_ndom h_lc + induction Ns with + | nil => rfl + | cons N Ns ih => + rw[multi_subst, multi_subst] + rw[ih] + · rw[subst_open_var] <;> aesop + · simp_all + aesop -lemma multi_subst_open (M P : Term Var) (Ns : Context Var (Term Var)) (x : Var) : - x ∉ M.fv ∪ fv Ns → - (multi_subst Ns (M ^ (Term.fvar x))) [x := P] = - (multi_subst Ns M) ^ P := by - intro h_fresh - induction Ns - · unfold Term.open' - rw[multi_subst, multi_subst, open'_fvar_subst] - simp_all - · case cons N Ns ih => - rw[multi_subst, multi_subst] - rw[←swap_subst_fresh] - rw[ih] - rw[subst_open] - sorry - +inductive saturated (S : Set (Term Var)) : Prop := +| intro : (∀ M ∈ S, LC M) → + (∀ M ∈ S, SN M) → + (∀ M, neutral M → LC M → M ∈ S) → + (∀ M N P, LC N → SN N → multi_app (M ^ N) P ∈ S → multi_app ((Term.abs M).app N) P ∈ S) → + saturated S -def is_saturated (S : Set (Term Var)) : Prop := - (∀ M ∈ S, SN M) ∧ - (∀ M, neutral M → M ∈ S) ∧ - (∀ M N P, SN N → multi_app (M ^ N) P ∈ S → multi_app ((Term.abs M).app N) P ∈ S) +@[simp] def semanticMap (τ : Ty Base) : Set (Term Var) := match τ with - | Ty.base _ => { t : Term Var | SN t } + | Ty.base _ => { t : Term Var | SN t ∧ LC t } | Ty.arrow τ₁ τ₂ => { t : Term Var | ∀ s : Term Var, s ∈ semanticMap τ₁ → (Term.app t s) ∈ semanticMap τ₂ } +lemma multi_app_lc : ∀ {M P : Term Var} {Ns : List (Term Var)}, + LC (multi_app M Ns) → LC P → LC (multi_app P Ns) := by + intro N P Ns + induction Ns <;> intro lc_Ns lc_P + · assumption + · case cons a l ih => + rw[multi_app] + rw[multi_app] at lc_Ns + cases lc_Ns + grind + def semanticMap_saturated (τ : Ty Base) : - @is_saturated Var (semanticMap τ) := by + @saturated Var (semanticMap τ) := by induction τ · case base b => constructor - · intro M hM - exact hM - · constructor - · intro M hneut - apply neutral_sn - assumption - · intro M N P sn_N h_app - apply multi_app_sn <;> assumption + · simp_all + · simp_all + · simp_all[neutral_sn] + · intro M N P lc_N sn_N h_app + constructor + · simp_all[multi_app_sn] + · apply multi_app_lc + · apply h_app.2 + · constructor + · apply LC.abs M.fv + intro x mem + sorry + · assumption · case arrow τ₁ τ₂ ih₁ ih₂ => constructor + · intro M hM + have H := ih₁.3 (.fvar (fresh {})) (.fvar (fresh {})) (.fvar (fresh {})) + specialize (hM (fvar (fresh {})) H) + apply (ih₂.1) at hM + cases hM + assumption · intro M hM apply sn_app_left M (Term.fvar (fresh {})) · constructor - · apply ih₂.1 - apply hM - apply ih₁.2.1 - constructor - · constructor - · intro M hneut s hs - apply ih₂.2.1 - apply neutral.app + · have H := ih₁.3 (.fvar (fresh {})) (.fvar (fresh {})) (.fvar (fresh {})) + specialize (hM (fvar (fresh {})) H) + apply ih₂.2 ; assumption + · intro M hneut mlc s hs + apply ih₂.3 + · constructor + · assumption + · apply ih₁.2 + assumption + · constructor · assumption · apply ih₁.1 - exact hs - · intro M N P sn_N h_app s hs - apply ih₂.2.2 M N (s::P) - · apply sn_N - · apply h_app assumption + · intro M N P lc_N sn_N h_app s hs + apply ih₂.4 M N (s::P) + · apply lc_N + · apply sn_N + · apply h_app + assumption @@ -175,8 +212,7 @@ lemma entails_context_empty {Γ : Context Var (Ty Base)} : entails_context [] Γ := by intro x τ h_mem rw[multi_subst] - apply (semanticMap_saturated τ).2.1 - constructor + apply (semanticMap_saturated τ).3 <;> constructor lemma entails_context_cons (Ns : Context Var (Term Var)) (Γ : Context Var (Ty Base)) @@ -205,7 +241,7 @@ lemma entails_context_cons (Ns : Context Var (Term Var)) (Γ : Context Var (Ty B def entails (Γ : Context Var (Ty Base)) (t : Term Var) (τ : Ty Base) := - ∀ Ns, (entails_context Ns Γ) → (multi_subst Ns t) ∈ semanticMap τ + ∀ Ns, context_LC Ns → (entails_context Ns Γ) → (multi_subst Ns t) ∈ semanticMap τ @@ -215,35 +251,44 @@ theorem soundness {Γ : Context Var (Ty Base)} {t : Term Var} {τ : Ty Base} : intro derivation_t induction derivation_t · case var Γ xσ_mem_Γ => - intro Ns hsat + intro Ns lc_Ns hsat apply hsat xσ_mem_Γ · case' abs σ Γ t τ L IH derivation_t => - intro Ns hsat s hsat_s + intro Ns lc_Ns hsat s hsat_s rw[multi_subst_abs] - apply (semanticMap_saturated _).2.2 _ _ [] + apply (semanticMap_saturated _).4 _ _ [] · apply (semanticMap_saturated _).1 assumption + · apply (semanticMap_saturated _).2 + assumption · rw[multi_app] - set x := fresh (t.fv ∪ L ∪ Ns.dom ∪ fv Ns ∪ Context.dom Γ) - have hfresh : x ∉ t.fv ∪ L ∪ Ns.dom ∪ fv Ns ∪ Context.dom Γ := by apply fresh_notMem + set x := fresh (t.fv ∪ L ∪ Ns.dom ∪ fv Ns ∪ Context.dom Γ ∪ (multi_subst Ns t).fv) + have hfresh : x ∉ t.fv ∪ L ∪ Ns.dom ∪ fv Ns ∪ Context.dom Γ ∪ (multi_subst Ns t).fv := by apply fresh_notMem have hfreshL : x ∉ L := by simp_all have H1 := derivation_t x hfreshL rw[entails] at H1 specialize H1 (⟨x,s⟩ :: Ns) - rw [multi_subst, multi_subst_open] at H1 + rw [multi_subst, multi_subst_open_var, ←subst_intro] at H1 · apply H1 - apply entails_context_cons <;> simp_all + · apply context_LC_cons + · apply (semanticMap_saturated _).1 + assumption + · assumption + · apply entails_context_cons <;> simp_all + · simp_all + · apply (semanticMap_saturated σ).1 + assumption · simp_all + · aesop · case app derivation_t derivation_t' IH IH' => - intro Ns hsat + intro Ns lc_Ns hsat rw[multi_subst_app] - apply IH Ns hsat - apply IH' Ns hsat + apply IH Ns lc_Ns hsat + apply IH' Ns lc_Ns hsat theorem strong_norm {Γ} {t : Term Var} {τ : Ty Base} (der : Γ ⊢ t ∶ τ) : SN t := by - have H := soundness der - specialize H [] entails_context_empty - apply (semanticMap_saturated τ).1 + have H := soundness der [] (by aesop) entails_context_empty + apply (semanticMap_saturated τ).2 assumption end LambdaCalculus.LocallyNameless.Stlc diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean index f72a8a98..9ba8832a 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean @@ -116,6 +116,10 @@ theorem beta_lc {M N : Term Var} (m_lc : M.abs.LC) (n_lc : LC N) : LC (M ^ N) := cases m_lc with | abs => grind [fresh_exists <| free_union [fv] Var] +@[scoped grind ←] +theorem beta_lc_reverse {M N : Term Var} (m_lc : M.abs.LC) (n_lc : LC N) : LC (M ^ N) := by + + /-- Opening then closing is equivalent to substitution. -/ @[scoped grind =] lemma open_close_to_subst (m : Term Var) (x y : Var) (k : ℕ) (m_lc : LC m) : diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean index 6eba6b7c..8eaf2763 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean @@ -32,7 +32,21 @@ lemma sn_app (t s : Term Var) : SN s → (∀ {t' s' : Term Var}, t ↠βᶠ t'.abs → s ↠βᶠ s' → SN (t' ^ s')) → SN (t.app s) := by - sorry + intro h_sn_t h_sn_s hβ + induction h_sn_t generalizing s with | sn t ht ih_t => + induction h_sn_s with | sn s hs ih_s => + constructor + intro u hstep + cases hstep with + | beta _ _ => apply hβ <;> rfl + | appL _ h_s_red => + apply ih_s _ h_s_red + intro t' s'' hstep1 hstep2 + exact hβ hstep1 (Relation.ReflTransGen.head h_s_red hstep2) + | appR _ h_t_red => + apply ih_t _ h_t_red _ (SN.sn s hs) + intro t' s' hstep1 hstep2 + exact hβ (Relation.ReflTransGen.head h_t_red hstep1) hstep2 @@ -86,42 +100,82 @@ lemma neutral_sn {t : Term Var} (Hneut : neutral t) : SN t := by intro t1' t2' hstep1 hstep2 have H_neut := neutral_mst t'_neut hstep1 contradiction - def multi_app (f : Term Var) (args : List (Term Var)) := match args with | [] => f | a :: as => Term.app (multi_app f as) a ---lemma open_sn : ∀ {i} {M : Term Var} {N : Term Var}, --- SN N → --- SN (M ⟦ i ↝ N ⟧) := by sorry - -lemma abs_sn : ∀ {M : Term Var}, - SN M → SN (Term.abs M) := by - intro M sn_M - induction sn_M - · constructor - intro M' h_step - -lemma app_sn : ∀ {t u : Term Var}, - SN t → - SN u → - (∀ t' s', t ↠βᶠ (Term.abs t') → s ↠βᶠ s' → SN (t' ^ s')) → - SN (Term.app t u) := by sorry - -lemma multi_app_sn : ∀ {l} {t u : Term Var}, - SN u → - SN (multi_app (t ^ u) l) → +lemma abs_sn : ∀ {M N : Term Var}, + SN (M ^ N) → SN (Term.abs M) := by + intro M N sn_M + generalize h : (M ^ N) = M_open at sn_M + revert N M + induction sn_M with + | sn M_open h_sn ih => + intro M N h + constructor + intro M' h_step + cases h_step with + | @abs h_M_red M' L H => + specialize ih (M' ^ N) + rw[←h] at ih + apply ih + · sorry + · rfl + +lemma step_open : ∀ {M M' N : Term Var}, + --LC N → + M ⭢βᶠ M' → + (M ^ N) ⭢βᶠ (M' ^ N) := by + intros M M' lc_n h_step + induction h_step with + | beta abs_lc n_lc => sorry + | appL lc_z st ih => + apply FullBeta.appL + · sorry + · assumption + | appR lc_z st ih => + apply FullBeta.appR + · sorry + · assumption + | abs L st ih => sorry + +/- +lemma open_sn : ∀ {M N : Term Var}, + SN (M ^ N) → + SN M := by + intro M N sn_M + generalize h : M ^ N = M_open at sn_M + revert M N + induction sn_M with + | sn M_open h_sn ih => + intro M N h + constructor + intro M' h_step + apply ih (M' ^ N) + · rw[←h] at * + apply step_open + apply h_step + · rfl +-/ + +lemma multi_app_sn : ∀ {l} {t s : Term Var}, + SN s → + SN (multi_app (t ^ s) l) → --------------------------- - SN (multi_app ((Term.abs t).app u) l) := by + SN (multi_app ((Term.abs t).app s) l) := by intro l - induction l <;> intros t u sn_u sn_app + induction l <;> intros t s sn_s tu_sn · case nil => rw[multi_app] - rw[multi_app] at sn_app - apply app_sn <;> try assumption - · sorry - · intro t' u' hstep1 hstep2 + rw[multi_app] at tu_sn + apply sn_app <;> try assumption + · apply (abs_sn tu_sn) + · intro t' s' hstep1 hstep2 sorry · case cons a l ih => - sorry + rw[multi_app] + apply sn_app + · apply ih + · assumption + · sorry From 24d92dbae1a0e61290fe2a7ad36624c06214ae60 Mon Sep 17 00:00:00 2001 From: David Wegmann Date: Sun, 15 Feb 2026 06:47:15 +0100 Subject: [PATCH 3/5] removed beta_lc_reverse --- .../LambdaCalculus/LocallyNameless/Untyped/Properties.lean | 3 --- 1 file changed, 3 deletions(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean index 9ba8832a..e06e6f87 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean @@ -116,9 +116,6 @@ theorem beta_lc {M N : Term Var} (m_lc : M.abs.LC) (n_lc : LC N) : LC (M ^ N) := cases m_lc with | abs => grind [fresh_exists <| free_union [fv] Var] -@[scoped grind ←] -theorem beta_lc_reverse {M N : Term Var} (m_lc : M.abs.LC) (n_lc : LC N) : LC (M ^ N) := by - /-- Opening then closing is equivalent to substitution. -/ @[scoped grind =] From 56ff9b99d3595e435978b2dfbc0a02cee167a596 Mon Sep 17 00:00:00 2001 From: David Wegmann Date: Mon, 16 Feb 2026 19:19:52 +0100 Subject: [PATCH 4/5] finished strong norm proof for stlc, but still depends on sorries in Untyped/StrongNorm --- .../LocallyNameless/Stlc/StrongNorm.lean | 25 ++++++++++++++----- .../LocallyNameless/Untyped/StrongNorm.lean | 6 +++-- 2 files changed, 23 insertions(+), 8 deletions(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean index 8757fe22..e4ba4ef2 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean @@ -2,6 +2,7 @@ import Cslib.Foundations.Data.Relation import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm +import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt namespace Cslib @@ -142,16 +143,28 @@ def semanticMap (τ : Ty Base) : Set (Term Var) := { t : Term Var | ∀ s : Term Var, s ∈ semanticMap τ₁ → (Term.app t s) ∈ semanticMap τ₂ } lemma multi_app_lc : ∀ {M P : Term Var} {Ns : List (Term Var)}, - LC (multi_app M Ns) → LC P → LC (multi_app P Ns) := by + LC (multi_app M Ns) → (LC M → LC P) → LC (multi_app P Ns) := by intro N P Ns induction Ns <;> intro lc_Ns lc_P - · assumption + · simp_all[multi_app] · case cons a l ih => rw[multi_app] rw[multi_app] at lc_Ns cases lc_Ns grind +theorem lcAt_openRec_lcAt (M N : Term Var) (i : ℕ) : + LcAt i (M⟦i ↝ N⟧) → LcAt (i + 1) M := by + induction M generalizing i <;> try grind + +lemma open_abs_lc : forall {M N : Term Var}, + LC (M ^ N) → LC (M.abs) := by + intro M N hlc + rw[←lcAt_iff_LC] + rw[←lcAt_iff_LC] at hlc + apply lcAt_openRec_lcAt _ _ _ hlc + + def semanticMap_saturated (τ : Ty Base) : @saturated Var (semanticMap τ) := by induction τ @@ -165,10 +178,10 @@ def semanticMap_saturated (τ : Ty Base) : · simp_all[multi_app_sn] · apply multi_app_lc · apply h_app.2 - · constructor - · apply LC.abs M.fv - intro x mem - sorry + · intro Hlc + constructor + · apply open_abs_lc + assumption · assumption · case arrow τ₁ τ₂ ih₁ ih₂ => constructor diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean index 8eaf2763..d88c6f14 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean @@ -120,7 +120,7 @@ lemma abs_sn : ∀ {M N : Term Var}, specialize ih (M' ^ N) rw[←h] at ih apply ih - · sorry + · sorry -- True, maybe lc issue · rfl lemma step_open : ∀ {M M' N : Term Var}, @@ -162,7 +162,7 @@ lemma open_sn : ∀ {M N : Term Var}, lemma multi_app_sn : ∀ {l} {t s : Term Var}, SN s → SN (multi_app (t ^ s) l) → - --------------------------- + ------------------------------------- SN (multi_app ((Term.abs t).app s) l) := by intro l induction l <;> intros t s sn_s tu_sn @@ -179,3 +179,5 @@ lemma multi_app_sn : ∀ {l} {t s : Term Var}, · apply ih · assumption · sorry + sorry + sorry From 22eed1377d837628bce4b02716fba51a17634fdf Mon Sep 17 00:00:00 2001 From: David Wegmann Date: Tue, 24 Feb 2026 20:41:51 +0100 Subject: [PATCH 5/5] almost finished strong norm proof, some lc issues remaining --- .../LocallyNameless/Untyped/FullBeta.lean | 23 ++ .../LocallyNameless/Untyped/StrongNorm.lean | 354 +++++++++++++++--- 2 files changed, 319 insertions(+), 58 deletions(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean index bb0a866c..ed2f614e 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean @@ -55,6 +55,8 @@ lemma step_lc_l (step : M ⭢βᶠ M') : LC M := by induction step <;> constructor all_goals assumption + + /-- Left congruence rule for application in multiple reduction. -/ @[scoped grind ←] theorem redex_app_l_cong (redex : M ↠βᶠ M') (lc_N : LC N) : app M N ↠βᶠ app M' N := by @@ -86,6 +88,20 @@ lemma redex_subst_cong (s s' : Term Var) (x y : Var) (step : s ⭢βᶠ s') : case abs => grind [abs <| free_union Var] all_goals grind +/-- Substitution respects a single reduction step. -/ +lemma redex_subst_cong_lc (s s' t : Term Var) (x : Var) (step : s ⭢βᶠ s') (h_lc : LC t) : + s [ x := t ] ⭢βᶠ s' [ x := t ] := by + induction step + case beta m n abs_lc n_lc => + cases abs_lc with | abs xs _ mem => + rw [subst_open x t n m (by grind)] + refine beta ?_ (by grind) + exact subst_lc (LC.abs xs m mem) h_lc + case abs => grind [abs <| free_union Var] + all_goals grind + + + /-- Abstracting then closing preserves a single reduction. -/ lemma step_abs_close {x : Var} (step : M ⭢βᶠ M') : M⟦0 ↜ x⟧.abs ⭢βᶠ M'⟦0 ↜ x⟧.abs := by grind [abs ∅, redex_subst_cong] @@ -97,6 +113,13 @@ lemma redex_abs_close {x : Var} (step : M ↠βᶠ M') : (M⟦0 ↜ x⟧.abs ↠ case single ih => exact Relation.ReflTransGen.single (step_abs_close ih) case trans l r => exact Relation.ReflTransGen.trans l r +/-- Multiple reduction of opening implies multiple reduction of abstraction. -/ +theorem step_abs_cong (xs : Finset Var) (cofin : ∀ x ∉ xs, (M ^ fvar x) ⭢βᶠ (M' ^ fvar x)) : + M.abs ⭢βᶠ M'.abs := by + have ⟨fresh, _⟩ := fresh_exists <| free_union [fv] Var + rw [open_close fresh M 0 ?_, open_close fresh M' 0 ?_] + all_goals grind [step_abs_close] + /-- Multiple reduction of opening implies multiple reduction of abstraction. -/ theorem redex_abs_cong (xs : Finset Var) (cofin : ∀ x ∉ xs, (M ^ fvar x) ↠βᶠ (M' ^ fvar x)) : M.abs ↠βᶠ M'.abs := by diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean index d88c6f14..2957f007 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean @@ -15,13 +15,196 @@ namespace LambdaCalculus.LocallyNameless.Untyped.Term attribute [grind =] Finset.union_singleton +lemma steps_lc_l [DecidableEq Var] [HasFresh Var] {M M' : Term Var} (steps : M ↠βᶠ M') (lc_M : LC M) : LC M' := by + induction steps <;> grind[FullBeta.step_lc_r] + +lemma steps_lc [DecidableEq Var] [HasFresh Var] + {M M' : Term Var} (steps : M ↠βᶠ M') (lc_M : LC M) : LC M' := by + induction steps <;> grind[FullBeta.step_lc_r] + +lemma steps_lc_or_rfl [HasFresh Var] [DecidableEq Var] {M M' : Term Var} : + M ↠βᶠ M' → + LC M' ∨ M = M' := by + intro redex + cases redex <;> grind[FullBeta.step_lc_r] + +@[simp] +def multi_app (f : Term Var) (args : List (Term Var)) := + match args with + | [] => f + | a :: as => Term.app (multi_app f as) a + + +@[reduction_sys "βᶠ"] +inductive multi_app_full_beta : List (Term Var) → List (Term Var) → Prop where +| step : N ⭢βᶠ N' → (∀ N ∈ Ns, LC N) → multi_app_full_beta (N :: Ns) (N' :: Ns) +| cons : LC N → multi_app_full_beta Ns Ns' → multi_app_full_beta (N :: Ns) (N :: Ns') + + + +lemma multi_app_step_lc_r [DecidableEq Var] [HasFresh Var] + {Ns Ns' : List (Term Var)} (step : Ns ⭢βᶠ Ns') : (∀ N ∈ Ns', LC N) := by + induction step <;> grind[FullBeta.step_lc_r] + +lemma multi_app_steps_lc [DecidableEq Var] [HasFresh Var] + {Ns Ns' : List (Term Var)} (step : Ns ↠βᶠ Ns') (H : ∀ N ∈ Ns, LC N) : (∀ N ∈ Ns', LC N) := by + induction step <;> grind[FullBeta.step_lc_r, multi_app_step_lc_r] + + +@[scoped grind ←] +lemma multi_app_lc {M : Term Var} {Ns : List (Term Var)} : + LC (M.multi_app Ns) ↔ + LC M ∧ + (∀ N ∈ Ns, LC N) + := by + constructor + · induction Ns + · case nil => grind[multi_app] + · case cons N Ns ih => + intro h_lc + cases h_lc + grind + · induction Ns <;> grind[multi_app, LC.app] + +@[scoped grind ←] +lemma step_multi_app_l {M M' : Term Var} {Ns : List (Term Var)} : + M ⭢βᶠ M' → + (∀ N ∈ Ns, LC N) → + M.multi_app Ns ⭢βᶠ M'.multi_app Ns := by + induction Ns <;> grind[multi_app, FullBeta.appR] + +@[scoped grind ←] +lemma step_multi_app_r {M : Term Var} {Ns Ns' : List (Term Var)} : + Ns ⭢βᶠ Ns' → + LC M → + M.multi_app Ns ⭢βᶠ M.multi_app Ns' := by + intro Ns_red; induction Ns_red <;> grind[multi_app,FullBeta.appL,FullBeta.appR] + + + +@[scoped grind ←] +lemma steps_multi_app_l {M M' : Term Var} {Ns : List (Term Var)} : + M ↠βᶠ M' → + (∀ N ∈ Ns, LC N) → + M.multi_app Ns ↠βᶠ M'.multi_app Ns := by + intro redex + induction redex <;> grind + +@[scoped grind ←] +lemma steps_multi_app_r {M : Term Var} {Ns Ns' : List (Term Var)} : + Ns ↠βᶠ Ns' → + LC M → + M.multi_app Ns ↠βᶠ M.multi_app Ns' := by + intro Ns_red; induction Ns_red <;> grind[multi_app,FullBeta.appL,FullBeta.appR] + + +lemma invert_multi_app_st [DecidableEq Var] [HasFresh Var] : ∀ {Ps} {M N Q : Term Var}, + multi_app (M.abs.app N) Ps ⭢βᶠ Q → + (∃ M', M.abs ⭢βᶠ Term.abs M' ∧ Q = multi_app (M'.abs.app N) Ps) ∨ + (∃ N', N ⭢βᶠ N' ∧ Q = multi_app (M.abs.app N') Ps) ∨ + (∃ Ps', Ps ⭢βᶠ Ps' ∧ Q = multi_app (M.abs.app N) Ps') ∨ + (Q = multi_app (M ^ N) Ps) := by + intro Ps + induction Ps with + | nil => + intro N N P h_red + rw[multi_app] at h_red + rw[multi_app] + cases h_red + · case beta abs_lc n_lc => aesop + · case appL M N' lc_z h_red => aesop + · case appR M M' lc_z h_red => + left + cases lc_z + · case abs M' xs h_lc => + exists M' + constructor + · apply FullBeta.step_abs_cong + assumption + · rfl + | cons P Ps ih => + intro M N Q h_red + have h_lc := (FullBeta.step_lc_l h_red) + rw [multi_app] at h_red + generalize Heq : (M.abs.app N).multi_app Ps = Q' + rw[Heq] at h_red + cases h_red + · case beta abs_lc n_lc => cases Ps <;> contradiction + · case appL Y M P' lc_z h_red => + right + right + left + exists (P' :: Ps) + constructor + · constructor + · assumption + · rw[multi_app_lc] at h_lc + simp_all + · aesop + · case appR M Q'' h_red P_lc => + rw[←Heq] at h_red + match (ih h_red) with + | .inl ⟨ M', st, Heq' ⟩ => aesop + | .inr (.inl ⟨ N', st, Heq' ⟩) => aesop + | .inr (.inr (.inl ⟨ Ps', st, Heq' ⟩)) => + right + right + left + exists (P :: Ps') + constructor + · constructor <;> assumption + · aesop + | .inr (.inr (.inr Heq')) => aesop + +lemma invert_multi_app_mst [DecidableEq Var] [HasFresh Var] : ∀ {Ps} {M N Q : Term Var}, + multi_app (M.abs.app N) Ps ↠βᶠ Q → + ∃ M' N' Ns', M.abs ↠βᶠ M'.abs ∧ N ↠βᶠ N' ∧ Ps ↠βᶠ Ns' ∧ + (Q = multi_app (M'.abs.app N') Ns' ∨ + (multi_app (M.abs.app N) Ps ↠βᶠ multi_app (M'^ N') Ns' ∧ + multi_app (M'^ N') Ns' ↠βᶠ Q)) := by + intro Ps M N Q h_red + induction h_red + · case refl => grind + · case tail Q' Q'' steps step ih => + match ih with + | ⟨ M', N', Ps', st_M, st_N, st_Ps, Cases ⟩ => + match Cases with + | .inl Heq => + rw[Heq] at step + match (invert_multi_app_st step) with + | .inl ⟨ M'', st, HeqM'' ⟩ => grind + | .inr (.inl ⟨ N', st, Heq' ⟩) => grind + | .inr (.inr (.inl ⟨ Ps', st, Heq' ⟩)) => grind + | .inr (.inr (.inr Heq')) => grind + | .inr ⟨ steps1, steps2 ⟩ => + exists M', N', Ps' + constructor + · assumption + · constructor + · assumption + · constructor + · assumption + · right + constructor + · assumption + · transitivity + · assumption + · apply Relation.ReflTransGen.single + assumption + + + inductive SN {α} : Term α → Prop -| sn t : (∀ t', (t ⭢βᶠ t') → SN t') → SN t +| sn t : (∀ (t' : Term α), (t ⭢βᶠ t') → SN t') → SN t @[aesop safe] lemma sn_step {t t' : Term Var} (t_st_t' : t ⭢βᶠ t') (sn_t : SN t) : SN t' := by cases sn_t; grind +@[aesop safe] +lemma sn_mst {t t' : Term Var} (t_st_t' : t ↠βᶠ t') (sn_t : SN t) : SN t' := by + induction t_st_t' <;> grind[sn_step] + lemma sn_fvar {x : Var} : SN (Term.fvar x) := by constructor intro t' hstep @@ -63,7 +246,23 @@ lemma sn_app_left (M N : Term Var) : Term.LC N → SN (M.app N) → SN M := by intro M' h_step apply ih (M'.app N) apply Term.FullBeta.appR <;> assumption - · apply lc_N + · assumption + · rfl + +lemma sn_app_right (M N : Term Var) : Term.LC M → SN (M.app N) → SN N := by + intro lc_N h_sn + generalize Heq : M.app N = P + rw[Heq] at h_sn + revert M N + induction h_sn + · case sn P h_sn ih => + intro M N lc_N Heq + rw[←Heq] at ih + constructor + intro N' h_step + apply ih (M.app N') + apply Term.FullBeta.appL <;> assumption + · assumption · rfl @[aesop safe constructors] @@ -84,6 +283,9 @@ lemma neutral_step {t : Term Var} : · case app IH Hneut => cases step <;> try aesop · contradiction + constructor + · assumption + · apply sn_step <;> assumption @[aesop safe] lemma neutral_mst {t t' : Term Var} : @@ -100,10 +302,9 @@ lemma neutral_sn {t : Term Var} (Hneut : neutral t) : SN t := by intro t1' t2' hstep1 hstep2 have H_neut := neutral_mst t'_neut hstep1 contradiction -def multi_app (f : Term Var) (args : List (Term Var)) := - match args with - | [] => f - | a :: as => Term.app (multi_app f as) a + +lemma redex_open_cong_lc (s s' t : Term Var) (step : s.abs ⭢βᶠ s'.abs) (h_lc : LC t) : + (s ^ t) ⭢βᶠ (s' ^ t) := by sorry lemma abs_sn : ∀ {M N : Term Var}, SN (M ^ N) → SN (Term.abs M) := by @@ -120,64 +321,101 @@ lemma abs_sn : ∀ {M N : Term Var}, specialize ih (M' ^ N) rw[←h] at ih apply ih - · sorry -- True, maybe lc issue + · apply redex_open_cong_lc <;> try assumption + · sorry + · sorry · rfl -lemma step_open : ∀ {M M' N : Term Var}, - --LC N → - M ⭢βᶠ M' → +/-- Substitution respects a single reduction step. -/ +lemma redex_subst_cong_lc (s s' t : Term Var) (x : Var) (step : s ⭢βᶠ s') (h_lc : LC t) : + s [ x := t ] ⭢βᶠ s' [ x := t ] := by + induction step + case beta m n abs_lc n_lc => + cases abs_lc with | abs xs _ mem => + rw [subst_open x t n m (by grind)] + refine beta ?_ (by grind) + exact subst_lc (LC.abs xs m mem) h_lc + case abs => grind [abs <| free_union Var] + all_goals grind + + +lemma step_open [DecidableEq Var] [HasFresh Var] : ∀ {M M' N : Term Var}, + LC N → + M.abs ⭢βᶠ M'.abs → (M ^ N) ⭢βᶠ (M' ^ N) := by - intros M M' lc_n h_step - induction h_step with - | beta abs_lc n_lc => sorry - | appL lc_z st ih => - apply FullBeta.appL - · sorry - · assumption - | appR lc_z st ih => - apply FullBeta.appR - · sorry - · assumption - | abs L st ih => sorry + intro M M' N lc_N h_step + cases h_step + · case abs L h_step => + let x := fresh (L ∪ M.fv ∪ M'.fv ∪ N.fv) + have x_fresh : x ∉ L ∪ M.fv ∪ M'.fv ∪ N.fv := by apply fresh_notMem + specialize h_step x (by simp_all) + rw[subst_intro x _ M (by simp_all) lc_N] + rw[subst_intro x _ M' (by simp_all) lc_N] + apply FullBeta.redex_subst_cong_lc + · assumption + assumption -/- -lemma open_sn : ∀ {M N : Term Var}, - SN (M ^ N) → - SN M := by - intro M N sn_M - generalize h : M ^ N = M_open at sn_M - revert M N - induction sn_M with - | sn M_open h_sn ih => - intro M N h - constructor - intro M' h_step - apply ih (M' ^ N) - · rw[←h] at * - apply step_open - apply h_step - · rfl --/ - -lemma multi_app_sn : ∀ {l} {t s : Term Var}, - SN s → - SN (multi_app (t ^ s) l) → + + + +lemma redex_open_cong_lc' (s s' t t' : Term Var) (step1 : t ↠βᶠ t') (step2 : s.abs ↠βᶠ s'.abs) (h_lc : LC t) : + (s ^ t) ↠βᶠ (s' ^ t') := by sorry + +lemma multi_app_sn [DecidableEq Var] [HasFresh Var] : ∀ {Ps} {M N : Term Var}, + SN N → + SN (multi_app (M ^ N) Ps) → + LC (multi_app (M ^ N) Ps) → ------------------------------------- - SN (multi_app ((Term.abs t).app s) l) := by - intro l - induction l <;> intros t s sn_s tu_sn + SN (multi_app ((Term.abs M).app N) Ps) := by + intro P + induction P <;> intros M N sn_N sn_MNPs lc_MNPs · case nil => - rw[multi_app] - rw[multi_app] at tu_sn - apply sn_app <;> try assumption - · apply (abs_sn tu_sn) - · intro t' s' hstep1 hstep2 - sorry - · case cons a l ih => - rw[multi_app] + apply sn_app + · apply abs_sn at sn_MNPs + assumption + · assumption + · intro M' N' hstep1 hstep2 + rw[multi_app] at sn_MNPs + have Hmst : (M ^ N) ↠βᶠ (M' ^ N') := by + apply redex_open_cong_lc' <;> try assumption + · sorry + apply sn_mst <;> assumption + · case cons P Ps ih => apply sn_app · apply ih · assumption - · sorry - sorry - sorry + · apply sn_app_left at sn_MNPs <;> grind[multi_app_lc] + · grind[multi_app_lc] + · apply sn_app_right at sn_MNPs + · assumption + · cases lc_MNPs + assumption + · intro Q' P' hstep1 hstep2 + match (invert_multi_app_mst hstep1) with + | ⟨ M', N', Ps', h_M_red, h_N_red, h_Ps_red, h_cases ⟩ => + match h_cases with + | Or.inl h_P => cases Ps' <;> rw[multi_app] at h_cases <;> contradiction + | Or.inr ⟨ h_st1, h_st2 ⟩ => + have H1 : (multi_app (M ^ N) Ps).app P ↠βᶠ Q' ^ P' := by + have H2 : (multi_app (M ^ N) Ps) ↠βᶠ (M' ^ N').multi_app Ps' := by + transitivity + · apply steps_multi_app_r + · assumption + · rw[multi_app_lc] at lc_MNPs + simp_all + · apply steps_multi_app_l + · apply redex_open_cong_lc' <;> try assumption + · sorry + · rw[multi_app_lc] at lc_MNPs + apply multi_app_steps_lc at h_Ps_red + simp_all + have H3 : (multi_app (M ^ N) Ps) ↠βᶠ Q'.abs := by + transitivity <;> try assumption + have H4 : Q'.abs.app P' ↠βᶠ Q' ^ P' := by grind[FullBeta.beta, steps_lc_l] + have H4 : ((M ^ N).multi_app Ps).app P ↠βᶠ Q'.abs.app P' := by + cases lc_MNPs + transitivity + · apply FullBeta.redex_app_r_cong <;> assumption + · apply FullBeta.redex_app_l_cong <;> grind[steps_lc_l] + transitivity <;> try assumption + apply sn_mst <;> try assumption