No incrementality in `decreasing_by`

I maneuvered myself into a position where I am editing a rather large and especially slow decreasing_by proof, and the apparant lack of incrementality is making progress really hard.

Not a MWE (that’s probably easier to construct using sleep) but a real-life example:

inductive Ty where
  | unit : Ty
  | arrow (t₁ t₂ : Ty) : Ty

def Env (n : Nat) := Fin n → Ty

def Env.add (Γ : Env n) (t : Ty) : Env (n + 1) :=
  Fin.cases t Γ

inductive Term : Env n → Ty → Type where
  | var (i : Fin n) : Term Γ (Γ i)
  | app (e₁ : Term Γ (.arrow t₁ t₂)) (e₂ : Term Γ t₁) : Term Γ t₂
  | lam (e : Term (Γ.add t₁) t₂) : Term Γ (.arrow t₁ t₂)

def Subst (Γ : Env n) (Δ : Env m) := (i : Fin n) → Term Δ (Γ i)

def Subst.id {Γ : Env n} : Subst Γ Γ :=
  fun i => .var i

def Subst.shift {Γ : Env n} : Subst Γ (Γ.add t) :=
  fun i => .var i.succ

attribute [simp] Subst.shift.eq_def

def IsVar : Term Γ t → Bool
  | .var _ => true
  | .app _ _ => false
  | .lam _ => false

attribute [simp] IsVar.eq_1 IsVar.eq_2 IsVar.eq_3

def IsRenaming (σ : Subst Γ Δ) : Bool := ∀ i, IsVar (σ i)

@[simp] theorem IsRenaming_shift: IsRenaming (@Subst.shift n t Γ) := by
  simp [IsRenaming, Subst.shift, IsVar]

def Term.helper (e : Term Γ t) (σ : Subst Γ Δ) (r : Term Δ t) : Term Δ t := match e with
  | .var i => σ i
  | _ => r

theorem isVar_helper : IsVar e → IsRenaming σ → IsVar (e.helper σ r) := by
  cases e <;> simp_all [IsRenaming, Term.helper]

def Term.subst (e : Term Γ t) (σ : Subst Γ Δ) : Term Δ t :=
  match e with
  | .var i => σ i
  | .app e₁ e₂ => .app (e₁.subst σ) (e₂.subst σ)
  | .lam e₁ =>
    .lam (e₁.subst (
        Fin.cases (.var 0) (fun i => (.helper (σ i) .shift <| (σ i).subst .shift))
    ))
termination_by (if IsVar e then 0 else 1, if IsRenaming σ then 0 else 1, sizeOf e)
decreasing_by
  · apply Prod.Lex.right'
    · split <;> simp
    apply Prod.Lex.right
    · decreasing_trivial
  · apply Prod.Lex.right'
    · split <;> simp
    apply Prod.Lex.right
    · decreasing_trivial
  · simp
    by_cases h : IsRenaming σ
    · apply Prod.Lex.left
      simp_all [IsRenaming]
    · apply Prod.Lex.right'
      · split <;> simp
      apply Prod.Lex.left
      simp [*]
  · simp [*]
    apply Prod.Lex.right'
    · split <;> simp
    apply Prod.Lex.right'
    · by_cases h : IsRenaming σ
      · simp [h]
        simp [IsRenaming]
        apply Fin.cases
        · simp
        · simp
          intro i
          apply isVar_helper
          · simp_all [IsRenaming]
          · simp
      · split <;> simp
    · decreasing_trivial

@[simp] theorem Term.helper_subst (e : Term Γ t) (σ : Subst Γ Δ) :
  e.helper σ (e.subst σ) = e.subst σ := by
  cases e
  · simp [Term.helper, Term.subst]
  · simp [Term.helper]
  · simp [Term.helper]

def Subst.shifted (σ : Subst Γ Δ) : Subst (Γ.add t) (Δ.add t) :=
  @Fin.cases _ _ (Term.var 0) (fun i => ((σ i).subst Subst.shift))

@[simp] theorem shifted_0 (σ : Subst Γ Δ) :
  (Subst.shifted σ (t := t)) 0 = .var 0 := by
  simp [Subst.shifted]

@[simp] theorem shifted_succ (σ : Subst Γ Δ) (i : Fin _):
  (Subst.shifted σ (t := t)) i.succ = (σ i).subst .shift := by
  simp [Subst.shifted]

@[simp] theorem IsRenaming_shifted :
  IsRenaming (Subst.shifted σ (t := t)) ↔ IsRenaming σ := by sorry

attribute [simp] Term.subst.eq_1 Term.subst.eq_2

@[simp] theorem Term.subst_lam :
  Term.subst (.lam e₁) σ =.lam (e₁.subst σ.shifted) := by
  simp [subst, Subst.shifted]

@[simp] theorem id_shifted : (@Subst.id _ Γ).shifted (t := t) = Subst.id := by
  funext i
  revert i
  apply Fin.cases
  · simp [Subst.id, Subst.shifted]
  · simp [Subst.id, Subst.shifted, Subst.shift]

theorem subst_id (e : Term Γ t) : e.subst .id = e := by
  induction e <;> simp_all [Subst.id]

theorem subst_subst {Γ : Env n} {Δ : Env n'} {Ω : Env n''} (e : Term Γ t) (σ₁ : Subst Γ Δ) (σ₂ : Subst Δ Ω) :
  (e.subst σ₁).subst σ₂ = e.subst (fun i => ((σ₁ i).subst σ₂)) := by
  fun_induction e.subst σ₁ generalizing n'' Ω
  · simp
  · simp_all
  next t _ ih1 ih2 =>
    simp
    simp at ih2
    rw [ih2 σ₂.shifted]; clear ih2
    congr
    apply funext
    apply Fin.cases
    · simp
    · simp
      intro i
      rw [ih1]
      simp
      sorry


set_option maxHeartbeats 400000

theorem subst_subst' {Γ : Env n} {Δ : Env n'} {Ω : Env n''} (e : Term Γ t) (σ₁ : Subst Γ Δ) (σ₂ : Subst Δ Ω) :
  (e.subst σ₁).subst σ₂ = (e.subst (fun i => ((σ₁ i).subst σ₂))) :=
  match e with
  | .var _ => by simp
  | .app e₁ e₂ =>
    have IH1 := subst_subst' e₂ σ₁ σ₂
    have IH2 := subst_subst' e₁ σ₁ σ₂
    by simp [IH1, IH2]
  | .lam e' =>
    have IH1 := subst_subst' e' σ₁.shifted σ₂.shifted
    have IH2 := fun i => subst_subst' (σ₁ i) Subst.shift σ₂.shifted
    have IH3 := fun i => subst_subst' (σ₁ i) σ₂ Subst.shift
    by
      simp
      rw [IH1]
      congr
      apply funext
      apply Fin.cases
      · simp
      · simp
        intro i
        specialize IH2 i
        specialize IH3 i
        rw [IH2, IH3]
        simp
-- Termination measure needed googling and finding
-- “Monadic Presentations of Lambda Terms Using Generalized Inductive Types”
termination_by (if IsVar e then 0 else 1,
  (if IsRenaming σ₁ then 0 else 1) + (if IsRenaming σ₂ then 0 else 1), sizeOf e)
decreasing_by
  · apply Prod.Lex.right'
    · split <;> simp
    apply Prod.Lex.right'
    · split <;> simp
    decreasing_trivial
  · apply Prod.Lex.right'
    · split <;> simp
    apply Prod.Lex.right'
    · split <;> simp
    decreasing_trivial
  · apply Prod.Lex.right'
    · split <;> simp
    apply Prod.Lex.right'
    · simp
    decreasing_trivial
  · by_cases h : IsRenaming σ₁
    · apply Prod.Lex.left
      simp_all [IsRenaming]
    · apply Prod.Lex.right'
      · split <;> simp
      apply Prod.Lex.left
      simp [*]
  · by_cases h : IsRenaming σ₁
    · apply Prod.Lex.left
      simp_all [IsRenaming]
    · apply Prod.Lex.right'
      · split <;> simp
      apply Prod.Lex.left
      simp [h]

Versions

4.24.0

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by reproducing the supplied decreasing_by example on Lean 4.24.0, focusing on the large Term.subst and subst_subst' proofs. Investigate the termination-checking behavior around these proofs; done should mean that progress in a large decreasing_by proof can be processed incrementally rather than requiring the whole proof to be reconsidered.