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

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))
  { rel_tac := λ _ _, `[exact _, inv_image.wf wrap.out r_wf⟩],
    dec_tac := `[exact prove_r _ _] }

Last updated: Aug 03 2023 at 10:10 UTC