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

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 :=


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