Untyped Lambda Calculus (various incomplete proofs)

stlc.lean

import tactic

-- I will stop myself from writing incomplete lambda calculus "things" on Lean. In the future this will be a nice project, but not now.

@[derive decidable_eq]
inductive term : Type
| app (M N : term) : term
| lam (M : term) : term
| var (x : ℕ) : term

open term

-- Suggested by Mario Carneiro (https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Substitution.20lemma)
@[simp] def shift_n : ℕ → term → term
| k (app M N) := app (shift_n k M) (shift_n k N)
| k (lam M) := lam (shift_n (k + 1) M)
| k (var x) := if x < k then var x else var (x + 1)

abbreviation shift := shift_n 0

@[simp] def subst_n : ℕ → term → term → term
| k L (app M N) := app (subst_n k L M) (subst_n k L N)
| k L (lam M) := lam (subst_n (k + 1) (shift L) M)
| k L (var x) := if x < k then var x else if x = k then L else var (x - 1)

abbreviation subst := subst_n 0

inductive beta : term → term → Prop
| app_left {M₁ M₂ N : term} : beta M₁ M₂ → beta (app M₁ N) (app M₂ N)
| app_right {M N₁ N₂ : term} : beta N₁ N₂ → beta (app M N₁) (app M N₂)
| lam {M L : term} : beta (app (lam M) L) (subst L M)

infix `—→`:40 := beta

infix `—→*`:40 := relation.refl_trans_gen beta

stlc1.lean

import logic.function.iterate
import tactic.basic

@[derive decidable_eq]
inductive term : Type
| app (M N : term) : term
| lam (M : term) : term
| var (x : ℕ) : term

open term

variables {x y z : ℕ} {M N L : term}

@[simp] def FV : term → set ℕ
| (app M N) := FV M ∪ FV N
| (lam M)   := FV M ∘ nat.succ
| (var x)   := {x}

instance (x : ℕ) : decidable (x ∈ FV M) :=
begin
  induction M with M N ih₁ ih₂ M ih y generalizing x,
  { cases ih₁ x with ih₁ ih₁; cases ih₂ x with ih₂ ih₂,
    { exact is_false (λ h, h.cases_on ih₁ ih₂) },
    all_goals { exact is_true (by exact or.inl ih₁ <|> exact or.inr ih₂) } },
  { exact decidable.cases_on (ih (x + 1)) is_false is_true },
  { exact dite (x = y) is_true is_false }
end

@[simp] def rename_ext (ρ : ℕ → ℕ) : ℕ → ℕ
| 0       := 0
| (x + 1) := ρ x + 1

@[simp] lemma rename_ext_id : rename_ext id = id :=
by { ext x, cases x; refl }

lemma rename_ext_succ (ρ : ℕ → ℕ) : rename_ext ρ ∘ nat.succ = nat.succ ∘ ρ :=
by { ext x, simp }

lemma rename_ext_comp (ρ₁ ρ₂ : ℕ → ℕ) :
  rename_ext ρ₁ ∘ rename_ext ρ₂ = rename_ext (ρ₁ ∘ ρ₂) :=
by { ext x, cases x; refl }

lemma iterate_rename_ext (ρ : ℕ → ℕ) :
  (rename_ext ρ)^[x] = rename_ext (ρ^[x]) :=
by { induction x; simp [*, rename_ext_comp] }

lemma iterate_rename_ext_eq {ρ : ℕ → ℕ} (h : x ≤ y) :
  rename_ext^[x] ρ y = ρ (y - x) + x :=
begin
  induction x with x ih generalizing y, refl,
  cases y, exact false.rec _ (nat.not_lt_zero _ h),
  simp [ih (nat.le_of_succ_le_succ h), function.iterate_succ'],
  refl
end

lemma rename_ext_inj : function.injective rename_ext :=
λ _ _ h, funext (λ x, nat.succ_inj (congr_fun h (x + 1)))

lemma rename_ext_inj_inj {ρ : ℕ → ℕ} (hρ : function.injective ρ) :
  function.injective (rename_ext ρ) :=
begin
  rintros ⟨⟩ ⟨⟩ h,
  { refl },
  { exact false.rec _ (nat.succ_ne_zero _ h.symm) },
  { exact false.rec _ (nat.succ_ne_zero _ h) },
  { rw hρ (nat.succ_inj h) }
end

lemma rename_ext_succ_inj (x : ℕ) :
  function.injective (rename_ext^[x] nat.succ) :=
begin
  intros n m h,
  induction x with x ih generalizing n m,
  { exact nat.succ_inj h },
  { rw function.iterate_succ' at h,
    exact rename_ext_inj_inj (ih : function.injective _) h }
end

@[simp] def rename : (ℕ → ℕ) → term → term
| ρ (app M N) := app (rename ρ M) (rename ρ N)
| ρ (lam M)   := lam (rename (rename_ext ρ) M)
| ρ (var x)   := var (ρ x)

lemma rename_id : rename id = id :=
by { ext M, induction M; simp * }

lemma rename_comp (ρ₁ ρ₂ : ℕ → ℕ) :
  rename ρ₁ ∘ rename ρ₂ = rename (ρ₁ ∘ ρ₂) :=
begin
  ext M,
  induction M with _ _ ih₁ ih₂ _ ih generalizing ρ₁ ρ₂,
  { simp only [rename, function.comp_app], exact ⟨ih₁ _ _, ih₂ _ _⟩ },
  { simp only [rename, ←rename_ext_comp ρ₁ ρ₂, function.comp_app], apply ih },
  { refl }
end

lemma iterate_rename (ρ : ℕ → ℕ) :
  (rename ρ)^[x] = rename (ρ^[x]) :=
by { induction x; simp [*, rename_id, rename_comp, rename_ext_comp] }

lemma rename_inj_inj {ρ : ℕ → ℕ} (hρ : function.injective ρ) :
  function.injective (rename ρ) :=
begin
  intros M N h,
  induction M with _ _ ih₁ ih₂ _ ih generalizing N ρ hρ;
    cases N; simp only [rename] at h; try { exfalso, exact h },
  { congr, exact ih₁ hρ h.1, exact ih₂ hρ h.2 },
  { congr, exact ih (rename_ext_inj_inj hρ) h },
  { congr, exact hρ h }
end

notation `rename_ext_succ^[` x `]` := rename (rename_ext^[x] nat.succ)

lemma rename_ext_iff (h : y ≤ x) :
  x + 1 = (rename_ext^[y] nat.succ z) ↔ x = z :=
begin
  split,
  { intro hM,
    induction z with z ih generalizing x y,
    { cases y,
      { apply nat.succ_inj hM },
      { rw function.iterate_succ' at hM,
        exact false.rec _ (nat.succ_ne_zero _ hM) } },
    { cases x,
      { rw nat.eq_zero_of_le_zero h at hM,
        exact false.rec _ (nat.succ_ne_zero _ (nat.succ_inj hM.symm)) },
      { cases y,
        { exact nat.succ_inj hM },
        { rw function.iterate_succ' at hM,
          congr, exact ih (nat.le_of_lt_succ h) (nat.succ_inj hM) } } } },
  { rintro rfl,
    induction y with y ih generalizing x, exact rfl,
    cases x,
    { exact false.rec _ (nat.not_lt_zero _ h) },
    { rw function.iterate_succ',
      congr, exact ih (nat.le_of_succ_le_succ h) } }
end

lemma FV_rename_ext_iff (h : y ≤ x) :
  x + 1 ∈ FV (rename_ext_succ^[y] (var z)) ↔ x = z :=
rename_ext_iff h

lemma FV_rename_ext_lt_of_FV_rename_ext_lt (hy : y < x) (hz : z < x) :
  x ∈ FV (rename_ext_succ^[y] M) → x ∈ FV (rename_ext_succ^[z] M) :=
begin
  intro h,
  induction M with _ _ ih₁ ih₂ _ ih w generalizing x y z,
  { exact h.cases_on (or.inl ∘ ih₁ hy hz) (or.inr ∘ ih₂ hy hz) },
  { simp only [rename] at ⊢ h,
    rw [←function.comp_app rename_ext, ←function.iterate_succ'] at ⊢ h,
    refine ih (nat.succ_lt_succ hy) (nat.succ_lt_succ hz) h },
  { induction x with x ih generalizing y z w,
    { exact false.rec _ (nat.not_lt_zero _ hy) },
    { cases y; cases z,
      { rw nat.succ_inj h, exact rfl },
      { rw [←nat.succ_inj h, FV_rename_ext_iff (nat.le_of_lt_succ hz)] },
      { congr,
        rwa FV_rename_ext_iff (nat.le_of_lt_succ hy) at h },
      { rw function.iterate_succ' at ⊢ h,
        cases w, exact false.rec _ (nat.succ_ne_zero _ h),
        congr,
        refine ih _ _ _ (nat.succ_inj h),
        exact nat.lt_of_succ_lt_succ hy,
        exact nat.lt_of_succ_lt_succ hz } } }
end

lemma not_FV_rename_ext_succ (x : ℕ) : x ∉ FV (rename_ext_succ^[x] M) :=
begin
  induction M with _ _ ih₁ ih₂ _ ih y generalizing x,
  { exact λ h, h.cases_on (ih₁ x) (ih₂ x) },
  { simp only [rename],
    rw [←function.comp_app rename_ext, ←function.iterate_succ'],
    exact ih (x + 1) },
  { induction x with x ih generalizing y,
    { exact nat.succ_ne_zero _ ∘ eq.symm },
    { rw function.iterate_succ',
      cases y,
      { exact nat.succ_ne_zero _ },
      { exact (ih _ ∘ nat.succ_inj) } } },
end

notation `shift` := rename nat.succ

lemma shift_eq_rename_ext_succ : shift = rename_ext_succ^[0] := rfl

lemma shift_inj : function.injective shift :=
λ _ _ h, rename_inj_inj @nat.succ_inj h

@[simp] def subst_ext (σ : ℕ → term) : ℕ → term
| 0       := var 0
| (x + 1) := shift (σ x)

lemma subst_ext_inj : function.injective subst_ext :=
λ _ _ h, funext (λ x, shift_inj (congr_fun h (x + 1)))

lemma subst_ext_inj_inj {σ : ℕ → term} (hσ : function.injective σ) :
  function.injective (subst_ext σ) :=
begin
  rintros ⟨⟩ ⟨⟩ h; try
  { exfalso,
    simp only [subst_ext] at h,
    cases σ ‹_›; simp only [rename] at h; try { exact h },
    apply nat.succ_ne_zero, exact h <|> exact h.symm },
  { refl },
  { congr, exact hσ (shift_inj h) }
end

@[simp] def subst : (ℕ → term) → term → term
| σ (app M N) := app (subst σ M) (subst σ N)
| σ (lam M)   := lam (subst (subst_ext σ) M)
| σ (var x)   := σ x

@[simp] def σ (x : ℕ) (L : term) (y : ℕ) : term :=
if x = y then L else var y

-- This changes the precedence of `[`. Let's hope this doesn't become an issue.
notation M `[`:std.prec.max_plus x ` := ` L `]` := subst (σ x L) M

lemma subst_ext_eq_shift (x : ℕ) : subst_ext (σ x M) = σ (x + 1) (shift M) :=
begin
  ext y,
  cases y,
  { simp [nat.succ_ne_zero x] },
  { by_cases x = y, simp [h], simp [h, h ∘ nat.succ_inj] }
end

lemma subst_eq_of_not_FV (h : x ∉ FV M) : M[x := L] = M :=
begin
  induction M with _ _ ih₁ ih₂ _ ih generalizing x L,
  { cases not_or_distrib.mp h with h₁ h₂, simp [ih₁ h₁, ih₂ h₂] },
  { simp [subst_ext_eq_shift, ih h] },
  { simp [show x ≠ _, from h] }
end

lemma FV_shift_of_FV (h : x ∈ FV M) : x + 1 ∈ FV (shift M) :=
begin
  induction M with _ _ ih₁ ih₂ _ ih generalizing x h,
  { exact h.cases_on (or.inl ∘ ih₁) (or.inr ∘ ih₂) },
  { simp only [rename],
    rw ←function.iterate_one rename_ext,
    rw shift_eq_rename_ext_succ at ih,
    refine FV_rename_ext_lt_of_FV_rename_ext_lt _ _ (ih h),
    exact nat.succ_pos _, exact nat.succ_lt_succ (nat.succ_pos _) },
  { show _ = _, simp [show x = _, from h] }
end

lemma FV_of_FV_shift (h : x + 1 ∈ FV (shift M)) : x ∈ FV M :=
begin
  induction M with _ _ ih₁ ih₂ _ ih generalizing x h,
  { exact h.cases_on (or.inl ∘ ih₁) (or.inr ∘ ih₂) },
  { simp only [rename] at h,
    rw ←function.iterate_one rename_ext at h,
    rw shift_eq_rename_ext_succ at ih,
    refine ih (FV_rename_ext_lt_of_FV_rename_ext_lt _ _ h),
    exact nat.succ_lt_succ (nat.succ_pos _), exact nat.succ_pos _, },
  { show _ = _, simp [nat.succ_inj h] }
end

lemma FV_shift_iff : x ∈ FV M ↔ x + 1 ∈ FV (shift M) :=
⟨FV_shift_of_FV, FV_of_FV_shift⟩

lemma not_FV_shift_iff : x ∉ FV M ↔ x + 1 ∉ FV (shift M) :=
by { split; contrapose!; exact FV_of_FV_shift <|> exact FV_shift_of_FV }

lemma not_FV_shift_of_not_FV (h : x ∉ FV M) : x + 1 ∉ FV (shift M) :=
not_FV_shift_iff.mp h

lemma not_FV_of_not_FV_shift (h : x + 1 ∉ FV (shift M)) : x ∉ FV M :=
not_FV_shift_iff.mpr h

lemma subst_ext_ext : subst_ext (σ x M) = σ (x + 1) (shift M) :=
begin
  ext y,
  induction y with y ih,
  { simp [nat.succ_ne_zero _] },
  { by_cases x = y, simp [h], simp [h, h ∘ nat.succ_inj] }
end

lemma iterate_subst_ext : subst_ext^[y] (σ x M) = σ (x + y) (shift^[y] M) :=
begin
  induction y with y ih generalizing x M,
  { simp [nat.add_zero] },
  { simp [ih, subst_ext_ext, nat.add_succ x y, ←nat.succ_add x y] },
end

lemma iterate_shift_app :
  shift^[x] (app M N) = app (shift^[x] M) (shift^[x] N) :=
by { induction x with x ih generalizing M N, simp, simp [ih] }

lemma iterate_rename_app (x : ℕ) (ρ : ℕ → ℕ) :
  (rename ρ)^[x] (app M N) = app ((rename ρ)^[x] M) ((rename ρ)^[x] N) :=
by { induction x generalizing M N; simp * }

lemma iterate_rename_succ : (rename nat.succ)^[x] = rename (+ x) :=
begin
  induction x with x ih,
  { have : rename (λ x, x) = id := rename_id,
    simp [nat.add_zero, this] },
  { simp only [ih, function.iterate_succ'], clear ih,
    ext M,
    cases M,
    { simp [rename, rename_comp] },
    { simp [rename, rename_comp, rename_ext_comp] },
    { simp [nat.succ_add] } }
end

lemma iterate_shift_lam :
  shift^[x] (lam M) = lam (rename (rename_ext (nat.add x)) M) :=
begin
  induction x with x ih generalizing M,
  { have : nat.add 0 = id := funext nat.zero_add,
    simp [rename_ext_id, rename_id, this] },
  { simp only [rename, function.comp_app, function.iterate_succ],
    rw [ih, ←function.comp_app (rename _), rename_comp, rename_ext_comp],
    congr' 3, ext y, change (x + y).succ = _ + _, simp [nat.succ_add] }
end

lemma iterate_shift_var :
  shift^[x] (var y) = var (y + x) :=
begin
  induction x with x ih generalizing y,
  { simp [nat.add_zero] },
  { simp [ih, nat.succ_add] }
end

lemma iterate_rename_ext_succ (h : x + y = z) :
  x + y + 1 = (rename_ext^[y]) nat.succ z :=
begin
  induction z with z ih generalizing y,
  { cases nat.eq_zero_of_add_eq_zero h with h₁ h₂,
    rw [h₁, h₂], refl },
  { cases y,
    { simp [h] },
    { specialize ih (nat.succ_inj h),
      simp [ih, function.iterate_succ', nat.succ_add] } }
end

lemma iterate_rename_ext_succ_iff :
  x + y = z ↔ x + y + 1 = (rename_ext^[y]) nat.succ z :=
begin
  split, exact iterate_rename_ext_succ,
  intros h,
  induction y with y ih generalizing z,
  { exact nat.succ_inj h },
  { simp [function.iterate_succ'] at h,
    cases z,
    { exact false.rec _ (nat.succ_ne_zero _ h) },
    { simp [←ih (nat.succ_inj h)] } }
end

lemma rename_ext_succ_var :
  rename_ext_succ^[y] (var x) = var (rename_ext^[y] nat.succ x) :=
by { cases y; refl }

lemma FV_of_subst_ne : M[x := L] ≠ M → x ∈ FV M :=
by { contrapose!, exact subst_eq_of_not_FV }

lemma iterate_rename_ext_eq_rename_ext (h : x ∉ FV M) :
  rename (rename_ext^[x + 1] nat.succ) M = rename (rename_ext^[x] nat.succ) M :=
begin
  induction M with _ _ ih₁ ih₂ M ih y generalizing x,
  { simp only [rename, function.comp_app, function.iterate_succ],
    exact ⟨ih₁ (h ∘ or.inl), ih₂ (h ∘ or.inr)⟩ },
  { specialize ih h, simp [*, function.iterate_succ'] at * },
  { induction x with x ih generalizing y,
    { cases y, exfalso, exact h rfl, refl },
    { cases y,
      { simp [function.iterate_succ'] },
      { specialize ih _ (h ∘ congr_arg nat.succ),
        simp [function.iterate_succ'] at ih,
        simp [ih, function.iterate_succ'] } } }
end

lemma subst_iterate_shift_eq_iterate_shift_subst :
  shift^[y] M[x := L] = (shift^[y] M)[x + y := (shift^[y]) L] :=
begin
  induction M with _ _ _ _ M ih z generalizing x y L,
  { simp [*, iterate_shift_app] },
  { simp only [subst_ext_ext, subst],
    sorry },
  { induction y with y ih generalizing x z L,
    { by_cases x = z; simp [*, nat.add_zero] },
    { simp only [ih, function.iterate_succ', function.comp_app],
      by_cases x = z,
      { simp [h, iterate_shift_var] },
      { simp [h, h ∘ nat.add_right_cancel, iterate_shift_var] } } }
end

lemma subst_shift_eq_shift_subst :
  shift M[x := L] = (shift M)[x + 1 := shift L] :=
begin
  have := subst_iterate_shift_eq_iterate_shift_subst,
  rwa function.iterate_one at this
end

example (h : x ≠ y) (hx : x ∉ FV L) :
  M[x := N][y := L] = M[y := L][x := N[y := L]] :=
begin
  induction M with _ _ ih₁ ih₂ M ih z generalizing x y N L,
  { simp [ih₁ h hx, ih₂ h hx] },
  { simp only [subst, subst_ext_eq_shift],
    have := ih (h ∘ nat.succ_inj) (not_FV_shift_iff.mp hx),
    rw [subst_shift_eq_shift_subst, this] },
  { by_cases x = z ∨ y = z, rcases h with rfl | rfl,
    { simp [h.symm] },
    { simp [subst_eq_of_not_FV hx, h] },
    { simp [not_or_distrib.mp h] } }
end

stlc2.lean

import logic.function.iterate
import tactic.basic

@[derive decidable_eq]
inductive term : Type
| app (M N : term) : term
| lam (M : term) : term
| var (x : ℕ) : term

open term

variables {x y z : ℕ} {M N L : term}

@[simp] def FV : term → set ℕ
| (app M N) := FV M ∪ FV N
| (lam M)   := FV M ∘ nat.succ
| (var x)   := {x}

instance (x : ℕ) : decidable (x ∈ FV M) :=
begin
  induction M with M N ih₁ ih₂ M ih y generalizing x,
  { cases ih₁ x with ih₁ ih₁; cases ih₂ x with ih₂ ih₂,
    { exact is_false (λ h, h.cases_on ih₁ ih₂) },
    all_goals { exact is_true (by exact or.inl ih₁ <|> exact or.inr ih₂) } },
  { exact decidable.cases_on (ih (x + 1)) is_false is_true },
  { exact dite (x = y) is_true is_false }
end

@[simp] def rename_ext (ρ : ℕ → ℕ) : ℕ → ℕ
| 0       := 0
| (x + 1) := ρ x + 1

@[simp] lemma rename_ext_id : rename_ext id = id :=
by { ext x, cases x; refl }

lemma rename_ext_comp (ρ₁ ρ₂ : ℕ → ℕ) :
  rename_ext ρ₁ ∘ rename_ext ρ₂ = rename_ext (ρ₁ ∘ ρ₂) :=
by { ext x, cases x; refl }

lemma iterate_rename_ext (ρ : ℕ → ℕ) :
  (rename_ext ρ)^[x] = rename_ext (ρ^[x]) :=
by { induction x; simp [*, rename_ext_comp] }

lemma rename_ext_inj : function.injective rename_ext :=
λ _ _ h, funext (λ x, nat.succ_inj (congr_fun h (x + 1)))

lemma rename_ext_inj_inj {ρ : ℕ → ℕ} (hρ : function.injective ρ) :
  function.injective (rename_ext ρ) :=
begin
  rintros ⟨⟩ ⟨⟩ h,
  { refl },
  { exact false.rec _ (nat.succ_ne_zero _ h.symm) },
  { exact false.rec _ (nat.succ_ne_zero _ h) },
  { rw hρ (nat.succ_inj h) }
end

lemma rename_ext_succ_inj (x : ℕ) :
  function.injective (rename_ext^[x] nat.succ) :=
begin
  intros n m h,
  induction x with x ih generalizing n m,
  { exact nat.succ_inj h },
  { rw function.iterate_succ' at h,
    exact rename_ext_inj_inj (ih : function.injective _) h }
end

@[simp] def rename : (ℕ → ℕ) → term → term
| ρ (app M N) := app (rename ρ M) (rename ρ N)
| ρ (lam M)   := lam (rename (rename_ext ρ) M)
| ρ (var x)   := var (ρ x)

@[simp] lemma rename_id : rename id = id :=
by { ext M, induction M; simp * }

lemma rename_comp (ρ₁ ρ₂ : ℕ → ℕ) :
  rename ρ₁ ∘ rename ρ₂ = rename (ρ₁ ∘ ρ₂) :=
begin
  ext M,
  induction M with _ _ ih₁ ih₂ _ ih generalizing ρ₁ ρ₂,
  { simp only [rename, function.comp_app], exact ⟨ih₁ _ _, ih₂ _ _⟩ },
  { simp only [rename, ←rename_ext_comp ρ₁ ρ₂, function.comp_app], apply ih },
  { refl }
end

lemma iterate_rename (ρ : ℕ → ℕ) :
  (rename ρ)^[x] = rename (ρ^[x]) :=
by { induction x; simp [*, rename_comp, rename_ext_comp] }

lemma rename_inj_inj {ρ : ℕ → ℕ} (hρ : function.injective ρ) :
  function.injective (rename ρ) :=
begin
  intros M N h,
  induction M with _ _ ih₁ ih₂ _ ih generalizing N ρ hρ;
    cases N; simp only [rename] at h; try { exfalso, exact h },
  { congr, exact ih₁ hρ h.1, exact ih₂ hρ h.2 },
  { congr, exact ih (rename_ext_inj_inj hρ) h },
  { congr, exact hρ h }
end

notation `rename_ext_succ^[` x `]` := rename (rename_ext^[x] nat.succ)

lemma rename_ext_iff (h : y ≤ x) :
  x + 1 = (rename_ext^[y] nat.succ z) ↔ x = z :=
begin
  split,
  { intro hM,
    induction z with z ih generalizing x y,
    { cases y,
      { apply nat.succ_inj hM },
      { rw function.iterate_succ' at hM,
        exact false.rec _ (nat.succ_ne_zero _ hM) } },
    { cases x,
      { rw nat.eq_zero_of_le_zero h at hM,
        exact false.rec _ (nat.succ_ne_zero _ (nat.succ_inj hM.symm)) },
      { cases y,
        { exact nat.succ_inj hM },
        { rw function.iterate_succ' at hM,
          congr, exact ih (nat.le_of_lt_succ h) (nat.succ_inj hM) } } } },
  { rintro rfl,
    induction y with y ih generalizing x, exact rfl,
    cases x,
    { exact false.rec _ (nat.not_lt_zero _ h) },
    { rw function.iterate_succ',
      congr, exact ih (nat.le_of_succ_le_succ h) } }
end

lemma FV_rename_ext_iff (h : y ≤ x) :
  x + 1 ∈ FV (rename_ext_succ^[y] (var z)) ↔ x = z :=
rename_ext_iff h

lemma FV_rename_ext_lt_of_FV_rename_ext_lt (hy : y < x) (hz : z < x) :
  x ∈ FV (rename_ext_succ^[y] M) → x ∈ FV (rename_ext_succ^[z] M) :=
begin
  intro h,
  induction M with _ _ ih₁ ih₂ _ ih w generalizing x y z,
  { exact h.cases_on (or.inl ∘ ih₁ hy hz) (or.inr ∘ ih₂ hy hz) },
  { simp only [rename] at ⊢ h,
    rw [←function.comp_app rename_ext, ←function.iterate_succ'] at ⊢ h,
    refine ih (nat.succ_lt_succ hy) (nat.succ_lt_succ hz) h },
  { induction x with x ih generalizing y z w,
    { exact false.rec _ (nat.not_lt_zero _ hy) },
    { cases y; cases z,
      { rw nat.succ_inj h, exact rfl },
      { rw [←nat.succ_inj h, FV_rename_ext_iff (nat.le_of_lt_succ hz)] },
      { congr,
        rwa FV_rename_ext_iff (nat.le_of_lt_succ hy) at h },
      { rw function.iterate_succ' at ⊢ h,
        cases w, exact false.rec _ (nat.succ_ne_zero _ h),
        congr,
        refine ih _ _ _ (nat.succ_inj h),
        exact nat.lt_of_succ_lt_succ hy,
        exact nat.lt_of_succ_lt_succ hz } } }
end

lemma not_FV_rename_ext_succ (x : ℕ) : x ∉ FV (rename_ext_succ^[x] M) :=
begin
  induction M with _ _ ih₁ ih₂ _ ih y generalizing x,
  { exact λ h, h.cases_on (ih₁ x) (ih₂ x) },
  { simp only [rename],
    rw [←function.comp_app rename_ext, ←function.iterate_succ'],
    exact ih (x + 1) },
  { induction x with x ih generalizing y,
    { exact nat.succ_ne_zero _ ∘ eq.symm },
    { rw function.iterate_succ',
      cases y,
      { exact nat.succ_ne_zero _ },
      { exact (ih _ ∘ nat.succ_inj) } } },
end

notation `shift` := rename nat.succ

lemma shift_eq_rename_ext_succ : shift = rename_ext_succ^[0] := rfl

lemma shift_inj : function.injective shift :=
λ _ _ h, rename_inj_inj @nat.succ_inj h

@[simp] def subst_ext (σ : ℕ → term) : ℕ → term
| 0       := var 0
| (x + 1) := shift (σ x)

lemma subst_ext_inj : function.injective subst_ext :=
λ _ _ h, funext (λ x, shift_inj (congr_fun h (x + 1)))

lemma subst_ext_inj_inj {σ : ℕ → term} (hσ : function.injective σ) :
  function.injective (subst_ext σ) :=
begin
  rintros ⟨⟩ ⟨⟩ h; try
  { exfalso,
    simp only [subst_ext] at h,
    cases σ ‹_›; simp only [rename] at h; try { exact h },
    apply nat.succ_ne_zero, exact h <|> exact h.symm },
  { refl },
  { congr, exact hσ (shift_inj h) }
end

@[simp] def subst : (ℕ → term) → term → term
| σ (app M N) := app (subst σ M) (subst σ N)
| σ (lam M)   := lam (subst (subst_ext σ) M)
| σ (var x)   := σ x

@[simp] def σ (x : ℕ) (L : term) (y : ℕ) : term :=
if x = y then L else var y

-- This changes the precedence of `[`. Let's hope this doesn't become an issue.
notation M `[`:std.prec.max_plus x ` := ` L `]` := subst (σ x L) M

lemma subst_ext_eq_shift (x : ℕ) : subst_ext (σ x M) = σ (x + 1) (shift M) :=
begin
  ext y,
  cases y,
  { simp [nat.succ_ne_zero x] },
  { by_cases x = y, simp [h], simp [h, h ∘ nat.succ_inj] }
end

lemma subst_eq_of_not_FV (h : x ∉ FV M) : M[x := L] = M :=
begin
  induction M with _ _ ih₁ ih₂ _ ih generalizing x L,
  { cases not_or_distrib.mp h with h₁ h₂, simp [ih₁ h₁, ih₂ h₂] },
  { simp [subst_ext_eq_shift, ih h] },
  { simp [show x ≠ _, from h] }
end

lemma FV_shift_of_FV (h : x ∈ FV M) : x + 1 ∈ FV (shift M) :=
begin
  induction M with _ _ ih₁ ih₂ _ ih generalizing x h,
  { exact h.cases_on (or.inl ∘ ih₁) (or.inr ∘ ih₂) },
  { simp only [rename],
    rw ←function.iterate_one rename_ext,
    rw shift_eq_rename_ext_succ at ih,
    refine FV_rename_ext_lt_of_FV_rename_ext_lt _ _ (ih h),
    exact nat.succ_pos _, exact nat.succ_lt_succ (nat.succ_pos _) },
  { show _ = _, simp [show x = _, from h] }
end

lemma FV_of_FV_shift (h : x + 1 ∈ FV (shift M)) : x ∈ FV M :=
begin
  induction M with _ _ ih₁ ih₂ _ ih generalizing x h,
  { exact h.cases_on (or.inl ∘ ih₁) (or.inr ∘ ih₂) },
  { simp only [rename] at h,
    rw ←function.iterate_one rename_ext at h,
    rw shift_eq_rename_ext_succ at ih,
    refine ih (FV_rename_ext_lt_of_FV_rename_ext_lt _ _ h),
    exact nat.succ_lt_succ (nat.succ_pos _), exact nat.succ_pos _, },
  { show _ = _, simp [nat.succ_inj h] }
end

lemma FV_shift_iff : x ∈ FV M ↔ x + 1 ∈ FV (shift M) :=
⟨FV_shift_of_FV, FV_of_FV_shift⟩

lemma not_FV_shift_iff : x ∉ FV M ↔ x + 1 ∉ FV (shift M) :=
by { split; contrapose!; exact FV_of_FV_shift <|> exact FV_shift_of_FV }

lemma not_FV_shift_of_not_FV (h : x ∉ FV M) : x + 1 ∉ FV (shift M) :=
not_FV_shift_iff.mp h

lemma not_FV_of_not_FV_shift (h : x + 1 ∉ FV (shift M)) : x ∉ FV M :=
not_FV_shift_iff.mpr h

lemma subst_ext_ext : subst_ext (σ x M) = σ (x + 1) (shift M) :=
begin
  ext y,
  induction y with y ih,
  { simp [nat.succ_ne_zero _] },
  { by_cases x = y, simp [h], simp [h, h ∘ nat.succ_inj] }
end

lemma iterate_subst_ext : subst_ext^[y] (σ x M) = σ (x + y) (shift^[y] M) :=
begin
  induction y with y ih generalizing x M,
  { simp [nat.add_zero] },
  { simp [ih, subst_ext_ext, nat.add_succ x y, ←nat.succ_add x y] },
end

@[simp] lemma iterate_shift_app :
  shift^[x] (app M N) = app (shift^[x] M) (shift^[x] N) :=
by { induction x with x ih generalizing M N, simp, simp [ih] }

lemma iterate_rename_app (x : ℕ) (ρ : ℕ → ℕ) :
  (rename ρ)^[x] (app M N) = app ((rename ρ)^[x] M) ((rename ρ)^[x] N) :=
by { induction x generalizing M N; simp * }

lemma iterate_rename_succ : (rename nat.succ)^[x] = rename (+ x) :=
begin
  induction x with x ih,
  { have : rename (λ x, x) = id := rename_id,
    simp [nat.add_zero, this] },
  { simp only [ih, function.iterate_succ'], clear ih,
    ext M,
    cases M,
    { simp [rename, rename_comp] },
    { simp [rename, rename_comp, rename_ext_comp] },
    { simp [nat.succ_add] } }
end

example : (rename (rename_ext nat.succ))^[x] = rename (rename_ext^[x] (+ x)) :=
begin
  induction x with x ih,
  { have : rename (λ x, x) = id := rename_id,
    simp [nat.add_zero, this] },
  { ext M,
    induction M with _ _ ih₁ ih₂ M ihM y,
    { rw [function.iterate_succ', function.comp_app, ih],
      simp only [rename],
      split; try { rw ←ih₁ <|> rw ←ih₂ };
      rw [←ih, ←function.comp_app (rename _), ←function.iterate_succ'] },
    { simp only [ih, function.iterate_succ', rename, rename_comp],

      sorry },
    { induction y; simp [*, nat.succ_add] } }
end

@[simp] lemma iterate_shift_lam :
  shift^[x] (lam M) = lam (rename (rename_ext (+ x)) M) :=
begin
  induction x with x ih generalizing M,
  { have : rename_ext (λ x, x) = id := rename_ext_id,
    simp [nat.add_zero, this] },
  { simp only [rename, function.comp_app, function.iterate_succ],
    rw [ih, ←function.comp_app (rename _), rename_comp, rename_ext_comp],
    congr, ext, simp [nat.succ_add] }
end

@[simp] lemma iterate_shift_var :
  shift^[x] (var y) = var (y + x) :=
begin
  induction x with x ih generalizing y,
  { simp [nat.add_zero] },
  { simp [ih, nat.succ_add] }
end

example :
  rename_ext_succ^[y] M[x + y := rename (+ y) L] = (rename_ext_succ^[y] M)[x + 1 + y := rename (λ x, x + 1 + y) L] :=
begin
  induction M with _ _ ih₁ ih₂ M ih z generalizing x y L,
  { sorry },
  { sorry },
  { induction y with y ih generalizing x z L,
    { by_cases x = z,
      { simp [h, nat.add_zero],
        rw [←function.comp_app (rename _), rename_comp] },
      { simp [h, h ∘ nat.succ_inj, nat.add_zero] } },
    { sorry } }
end

example : shift M[x := L] = (shift M)[x + 1 := shift L] :=
begin
  induction M with _ _ ih₁ ih₂ M ih y generalizing x L,
  { simp only [rename, subst], exact ⟨ih₁, ih₂⟩ },
  { simp [subst_ext_ext],
    rw [←function.comp_app (rename _) (rename _), rename_comp],
    rw ←function.iterate_one rename_ext,

    sorry },
  { by_cases x = y, simp [h], simp [h, h ∘ nat.succ_inj] }
end

lemma iterate_subst_shift_eq_shift_subst :
  shift^[y] M[x := L] = (shift^[y] M)[x + y := (shift^[y]) L] :=
begin
  induction M with _ _ ih₁ ih₂ M ih₁ z generalizing x y L,
  { simp only [subst, iterate_shift_app] at *, exact ⟨ih₁, ih₂⟩ },
  { induction y with y ih₂ generalizing x L,
    { repeat { rw function.iterate_zero_apply }, refl },
    { rw [function.iterate_succ', function.comp_app, ih₂],
      rw ←function.iterate_succ',
      simp [subst_ext_ext],
      rw ←function.comp_app (rename _),
      sorry } },
  { by_cases x = z, simp [h], simp [h, h ∘ nat.add_right_cancel] }

  --induction M with _ _ ih₁ ih₂ M ih y,
  --{ simp only [rename, subst] at *, exact ⟨ih₁, ih₂⟩ },
  --{ repeat { rw tmp at * },
  --  simp at *,
  --  repeat { rw ←tmp },
  --  sorry },
  --{ by_cases x = y, simp [h], simp [h, h ∘ nat.succ_inj] }

  --induction M[x := L] with _ _ ih _ _ ih y generalizing x M L;
  --try
  --{ exfalso,
  --  have h₁ := @ih 0 (var 0) (var 0),
  --  have h₂ := @ih 0 (var 0) (var 1),
  --  rw h₁ at h₂,
  --  simp at *,
  --  exact nat.zero_ne_one h₂ },
  --induction M with K₁ K₂ ih₁ ih₂ M ih y generalizing x L,
  --{ exfalso,
  --  have h₁ := @ih₁ 0 (var 0),
  --  have h₂ := @ih₂ 0 (var 0),
  --  rw h₁ at h₂,
  --  simp at *,
  --  sorry },

  --induction M with _ _ ih₁ ih₂ M ih y,
  --{ simp only [rename, subst] at *, exact ⟨ih₁, ih₂⟩ },
  --{ 
  --  -- Attempt.
  --  --simp only [rename, function.iterate_zero, id.def],
  --  --rw [←function.iterate_one rename_ext, ←shift_def],
  --  --
  --  -- Attempt.
  --  --by_cases x ∈ FV (lam M),
  --  --{ simp at h,
  --  --  sorry },
  --  --{ have := not_FV_shift_of_not_FV h,
  --  --  rw [subst_eq_of_not_FV h, subst_eq_of_not_FV this] }
  --  },
  --{ by_cases x = y, simp [h], simp [h, h ∘ nat.succ_inj] }
end

lemma subst_shift_eq_shift_subst :
  shift M[x := L] = (shift M)[x + 1 := shift L] :=
function.iterate_one shift ▸ iterate_subst_shift_eq_shift_subst

example (h : x ≠ y) (hx : x ∉ FV L) :
  M[x := N][y := L] = M[y := L][x := N[y := L]] :=
begin
  induction M with _ _ ih₁ ih₂ M ih z generalizing x y N L,
  { simp [ih₁ h hx, ih₂ h hx] },
  { simp only [subst, subst_ext_eq_shift],
    have := ih (h ∘ nat.succ_inj) (not_FV_shift_iff.mp hx),
    rw [subst_shift_eq_shift_subst, this] },
  { by_cases x = z ∨ y = z, rcases h with rfl | rfl,
    { simp [h.symm] },
    { simp [subst_eq_of_not_FV hx, h] },
    { simp [not_or_distrib.mp h] } }
end

stlc3.lean

import data.finset
import tactic.basic

@[derive decidable_eq]
inductive term : Type
| app (M N : term) : term
| lam (M : term) : term
| var (x : ℕ) : term

open term

@[simp] def FV : term → finset ℕ
| (app M N) := FV M ∪ FV N
| (lam M)   := finset.image nat.pred (FV M \ {0})
| (var x)   := {x}

instance (x : ℕ) (M : term) : decidable (x ∈ FV M) :=
begin
  induction M with M N ih₁ ih₂ M ih y generalizing x,
  { simp only [FV, finset.mem_union],
    cases ih₁ x with ih₁ ih₁; cases ih₂ x with ih₂ ih₂,
    { exact is_false (λ h, h.cases_on ih₁ ih₂) },
    all_goals { exact is_true (by exact or.inl ih₁ <|> exact or.inr ih₂) } },
  { suffices : decidable (∃ y, y ∈ FV M ∧ y ≠ 0 ∧ y - 1 = x),
    { simpa [and_assoc] },
    cases ih (x + 1) with ih ih,
    { apply is_false,
      rintro ⟨_ | y, h⟩,
      { exact h.2.1 rfl },
      { exact ih (nat.pred_succ y ▸ h.2.2 ▸ h.1) } },
    { exact is_true ⟨x + 1, ih, nat.succ_ne_zero x, nat.pred_succ x⟩ } },
  { by_cases x = y, simp [h], exact is_true trivial, simp, exact is_false h }
end

@[simp] def rename_ext (ρ : ℕ → ℕ) : ℕ → ℕ
| 0       := 0
| (x + 1) := ρ x + 1

@[simp] def rename : (ℕ → ℕ) → term → term
| ρ (app M N) := app (rename ρ M) (rename ρ N)
| ρ (lam M)   := lam (rename (rename_ext ρ) M)
| ρ (var x)   := var (ρ x)

notation `shift` := rename nat.succ

@[simp] def subst_ext (σ : ℕ → term) : ℕ → term
| 0       := var 0
| (x + 1) := shift (σ x)

@[simp] def subst : (ℕ → term) → term → term
| σ (app M N) := app (subst σ M) (subst σ N)
| σ (lam M)   := lam (subst (subst_ext σ) M)
| σ (var x)   := σ x

@[simp] def σ (x : ℕ) (L : term) (y : ℕ) : term :=
if x = y then L else var y

-- This changes the precedence of `[`. Let's hope this doesn't become an issue.
notation M `[`:std.prec.max_plus x ` := ` L `]` := subst (σ x L) M

variables {x y z : ℕ} {M N L : term}

-- Type copied.
lemma shift_non_free : x ∉ FV M → x + 1 ∉ FV (shift M) :=
begin
  contrapose!,
  intro h,
  induction M with _ _ ih₁ ih₂ M ih generalizing x h,
  { simp only [FV, rename, finset.mem_union] at *,
    exact h.cases_on (or.inl ∘ ih₁) (or.inr ∘ ih₂) },
  { simp [and_assoc] at *,
    rcases h with ⟨y, h₁, h₂, h₃⟩,
    sorry },
  { simp only [FV, rename, finset.mem_singleton] at *,
    exact nat.succ_inj h }
  --intro h,
  --induction M with M N ih₁ ih₂ M ih y generalizing x,
  --{ simp only [FV, rename, finset.mem_union] at *,
  --  cases not_or_distrib.mp h with h₁ h₂,
  --  exact not_or_distrib.mpr ⟨ih₁ h₁, ih₂ h₂⟩ },
  --{ intro a,
  --  sorry },
  --{ simp only [FV, rename, finset.mem_singleton] at *,
  --  exact h ∘ nat.succ_inj }
end

-- Type copied.
lemma subst_shift_eq_shift_subst_shift :
  shift M[x := L] = (shift M)[x + 1 := shift L] :=
begin
  induction M with _ _ ih₁ ih₂ M ih y,
  { simp [ih₁, ih₂] },
  { sorry },
  { by_cases x = y, simp [h], simp [h, h ∘ nat.succ_inj] }
end

stlc4.lean

import tactic.basic

@[derive decidable_eq]
inductive preterm : Type
| abs (x : ℕ) (M : preterm) : preterm
| app (M N : preterm) : preterm
| var (x : ℕ) : preterm

-- Note that `λx.fy` is `λx.(fy)` and not `(λx.f)y`.

open preterm

-- Free variables.
@[simp]
def FV : preterm → set ℕ
| (abs x M) := FV M \ {x}
| (app M N) := FV M ∪ FV N
| (var x)   := {x}

instance (x : ℕ) (M : preterm) : decidable (x ∈ FV M) :=
begin
  induction M with y M ih M N ih₁ ih₂ y,
  { by_cases x = y,
    { exact is_false (h.symm ▸ λ h, h.2 rfl) },
    { cases ih,
      { exact is_false (mt and.left ih) },
      { exact is_true ⟨ih, h⟩ } } },
  { cases ih₁; cases ih₂,
    { refine is_false (λ h, or.cases_on h (λ h, ih₁ h) (λ h, ih₂ h)) },
    all_goals { exact is_true (by exact or.inl ih₁ <|> exact or.inr ih₂) } },
  { by_cases x = y, exact is_true h, exact is_false h },
end

-- Bound variables.
@[simp]
def BV : preterm → set ℕ
| (abs x M) := FV M ∪ {x}
| (app M N) := FV M ∪ FV N
| (var x)   := ∅

-- Names of bound variables should always differ from free ones.
@[simp]
def behaved (s : set ℕ) : preterm → Prop
| (abs x M) := behaved M ∧ x ∉ s
| (app M N) := behaved M ∧ behaved N
| (var x)   := true

lemma behaved.subset {M : preterm} {s t : set ℕ} (h : s ⊆ t) :
  behaved t M → behaved s M :=
begin
  change ∀ _, _ at h,
  induction M with _ _ ih; try { unfold behaved, cc },
  exact λ ⟨h₁, h₂⟩, ⟨ih h₁, λ hs, h₂ (h _ hs)⟩
end

def term : Type := {M : preterm // behaved (FV M) M}

@[simp]
def closed (M : term) : Prop := FV M.val = ∅

-- Substitute `x` for `N`.
@[reducible]
def subst.main (x : ℕ) (N : preterm) : preterm → preterm
| (abs y M) := abs y $ if x = y then M else subst.main M
| (app P Q) := app (subst.main P) (subst.main Q)
| (var y)   := if x = y then N else var y

lemma subst.eq {x : ℕ} {M N : preterm} (h : x ∉ FV M) :
  subst.main x N M = M :=
begin
  induction M with y _ ih _ _ ih₁ ih₂; unfold subst.main,
  { by_cases this : x = y,
    { rwa if_pos },
    { rwa [if_neg, ih (λ x, h ⟨x, this⟩)] } },
  { rw [ih₁ (h ∘ or.inl), ih₂ (h ∘ or.inr)] },
  { rwa if_neg },
end

variables {x y z : ℕ} {M N L : term}

meta def so_sorry : tactic unit := tactic.all_goals' tactic.admit

example {s t : set ℕ} : s ⊆ s ∪ t := λ _, or.inl

lemma subst.sound {L : preterm} (h : closed N) :
  L = subst.main x N.val M.val → behaved (FV L) L :=
begin
  rintro rfl,
  sorry,
  --induction M.val with y M ih _ _ ih₁ ih₂ y,
  --{ simp only [FV, behaved],
  --  by_cases this : x = y; split,
  --  { sorry },
  --  { rw if_pos this, exact λ h, h.2 rfl },
  --  { rw if_neg this, refine behaved.subset (λ _, and.left) ih },
  --  { rw if_neg this, exact λ h, h.2 rfl }
  --  --by_cases x = y; split,
  --  --{ rw if_pos h, refine behaved.subset (λ _, and.left) _,
  --  --  by_cases x ∈ FV M,
  --  --  { sorry },
  --  --  { rwa subst.eq h at ih } },
  --  },
  --{ simp only [FV, behaved],
  --  split,
  --  { refine behaved.subset (λ _, or.inr) _,
  --  
  --    so_sorry },
  --  sorry },
  --by_cases x = y; unfold subst.main,
  --{ rw if_pos h, exact N.property },
  --{ rw if_neg h, simp }  
end

def subst (x : ℕ) {N : term} (hN : closed N) (M : term) : term :=
⟨subst.main x N.val M.val, subst.sound hN rfl⟩

notation M `[` x ` := ` N `]` := subst x N M

/-
example (M N : term) (h₁ : x ≠ y) (h₂ : x ∉ FV L) :
  M[x := N][y := L] = M[y := L][x := N[y := L]] :=
begin
  induction M with z M ih _ _ _ _ z; unfold subst,
  { by_cases x = z ∨ y = z, rcases h with rfl | rfl, cc,
    rw [if_pos, if_neg, if_neg, if_pos], 
    all_goals { try { cc } },
    congr, suffices : y ∉ FV N, rw subst.eq this,
    intro h,
    apply h₁,

    sorry },
  { congr' },
  { by_cases x = z ∨ y = z, rcases h with rfl | rfl,
    { rw [if_pos, if_neg], unfold subst,
      all_goals { cc } },
    { rw [if_neg, if_pos], unfold subst,
      rw [if_pos, subst.eq h₂],
      all_goals { cc } },
    { rw [if_neg, if_neg], unfold subst,
      all_goals { cc } } }
end
-/

stlc5.lean

import data.fin
import algebra.order

@[derive decidable_eq]
inductive term : ℕ → Type
| app {Γ : ℕ} (M N : term Γ) : term Γ
| lam {Γ : ℕ} (M : term (Γ + 1)) : term Γ
| var {Γ : ℕ} (x : fin Γ) : term Γ

open term

variables {Γ Δ : ℕ}

def rename_ext (ρ : fin Γ → fin Δ) (x : fin (Γ + 1)) : fin (Δ + 1) :=
if h : x = 0 then 0 else fin.succ $ ρ (x.pred h)

def rename : ∀ {Γ Δ}, (fin Γ → fin Δ) → term Γ → term Δ
| Γ Δ ρ (app M N) := app (rename ρ M) (rename ρ N)
| Γ Δ ρ (lam M)   := lam (rename (rename_ext ρ) M)
| Γ Δ ρ (var x)   := var (ρ x)

def subst_ext (σ : fin Γ → term Δ) : fin (Γ + 1) → term (Δ + 1)
| ⟨0, _⟩     := var 0
| ⟨x + 1, h⟩ := rename fin.succ (σ ⟨x, nat.lt_of_succ_lt_succ h⟩)

def subst : ∀ {Γ Δ : ℕ}, (fin Γ → term Δ) → term Γ → term Δ
| Γ Δ σ (app M N) := app (subst σ M) (subst σ N)
| Γ Δ σ (lam M)   := lam (subst (subst_ext σ) M)
| Γ Δ σ (var x)   := σ x

def subst' (x : fin (Γ + 1)) (N : term Γ) (M : term (Γ + 1)) : term Γ :=
let σ (y : fin (Γ + 1)) : term Γ :=
  @ordering.cases_on (λ o, cmp x y = o → term Γ) (cmp x y)
    -- `ordering.lt`
    (λ h, let h := (ordering.compares.eq_lt (cmp_compares x y)).mp h
      in var (y.pred (fin.ne_of_vne (ne_bot_of_gt h))))
    -- `ordering.eq`
    (λ h, N)
    -- `ordering.gt`
    (λ h, let h := (ordering.compares.eq_gt (cmp_compares x y)).mp h
      in var ⟨y, lt_of_lt_of_le h (nat.lt_succ_iff.mp x.is_lt)⟩) rfl
in subst σ M

notation M `[` x ` := ` N `]` := subst' x N M

stlc6.lean

import logic.function.iterate
import tactic.basic

@[derive decidable_eq]
inductive term : Type
| app (M N : term) : term
| lam (M : term) : term
| var (x : ℕ) : term

open term

variables {x y z : ℕ} {M N L : term}

@[simp] def FV : term → set ℕ
| (app M N) := FV M ∪ FV N
| (lam M)   := FV M ∘ nat.succ
| (var x)   := {x}

instance (x : ℕ) : decidable (x ∈ FV M) :=
begin
  induction M with M N ih₁ ih₂ M ih y generalizing x,
  { cases ih₁ x with ih₁ ih₁; cases ih₂ x with ih₂ ih₂,
    { exact is_false (λ h, h.cases_on ih₁ ih₂) },
    all_goals { exact is_true (by exact or.inl ih₁ <|> exact or.inr ih₂) } },
  { exact decidable.cases_on (ih (x + 1)) is_false is_true },
  { exact dite (x = y) is_true is_false }
end

@[simp] def rename_ext (ρ : ℕ → ℕ) : ℕ → ℕ
| 0       := 0
| (x + 1) := ρ x + 1

lemma rename_ext_inj : function.injective rename_ext :=
λ _ _ h, funext (λ x, nat.succ_inj (congr_fun h (x + 1)))

lemma rename_ext_inj_inj {ρ : ℕ → ℕ} (hρ : function.injective ρ) :
  function.injective (rename_ext ρ) :=
begin
  rintros ⟨⟩ ⟨⟩ h,
  { refl },
  { exact false.rec _ (nat.succ_ne_zero _ h.symm) },
  { exact false.rec _ (nat.succ_ne_zero _ h) },
  { rw hρ (nat.succ_inj h) }
end

lemma rename_ext_succ_inj (x : ℕ) :
  function.injective (rename_ext^[x] nat.succ) :=
begin
  intros n m h,
  induction x with x ih generalizing n m,
  { exact nat.succ_inj h },
  { rw function.iterate_succ' at h,
    exact rename_ext_inj_inj (ih : function.injective _) h }
end

@[simp] def rename : (ℕ → ℕ) → term → term
| ρ (app M N) := app (rename ρ M) (rename ρ N)
| ρ (lam M)   := lam (rename (rename_ext ρ) M)
| ρ (var x)   := var (ρ x)

lemma rename_inj_inj {ρ : ℕ → ℕ} (hρ : function.injective ρ) :
  function.injective (rename ρ) :=
begin
  intros M N h,
  induction M with _ _ ih₁ ih₂ _ ih generalizing N ρ hρ;
    cases N; simp only [rename] at h; try { exfalso, exact h },
  { congr, exact ih₁ hρ h.1, exact ih₂ hρ h.2 },
  { congr, exact ih (rename_ext_inj_inj hρ) h },
  { congr, exact hρ h }
end

notation `rename_ext_succ^[` x `]` := rename (rename_ext^[x] nat.succ)

lemma rename_ext_iff (h : y ≤ x) :
  x + 1 = (rename_ext^[y] nat.succ z) ↔ x = z :=
begin
  split,
  { intro hM,
    induction z with z ih generalizing x y,
    { cases y,
      { apply nat.succ_inj hM },
      { rw function.iterate_succ' at hM,
        exact false.rec _ (nat.succ_ne_zero _ hM) } },
    { cases x,
      { rw nat.eq_zero_of_le_zero h at hM,
        exact false.rec _ (nat.succ_ne_zero _ (nat.succ_inj hM.symm)) },
      { cases y,
        { exact nat.succ_inj hM },
        { rw function.iterate_succ' at hM,
          congr, exact ih (nat.le_of_lt_succ h) (nat.succ_inj hM) } } } },
  { rintro rfl,
    induction y with y ih generalizing x, exact rfl,
    cases x,
    { exact false.rec _ (nat.not_lt_zero _ h) },
    { rw function.iterate_succ',
      congr, exact ih (nat.le_of_succ_le_succ h) } }
end

lemma FV_rename_ext_iff (h : y ≤ x) :
  x + 1 ∈ FV (rename_ext_succ^[y] (var z)) ↔ x = z :=
rename_ext_iff h

lemma FV_rename_ext_lt_of_FV_rename_ext_lt (hy : y < x) (hz : z < x) :
  x ∈ FV (rename_ext_succ^[y] M) → x ∈ FV (rename_ext_succ^[z] M) :=
begin
  intro h,
  induction M with _ _ ih₁ ih₂ _ ih w generalizing x y z,
  { exact h.cases_on (or.inl ∘ ih₁ hy hz) (or.inr ∘ ih₂ hy hz) },
  { simp only [rename] at ⊢ h,
    rw [←function.comp_app rename_ext, ←function.iterate_succ'] at ⊢ h,
    refine ih (nat.succ_lt_succ hy) (nat.succ_lt_succ hz) h },
  { induction x with x ih generalizing y z w,
    { exact false.rec _ (nat.not_lt_zero _ hy) },
    { cases y; cases z,
      { rw nat.succ_inj h, exact rfl },
      { rw [←nat.succ_inj h, FV_rename_ext_iff (nat.le_of_lt_succ hz)] },
      { congr,
        rwa FV_rename_ext_iff (nat.le_of_lt_succ hy) at h },
      { rw function.iterate_succ' at ⊢ h,
        cases w, exact false.rec _ (nat.succ_ne_zero _ h),
        congr,
        refine ih _ _ _ (nat.succ_inj h),
        exact nat.lt_of_succ_lt_succ hy,
        exact nat.lt_of_succ_lt_succ hz } } }
end

lemma not_FV_rename_ext_succ (x : ℕ) : x ∉ FV (rename_ext_succ^[x] M) :=
begin
  induction M with _ _ ih₁ ih₂ _ ih y generalizing x,
  { exact λ h, h.cases_on (ih₁ x) (ih₂ x) },
  { simp only [rename],
    rw [←function.comp_app rename_ext, ←function.iterate_succ'],
    exact ih (x + 1) },
  { induction x with x ih generalizing y,
    { exact nat.succ_ne_zero _ ∘ eq.symm },
    { rw function.iterate_succ',
      cases y,
      { exact nat.succ_ne_zero _ },
      { exact (ih _ ∘ nat.succ_inj) } } },
end

notation `shift` := rename nat.succ

lemma shift_eq_rename_ext_succ : shift = rename_ext_succ^[0] := rfl

lemma shift_inj : function.injective shift :=
λ _ _ h, rename_inj_inj @nat.succ_inj h

@[simp] def subst_ext (σ : ℕ → term) : ℕ → term
| 0       := var 0
| (x + 1) := shift (σ x)

lemma subst_ext_inj_inj {σ : ℕ → term} (hσ : function.injective σ) :
  function.injective (subst_ext σ) :=
begin
  rintros ⟨⟩ ⟨⟩ h; try
  { exfalso,
    simp only [subst_ext] at h,
    cases σ ‹_›; simp only [rename] at h; try { exact h },
    apply nat.succ_ne_zero, exact h <|> exact h.symm },
  { refl },
  { congr, exact hσ (rename_inj_inj @nat.succ_inj h) }
end

@[simp] def subst : (ℕ → term) → term → term
| σ (app M N) := app (subst σ M) (subst σ N)
| σ (lam M)   := lam (subst (subst_ext σ) M)
| σ (var x)   := σ x

@[simp] def σ (x : ℕ) (L : term) (y : ℕ) : term :=
if x = y then L else var y

-- This changes the precedence of `[`. Let's hope this doesn't become an issue.
notation M `[`:std.prec.max_plus x ` := ` L `]` := subst (σ x L) M

lemma subst_ext_eq_shift (x : ℕ) : subst_ext (σ x M) = σ (x + 1) (shift M) :=
begin
  ext y,
  cases y,
  { simp [nat.succ_ne_zero x] },
  { by_cases x = y, simp [h], simp [h, h ∘ nat.succ_inj] }
end

lemma subst_eq_of_not_FV (h : x ∉ FV M) : M[x := L] = M :=
begin
  induction M with _ _ ih₁ ih₂ _ ih generalizing x L,
  { cases not_or_distrib.mp h with h₁ h₂, simp [ih₁ h₁, ih₂ h₂] },
  { simp [subst_ext_eq_shift, ih h] },
  { simp [show x ≠ _, from h] }
end

lemma FV_shift_of_FV (h : x ∈ FV M) : x + 1 ∈ FV (shift M) :=
begin
  induction M with _ _ ih₁ ih₂ _ ih generalizing x h,
  { exact h.cases_on (or.inl ∘ ih₁) (or.inr ∘ ih₂) },
  { simp only [rename],
    rw ←function.iterate_one rename_ext,
    rw shift_eq_rename_ext_succ at ih,
    refine FV_rename_ext_lt_of_FV_rename_ext_lt _ _ (ih h),
    exact nat.succ_pos _, exact nat.succ_lt_succ (nat.succ_pos _) },
  { show _ = _, simp [show x = _, from h] }
end

lemma FV_of_FV_shift (h : x + 1 ∈ FV (shift M)) : x ∈ FV M :=
begin
  induction M with _ _ ih₁ ih₂ _ ih generalizing x h,
  { exact h.cases_on (or.inl ∘ ih₁) (or.inr ∘ ih₂) },
  { simp only [rename] at h,
    rw ←function.iterate_one rename_ext at h,
    rw shift_eq_rename_ext_succ at ih,
    refine ih (FV_rename_ext_lt_of_FV_rename_ext_lt _ _ h),
    exact nat.succ_lt_succ (nat.succ_pos _), exact nat.succ_pos _, },
  { show _ = _, simp [nat.succ_inj h] }
end

lemma FV_shift_iff : x ∈ FV M ↔ x + 1 ∈ FV (shift M) :=
⟨FV_shift_of_FV, FV_of_FV_shift⟩

lemma not_FV_shift_iff : x ∉ FV M ↔ x + 1 ∉ FV (shift M) :=
by { split; contrapose!; exact FV_of_FV_shift <|> exact FV_shift_of_FV }

lemma not_FV_shift_of_not_FV (h : x ∉ FV M) : x + 1 ∉ FV (shift M) :=
not_FV_shift_iff.mp h

lemma not_FV_of_not_FV_shift (h : x + 1 ∉ FV (shift M)) : x ∉ FV M :=
not_FV_shift_iff.mpr h

example (h : M[x := L] = N) :
  (lam (shift M))[x := shift L] = lam (shift N) :=
begin
  sorry
end

lemma tmp : σ (x + 1) (shift M) = subst_ext (σ x M) :=
begin
  ext y,
  induction y with y ih,
  { simp [nat.succ_ne_zero _] },
  { by_cases x = y, simp [h], simp [h, h ∘ nat.succ_inj] }
end

example : σ (x + y) (shift^[y] M) = (subst_ext^[y]) (σ x M) :=
begin
  induction y with y ih generalizing x M,
  { simp [nat.add_zero] },
  { simp [nat.add_succ x y, ←nat.succ_add x y, ih, tmp] },
end

lemma subst_shift_eq_shift_subst :
  shift M[x := L] = (shift M)[x + 1 := shift L] :=
begin
  induction M with _ _ ih₁ ih₂ M ih y,
  { simp only [rename, subst] at *, exact ⟨ih₁, ih₂⟩ },
  { repeat { rw tmp at * },
    simp at *,
    repeat { rw ←tmp },
    sorry },
  { by_cases x = y, simp [h], simp [h, h ∘ nat.succ_inj] }

  --induction M[x := L] with _ _ ih _ _ ih y generalizing x M L;
  --try
  --{ exfalso,
  --  have h₁ := @ih 0 (var 0) (var 0),
  --  have h₂ := @ih 0 (var 0) (var 1),
  --  rw h₁ at h₂,
  --  simp at *,
  --  exact nat.zero_ne_one h₂ },
  --induction M with K₁ K₂ ih₁ ih₂ M ih y generalizing x L,
  --{ exfalso,
  --  have h₁ := @ih₁ 0 (var 0),
  --  have h₂ := @ih₂ 0 (var 0),
  --  rw h₁ at h₂,
  --  simp at *,
  --  sorry },

  --induction M with _ _ ih₁ ih₂ M ih y,
  --{ simp only [rename, subst] at *, exact ⟨ih₁, ih₂⟩ },
  --{ 
  --  -- Attempt.
  --  --simp only [rename, function.iterate_zero, id.def],
  --  --rw [←function.iterate_one rename_ext, ←shift_def],
  --  --
  --  -- Attempt.
  --  --by_cases x ∈ FV (lam M),
  --  --{ simp at h,
  --  --  sorry },
  --  --{ have := not_FV_shift_of_not_FV h,
  --  --  rw [subst_eq_of_not_FV h, subst_eq_of_not_FV this] }
  --  },
  --{ by_cases x = y, simp [h], simp [h, h ∘ nat.succ_inj] }
end

example (h : x ≠ y) (hx : x ∉ FV L) :
  M[x := N][y := L] = M[y := L][x := N[y := L]] :=
begin
  induction M with _ _ ih₁ ih₂ M ih z generalizing x y N L,
  { simp [ih₁ h hx, ih₂ h hx] },
  { simp only [subst, subst_ext_eq_shift],
    have := ih (h ∘ nat.succ_inj) (not_FV_shift_iff.mp hx),
    rw [subst_shift_eq_shift_subst, this] },
  { by_cases x = z ∨ y = z, rcases h with rfl | rfl,
    { simp [h.symm] },
    { simp [subst_eq_of_not_FV hx, h] },
    { simp [not_or_distrib.mp h] } }
end

stlc7.lean

import logic.function.iterate
import tactic.basic

@[derive decidable_eq]
inductive term : Type
| app (M N : term) : term
| lam (M : term) : term
| var (x : ℕ) : term

open term

variables {x y z : ℕ} {M : term}

@[simp] def FV : term → set ℕ
| (app M N) := FV M ∪ FV N
| (lam M)   := FV M ∘ nat.succ
| (var x)   := {x}

@[simp] def rename_ext (ρ : ℕ → ℕ) : ℕ → ℕ
| 0       := 0
| (x + 1) := ρ x + 1

lemma rename_ext_inj : function.injective rename_ext :=
λ _ _ h, funext (λ x, nat.succ_inj (congr_fun h (x + 1)))

lemma rename_ext_inj_inj {f : ℕ → ℕ} (hf : function.injective f) :
  function.injective (rename_ext f) :=
begin
  rintros ⟨⟩ ⟨⟩ h,
  { refl },
  { exact false.rec _ (nat.succ_ne_zero _ h.symm) },
  { exact false.rec _ (nat.succ_ne_zero _ h) },
  { rw hf (nat.succ_inj h) }
end

lemma rename_ext_succ_inj (x : ℕ) :
  function.injective (rename_ext^[x] nat.succ) :=
begin
  intros n m h,
  induction x with x ih generalizing n m,
  { exact nat.succ_inj h },
  { rw function.iterate_succ' at h,
    exact rename_ext_inj_inj (ih : function.injective _) h }
end

@[simp] def rename : (ℕ → ℕ) → term → term
| ρ (app M N) := app (rename ρ M) (rename ρ N)
| ρ (lam M)   := lam (rename (rename_ext ρ) M)
| ρ (var x)   := var (ρ x)

lemma rename_inj_inj {ρ : ℕ → ℕ} (hf : function.injective ρ) :
  function.injective (rename ρ) :=
begin
  intros M N h,
  induction M with _ _ ih₁ ih₂ M ih x generalizing N ρ hf;
    cases N; simp only [rename] at h; try { exfalso, exact h },
  { congr, exact ih₁ hf h.1, exact ih₂ hf h.2 },
  { congr, exact ih (rename_ext_inj_inj hf) h },
  { congr, exact hf h }
end

notation `rename_ext_succ^[` x `]` := rename (rename_ext^[x] nat.succ)

lemma rename_ext_succ_iff (h : y ≤ x) :
  x + 1 = (rename_ext^[y] nat.succ z) ↔ x = z :=
begin
  split,
  { intro hM,
    induction z with z ih generalizing x y,
    { cases y,
      { apply nat.succ_inj hM },
      { rw function.iterate_succ' at hM,
        exact false.rec _ (nat.succ_ne_zero _ hM) } },
    { cases x,
      { rw nat.eq_zero_of_le_zero h at hM,
        exact false.rec _ (nat.succ_ne_zero _ (nat.succ_inj hM.symm)) },
      { cases y,
        { exact nat.succ_inj hM },
        { rw function.iterate_succ' at hM,
          congr, exact ih (nat.le_of_lt_succ h) (nat.succ_inj hM) } } } },
  { rintro rfl,
    induction y with y ih generalizing x, exact rfl,
    cases x,
    { exact false.rec _ (nat.not_lt_zero _ h) },
    { rw function.iterate_succ',
      congr, exact ih (nat.le_of_succ_le_succ h) } }
end

lemma FV_rename_ext_succ_iff (h : y ≤ x) :
  x + 1 ∈ FV (rename_ext_succ^[y] (var z)) ↔ x = z :=
rename_ext_succ_iff h

lemma FV_rename_ext_succ_lt_of_FV_rename_ext_succ_lt (hy : y < x) (hz : z < x) :
  x ∈ FV (rename_ext_succ^[y] M) → x ∈ FV (rename_ext_succ^[z] M) :=
begin
  intro h,
  induction M with _ _ ih₁ ih₂ _ ih w generalizing x y z,
  { exact h.cases_on (or.inl ∘ ih₁ hy hz) (or.inr ∘ ih₂ hy hz) },
  { simp only [rename] at ⊢ h,
    rw [←function.comp_app rename_ext, ←function.iterate_succ'] at ⊢ h,
    refine ih (nat.succ_lt_succ hy) (nat.succ_lt_succ hz) h },
  { induction x with x ih generalizing y z w,
    { exact false.rec _ (nat.not_lt_zero _ hy) },
    { cases y; cases z,
      { rw nat.succ_inj h, exact rfl },
      { rw [←nat.succ_inj h, FV_rename_ext_succ_iff (nat.le_of_lt_succ hz)] },
      { congr,
        rwa FV_rename_ext_succ_iff (nat.le_of_lt_succ hy) at h },
      { rw function.iterate_succ' at ⊢ h,
        cases w, exact false.rec _ (nat.succ_ne_zero _ h),
        congr,
        refine ih _ _ _ (nat.succ_inj h),
        exact nat.lt_of_succ_lt_succ hy,
        exact nat.lt_of_succ_lt_succ hz } } }
end

lemma not_FV_rename_ext_succ (x : ℕ) : x ∉ FV (rename_ext_succ^[x] M) :=
begin
  induction M with _ _ ih₁ ih₂ _ ih y generalizing x,
  { exact λ h, h.cases_on (ih₁ x) (ih₂ x) },
  { simp only [rename],
    rw [←function.comp_app rename_ext, ←function.iterate_succ'],
    exact ih (x + 1) },
  { induction x with x ih generalizing y,
    { exact nat.succ_ne_zero _ ∘ eq.symm },
    { rw function.iterate_succ',
      cases y,
      { exact nat.succ_ne_zero _ },
      { exact (ih _ ∘ nat.succ_inj) } } },
end

stlc8.lean

import data.fin
import algebra.order

@[derive decidable_eq]
inductive term : ℕ → Type
| app {Γ : ℕ} (M N : term Γ) : term Γ
| lam {Γ : ℕ} (M : term (Γ + 1)) : term Γ
| var {Γ : ℕ} (x : fin Γ) : term Γ

open term

variables {Γ Δ : ℕ}

def rename_ext (ρ : fin Γ → fin Δ) (x : fin (Γ + 1)) : fin (Δ + 1) :=
if h : x = 0 then 0 else fin.succ $ ρ (x.pred h)

def rename : ∀ {Γ Δ}, (fin Γ → fin Δ) → term Γ → term Δ
| Γ Δ ρ (app M N) := app (rename ρ M) (rename ρ N)
| Γ Δ ρ (lam M)   := lam (rename (rename_ext ρ) M)
| Γ Δ ρ (var x)   := var (ρ x)

def subst_ext (σ : fin Γ → term Δ) : fin (Γ + 1) → term (Δ + 1)
| ⟨0, _⟩     := var 0
| ⟨x + 1, h⟩ := rename fin.succ (σ ⟨x, nat.lt_of_succ_lt_succ h⟩)

def subst : ∀ {Γ Δ : ℕ}, (fin Γ → term Δ) → term Γ → term Δ
| Γ Δ σ (app M N) := app (subst σ M) (subst σ N)
| Γ Δ σ (lam M)   := lam (subst (subst_ext σ) M)
| Γ Δ σ (var x)   := σ x

def subst' (x : fin (Γ + 1)) (N : term Γ) (M : term (Γ + 1)) : term Γ :=
let σ (y : fin (Γ + 1)) : term Γ :=
  @ordering.cases_on (λ o, cmp x y = o → term Γ) (cmp x y)
    -- `ordering.lt`
    (λ h, let h := (ordering.compares.eq_lt (cmp_compares x y)).mp h
      in var (y.pred (fin.ne_of_vne (ne_bot_of_gt h))))
    -- `ordering.eq`
    (λ h, N)
    -- `ordering.gt`
    (λ h, let h := (ordering.compares.eq_gt (cmp_compares x y)).mp h
      in var ⟨y, lt_of_lt_of_le h (nat.lt_succ_iff.mp x.is_lt)⟩) rfl
in subst σ M

notation M `[` x ` := ` N `]` := subst' x N M