## Stream: new members

### Topic: Well founded definition

#### 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?

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


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

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


#### 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.

#### 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?

It does

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


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

#### Eric Wieser (Jul 27 2020 at 10:52):

Instead of just "the default decreasing tactic"

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

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


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

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

#### 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?

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

#### 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?

#### Eric Wieser (Jul 28 2020 at 14:29):

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

#### Johan Commelin (Jul 28 2020 at 14:29):

Aah, you can do that

#### Johan Commelin (Jul 28 2020 at 14:30):

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

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

#### Eric Wieser (Jul 28 2020 at 14:35):

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

#### Johan Commelin (Jul 28 2020 at 14:41):

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

#### Johan Commelin (Jul 28 2020 at 14:41):

I always forget the correct incantation

#### Johan Commelin (Jul 28 2020 at 14:41):

We should add it to that docs page

#### Johan Commelin (Jul 28 2020 at 14:42):

Last updated: May 11 2021 at 00:31 UTC