Question about termination

Stream: lean4

[Ben Selfridge]

Hello,

Consider the following MRE:

section
inductive Var
| A : Var

inductive A
| Var : A
| A : A → A

def subst (aₓ : A) (a : A) : A := match a with
  | A.Var => aₓ
  | A.A a' => subst aₓ a'
end

def subst' (aₓ : A) (a : A) : A := match (true, a) with
  | (true, A.Var) => aₓ
  | (true, A.A a') => subst' aₓ a'
  | (false, _) => a
end

Lean can prove termination for subst not subst'. I was wondering if anyone could explain why.

[Ben Selfridge]

Followup.

I tried the obvious termination_by a, and it failed to go through (unsurprisingly). When I tried to add a decreasing_by clause, the context did not know that a = A.a a'. It had no information about either variable.

[Henrik Böving]

You can do it manually:

inductive Var
| A : Var

inductive A
| Var : A
| A : A → A

def subst (aₓ : A) (a : A) : A :=
  match a with
  | A.Var => aₓ
  | A.A a' => subst aₓ a'

def subst' (aₓ : A) (a : A) : A :=
  match h:(true, a) with
  | (true, A.Var) => aₓ
  | (true, A.A a') =>
    have : sizeOf a' < sizeOf a := by
      simp at h
      rw [h]
      simp
    subst' aₓ a'
  | (false, _) => a
termination_by a

[Ben Selfridge]

Thanks!

[Henrik Böving]

It is a bit unfortunate it can't guess this on it's own though

[Ben Selfridge]

It is!

[Henrik Böving]

I guess you could open an issue about it so we don't forget about it

[Ben Selfridge]

Just did that. But I'm glad I asked, because I didn't realize you could do termination proofs within the clauses of a function definition like this. Super cool!