# Zulip Chat Archive

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

s but not `have`

s for some reason?

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

But outside of tactic mode, it can see `have`

s?

#### 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:37):

Is it worth making an issue on github about this?

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