failed to prove recursive application is decreasing

Stream: new members

[Vincent Beffara]

Hi, trying to define some custom well-founded order for use in recursive definitions, failing, and simplifying until I get a reasonably simple case where things still fail and I don't get why:

variable V : Type

structure toto := (val : list V)

inductive shorter : toto V -> toto V -> Prop
| step : ∀ (z : V) (l : list V), shorter ⟨l⟩ ⟨z::l⟩

lemma shorter_wf : well_founded (shorter V)
    := by { apply well_founded.intro, intro l, cases l with xs,
        induction xs with y ys; apply acc.intro; intros; cases a,
        apply xs_ih }

instance : has_well_founded (toto V) := ⟨shorter V, shorter_wf V⟩

def fold : toto V -> Prop
    | ⟨[]⟩    := true
    | ⟨x::xs⟩ := have h : shorter V ⟨xs⟩ ⟨x::xs⟩ := shorter.step x xs,
        fold ⟨xs⟩

Lean tells me that it cannot show shorter V {val := xs} {val := x :: xs} even though I have h in the state which states exactly that, and lean telling me that it will try to use assumption. What am I missing?

[Vincent Beffara]

Usually the answer would be "if assumption fails, try convert instead and it will tell you why" but here I don't know how to try that ...

[Joe]

variable V : Type

structure toto := (val : list V)

inductive shorter : toto V -> toto V -> Prop
| step : ∀ (z : V) (l : list V), shorter ⟨l⟩ ⟨z::l⟩

def fold : toto V -> Prop
    | ⟨[]⟩    := true
    | ⟨x::xs⟩ := fold ⟨xs⟩

[Joe]

I think this works just fine. But I don't understand what is happening.

[Vincent Beffara]

Yes because it is probably generating something like sizeof automatically, but that fails in my real use case ...

[Vincent Beffara]

Or inferring structural induction or something

[Kevin Buzzard]

Usually the answer would be "if assumption fails, try convert instead and it will tell you why" but here I don't know how to try that ...

I don't think this can be it, because if you prepend set_option pp.all true you can see that they really are the same term:

h : shorter V (@toto.mk V xs) (@toto.mk V (@list.cons.{0} V x xs))
⊢ shorter V (@toto.mk V xs) (@toto.mk V (@list.cons.{0} V x xs))

[Chris Hughes]

You need the using_well_founded keyword. This code works.

variable V : Type

structure toto := (val : list V)

inductive shorter : toto V -> toto V -> Prop
| step : ∀ (z : V) (l : list V), shorter ⟨l⟩ ⟨z::l⟩

lemma shorter_wf : well_founded (shorter V)
    := by { apply well_founded.intro, intro l, cases l with xs,
        induction xs with y ys; apply acc.intro; intros; cases a,
        apply xs_ih }

instance : has_well_founded (toto V) := ⟨shorter V, shorter_wf V⟩

def fold : toto V -> Prop
    | ⟨[]⟩    := true
    | ⟨x::xs⟩ := have h : shorter V ⟨xs⟩ ⟨x::xs⟩ := shorter.step x xs,
        fold ⟨xs⟩
using_well_founded { rel_tac := λ _ _, `[exact ⟨_, shorter_wf V⟩],
  dec_tac := `[exact h] }

I wrote some docs a while ago about using_well_founded at https://github.com/leanprover-community/mathlib/blob/master/docs/extras/well_founded_recursion.md

[Kieran Beltran]

Extended an example from article ... https://ahelwer.ca/post/2020-04-05-lean-assignment/

receiving the error(s) in rows 45 and 71 see attached.

love02_definitions_and_statements_examples.lean

Still fairly new to Lean...Appreciate any help. -K

[Kyle Miller]

Some fixes to convince Lean they're well-defined:

Line 45

def sum_of_first_n_even_nat : ℕ → ℕ
| 0 := 0
| (n+1) := ((n+1) * 2) + sum_of_first_n_even_nat n

Line 71

def sum_of_first_n_odd_nat : ℕ → ℕ
| 0 := 0
| (n+1) := (((n+1) * 2) - 1) + sum_of_first_n_odd_nat n

The proofs in the file still hold without any further modification.

[Kyle Miller]

I'm guessing Lean's not certain that n-1 in the original definition is actually less than n (since 0-1 = 0). I'm not sure what's changed since April 2020 that made it stop working.

[Kieran Beltran]

Thank-you Kyle. I guess in this simple example shows, having the recursion step defined (pattern matching on naturals) so as to ensure the recursion index doesn't result in f(0-1) = f(0) makes good sense. When I write it out by hand it appears simpler also. -K