Zulip Chat Archive

Stream: new members

Topic: failed to prove recursive application is decreasing


view this post on Zulip 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?

view this post on Zulip 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 ...

view this post on Zulip 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

view this post on Zulip Joe (Jan 02 2020 at 00:18):

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

view this post on Zulip 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 ...

view this post on Zulip Vincent Beffara (Jan 02 2020 at 11:23):

Or inferring structural induction or something

view this post on Zulip 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))

view this post on Zulip 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


Last updated: May 11 2021 at 00:31 UTC