Zulip Chat Archive

Stream: new members

Topic: Addition World Level 2


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.

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?

Wrenna Robson (Nov 12 2020 at 20:09):

You're getting some kind of error, yeah?

Wrenna Robson (Nov 12 2020 at 20:13):

@racecar

racecar (Nov 12 2020 at 20:20):

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

Ruben Van de Velde (Nov 12 2020 at 20:20):

Induction is a good idea

Wrenna Robson (Nov 12 2020 at 20:20):

Yes.

Ruben Van de Velde (Nov 12 2020 at 20:20):

The question is what variable to induct on

Wrenna Robson (Nov 12 2020 at 20:21):

Oh! Ah.

Wrenna Robson (Nov 12 2020 at 20:21):

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

racecar (Nov 12 2020 at 20:21):

I induced on b because it occurs in both braces.

Wrenna Robson (Nov 12 2020 at 20:22):

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

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

Ruben Van de Velde (Nov 12 2020 at 20:31):

Spoiler

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,

Wrenna Robson (Nov 12 2020 at 20:37):

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

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

racecar (Nov 12 2020 at 20:40):

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

Wrenna Robson (Nov 12 2020 at 20:41):

Maybe looking rightwards would help...

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?

Mario Carneiro (Nov 12 2020 at 22:16):

rw <- lemma

racecar (Nov 12 2020 at 22:18):

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

Kevin Buzzard (Nov 12 2020 at 23:30):

Why don't you read the hint?

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.

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

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.

Ruben Van de Velde (Nov 13 2020 at 22:04):

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

racecar (Nov 14 2020 at 08:46):

Thanks, solved it.


Last updated: Dec 20 2023 at 11:08 UTC