Stream: new members

Topic: induction can't prove well-founded

Patrick Lutz (Jul 30 2020 at 20:06):

I was trying to prove something with induction using pattern-matching and I ran into a confusing problem. The following is the best mwe that I can come up with to demonstrate the thing I'm confused about.

The following proof doesn't work.

import tactic

constant shrink : ℕ → ℕ
constant good : ℕ → Prop
axiom shrink_decreasing (n : ℕ) : n > 0 → shrink n < n
axiom zero_good : good 0
axiom good_of_shrink_good (n : ℕ) : good (shrink n) → good n

lemma all_good : ∀ n, good n
| 0 := zero_good
| (n + 1) :=
begin
have : shrink (n + 1) < n + 1 := shrink_decreasing (n + 1) (by linarith),
have : good (shrink (n + 1)) := all_good (shrink (n + 1)),
exact good_of_shrink_good (n + 1) this,
end


The error is failed to prove recursive application is decreasing which I find strange because I provided the proof that shrink (n + 1) < n + 1. The most confusing thing to me about this is that the error message says that the following was the place where the decreasing tactic got stuck

state:
all_good : ∀ (n : ℕ), good n,
n : ℕ
⊢ shrink (n + 1) < n + 1


which for some reason does not contain the have statement I provided in the proof. What's going on?

Chris B (Jul 30 2020 at 20:16):

Someone more knowledgeable will have to explain what's going on, but moving the assumption outside the tactic block works for me.

lemma all_good : ∀ n, good n
| 0 := zero_good
| (n + 1) :=
have h1 : shrink (n + 1) < n + 1 := shrink_decreasing (n + 1) (by linarith),
begin
have : good (shrink (n + 1)) := all_good (shrink (n + 1)),
exact good_of_shrink_good (n + 1) this,
end


Patrick Lutz (Jul 30 2020 at 20:18):

Weird, I just realized changing the first have to a let also makes it work

Patrick Lutz (Jul 30 2020 at 20:19):

So when in tactic mode, the decreasing tactic can see local lets but not haves for some reason?

Patrick Lutz (Jul 30 2020 at 20:19):

But outside of tactic mode, it can see haves?

Patrick Lutz (Jul 30 2020 at 20:20):

The weirdest part is I think I've used this sort of pattern before with no problems. Though I can't find a good example now, so maybe I'm mistaken

Mario Carneiro (Jul 30 2020 at 20:29):

I can confirm that you need to do this, I don't have a good explanation besides lean being lean

Mario Carneiro (Jul 30 2020 at 20:30):

you can also write something like

lemma all_good : ∀ n, good n
| 0 := zero_good
| (n + 1) :=
begin
have : good (shrink (n + 1)) := all_good (shrink (n + 1)),
exact
have h1 : shrink (n + 1) < n + 1 := shrink_decreasing (n + 1) (by linarith),
good_of_shrink_good (n + 1) this,
end


Patrick Lutz (Jul 30 2020 at 20:37):

Mario Carneiro said:

I can confirm that you need to do this, I don't have a good explanation besides lean being lean

It's a little annoying because the error message explicitly advises you to include the proof that it's decreasing as a have statement. If this only works in term proofs and not in tactic proofs, it's kind of misleading.

Patrick Lutz (Jul 30 2020 at 20:38):

Patrick Lutz said:

It's a little annoying because the error message explicitly advises you to include the proof that it's decreasing as a have statement. If this only works in term proofs and not in tactic proofs, it's kind of misleading.

I.e.

The default decreasing tactic uses the 'assumption' tactic, thus hints (aka local proofs)
can be provided using 'have'-expressions.


Patrick Stevens (Jul 31 2020 at 05:47):

This is documented to a certain extent at https://leanprover-community.github.io/extras/well_founded_recursion.html, which as a document I found very helpful to read. The relevant quote:

Note that the have must not be in tactics mode, i.e. inside any begin end. If you are in tactics mode, there is the option of putting the have statement inside the exact statement, as in the following example.

Last updated: May 13 2021 at 17:42 UTC