Zulip Chat Archive
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 wellfounded docs I wrote a couple of years ago. https://github.com/leanprovercommunity/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