splitting strong norm development into multiple files

Author: WegmannDavid

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

@@ -1,3 +1,5 @@
+module
+
 import Cslib.Foundations.Data.Relation
 import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic
 import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
@@ -21,10 +23,10 @@ open scoped Term
 
 abbrev Environment (Var : Type u) := Context Var (Term Var)
 
-def multi_subst (σ : Environment Var) (M : Term Var) : Term Var :=
+def multiSubst (σ : Environment Var) (M : Term Var) : Term Var :=
   match σ with
   | [] => M
-  | ⟨ i, sub ⟩ :: σ' => (multi_subst σ' M) [ i := sub ]
+  | ⟨ i, sub ⟩ :: σ' => (multiSubst σ' M) [ i := sub ]
 
 def fv (Ns : Environment Var) : Finset Var :=
   match Ns with
@@ -45,48 +47,48 @@ lemma context_LC_cons {Γ : Environment Var} {x : Var} {sub : Term Var} :
 
 
 
-def multi_subst_fvar_fresh (Ns : Environment Var) :
-  ∀ x ∉ Ns.dom, multi_subst Ns (Term.fvar x) = Term.fvar x := by
+def multiSubst_fvar_fresh (Ns : Environment Var) :
+  ∀ x ∉ Ns.dom, multiSubst Ns (Term.fvar x) = Term.fvar x := by
   induction Ns <;> intro x h_fresh
   · case nil =>
-      simp [multi_subst]
+      simp [multiSubst]
   · case cons N Ns ih =>
-      simp only [multi_subst]
+      simp only [multiSubst]
       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}
+lemma multiSubst_preserves_not_fvar {x : Var}
   (M : Term Var)
   (Ns : Environment Var)
   (nmem : x ∉ M.fv ∪ fv Ns) :
-  x ∉ (multi_subst Ns M).fv := by
+  x ∉ (multiSubst Ns M).fv := by
   induction Ns
   · case nil =>
-      rw[multi_subst]
+      rw[multiSubst]
       simp_all
   · case cons N Ns ih =>
-      rw[multi_subst]
+      rw[multiSubst]
       apply subst_preserve_not_fvar
       rw[fv] at nmem
       simp_all
 
 
 
-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
+def multiSubst_app (M N : Term Var) (Ps : Environment Var) :
+        multiSubst Ps (Term.app M N) = Term.app (multiSubst Ps M) (multiSubst Ps N) := by
   induction Ps
   · rfl
-  · case cons N Ns ih => rw[multi_subst,multi_subst,ih]; rfl
+  · case cons N Ns ih => rw[multiSubst,multiSubst,ih]; rfl
 
-def multi_subst_abs (M : Term Var) (Ns : Environment Var) :
-    multi_subst Ns (Term.abs M) =
-    Term.abs (multi_subst Ns M) := by
+def multiSubst_abs (M : Term Var) (Ns : Environment Var) :
+    multiSubst Ns (Term.abs M) =
+    Term.abs (multiSubst Ns M) := by
   induction Ns
   · rfl
-  · case cons N Ns ih => rw[multi_subst, ih]; rfl
+  · case cons N Ns ih => rw[multiSubst, 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
@@ -112,16 +114,16 @@ lemma open'_fvar_subst (M N : Term Var) (x : Var) (H : x ∉ Term.fv M) :
       rw[ih_r H.2]
 
 
-lemma multi_subst_open_var (M : Term Var) (Ns : Environment Var) (x : Var) :
+lemma multiSubst_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
+  (multiSubst Ns (M ^ (Term.fvar x))) =
+  (multiSubst 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[multiSubst, multiSubst]
     rw[ih]
     · rw[subst_open_var] <;> aesop
     · simp_all
@@ -131,7 +133,7 @@ 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) →
+          (∀ M N P, LC N → SN N → multiApp (M ^ N) P ∈ S → multiApp ((Term.abs M).app N) P ∈ S) →
           saturated S
 
 
@@ -142,14 +144,14 @@ def semanticMap (τ : Ty Base) : Set (Term Var) :=
   | 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 M → LC P) → LC (multi_app P Ns) := by
+lemma multiApp_lc : ∀ {M P : Term Var} {Ns : List (Term Var)},
+  LC (multiApp M Ns) → (LC M → LC P) → LC (multiApp P Ns) := by
   intro N P Ns
   induction Ns <;> intro lc_Ns lc_P
-  · simp_all[multi_app]
+  · simp_all[multiApp]
   · case cons a l ih =>
-      rw[multi_app]
-      rw[multi_app] at lc_Ns
+      rw[multiApp]
+      rw[multiApp] at lc_Ns
       cases lc_Ns
       grind
 
@@ -165,8 +167,8 @@ def semanticMap_saturated (τ : Ty Base) :
       · simp_all[neutral_sn]
       · intro M N P lc_N sn_N h_app
         constructor
-        · simp_all[multi_app_sn]
-        · apply multi_app_lc
+        · simp_all[multiApp_sn]
+        · apply multiApp_lc
           · apply h_app.2
           · intro Hlc
             constructor
@@ -209,12 +211,12 @@ def semanticMap_saturated (τ : Ty Base) :
 
 
 def entails_context (Ns : Context Var (Term Var)) (Γ : Context Var (Ty Base)) :=
-  ∀ {x τ}, ⟨ x, τ ⟩ ∈ Γ → (multi_subst Ns (Term.fvar x)) ∈ semanticMap τ
+  ∀ {x τ}, ⟨ x, τ ⟩ ∈ Γ → (multiSubst Ns (Term.fvar x)) ∈ semanticMap τ
 
 lemma entails_context_empty {Γ : Context Var (Ty Base)} :
   entails_context [] Γ := by
   intro x τ h_mem
-  rw[multi_subst]
+  rw[multiSubst]
   apply (semanticMap_saturated τ).3 <;> constructor
 
 
@@ -224,27 +226,27 @@ lemma entails_context_cons (Ns : Context Var (Term Var)) (Γ : Context Var (Ty B
   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[multiSubst]
   rw[entails_context] at h_entails
   cases h_mem
   · case head =>
-    rw[multi_subst_fvar_fresh]
+    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 multi_subst_preserves_not_fvar
+    · 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, context_LC Ns → (entails_context Ns Γ) → (multi_subst Ns t) ∈ semanticMap τ
+  ∀ Ns, context_LC Ns → (entails_context Ns Γ) → (multiSubst Ns t) ∈ semanticMap τ
 
 
 
@@ -258,20 +260,20 @@ theorem soundness {Γ : Context Var (Ty Base)} {t : Term Var} {τ : Ty Base} :
       apply hsat xσ_mem_Γ
   · case' abs σ Γ t τ L IH derivation_t =>
       intro Ns lc_Ns hsat s hsat_s
-      rw[multi_subst_abs]
+      rw[multiSubst_abs]
       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 Γ ∪ (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
+      · rw[multiApp]
+        set x := fresh (t.fv ∪ L ∪ Ns.dom ∪ fv Ns ∪ Context.dom Γ ∪ (multiSubst Ns t).fv)
+        have hfresh : x ∉ t.fv ∪ L ∪ Ns.dom ∪ fv Ns ∪ 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 [multi_subst, multi_subst_open_var, ←subst_intro] at H1
+        rw [multiSubst, multiSubst_open_var, ←subst_intro] at H1
         · apply H1
           · apply context_LC_cons
             · apply (semanticMap_saturated _).1
@@ -285,7 +287,7 @@ theorem soundness {Γ : Context Var (Ty Base)} {t : Term Var} {τ : Ty Base} :
         · aesop
   · case app derivation_t derivation_t' IH IH' =>
       intro Ns lc_Ns hsat
-      rw[multi_subst_app]
+      rw[multiSubst_app]
       apply IH Ns lc_Ns hsat
       apply IH' Ns lc_Ns hsat
 

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

@@ -76,6 +76,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
@@ -159,8 +168,10 @@ lemma invert_steps_abs {s t : Term Var} (step : s.abs ↠βᶠ t) :
           apply step_abs_cong at step
           grind
 
+
+
 lemma steps_open_cong_abs (s s' t : Term Var)
-  (steps : s.abs↠βᶠ s'.abs) (lc_s : LC s.abs) (lc_t : LC t) :
+  (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