Zulip Chat Archive

Stream: new members

Topic: Well founded definition


view this post on Zulip Daan van Gent (Jul 26 2020 at 17:11):

I have a definition (minimal working example) of a recursive definition:

def test : list  × list   list  × list 
| ([],m) := ([],m)
| (a::l,m) := test(l,m)

It gives me errors about well-foundedness. How do I prove that it is?

view this post on Zulip Alex J. Best (Jul 26 2020 at 17:36):

Maybe your MWE is a little too minimal, as in this case you don't need an inductive definition at all, or at least you can make an induction on the first argument as a separate def and then make a function from pairs to pairs using that.
However the way to do this using a recursor is to specify why its well founded, in this case by saying that the length of the first list in the pair is the thing which gets smaller at each step

def test : list  × list   list  × list 
| ([],m) := ([],m)
| (a::l,m) := test(l,m)
using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf (λ f, f.1.length)]}

#eval test ([1,2], [2,3])

view this post on Zulip Alex J. Best (Jul 26 2020 at 17:37):

The syntax looks a bit complicated but this line is pretty common, most of the time all you need to change is the (λ f, f.1.length) part to be a function from your input to nat that decreases with each step, see https://leanprover-community.github.io/extras/well_founded_recursion.html

view this post on Zulip Bhavik Mehta (Jul 26 2020 at 18:41):

You could alternatively do

def test_aux : list   list   list  × list 
| [] m := ([], m)
| (a::l) m := test_aux l m

def test (lm : list  × list ) : list  × list  := test_aux lm.1 lm.2

view this post on Zulip Daan van Gent (Jul 27 2020 at 10:01):

Great! Thanks Alex. I did not notice my mwe was a bit degenerate. The solution Bhavik wrote out does also work for my original problem it seems, so thanks for that as well, but I am glad to learn the general solution.

view this post on Zulip Eric Wieser (Jul 27 2020 at 10:37):

Could lean provide a has_well_founded for product types to make the test_aux version unecessary?

view this post on Zulip Mario Carneiro (Jul 27 2020 at 10:40):

It does

view this post on Zulip Mario Carneiro (Jul 27 2020 at 10:46):

The problem is not that the theorem is not true, it is just not proven automatically

def test : list  × list   list  × list 
| ([],m) := ([],m)
| (a::l,m) := test(l,m)
using_well_founded {dec_tac := `[apply prod.lex.left, well_founded_tactics.default_dec_tac]}

view this post on Zulip Eric Wieser (Jul 27 2020 at 10:52):

It would be great if well_founded_tactics.default_dec_tac could be in the error message

view this post on Zulip Eric Wieser (Jul 27 2020 at 10:52):

Instead of just "the default decreasing tactic"

view this post on Zulip Mario Carneiro (Jul 27 2020 at 10:54):

The usual way you prove well foundedness assumptions is to throw away the default tactic and give a manual proof

view this post on Zulip Mario Carneiro (Jul 27 2020 at 10:56):

def test : list  × list   list  × list 
| ([],m) := ([],m)
| (a::l,m) :=
  have has_well_founded.r (l, m) (a :: l, m) :=
  prod.lex.left _ _ (show l.sizeof < (a :: l).sizeof,
    by well_founded_tactics.default_dec_tac),
  test(l,m)
using_well_founded {dec_tac := tactic.assumption}

view this post on Zulip Mario Carneiro (Jul 27 2020 at 10:59):

And usually when you do this you find that the well founded measure is not very good, so you provide your own

def test : list  × list   list  × list 
| ([],m) := ([],m)
| (a::l,m) :=
  have l.length < (a :: l).length := nat.lt_succ_self _,
  test(l,m)
using_well_founded {
  dec_tac := tactic.assumption,
  rel_tac := λ _ _, `[exact ⟨_, measure_wf (λ f, f.1.length)]}

although as Alex showed, well_founded_tactics.default_dec_tac will prove this side goal on its own

view this post on Zulip Eric Wieser (Jul 27 2020 at 11:30):

If I add these simp lemmas, then simp can handle the proof:

@[simp]
lemma prod_lex_iff {α : Type u} {β : Type v} {ra : α  α  Prop} {rb : β  β  Prop} {a₁ : α} {b₁ : β} {a₂ : α} {b₂ : β}
 : prod.lex ra rb (a₁, b₁) (a₂, b₂)  ra a₁ a₂  (a₁ = a₂  rb b₁ b₂)
:= begin
  split,
  {
    intro h,
    cases h,
    exact or.inl h_h,
    simp only [true_and, eq_self_iff_true],
    exact or.inr h_h,
  },
  intro h,
  cases h,
  apply prod.lex.left,
  exact h,
  rw h.left,
  apply prod.lex.right,
  exact h.right,
end

@[simp] lemma append_ne_self {α : Type u} (a : α) (l : list α) : (list.cons a l)  l := begin
  induction l,
  simp,
  simp,
  intro h,
  rw h,
  exact l_ih,
end
@[simp] lemma self_ne_append {α : Type u} (a : α) (l : list α) : l  (list.cons a l) := ne.symm $ append_ne_self a l

but looks like well_founded_tactics.default_dec_tac does not attempt simp anyway

view this post on Zulip Eric Wieser (Jul 27 2020 at 11:33):

Would adding a if t.is_napp_of `prod.lex` to well_founded_tactics.process_lex make the proof automatic here?

view this post on Zulip Eric Wieser (Jul 28 2020 at 14:22):

Opened a PR I have no idea how to build or test at https://github.com/leanprover-community/lean/pull/414

view this post on Zulip Johan Commelin (Jul 28 2020 at 14:24):

@Eric Wieser https://github.com/leanprover-community/lean/blob/master/doc/make/index.md#generic-build-instructions
Do those help?

view this post on Zulip Eric Wieser (Jul 28 2020 at 14:29):

I was hoping to rebuild the core lib without having to rebuild the C++ component

view this post on Zulip Johan Commelin (Jul 28 2020 at 14:29):

Aah, you can do that

view this post on Zulip Johan Commelin (Jul 28 2020 at 14:30):

I think you need to run lean --make in library/

view this post on Zulip Eric Wieser (Jul 28 2020 at 14:35):

The other issue I have is swapping out my git library in place of my .elan one

view this post on Zulip Eric Wieser (Jul 28 2020 at 14:35):

I suppose I could just edit the elan one in place...

view this post on Zulip Johan Commelin (Jul 28 2020 at 14:41):

No... you need to tell elan about the new one

view this post on Zulip Johan Commelin (Jul 28 2020 at 14:41):

I always forget the correct incantation

view this post on Zulip Johan Commelin (Jul 28 2020 at 14:41):

We should add it to that docs page

view this post on Zulip Johan Commelin (Jul 28 2020 at 14:42):

See for example:
https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/lean.23211.20don't.20unfold.20irred.20defs/near/196194753


Last updated: May 11 2021 at 00:31 UTC