Addition World Level 2

Stream: new members

[racecar]

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]

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

[Wrenna Robson]

You're getting some kind of error, yeah?

[Wrenna Robson]

@racecar

[racecar]

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

[Ruben Van de Velde]

Induction is a good idea

[Wrenna Robson]

Yes.

[Ruben Van de Velde]

The question is what variable to induct on

[Wrenna Robson]

Oh! Ah.

[Wrenna Robson]

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

[racecar]

I induced on b because it occurs in both braces.

[Wrenna Robson]

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

[Ruben Van de Velde]

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]

Spoiler

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

[racecar]

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]

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

[Wrenna Robson]

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

[racecar]

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

[Wrenna Robson]

Maybe looking rightwards would help...

[racecar]

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

[Mario Carneiro]

rw <- lemma

[racecar]

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

[Kevin Buzzard]

Why don't you read the hint?

[racecar]

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]

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]

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]

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

[racecar]

Thanks, solved it.