natural number game solution

Stream: new members

[Joseph O]

For level 6 of Addition World, I came up with

rw add_assoc,
rw add_assoc,
rw add_comm c b,
refl,

and it works, but in the solutions, it had

rw add_assoc,
rw add_comm b c,
rw ←add_assoc,
refl,

is there anything different or better about the latter rather than the first?

[Joseph O]

It seems to be the same as mine, but just switching around the order. Is the latter solution more readable though?

[Eric Rodriguez]

no, they're both reasonable!

[Joseph O]

Which would you prefer?

[Arthur Paulino]

You should be able to say rw [add_assoc, add_assoc, add_comm c b], refl,

[Arthur Paulino]

(just to explore the syntax)

[Joseph O]

Arthur Paulino said:

You should be able to say rw [add_assoc, add_assoc, add_comm c b], refl,

they didn't show us that in the nat number game yet

[Arthur Paulino]

Right, I wouldn't worry too much about finding the best proof at this point. You'll know more tricks as the game progresses

[Notification Bot]

This topic was moved here from #general > natural number game solution by Kyle Miller.

[Kyle Miller]

(@Joseph O I think questions about NNG levels generally go in this stream, so I moved it over.)

I agree with what Eric and Arthur have said -- both of your solutions are fine!

[Kyle Miller]

In the future, you'll also have tactics like ring which can solve the entire thing for you in a single command. That's probably the most readable.

[Kyle Miller]

But for now, you're practicing rewrites.