induction can't prove well-founded

Stream: new members

[Patrick Lutz]

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]

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]

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

[Patrick Lutz]

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

[Patrick Lutz]

But outside of tactic mode, it can see haves?

[Patrick Lutz]

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]

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

[Mario Carneiro]

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]

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]

Is it worth making an issue on github about this?

[Patrick Lutz]

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]

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.