Zulip Chat Archive

Stream: new members

Topic: Addition World Level 2


view this post on Zulip racecar (Nov 12 2020 at 20:02):

Hello,

Can you give me some pointers about solving Addition World Level 2? I tried every combination of previously learned tactics and nothing seems to get me closer to the solution.

I attempted to use induction, but I'm just spinning in circles.

induction b with d hd,
rw zero_add,
rw add_zero,
refl,

Any advice?
Thanks.

view this post on Zulip Wrenna Robson (Nov 12 2020 at 20:09):

I think you've got off to a great start, but I see the problem. What's your thinking so far?

view this post on Zulip Wrenna Robson (Nov 12 2020 at 20:09):

You're getting some kind of error, yeah?

view this post on Zulip Wrenna Robson (Nov 12 2020 at 20:13):

@racecar

view this post on Zulip racecar (Nov 12 2020 at 20:20):

@Wrenna Robson No error per se but I don't see a way out of the circle.

view this post on Zulip Ruben Van de Velde (Nov 12 2020 at 20:20):

Induction is a good idea

view this post on Zulip Wrenna Robson (Nov 12 2020 at 20:20):

Yes.

view this post on Zulip Ruben Van de Velde (Nov 12 2020 at 20:20):

The question is what variable to induct on

view this post on Zulip Wrenna Robson (Nov 12 2020 at 20:21):

Oh! Ah.

view this post on Zulip Wrenna Robson (Nov 12 2020 at 20:21):

Yes Ruben is quite right, I hadn't seen that.

view this post on Zulip racecar (Nov 12 2020 at 20:21):

I induced on b because it occurs in both braces.

view this post on Zulip Wrenna Robson (Nov 12 2020 at 20:22):

That is true - perhaps try inducting on a or c and seeing where that gets you?

view this post on Zulip Ruben Van de Velde (Nov 12 2020 at 20:23):

The nice thing about this setup is that you have very little to work with, so either you get stuck very quickly, or find the proof quickly :)

view this post on Zulip Ruben Van de Velde (Nov 12 2020 at 20:31):

Spoiler

view this post on Zulip racecar (Nov 12 2020 at 20:36):

When inducing on a I get a better goal, but using add_succ fails to find a pattern to apply it to.

induction a with d hd,
rw zero_add,
rw zero_add,
refl,
rw add_succ,

view this post on Zulip Wrenna Robson (Nov 12 2020 at 20:37):

Well, add_succ works on expressions of the form a + succ b, right?

view this post on Zulip Wrenna Robson (Nov 12 2020 at 20:37):

But you don't have any of those - you need the succ to be on the right...

view this post on Zulip racecar (Nov 12 2020 at 20:40):

Hmm...how indeed :thinking: :thinking: :thinking:

view this post on Zulip Wrenna Robson (Nov 12 2020 at 20:41):

Maybe looking rightwards would help...

view this post on Zulip racecar (Nov 12 2020 at 22:14):

I can't figure out how to instruct the compiler to reverse the order, do you mind sharing the answer?

view this post on Zulip Mario Carneiro (Nov 12 2020 at 22:16):

rw <- lemma

view this post on Zulip racecar (Nov 12 2020 at 22:18):

rw <- add_succ, still fails to find the pattern.

view this post on Zulip Kevin Buzzard (Nov 12 2020 at 23:30):

Why don't you read the hint?

view this post on Zulip racecar (Nov 13 2020 at 21:11):

I don't get the hint or what it's supposed to be. On the right hand side of the website I don't see any UI elements indicating a hint, and any combination of tactics fails to find anything.

view this post on Zulip Ruben Van de Velde (Nov 13 2020 at 21:58):

Possibly Kevin was referring to my comment upthread?

You've got one lemma you can use in the induction step, and it tells you something about a + succ b. There's only one variable you can induct on that puts succ _ on the right of the addition in the left- and right-hand sides of the equation

view this post on Zulip Kevin Buzzard (Nov 13 2020 at 22:01):

Are we talking about associativity of addition, addition world level 2? In the text it says "Hint" and then there's a hint. And it says to ignore the hint at your peril, and your description of what you've tried so far is precisely what happens if you ignore the hint.

view this post on Zulip Ruben Van de Velde (Nov 13 2020 at 22:04):

Doh, I went looking for a hint on that page and still missed it

view this post on Zulip racecar (Nov 14 2020 at 08:46):

Thanks, solved it.


Last updated: May 14 2021 at 06:16 UTC