added general lemmas for strong normalization of untyped lambda terms…

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

@@ -0,0 +1,175 @@
+module
+
+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
+import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiSubst
+
+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
+
+
+
+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 → multiApp (M ^ N) P ∈ S → multiApp ((Term.abs M).app N) P ∈ S) →
+          saturated S
+
+
+@[simp]
+def semanticMap (τ : Ty Base) : Set (Term Var) :=
+  match τ with
+  | Ty.base _ => { t : Term Var | SN t ∧ LC t }
+  | Ty.arrow τ₁ τ₂ =>
+    { t : Term Var | ∀ s : Term Var, s ∈ semanticMap τ₁ → (Term.app t s) ∈ semanticMap τ₂ }
+
+
+
+def semanticMap_saturated (τ : Ty Base) :
+    @saturated Var (semanticMap τ) := by
+  induction τ
+  · case base b =>
+      constructor
+      · simp_all
+      · simp_all
+      · simp_all[neutral_sn]
+      · intro M N P lc_N sn_N h_app
+        constructor
+        · simp_all[multiApp_sn]
+        · have H := h_app.2
+          rw[multiApp_lc] at *
+          grind[open_abs_lc]
+  · 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
+        · 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
+            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
+
+
+
+
+
+def entails_context (Ns : Term.Environment Var) (Γ : Context Var (Ty Base)) :=
+  ∀ {x τ}, ⟨ x, τ ⟩ ∈ Γ → (multiSubst Ns (Term.fvar x)) ∈ semanticMap τ
+
+lemma entails_context_empty {Γ : Context Var (Ty Base)} :
+  entails_context [] Γ := by
+  intro x τ h_mem
+  rw[multiSubst]
+  apply (semanticMap_saturated τ).3 <;> constructor
+
+
+lemma entails_context_cons (Ns : Term.Environment Var) (Γ : Context Var (Ty Base))
+  (x : Var) (τ : Ty Base) (sub : Term Var) :
+  x ∉ Ns.dom ∪ Ns.fv ∪ Γ.dom →
+  sub ∈ semanticMap τ →
+  entails_context Ns Γ → entails_context (⟨ x, sub ⟩ :: Ns) (⟨ x, τ ⟩ :: Γ) := by
+  intro h_fresh h_mem h_entails y σ h_mem
+  rw[multiSubst]
+  rw[entails_context] at h_entails
+  cases h_mem
+  · case head =>
+    rw[multiSubst_fvar_fresh]
+    · rw[subst_fvar]
+      simp_all
+    · simp_all
+  · case tail h_mem =>
+    specialize (h_entails h_mem)
+    rw [subst_fresh]
+    · assumption
+    · apply multiSubst_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, env_LC Ns → (entails_context Ns Γ) → (multiSubst 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 lc_Ns hsat
+      apply hsat xσ_mem_Γ
+  · case' abs σ Γ t τ L IH derivation_t =>
+      intro Ns lc_Ns hsat s hsat_s
+      rw[multiSubst_abs]
+      apply (semanticMap_saturated _).4 _ _ []
+      · apply (semanticMap_saturated _).1
+        assumption
+      · apply (semanticMap_saturated _).2
+        assumption
+      · rw[multiApp]
+        set x := fresh (t.fv ∪ L ∪ Ns.dom ∪ Ns.fv ∪ Context.dom Γ ∪ (multiSubst Ns t).fv)
+        have hfresh : x ∉ t.fv ∪ L ∪ Ns.dom ∪ Ns.fv ∪ Context.dom Γ  ∪ (multiSubst 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 [multiSubst, multiSubst_open_var, ←subst_intro] at H1
+        · apply H1
+          · apply env_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 lc_Ns hsat
+      rw[multiSubst_app]
+      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 [] (by aesop) entails_context_empty
+  apply (semanticMap_saturated τ).2
+  assumption
+
+end LambdaCalculus.LocallyNameless.Stlc
+
+end Cslib

Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean

@@ -8,6 +8,7 @@ module
 
 public import Cslib.Foundations.Data.Relation
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
 
 public section
 
@@ -55,6 +56,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
@@ -74,6 +77,15 @@ lemma step_lc_r (step : M ⭢βᶠ M') : LC M' := by
   case' abs => constructor; assumption
   all_goals grind
 
+lemma steps_lc {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 {M M' : Term Var} :
+  M ↠βᶠ M' →
+  LC M' ∨ M = M' := by
+  intro redex
+  cases redex <;> grind[FullBeta.step_lc_r]
+
 /-- Substitution respects a single reduction step. -/
 lemma redex_subst_cong (s s' : Term Var) (x y : Var) (step : s ⭢βᶠ s') :
     s [ x := fvar y ] ⭢βᶠ s' [ x := fvar y ] := by
@@ -86,6 +98,24 @@ 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,13 +127,121 @@ 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
   have ⟨fresh, _⟩ := fresh_exists <| free_union [fv] Var
   rw [open_close fresh M 0 ?_, open_close fresh M' 0 ?_]
   all_goals grind [redex_abs_close]
 
+theorem redex_abs_fvar_finset_exists (xs : Finset Var)
+  (M M' : Term Var)
+  (step : M.abs ⭢βᶠ M'.abs) :
+  ∃ (L : Finset Var), ∀ x ∉ L, (M ^ fvar x) ⭢βᶠ (M' ^ fvar x) := by
+  cases step
+  case abs L cofin => exists L
+
+
+lemma step_open_cong1 (s s' t : Term Var) (L : Finset Var)
+  (step : ∀ x ∉ L, (s ^ (fvar x)) ⭢βᶠ (s' ^ (fvar x))) (h_lc : LC t) :
+  (s ^ t) ⭢βᶠ (s' ^ t) := by
+  let x := fresh (L ∪ s.fv ∪ s'.fv)
+  have H : x ∉ (L ∪ s.fv ∪ s'.fv) := fresh_notMem (L ∪ s.fv ∪ s'.fv)
+  rw[subst_intro x t s, subst_intro x t s'] <;> simp_all[redex_subst_cong_lc]
+
+lemma invert_steps_abs {s t : Term Var} (step : s.abs ↠βᶠ t) :
+  ∃ (s' : Term Var), s.abs ↠βᶠ s'.abs ∧ t = s'.abs := by
+  induction step
+  · case refl => aesop
+  · case tail steps step ih =>
+      match ih with
+      | ⟨ s', step_s, eq⟩ =>
+        rw[eq] at step
+        cases step
+        · case abs s'' L step =>
+          apply step_abs_cong at step
+          grind
+
+
+
+lemma steps_open_l_abs (s s' t : Term Var)
+  (steps : s.abs ↠βᶠ s'.abs) (lc_s : LC 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
+  revert s s'
+  induction steps
+  · case refl => grind
+  · case tail steps step ih =>
+    intro s s'' lc_sabs eq1 eq2
+    rw[←eq1] at steps
+    match (invert_steps_abs steps) with
+    | ⟨s', step_s, eq⟩ =>
+      specialize (ih s s' lc_sabs eq1 eq.symm)
+      transitivity
+      · apply ih
+      · rw[eq,←eq2] at step
+        apply Relation.ReflTransGen.single
+        have ⟨ L, cofin⟩ := redex_abs_fvar_finset_exists (free_union [fv] Var) s' s'' step
+        apply step_open_cong1
+        · assumption
+        · assumption
+
+lemma step_subst_r {x : Var} (s t t' : Term Var) (step : t ⭢βᶠ t') (h_lc : LC s) :
+    (s [ x := t ]) ↠βᶠ (s [ x := t' ]) := by
+  induction h_lc
+  · case fvar y =>
+      rw[Term.subst_fvar, Term.subst_fvar]
+      grind
+  · case abs L N h_lc ih =>
+      simp[subst_abs]
+      apply FullBeta.redex_abs_cong (L ∪ {x})
+      intro y h_fresh
+      rw[←Term.subst_open_var, ←Term.subst_open_var] <;> try grind[FullBeta.step_lc_r, FullBeta.step_lc_l]
+  · case app l r ih_l ih_r =>
+    transitivity
+    · apply FullBeta.redex_app_r_cong
+      · apply ih_r
+      · grind[Term.subst_lc, FullBeta.step_lc_l]
+    · apply FullBeta.redex_app_l_cong
+      · apply ih_l
+      · grind[Term.subst_lc, FullBeta.step_lc_r]
+
+lemma steps_subst_cong2 {x : Var} (s t t' : Term Var) (step : t ↠βᶠ t') (h_lc : LC s) :
+    (s [ x := t ]) ↠βᶠ (s [ x := t' ]) := by
+  induction step
+  · case refl => rfl
+  · case tail t' t'' steps step ih =>
+    transitivity
+    · apply ih
+    · apply step_subst_r <;> assumption
+
+lemma steps_open_cong_abs (s s' t t' : Term Var)
+    (step1 : t ↠βᶠ t')
+    (step2 : s.abs ↠βᶠ s'.abs)
+    (lc_t : LC t)
+    (lc_s : LC s.abs) :
+    (s ^ t) ↠βᶠ (s' ^ t') := by
+    have lcsabs := lc_s
+    cases lc_s
+    · case abs _ L h_lc =>
+      let x := fresh (L ∪ s.fv ∪ s'.fv ∪ t.fv ∪ t'.fv)
+      have H : x ∉ (L ∪ s.fv ∪ s'.fv ∪ t.fv ∪ t'.fv) := fresh_notMem _
+      rw[subst_intro x t s, subst_intro x t' s'] <;> try grind[FullBeta.steps_lc]
+      · transitivity
+        · apply steps_subst_cong2
+          · assumption
+          · grind
+        · rw[←subst_intro, ←subst_intro] <;> try grind[FullBeta.steps_lc]
+          · apply FullBeta.steps_open_l_abs <;> try grind[FullBeta.steps_lc]
+
 end LambdaCalculus.LocallyNameless.Untyped.Term.FullBeta
 
 end Cslib

Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean

@@ -86,4 +86,15 @@ theorem lcAt_iff_LC (M : Term Var) [HasFresh Var] : LcAt 0 M ↔ M.LC := by
         grind [fresh_exists L]
     | _ => grind [cases LC]
 
+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 [HasFresh Var] : 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
+
 end Cslib.LambdaCalculus.LocallyNameless.Untyped.Term