Zulip Chat Archive

Stream: new members

Topic: failed to prove recursive application is decreasing


Vincent Beffara (Jan 01 2020 at 22:31):

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 (Jan 01 2020 at 22:33):

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 (Jan 02 2020 at 00:12):

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 (Jan 02 2020 at 00:18):

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

Vincent Beffara (Jan 02 2020 at 11:23):

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

Vincent Beffara (Jan 02 2020 at 11:23):

Or inferring structural induction or something

Kevin Buzzard (Jan 02 2020 at 11:51):

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 (Jan 02 2020 at 12:23):

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 (Oct 16 2021 at 02:13):

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 (Oct 16 2021 at 02:42):

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 (Oct 16 2021 at 02:44):

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 (Oct 16 2021 at 09:45):

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


Last updated: Dec 20 2023 at 11:08 UTC