finished proof, no sorries left, but the proofs are still messy

Author: WegmannDavid

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

@@ -153,16 +153,6 @@ lemma multi_app_lc : ∀ {M P : Term Var} {Ns : List (Term Var)},
       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) :

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

@@ -102,6 +102,10 @@ lemma redex_subst_cong_lc (s s' t : Term Var) (x : Var) (step : s ⭢βᶠ s') (
 
 
 
+
+
+
+
 /-- 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]
@@ -127,6 +131,59 @@ theorem redex_abs_cong (xs : Finset Var) (cofin : ∀ x ∉ xs, (M ^ fvar x) ↠
   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_cong_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
+
+
+
 end LambdaCalculus.LocallyNameless.Untyped.Term.FullBeta
 
 end Cslib

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

@@ -103,6 +103,7 @@ theorem subst_lc {x : Var} {e u : Term Var} (e_lc : LC e) (u_lc : LC u) : LC (e
   case' abs => apply LC.abs (free_union Var)
   all_goals grind
 
+
 /-- Opening to a term `t` is equivalent to opening to a free variable and substituting for `t`. -/
 lemma subst_intro (x : Var) (t e : Term Var) (mem : x ∉ e.fv) (t_lc : LC t) :
     e ^ t = (e ^ fvar x) [ x := t ] := by grind [subst_fresh]

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

@@ -1,6 +1,7 @@
 module
 
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
 
 public section
 
@@ -15,6 +16,8 @@ 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]
 
@@ -42,6 +45,7 @@ inductive multi_app_full_beta : List (Term Var) → List (Term Var) → Prop whe
 
 
 
+
 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]
@@ -303,87 +307,109 @@ lemma neutral_sn {t : Term Var} (Hneut : neutral t) : SN t := by
       have H_neut := neutral_mst t'_neut hstep1
       contradiction
 
-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
-  intro M N sn_M
+lemma abs_sn [DecidableEq Var] [HasFresh Var] : ∀ {M N : Term Var},
+  SN (M ^ N) → LC N → SN (Term.abs M) := by
+  intro M N sn_M lc_N
   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
+      intro M N lc_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
-        · apply redex_open_cong_lc <;> try assumption
-          · sorry
-          · sorry
+        · apply FullBeta.step_open_cong1 <;> assumption
+        · assumption
         · rfl
 
-/-- 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
+lemma step_subst_cong2 [DecidableEq Var] [HasFresh Var] {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 [DecidableEq Var] [HasFresh Var] {x : Var} (s t t' : Term Var) (step : t ↠βᶠ t') (h_lc : LC s) :
+    (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
-  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
-
+  · case refl => rfl
+  · case tail t' t'' steps step ih =>
+    transitivity
+    · apply ih
+    · apply step_subst_cong2 <;> assumption
+
+lemma steps_open_cong_abs [DecidableEq Var] [HasFresh Var] (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[steps_lc]
+      · transitivity
+        · apply steps_subst_cong2
+          · assumption
+          · grind
+        · rw[←subst_intro, ←subst_intro] <;> try grind[steps_lc]
+          apply FullBeta.steps_open_cong_abs <;> try grind[steps_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
 
-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 N →
   LC (multi_app (M ^ N) Ps) →
   -------------------------------------
   SN (multi_app ((Term.abs M).app N) Ps) := by
   intro P
-  induction P <;> intros M N sn_N sn_MNPs lc_MNPs
+  induction P <;> intros M N sn_N sn_MNPs lc_N lc_MNPs
   · case nil =>
       apply sn_app
       · apply abs_sn at sn_MNPs
-        assumption
+        simp_all
       · 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 steps_open_cong_abs <;> try assumption
+          simp_all
+          apply open_abs_lc <;> assumption
         apply sn_mst <;> assumption
   · case cons P Ps ih =>
       apply sn_app
-      · apply ih
-        · assumption
+      · apply ih <;> try assumption
         · apply sn_app_left at sn_MNPs <;> grind[multi_app_lc]
         · grind[multi_app_lc]
       · apply sn_app_right at sn_MNPs
@@ -404,8 +430,10 @@ lemma multi_app_sn [DecidableEq Var] [HasFresh Var] : ∀ {Ps} {M N : Term Var},
                   · 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 steps_open_cong_abs M M' N N' <;> try assumption
+                    · apply open_abs_lc
+                      · apply lc_MNPs.1
                   · rw[multi_app_lc] at lc_MNPs
                     apply multi_app_steps_lc at h_Ps_red
                     simp_all