Limitations of the automation of wellfounded relationship

Stream: general

[Valentin Robert]

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]

(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]

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 _ _] }