induction proof on n for TPIL exercise 7.10.1 trunc_sub

Stream: new members

[Yakov Pechersky]

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]

@Yakov Pechersky Hi, welcome! Try show pred _ = _. Let us know if that hint gets you back on track.

[Johan Commelin]

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]

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]

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

[Mario Carneiro]

the nat.rec term is trunc_sub (nat.succ k) k, which your induction hypothesis will not help with

[Yakov Pechersky]

I'm just not sure how to get the pred to enter into the nat.rec (*here* nat.succ k)

[Mario Carneiro]

That's a lemma

[Mario Carneiro]

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

[Mario Carneiro]

which you have to prove by induction

[Yakov Pechersky]

Aha! Yes, I was missing that.

[Yakov Pechersky]

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]

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

[Mario Carneiro]

(By the way, you presumably know that trunc_sub is also known as -)

[Yakov Pechersky]

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]

Because pred 0 = 0 and pred 1 = 0.

[Yakov Pechersky]

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]

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]

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]

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]

notice that unfold turns the statement into something about rec instead of rec_on

[Mario Carneiro]

rw is just using the definition for trunc_sub

[Mario Carneiro]

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]

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]

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]

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]

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]

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]

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]

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]

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]

but there is nothing wrong with a tactic proof by induction. Other methods are sometimes shorter and sometimes not

[Yakov Pechersky]

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