# Zulip Chat Archive

## Stream: new members

### Topic: induction proof on n for TPIL exercise 7.10.1 trunc_sub

#### Yakov Pechersky (Jun 04 2020 at 05:12):

I'm trying to learn Lean via reading and doing exercises in TPIL. Right now, I'm stuck at proving the following theorem:

```
theorem my_sub_self (n : nat) : trunc_sub n n = 0 :=
begin
apply nat.rec_on n,
refl,
intros k hn,
sorry,
end
```

The definition and a simple theorem I have are:

```
def trunc_sub (m n : nat) : nat :=
nat.rec_on n m (λ n minus_m_n, pred minus_m_n)
@[simp] theorem trunc_sub_zero_right (n : nat) : trunc_sub n 0 = n :=
begin
induction n with k,
refl,
rw trunc_sub,
change nat.succ k = nat.succ k,
refl,
end
```

I tried finishing off the theorem with some `rw trunc_sub at *`

and `simp`

, but I am not sure how to simplify the `nat.rec`

or `nat.rec_on`

in a way that recognizes that it is only in the `nat.succ k`

case at that point in the proof. I think I'm just not understanding something about how to work with `rec`

and `rec_on`

.

I can include my definition of `pred`

and associated theorems like `pred (succ n) = n`

if that is helpful (or helps indicate that I have some grasp of Lean).

As a new-member introduction, I'm a computational chemist based in NYC. To learn Lean, I'm hoping to work through Benedict Gross's group theory class (which I've done before), but formalizing the notes and exercises.

#### Johan Commelin (Jun 04 2020 at 05:17):

@Yakov Pechersky Hi, welcome! Try `show pred _ = _`

. Let us know if that hint gets you back on track.

#### Johan Commelin (Jun 04 2020 at 05:21):

In other words, lean realizes that it is in the `nat.succ`

case of the proof, and using `show`

you ask it to restate the goal in a way that is equal to the preceding goal *by definition*.

#### Yakov Pechersky (Jun 04 2020 at 05:24):

I'm trying to follow your hint here. After including that in the proof, my goal state is currently:

```
1 goal
n k : ℕ,
hn : trunc_sub k k = 0
⊢ pred (nat.rec (nat.succ k) (λ (n minus_m_n : ℕ), pred minus_m_n) k) = 0
```

#### Mario Carneiro (Jun 04 2020 at 05:25):

That state looks problematic, because the base case has also shifted

#### Mario Carneiro (Jun 04 2020 at 05:25):

the `nat.rec`

term is `trunc_sub (nat.succ k) k`

, which your induction hypothesis will not help with

#### Yakov Pechersky (Jun 04 2020 at 05:26):

I'm just not sure how to get the `pred`

to enter into the `nat.rec (*here* nat.succ k)`

#### Mario Carneiro (Jun 04 2020 at 05:26):

That's a lemma

#### Mario Carneiro (Jun 04 2020 at 05:27):

more simply stated as `pred (trunc_sub m n) = trunc_sub (pred m) n`

#### Mario Carneiro (Jun 04 2020 at 05:27):

which you have to prove by induction

#### Yakov Pechersky (Jun 04 2020 at 05:27):

Aha! Yes, I was missing that.

#### Yakov Pechersky (Jun 04 2020 at 05:28):

I tried looking at the source for `add_right_neg`

and learn from that. Thanks for the guidance, I'll try proving the lemma first.

#### Mario Carneiro (Jun 04 2020 at 05:28):

it generalizes to `trunc_sub (trunc_sub m n) k = trunc_sub m (n + k)`

#### Mario Carneiro (Jun 04 2020 at 05:29):

(By the way, you presumably know that `trunc_sub`

is also known as `-`

)

#### Yakov Pechersky (Jun 04 2020 at 05:31):

Yeah, other than the nasty thing about it that `succ (pred n) = succ (pred m)`

does not imply `n = m`

, so `succ (trunc_sub m n)`

doesn't have to equal `trunc_sub (succ m) n`

.

#### Yakov Pechersky (Jun 04 2020 at 05:32):

Because `pred 0 = 0`

and `pred 1 = 0`

.

#### Yakov Pechersky (Jun 04 2020 at 05:42):

On this topic, why does using `unfold`

work but `rw`

does not work?

```
@[simp] theorem pred_trunc_sub (m n : nat) : pred (trunc_sub m n) = trunc_sub (pred m) n :=
begin
induction n with k hn,
refl,
unfold trunc_sub at *,
rw hn,
end
```

#### Yakov Pechersky (Jun 04 2020 at 06:05):

My current solution is below. Please let me know if there are better stylistic or semantic choices.

```
@[simp] theorem my_sub_self (n : nat) : trunc_sub n n = 0 :=
begin
apply nat.rec_on n,
refl,
intros k hn,
rw <- pred_succ k at hn,
rw <- pred_trunc_sub at hn, --pred_trunc_sub (m n : nat) : pred (trunc_sub m n) = trunc_sub (pred m) n
rw pred_succ at hn,
unfold trunc_sub at *,
rw hn,
end
```

#### Mario Carneiro (Jun 04 2020 at 06:29):

Yakov Pechersky said:

Yeah, other than the nasty thing about it that

`succ (pred n) = succ (pred m)`

does not imply`n = m`

, so`succ (trunc_sub m n)`

doesn't have to equal`trunc_sub (succ m) n`

.

That's why the lemma is about `pred`

and not `succ`

. You can view `trunc_sub m n`

as `pred^[n] m`

, and so it has nice additivity properties with respect to `n`

, irrespective of what `pred`

does

#### Mario Carneiro (Jun 04 2020 at 06:32):

On this topic, why does using unfold work but rw does not work?

You can see that `unfold`

does rather more than just unfold `trunc_sub`

, because it is actually `simp`

with special configuration options and it does some beta/iota reduction when it can

#### Mario Carneiro (Jun 04 2020 at 06:33):

notice that `unfold`

turns the statement into something about `rec`

instead of `rec_on`

#### Mario Carneiro (Jun 04 2020 at 06:33):

`rw`

is just using the definition for `trunc_sub`

#### Mario Carneiro (Jun 04 2020 at 06:34):

Stylistically, you could write the proof like so:

```
@[simp] theorem pred_trunc_sub (m n : nat) : pred (trunc_sub m n) = trunc_sub (pred m) n :=
begin
induction n with k hn,
{ refl },
unfold trunc_sub at *,
rw hn,
end
@[simp] theorem my_sub_self (n : nat) : trunc_sub n n = 0 :=
begin
induction n with k hn,
{ refl },
rw [← pred_succ k, ← pred_trunc_sub, pred_succ] at hn,
unfold trunc_sub at *,
rw hn,
end
```

#### Yakov Pechersky (Jun 04 2020 at 06:36):

If I want to avoid using simp for pedagogical purposes, what would be the way to invoke the beta and iota reduction after `rw`

, like the transformation of `rec_on`

to `rec`

and the application of `pred`

in the right place? Thanks for the style tips!

#### Mario Carneiro (Jun 04 2020 at 06:39):

But actually the use of `nat.rec_on`

is itself non-idiomatic. You get better equations and better presentation by using the equation compiler:

```
def trunc_sub (m : ℕ) : ℕ → ℕ
| 0 := m
| (n+1) := pred (trunc_sub n)
@[simp] theorem pred_trunc_sub (m n : nat) : pred (trunc_sub m n) = trunc_sub (pred m) n :=
begin
induction n with k hn,
{ refl },
rw [trunc_sub, trunc_sub, hn],
end
@[simp] theorem my_sub_self (n : nat) : trunc_sub n n = 0 :=
begin
induction n with k hn,
{ refl },
rw [trunc_sub, pred_trunc_sub, pred_succ, hn],
end
```

#### Mario Carneiro (Jun 04 2020 at 06:41):

and you can express the inductive proofs using the equation compiler as well, resulting in this mathlib-esque proof:

```
@[simp] theorem pred_trunc_sub (m) : ∀ n, pred (trunc_sub m n) = trunc_sub (pred m) n
| 0 := rfl
| (n+1) := by rw [trunc_sub, trunc_sub, pred_trunc_sub]
@[simp] theorem my_sub_self : ∀ n, trunc_sub n n = 0
| 0 := rfl
| (n+1) := by rw [trunc_sub, pred_trunc_sub, pred_succ, my_sub_self]
```

#### Yakov Pechersky (Jun 04 2020 at 06:42):

Ah, cool! The TPIL document's `add`

example is using `nat.rec_on`

, so I stuck with it:

```
def add (m n : nat) : nat :=
nat.rec_on n m (λ n add_m_n, succ add_m_n)
```

#### Mario Carneiro (Jun 04 2020 at 06:43):

The problem with definitions using `nat.rec_on`

directly is that the equation you get for it is `add m n = nat.rec_on n m (λ n add_m_n, succ add_m_n)`

, when the equations you would like are `add m 0 = m`

and `add m (succ n) = succ (add m n)`

#### Mario Carneiro (Jun 04 2020 at 06:44):

You can prove these equations yourself of course (by `rfl`

), and if you use them to rewrite instead of unfolding the `rec_on`

definition everything goes more smoothly because you don't have that big recursor term appearing. If you use the equation compiler to write your definition this happens automatically

#### Yakov Pechersky (Jun 04 2020 at 06:48):

When developing new definitions and theorems, is it an incremental improvement approach of first doing a tactic style `begin ... end`

and then refactoring to an equation compiler, or just internalize using the eq compiler from the get-go?

#### Mario Carneiro (Jun 04 2020 at 06:49):

I would probably write a proof in tactic style first and then refactor if at the end of it I can see that I didn't really make much use of the flexibility of tactic mode

#### Mario Carneiro (Jun 04 2020 at 06:50):

but there is nothing wrong with a tactic proof by `induction`

. Other methods are sometimes shorter and sometimes not

#### Yakov Pechersky (Jun 04 2020 at 06:51):

Got it. Thanks for the walkthrough! I'll try these ideas with the `length`

and `reverse`

exercises.

Last updated: May 10 2021 at 23:11 UTC