Function decreasing on n-th argument

Stream: new members

[Pedro Minicz]

How do I tell Lean that a given function is decreasing on the n-th argument? shift.main is "obviously" decreasing on the third argument (term (D + G)).

import tactic.linarith

inductive term : ℕ → Type
| app {G : ℕ} (M N : term G) : term G
| lam {G : ℕ} (M : term (G + 1)) : term G
| var {G : ℕ} (x : fin G) : term G

open term

def shift.elem : ∀ {G D : ℕ}, fin (G + D) → fin (G + D + 1)
| 0       D x          := x + 1
| (G + 1) D ⟨0, h⟩     := ⟨0, nat.lt.step h⟩
| (G + 1) D ⟨x + 1, h⟩ := shift.elem ⟨x, nat.lt_of_succ_lt h⟩

def shift.main : ∀ {G D : ℕ}, term (D + G) → term (D + G + 1)
| G D (app M N) := app (shift.main M) (shift.main N)
| G D (lam M)   := lam (shift.main M) -- Lean complains here.
| G D (var x)   := var (shift.elem x)

I suspect telling Lean that might not be enough, though, so for a second question: where can I read on well founded relations on Lean (and in general)?

[Mario Carneiro]

If this was a recursion on the third argument, it would not have D + G in the index

[Marc Huisinga]

tpil: https://leanprover.github.io/theorem_proving_in_lean/induction_and_recursion.html#well-founded-recursion-and-induction
mathlib docs: https://leanprover-community.github.io/extras/well_founded_recursion.html

[Mario Carneiro]

Don't let well founded recursion errors fool you; that's just the fallback because the structural recursion compilation failed

[Mario Carneiro]

this should be a structural recursion

[Pedro Minicz]

Mario Carneiro said:

Don't let well founded recursion errors fool you; that's just the fallback because the structural recursion compilation failed

I see. That makes sense.

[Pedro Minicz]

Mario Carneiro said:

If this was a recursion on the third argument, it would not have D + G in the index

Yes! Indeed. Changing that fixed the issue.

[Pedro Minicz]

Why can't Lean see that M is structurally smaller than lam M. It may have something to do with the fact that lam M has type term Γ while M : term (Γ + 1).

import data.fin

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

open term

def shift.main : ∀ {Γ : ℕ}, fin (Γ + 1) → term Γ → term (Γ + 1)
| Γ σ (app M N) := app (shift.main σ M) (shift.main σ N)
| Γ σ (lam M)   := lam (@shift.main (Γ + 1) (σ + 1) M)
| Γ σ (var x)   := var $ if σ ≤ x then x + 1 else x

abbreviation shift {Γ : ℕ} : term Γ → term (Γ + 1) := shift.main 0

def subst.main : ∀ {Γ : ℕ}, fin (Γ + 1) → term Γ → term (Γ + 1) → term Γ
| Γ σ L (app M N) := app (subst.main σ L M) (subst.main σ L N)
| Γ σ L (lam M)   := lam (@subst.main (Γ + 1) (σ + 1) (shift L) M) -- This line.
| Γ σ L (var x)   := sorry