Well founded definition

Stream: new members

[Daan van Gent]

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?

[Alex J. Best]

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

[Alex J. Best]

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

[Bhavik Mehta]

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

[Daan van Gent]

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.

[Eric Wieser]

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

[Mario Carneiro]

It does

[Mario Carneiro]

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

[Eric Wieser]

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

[Eric Wieser]

Instead of just "the default decreasing tactic"

[Mario Carneiro]

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

[Mario Carneiro]

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}

[Mario Carneiro]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Johan Commelin]

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

[Eric Wieser]

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

[Johan Commelin]

Aah, you can do that

[Johan Commelin]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Johan Commelin]

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

[Johan Commelin]

I always forget the correct incantation

[Johan Commelin]

We should add it to that docs page

[Johan Commelin]

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