feat(LocallyNameless/Untyped): subst_intro weaker precondition (#666)

- New theorem `subst_intro_openRec`
- `subst_intro` no longer needs `LC t`
- `subst_intro` no longer needs `subst_fresh`
- `subst_intro` new proof based on `subst_intro_openRec`
- Updated `preservation_open` in STLC to take advantage of the weaker
precondition

Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>

Author: lengyijun

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

@@ -125,7 +125,7 @@ theorem preservation_open {xs : Finset Var}
     (cofin : ∀ x ∉ xs, ⟨x, σ⟩ :: Γ ⊢ m ^ fvar x ∶ τ) (der : Γ ⊢ n ∶ σ) :
     Γ ⊢ m ^ n ∶ τ := by
   have ⟨fresh, _⟩ := fresh_exists <| free_union [Term.fv] Var
-  grind [subst_intro fresh _ _ ?_ der.lc, typing_subst_head]
+  grind [subst_intro fresh _ _ ?_, typing_subst_head]
 
 end LambdaCalculus.LocallyNameless.Stlc.Typing
 

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

@@ -74,6 +74,16 @@ lemma subst_preserve_not_fvar {y : Var} (m n : Term Var) :
 lemma subst_refl (m : Term Var) (x : Var) : m[x := fvar x] = m := by
   induction m <;> grind
 
+lemma subst_intro_openRec {x} {t e : Term Var} (mem : x ∉ e.fv) {k : ℕ} :
+    e ⟦k ↝ t⟧ = (e ⟦ k ↝ fvar x⟧)[ x := t ] := by
+  induction e generalizing k with 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) :
+    e ^ t = (e ^ fvar x) [ x := t ] := subst_intro_openRec mem
+
+scoped grind_pattern subst_intro => open' e t, open' e (fvar x)
+
 variable [HasFresh Var]
 
 omit [DecidableEq Var] in
@@ -115,12 +125,6 @@ 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]
-
-scoped grind_pattern subst_intro => open' e t, open' e (fvar x)
-
 set_option linter.unusedDecidableInType false in
 /-- Opening of locally closed terms is locally closed. -/
 @[scoped grind ←]