## 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,
refl,


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?

@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

Yes.

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

The question is what variable to induct on

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

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,
refl,


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