Zulip Chat Archive

Stream: new members

Topic: induction proof on n for TPIL exercise 7.10.1 trunc_sub


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 04 2020 at 05:25):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Jun 04 2020 at 05:26):

That's a lemma

view this post on Zulip Mario Carneiro (Jun 04 2020 at 05:27):

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

view this post on Zulip Mario Carneiro (Jun 04 2020 at 05:27):

which you have to prove by induction

view this post on Zulip Yakov Pechersky (Jun 04 2020 at 05:27):

Aha! Yes, I was missing that.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jun 04 2020 at 05:28):

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

view this post on Zulip Mario Carneiro (Jun 04 2020 at 05:29):

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

view this post on Zulip 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.

view this post on Zulip Yakov Pechersky (Jun 04 2020 at 05:32):

Because pred 0 = 0 and pred 1 = 0.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 04 2020 at 06:33):

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

view this post on Zulip Mario Carneiro (Jun 04 2020 at 06:33):

rw is just using the definition for trunc_sub

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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]

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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