## Stream: general

### Topic: Limitations of the automation of wellfounded relationship

#### Valentin Robert (Aug 15 2021 at 21:01):

I'm playing with a more complex example, but it basically boils down to the following.

While this is accepted by Lean:

inductive x : Type
| mkx : (ℕ → x) → x

def catax : x → ℕ
| (x.mkx f) := catax (f 0)


The following confuses it enough about the wellfoundedness of the recursion:

inductive wrap : Type
| mkwrap : x → wrap

def cataw : wrap → ℕ
| (wrap.mkwrap (x.mkx f)) := cataw (wrap.mkwrap (f 0))


Essentially the argument for wellfoundedness is that mkwrap behaves covariantly/positively w.r.t. its argument, so for the same reason that catax was accepted, cataw ought to be okay, even though Lean can't see that.

Two questions:

• Any chance of supporting this automatically?

• What's my quickest route to allow the second definition?

#### Floris van Doorn (Aug 16 2021 at 00:44):

(1) It is unlikely that anything about the Lean 3 equation compiler will be changed (with Lean 4 around the corner), so I don't think this will be supported automatically in Lean 3
(2) You can use using_well_founded { rel_tac := ... } to specify the measure that is decreasing in the recursive call. You want a have statement in your definition that actually states that the given measure is decreasing. Search mathlib for using_well_founded for examples.

#### Chris Hughes (Aug 16 2021 at 04:09):

I managed to define the well founded relation to allow the second definition. The best way to understand this is probably to read the well-founded docs I wrote a couple of years ago. https://github.com/leanprover-community/mathlib/blob/master/docs/extras/well_founded_recursion.md

import tactic.rcases

inductive x : Type
| mkx : (ℕ → x) → x

def catax : x → ℕ
| (x.mkx f) := catax (f 0)

inductive wrap : Type
| mkwrap : x → wrap

def wrap.out (w : wrap) : x := wrap.rec_on w id

def r (a b : x) : Prop :=
∃ (n : ℕ) (f : ℕ → x), a = f n ∧ b = x.mkx f

lemma r_wf : well_founded r :=
⟨λ a, begin
induction a with f ih,
dsimp at ih,
refine acc.intro _ _,
assume b hb,
rcases hb with ⟨n, g, rfl, h⟩,
simp only at h,
subst f,
exact ih _
end⟩

def has_well_founded_wrap : has_well_founded wrap :=
⟨_, inv_image.wf wrap.out r_wf⟩

def prove_r (f : ℕ → x) (n : ℕ) : @has_well_founded.r wrap
has_well_founded_wrap (wrap.mkwrap (f n)) (wrap.mkwrap (x.mkx f)) :=
⟨n, f, rfl, rfl⟩

def cataw : wrap → ℕ
| (wrap.mkwrap (x.mkx f)) := cataw (wrap.mkwrap (f 0))
using_well_founded
{ rel_tac := λ _ _, [exact ⟨_, inv_image.wf wrap.out r_wf⟩],
dec_tac := [exact prove_r _ _] }


Last updated: Aug 03 2023 at 10:10 UTC