## 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

Last updated: May 11 2021 at 00:31 UTC